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 |
---|---|