Subgoal *1/2' (IMPLIES (AND (CONSP A) (EQUAL (APP (APP (CDR A) B) C) (APP (CDR A) (APP B C)))) (EQUAL (APP (IF (CONSP A) (CONS (CAR A) (APP (CDR A) B)) B) C) (APP A (APP B C)))).
Note that the IF
expression above is the simplified body of APP
. But
we know the test (CONSP A)
is true, by the first hypothesis. Click on
the link above to replace the test by T
. Actually this step and several
subsequent ones are done during the simplification of the body of APP
but
we want to illustrate the basic principles of simplification without
bothering with every detail.