(defun memb (e x) (if (endp x) nil (if (equal e (car x)) t (memb e (cdr x))))) (defun ap (x y) (if (endp x) y (cons (car x) (ap (cdr x) y)))) (defun rm! (e x) (if (endp x) nil (if (equal e (car x)) (rm! e (cdr x)) (cons (car x) (rm! e (cdr x)))))) (defun set-equal (x y) (if (endp x) (endp y) (and (memb (car x) y) (set-equal (rm! (car x) (cdr x)) (rm! (car x) y))))) (defthm memb-rm! (equal (memb e (rm! d x)) (if (equal e d) nil (memb e x)))) #| (defthm memb-rm!-fact1 (implies (equal e d) (not (memb e (rm! d x))))) (defthm memb-rm!-fact2 (implies (not (equal e d)) (equal (memb e (rm! d x)) (memb e x)))) |# (defthm set-equal-prop1 (implies (set-equal x y) (iff (memb e x) (memb e y)))) ; ----------------------------------------------------------------- ; This is easily proved: (thm (equal (ap (ap a b) c) (ap a (ap b c)))) ; This is is "impossible" to prove by induction: (thm (equal (ap (ap a a) a) (ap a (ap a a)))) ; This can be easily proved: (thm (equal (ap (ap a b) b) (ap a (ap b b)))) ; ----------------------------------------------------------------- (defun subset (x y) (if (endp x) t (and (memb (car x) y) (subset (cdr x) y)))) (defthm rm!-ap (equal (rm! e (ap a b)) (ap (rm! e a) (rm! e b)))) (defthm subset-rm! (implies (subset x y) (subset (rm! e x) (rm! e y)))) ;----------------------------------------------------------------- (i-am-here) *** Key checkpoint under a top-level induction: *** Subgoal *1/3.1' (IMPLIES (AND (CONSP A) (NOT (MEMB (CAR A) B)) (SUBSET B A)) (SET-EQUAL (AP (RM! (CAR A) (CDR A)) (RM! (CAR A) B)) (RM! (CAR A) (CDR A)))) ;----------------------------------------------------------------- (defthm car-ap (equal (car (ap a b)) (if (endp a) (car b) (car a)))) (defthm cdr-ap (equal (cdr (ap a b)) (if (endp a) (cdr b) (ap (cdr a) b)))) (defthm set-equal-prop2-lemma (implies (subset b a) (set-equal (ap a b) a)) :hints (("Goal" :induct (set-equal a b)) ("Subgoal *1/2''" :use (:instance subset-rm! (x b) (y a) (e (car a)))) ("Subgoal *1/3'" :expand ((SET-EQUAL (AP A B) A))))) (defthm set-equal-prop2 (set-equal (ap a a) a))