I have a problem with my gcl calculator. Here are two little proofs which try to simplify a weakest precondition. This problem is similar to some found in exercise 5.2 in Programming in the 1990s.

The first step of both is the same. In the 2nd step, the left proof matches wp.(x := E).R with the entire expression, and the right proof matches wp.(x := E).R with the more deeply nested wp expression. The left calculation ends up doing a textual-substitution and creating an expression that doesn't make sense. The right calculation succeeds.

I would like this calculator to not allow the left calculation to happen. The 2nd steps in both proofs seem valid to me. Is there something I've missed?

bad	good