Correctness of Transformations

It is not always easy to be certain that transformed code will give exactly the same results.

( (> (* ?n ?x)
     (* ?n ?y))         (> ?x ?y) )

( (not (not ?x))        ?x )

( (= (if ?p ?qu ?qv)
     ?qu)               ?p )

These transformations are usually correct, but it is possible to construct an example for each in which the transformation changes the result. We must be careful to use only correct transforms.