Major Section: INTRODUCTION-TO-THE-THEOREM-PROVER
This answer is in the form of a script sufficient to lead ACL2 to a proof.
subsetp-reflexiveat 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-reflexivesucceeds. (defthm subsetp-reflexive (subsetp x x)) ; A weaker version of the lemma, namely the one in which we ; add the hypothesis that
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
bis ; 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.