The inductive step of the

The correct answer to Question 2 in logic-knowledge-taken-for-granted is *Subgoal (i)* plus any one of the
other other three. For your reference, the four choices were:

Subgoal (i): (implies (and (not (endp z)) (true-listp z)) (true-listp (cdr z)))Subgoal (ii): (implies (and (not (endp z)) (true-listp z) (equal (rev (rev (cdr z))) (cdr z))) (equal (rev (rev z)) z))Subgoal (iii): (implies (and (not (endp z)) (equal (rev (rev (cdr z))) (cdr z))) (equal (rev (rev z)) z))Subgoal (iv): (implies (and (not (endp z)) (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z))) (equal (rev (rev z)) z))

In particular, it is wrong to think the Induction Step of the proof of

(implies (true-listp z) (equal (rev (rev z)) z))

can be established by proving just *Subgoal (ii)*, *Subgoal
(iii)*, *Subgoal (iv)*, or combinations of those three. You must also
prove *Subgoal (i)* or something like it!

The Inductive Step for the conjecture above is

Induction Step: (implies (and (not (endp z)) ;Induction Hypothesis: (implies (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z)))) ;Induction Conclusion: (implies (true-listp z) (equal (rev (rev z)) z)))

Note that the Inductive Hypothesis is an implication:

(implies (true-listp (cdr z)) (equal (rev (rev (cdr z))) (cdr z)))

This hypothesis can be true two different ways. The ``normal'' way —
the way everybody remembers — is that

In this case, the Induction Step simplifies to

Induction Step: (implies (and (not (endp z)) (not (true-listp (cdr z)))) (implies (true-listp z) (equal (rev (rev z)) z)))

By Promotion (see the list of tautologies in our discussion of

Induction Step': (implies (and (not (endp z)) (not (true-listp (cdr z))) (true-listp z)) (equal (rev (rev z)) z))

Using the Contrapositive and rearranging the order of the hypotheses (see

Induction Step'': (implies (and (not (endp z)) (true-listp z) (not (equal (rev (rev z)) z))) (true-listp (cdr z)))

Notice that *Subgoal (i)* implies *Induction Step''*:

Subgoal (i): (implies (and (not (endp z)) (truelistp z)) (truelistp (cdr z)))

Every inductive proof of an implication raises a case like this. If we
denote the conjecture

( c & (p' ---> q')) ---> (p ---> q)

where

( c & p & (p' ---> q')) ---> q

It is then very common to prove that

(i): (c & p) ---> p'

and then prove that

(ii): (c & p & q') ---> q

These correspond exactly to our choices *Subgoal (i)* and *Subgoal
(ii)*.

It is sometimes helpful to remember this diagram:

(c & (p' ---> q') ^ | | | | v --> (p ---> q )

When you understand why *Subgoals (i)* and *(ii)* are sufficient,
use your browser's **Back Button** to return to logic-knowledge-taken-for-granted and go to question Q3.