@soupless If you want precedence rules for those, you would of course need to define some syntax for specifying those. I don't have a clear idea of what is the best way.

@soupless Why include so many steps in the proof but omit the most important steps?

How did you get "z = d"?

Nevertheless, the proof outline is correct.