Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER

This answer is in the form of a script sufficient to lead ACL2 to a proof.

; Trying`subsetp-reflexive`

at this point produces the key checkpoint:; (IMPLIES (AND (CONSP X) ; (SUBSETP (CDR X) (CDR X))) ; (SUBSETP (CDR X) X))

; which suggests the generalization:

(defthm subsetp-cdr (implies (subsetp a (cdr b)) (subsetp a b)))

; And now

`subsetp-reflexive`

succeeds.(defthm subsetp-reflexive (subsetp x x))

; A weaker version of the lemma, namely the one in which we ; add the hypothesis that

`b`

is a`cons`

, is also sufficient.; (defthm subsetp-cdr-weak ; (implies (and (consp b) ; (subsetp a (cdr b))) ; (subsetp a b)))

; But the

`(consp b)`

hypothesis is not really necessary in ; ACL2's type-free logic because`(cdr b)`

is`nil`

if`b`

is ; not a`cons`

. For the reasons explained in the tutorial, we ; prefer the strong version.

Use your browser's **Back Button** now to return to
introductory-challenge-problem-2.