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
(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.