Answer to challenge problem 2 for the new user of ACL2
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 bis 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 nilif 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.