### INTRODUCTORY-CHALLENGE-PROBLEM-2-ANSWER

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