rendered paste body#192:
(true-listp y) -> (true-listp (cons x y))
<-> {Re: def true-listp}
(true-listp y) -> (if (consp (cons x y))
(true-listp (cdr (cons x y)))
(equal (cons x y) nil)))
<-> {Comp.}
(true-listp y) -> (if t
(true-listp (cdr (cons x y)))
(equal (cons x y) nil)))
<-> {Re: if-ax1}
(true-listp y) -> (true-listp (cdr (cons x y)))
<-> {Re: cdr-cons axiom}
(true-listp y) -> (true-listp y)
<-> {Hyp}
(true-listp y) -> t
<-> {Re: short-circuit}
t
#196:
((P -> Q) ^ (P -> R)) -> (P -> (Q ^ R))
<-> {Promotion}
((P -> Q) ^ (P -> R) ^ P) -> (Q ^ R)
<-> {Forward Chaining}
(Q ^ R ^ P) -> (Q ^ R)
<-> {Hyp twice}
(Q ^ R ^ P) -> (t ^ t)
<-> {Comp}
(Q ^ R ^ P) -> t
<-> {Short Circuit}
t
#198:
((A -> D) ^ (B -> E) ^ (D -> (E -> C))) -> ((A ^ B) -> C)
<-> {Promotion}
((A -> D) ^ (B -> E) ^ (D -> (E -> C)) ^ (A ^ B)) -> (C)
<-> {Associativity}
((A -> D) ^ (B -> E) ^ (D -> (E -> C)) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ (B -> E) ^ (D -> (E -> C)) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ (B -> E) ^ (E -> C) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ E ^ (E -> C) ^ A ^ B) -> (C)
<-> {Forward Chaining}
(D ^ E ^ C ^ A ^ B) -> (C)
<-> {Hyp}
(D ^ E ^ C ^ A ^ B) -> t
<-> {Short Circuit}
t
#205:
(not (consp a)) -> (app (app a b) c) = (app a (app b c))
<-> {Re: def consp}
(not (not (endp a))) -> (app (app a b) c) = (app a (app b c))
<-> {Comp}
(endp a) -> (app (app a b) c) = (app a (app b c))
<-> {Re: def app}
(endp a) -> (if (endp (app a b))
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (app a (app b c))
<-> {Re: def app}
(endp a) -> (if (endp (if (endp a)
b
(cons (car a) (app (cdr a) b)))
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (app a (app b c))
<-> {Hyp}
(endp a) -> (if (endp (if t
b
(cons (car a) (app (cdr a) b)))
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (app a (app b c))
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (app a (app b c))
<-> {Re: def app}
(endp a) -> (if (endp b)
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (if (endp a)
(app b c)
(cons (car a) (app (cdr a) (app b c)))
<-> {Hyp}
(endp a) -> (if (endp b)
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (if t
(app b c)
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
c
(cons (car (app a b)) (app (cdr (app a b)) c)))
= (app b c)
<-> {Re: def app}
(endp a) -> (if (endp b)
c
(cons (car (if (endp a)
b
(cons (car a) (app (cdr a) b))))) (app (cdr (app a b)) c)))
= (app b c)
<-> {Hyp}
(endp a) -> (if (endp b)
c
(cons (car (if t
b
(cons (car a) (app (cdr a) b))))) (app (cdr (app a b)) c)))
= (app b c)
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
c
(cons (car b) (app (cdr (app a b)) c)))
= (app b c)
<-> {Re: def app}
(endp a) -> (if (endp b)
c
(cons (car b) (app (cdr (if (endp a)
b
(cons (car a) (app (cdr a) b)))) c)))
= (app b c)
<-> {Hyp}
(endp a) -> (if (endp b)
c
(cons (car b) (app (cdr (if t
b
(cons (car a) (app (cdr a) b)))) c)))
= (app b c)
<-> {Re: if-ax1}
(endp a) -> (if (endp b)
c
(cons (car b) (app (cdr b) c)))
= (app b c)
<-> {Re: def app}
(endp a) -> (if (endp b)
c
(cons (car b) (app (cdr b) c)))
= (if (endp b)
c
(cons (car b) (app (cdr b) c)))
<-> {Equal-reflexive}
(endp a) -> t
<-> {Short circuit}
t
#206:
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (app a b) c) = (app a (app b c))
<-> {Re: def app}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (if (not (consp a))
b
(cons (car a) (app (cdr a) b))) c)
=
(app a (app b c))
<-> {Hyp}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (if nil
b
(cons (car a) (app (cdr a) b))) c)
=
(app a (app b c))
<-> {Re: if-ax2}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (cons (car a) (app (cdr a) b)) c)
=
(app a (app b c))
<-> {Re: def app}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (cons (car a) (app (cdr a) b)) c)
=
(if (not (consp a))
(app b c)
(cons (car a) (app (cdr a) (app b c))))
<-> {Hyp}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (cons (car a) (app (cdr a) b)) c)
=
(if nil
(app b c)
(cons (car a) (app (cdr a) (app b c))))
<-> {Re: if-ax2}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (cons (car a) (app (cdr a) b)) c)
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: def app}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(if (not (consp (cons (car a) (app (cdr a) b))))
c
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c)))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: consp-cons}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(if nil
c
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c)))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: if-ax2}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c)))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: car-cons}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (cdr (cons (car a) (app (cdr a) b))) c))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: cdr-cons}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (app (cdr a) b) c))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Hyp}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (cdr a) (app b c)))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Equal-reflexive}
((consp a)
^
(app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
t
<-> {Short Circuit}
t
#214: (app-associative)
(app (app a b) c) = (app a (app b c))
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case:
(not (consp a)) -> (app (app a b) c) = (app a (app b c))
<-> {Re: Def app}
(not (consp a))
->
(app (if (not (consp a))
b
(cons (car a) (app (cdr a) b)))
c)
=
(app a (app b c))
<-> {Hyp & Re: if-ax1}
(not (consp a))
->
(app b c)
=
(app a (app b c))
<-> {Re: def app}
(not (consp a))
->
(app b c)
=
(if (not (consp a))
(app b c)
(cons (car a) (app (cdr a) (app b c))))
<-> {Hyp & Re: if-ax1}
(not (consp a))
->
(app b c)
=
(app b c)
<-> {Equal-reflexive}
(not (consp a))
->
t
<-> {Short Circuit}
t
4. Induction Step
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (app a b) c) = (app a (app b c))
<-> {Re: def app twice}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (if (not (consp a))
b
(cons (car a) (app (cdr a) b)))
c)
=
(if (not (consp a))
(app b c)
(cons (car a) (app (cdr a) (app b c))))
<-> {Hyp & Re: if-ax2 Twice}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(app (cons (car a) (app (cdr a) b)) c)
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: def app}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(if (not (consp (cons (car a) (app (cdr a) b))))
c
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: consp-cons & if-ax2}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car (cons (car a) (app (cdr a) b))) (app (cdr (cons (car a) (app (cdr a) b))) c))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: car-cons}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (cdr (cons (car a) (app (cdr a) b))) c))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Re: cdr-cons}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (app (cdr a) b) c))
=
(cons (car a) (app (cdr a) (app b c)))
<-> {Hyp}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
(cons (car a) (app (app (cdr a) b) c))
=
(cons (car a) (app (app (cdr a) b) c))
<-> {Equal-reflexive}
(consp a) ^ ((app (app (cdr a) b) c) = (app (cdr a) (app b c)))
->
t
<-> {Short Circuit}
t
Q.E.D.
#216: (mapnil-app)
(mapnil (app a b)) = (app (mapnil a) (mapnil b))
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case:
(not (consp a)) -> (mapnil (app a b)) = (app (mapnil a) (mapnil b))
<-> {Re: def app}
(not (consp a))
->
(mapnil (if (not (consp a))
b
(cons (car a) (app (cdr a) b))))
=
(app (mapnil a) (mapnil b))
<-> {Hyp & Re: if-ax1}
(not (consp a))
->
(mapnil b)
=
(app (mapnil a) (mapnil b))
<-> {Re: def mapnil}
(not (consp a))
->
(mapnil b)
=
(app (if (endp a)
nil
(cons nil (mapnil (cdr x))))
(mapnil b))
<-> {Re: def endp & if-ax1}
(not (consp a))
->
(mapnil b)
=
(app nil (mapnil b))
<-> {Re: def app}
(not (consp a))
->
(mapnil b)
=
(if (not (consp nil))
(mapnil b)
(cons (car nil) (app (cdr nil) (mapnil b))))
<-> {Comp}
(not (consp a))
->
(mapnil b)
=
(if t
(mapnil b)
(cons (car nil) (app (cdr nil) (mapnil b))))
<-> {Re: if-ax1}
(not (consp a))
->
(mapnil b)
=
(mapnil b)
<-> {Equal-reflexive}
(not (consp a))
->
t
<-> {Short circuit}
t
4. Induction Step
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(mapnil (app a b)) = (app (mapnil a) (mapnil b))
<-> {Re: def app}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(mapnil (if (not (consp a))
b
(cons (car a) (app (cdr a) b)))
=
(app (mapnil a) (mapnil b))
<-> {Hyp & Re: if-ax2}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(mapnil (cons (car a) (app (cdr a) b)))
=
(app (mapnil a) (mapnil b))
<-> {Re: def mapnil}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(if (endp (cons (car a) (app (cdr a) b)))
nil
(cons nil (mapnil (cdr (cons (car a) (app (cdr a) b))))))
=
(app (mapnil a) (mapnil b))
<-> {Re: def endp}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(if (not (consp (cons (car a) (app (cdr a) b))))
nil
(cons nil (mapnil (cdr (cons (car a) (app (cdr a) b))))))
=
(app (mapnil a) (mapnil b))
<-> {Re: consp-cons & if-ax2}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (cdr (cons (car a) (app (cdr a) b)))))
=
(app (mapnil a) (mapnil b))
<-> {Re: cdr-cons}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(app (mapnil a) (mapnil b))
<-> {Re: def mapnil & def endp}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(app (if (not (consp a))
nil
(cons nil (mapnil (cdr a))))
(mapnil b))
<-> {Hyp & Re: if-ax2}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(app (cons nil (mapnil (cdr a))) (mapnil b))
<-> {Re: def app}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(if (not (consp (cons nil (mapnil (cdr a)))))
(mapnil b)
(cons (car (cons nil (mapnil (cdr a)))) (mapnil b)))
<-> {Re: consp-cons & if-ax2}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(cons (car (cons nil (mapnil (cdr a)))) (mapnil b)))
<-> {Re: car-cons}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil (app (cdr a) b)))
=
(cons nil (mapnil b))
<-> {Hyp}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (app (mapnil (cdr a)) (mapnil b)))
=
(cons nil (mapnil b))
<-> {Re: def app}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (if (not (consp (mapnil (cdr a))))
(mapnil b)
(cons (car (mapnil (cdr a))) (app (cdr (mapnil (cdr a))) (mapnil b)))))
=
(cons nil (mapnil b))
<-> {Hyp & Re: if-ax1}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
(cons nil (mapnil b))
=
(cons nil (mapnil b))
<-> {Equal-reflexive}
(consp a) ^ ((mapnil (app (cdr a) b)) = (app (mapnil (cdr a)) (mapnil b)))
->
t
<-> {Short circuit}
t
#217: (mapnil-rev)
(rev (mapnil a)) = (mapnil (rev a))
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case:
(not (consp a)) -> (rev (mapnil a)) = (mapnil (rev a))
<-> {Re: def mapnil & def endp}
(not (consp a))
->
(rev (if (not (consp a))
nil
(cons nil (mapnil (cdr a)))))
=
(mapnil (rev a))
<-> {Hyp & Re: if-ax1}
(not (consp a))
->
(rev nil)
=
(mapnil (rev a))
<-> {Re: def rev & def endp}
(not (consp a))
->
(rev nil)
=
(mapnil (if (not (consp a))
nil
(app (rev (cdr x)) (cons (car x) nil))))
<-> {Hyp & Re: if-ax1}
(not (consp a))
->
(rev nil)
=
(mapnil nil)
<-> {Re: def mapnil}
(not (consp a))
->
(rev nil)
=
(if (endp nil)
nil
(cons nil (mapnil (cdr nil))))
<-> {Comp & if-ax1}
(not (consp a))
->
(rev nil)
=
nil
<-> {Re: def rev}
(not (consp a))
->
(if (endp nil)
nil
(app (rev (cdr nil)) (cons (car nil) nil)))
=
nil
<-> {Comp & Re: if-ax1}
(not (consp a))
->
nil
=
nil
<-> {Equal-reflexive}
(not (consp a))
->
t
<-> {Short Circuit}
t
4. Induction Step
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(rev (mapnil a)) = (mapnil (rev a))
<-> {Re: def mapnil & def endp}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(rev (if (not (consp a))
nil
(cons nil (mapnil (cdr a))))
=
(mapnil (rev a))
<-> {Hyp & Re: if-ax2}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(rev (cons nil (mapnil (cdr a))))
=
(mapnil (rev a))
<-> {Re: def rev & def endp}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(rev (cons nil (mapnil (cdr a))))
=
(mapnil (if (not (consp a))
nil
(app (rev (cdr a)) (cons (car a) nil))))
<-> {Hyp & Re: if-ax2}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(rev (cons nil (mapnil (cdr a))))
=
(mapnil (app (rev (cdr a)) (cons (car a) nil)))
<-> {Re: def rev}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(if (not (consp (cons nil (mapnil (cdr a)))))
nil
(app (rev (cdr (cons nil (mapnil (cdr a))))) (cons (car (cons nil (mapnil (cdr a)))) nil)))
=
(mapnil (app (rev (cdr a)) (cons (car a) nil)))
<-> {Re: consp-cons & if-ax2}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (rev (cdr (cons nil (mapnil (cdr a))))) (cons (car (cons nil (mapnil (cdr a)))) nil))
=
(mapnil (app (rev (cdr a)) (cons (car a) nil)))
<-> {Re: q216 mapnil-app}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (rev (cdr (cons nil (mapnil (cdr a))))) (cons (car (cons nil (mapnil (cdr a)))) nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))
<-> {Re: cdr-cons}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (rev (mapnil (cdr a))) (cons (car (cons nil (mapnil (cdr a)))) nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))
<-> {Re: car-cons}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (rev (mapnil (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))
<-> {Hyp}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (mapnil (cons (car a) nil)))
<-> {Re: def mapnil & def endp}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (if (not (consp (cons (car a) nil)))
nil
(cons nil (mapnil (cdr x)))))
<-> {Re: consp-cons & if-ax2}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (cons nil (mapnil (cdr x))))
<-> {Comp}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
(app (mapnil (rev (cdr a))) (cons nil nil))
=
(app (mapnil (rev (cdr a))) (cons nil nil))
<-> {Equal-reflexive}
(consp a) ^ ((rev (mapnil (cdr a))) = (mapnil (rev (cdr a))))
->
t
<-> {Short Circuit}
t
Q.E.D.
#218: (rev-rev)
(true-listp a) -> (rev (rev a)) = a
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case:
(not (consp a)) -> ((true-listp a) -> (rev (rev a)) = a)
<-> {Re: def rev & def endp}
(not (consp a)) -> ((true-listp a)
->
(rev (if (not (consp a))
nil
(app (rev (cdr x)) (cons (car x) nil))))
=
a
<-> {Hyp & Re: if-ax1}
(not (consp a)) -> ((true-listp a)
->
(rev nil)
=
a
<-> {Re: def rev & def endp}
(not (consp a)) -> ((true-listp a)
->
(if (not (consp nil))
nil
(app (rev (cdr x)) (cons (car x) nil)))
=
a
<-> {Comp & Re: if-ax1}
(not (consp a)) -> ((true-listp a)
->
nil
=
a
<-> {Re: def true-listp}
(not (consp a)) -> (if (consp a)
(true-listp (cdr a))
(equal a nil))
->
nil
=
a
<-> {Hyp & Re: if-ax2}
(not (consp a)) -> (equal a nil)
->
nil
=
a
<-> {Hyp}
(not (consp a)) -> (equal a nil)
->
t
<-> {Short-circuit}
t
4. Induction Step
(consp a) ^ ((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
((true-listp a) -> (rev (rev a)) = a)
<-> {Re: def rev & def endp}
(consp a) ^ ((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
((true-listp a)
->
(rev (if (not (consp a))
nil
(app (rev (cdr a)) (cons (car a) nil))))
=
a
<-> {Promotion}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(rev (if (not (consp a))
nil
(app (rev (cdr a)) (cons (car a) nil))))
=
a
<-> {Hyp & Re: if-ax2}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(rev (app (rev (cdr a)) (cons (car a) nil)))
=
a
<-> {Re: Q219 rev-app}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (rev (cons (car a) nil)) (rev (rev (cdr a))))
=
a
<-> {Hyp}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (rev (cons (car a) nil)) (cdr a))
=
a
<-> {Re: def rev & def endp}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app ((if (not (consp (cons (car a) nil))))
nil
(app (rev (cdr (cons (car a) nil))) (cons (car (cons (car a) nil)) nil)))
(cdr a))
=
a
<-> {Re: consp-cons & if-ax2}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (app (rev (cdr (cons (car a) nil))) (cons (car (cons (car a) nil)) nil))
(cdr a))
=
a
<-> {Re: cdr-cons}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (app (rev nil) (cons (car (cons (car a) nil)) nil))
(cdr a))
=
a
<-> {Re: car-cons}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (app (rev nil) (cons (car a) nil))
(cdr a))
=
a
<-> {Re: def rev & def endp}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (app (if (not (consp nil))
nil
(app (rev (cdr nil)) (cons (car nil) nil)))
(cons (car a) nil))
(cdr a))
=
a
<-> {Comp & Re: if-ax1}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (app nil (cons (car a) nil))
(cdr a))
=
a
<-> {Re: def app & def endp}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (if (not (consp nil))
(cons (car a) nil)
(cons (car nil) (app (cdr nil) (cons (car a) nil))))
(cdr a))
=
a
<-> {Comp & Re: if-ax1}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(app (cons (car a) nil) (cdr a))
=
a
<-> {Re: def app & def endp}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(if (not (consp (cons (car a) nil)))
(cdr a)
(cons (car (cons (car a) nil)) (app (cdr (cons (car a) nil)) (cdr a))))
=
a
<-> {Re: consp-cons & if-ax2}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(cons (car (cons (car a) nil)) (app (cdr (cons (car a) nil)) (cdr a)))
=
a
<-> {Re: car-cons}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(cons (car a) (app (cdr (cons (car a) nil)) (cdr a)))
=
a
<-> {Re: cdr-cons}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(cons (car a) (app nil (cdr a)))
=
a
<-> {Re: def app & def endp}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(cons (car a) (if (not (consp nil))
(cdr a)
(cons (car nil) (app (cdr nil) (cdr a)))))
=
a
<-> {Comp & Re: if-ax1}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
(cons (car a) (cdr a))
=
a
<-> {Re: cons-car-cdr axiom}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
a
=
a
<-> {Equal-reflexive}
(consp a) ^ (true-listp a)
^
((true-listp (cdr a)) -> (rev (rev (cdr a))) = (cdr a))
->
t
<-> {Short Circuit}
t
Q.E.D.
#220: (mem-app)
(mem e (app a b)) <-> ((mem e a) | (mem e b))
lemma: (x <-> x) ; due to equal-reflexive, anything is iff equivalent to itself.
{Sruct Ind.}
1. a is the induction variable
2. a -> cdr a
3. Base Case:
(not (consp a)) ->
((mem e (app a b))
<->
((mem e a) | (mem e b)))
<-> {Re: def app & def endp}
(not (consp a)) ->
((mem e (if (not (consp a)
b
(cons (car a) (app (cdr a) b))))
<->
((mem e a) | (mem e b)))
<-> {Hyp & Re: if-ax1}
(not (consp a)) ->
(mem e b)
<->
((mem e a) | (mem e b)))
<-> {Re: def mem & def endp}
(not (consp a)) ->
(mem e b)
<->
((if (not (consp a))
nil
(if (equal x (car y))
t
(mem x (cdr y)))) | (mem e b))
<-> {Hyp & Re: if-ax1}
(not (consp a)) ->
(mem e b)
<->
(nil | (mem e b))
<-> {Short Circuit}
(not (consp a)) ->
(mem e b)
<->
(mem e b)
<-> {Re: def lemma}
(not (consp a)) -> t
<-> {Short Circuit}
t
4. Induction Step
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
((mem e (app a b))
<->
((mem e a) | (mem e b))
<-> {Re: def app & def endp}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
((mem e (if (not (consp a))
b
(cons (car a) (app (cdr a) b)))
<->
((mem e a) | (mem e b))
<-> {Hyp & Re: if-ax2}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(mem e (cons (car a) (app (cdr a) b)))
<->
((mem e a) | (mem e b))
<-> {Re: def mem & def endp}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (not (consp (cons (car a) (app (cdr a) b))))
nil
(if (equal e (car (cons (car a) (app (cdr a) b))))
t
(mem e (cdr (cons (car a) (app (cdr a) b))))))
<->
((mem e a) | (mem e b))
<-> {Re: consp-cons & if-ax2}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (equal e (car (cons (car a) (app (cdr a) b))))
t
(mem e (cdr (cons (car a) (app (cdr a) b)))))
<->
((mem e a) | (mem e b))
<-> {Re: cdr-cons}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (equal e (car (cons (car a) (app (cdr a) b))))
t
(mem e (app (cdr a) b)))
<->
((mem e a) | (mem e b))
<-> {Re: car-cons}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (equal e (car a))
t
(mem e (app (cdr a) b)))
<->
((mem e a) | (mem e b))
<-> {Re: def mem & def endp}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (equal e (car a))
t
(mem e (app (cdr a) b)))
<->
(if (not (consp a))
nil
(if (equal e (car a))
t
(mem e (cdr a)))) | (mem e b)
<-> {Hyp & Re: if-ax2}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (equal e (car a))
t
(mem e (app (cdr a) b)))
<->
(if (equal e (car a))
t
(mem e (cdr a))) | (mem e b)
<-> {Hyp}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
(if (equal e (car a))
t
(mem e (app (cdr a) b)))
<->
(if (equal e (car a))
t
(mem e (app (cdr a) b)))
<-> {Re: def lemma}
(consp a) ^ ((mem e (app (cdr a) b)) <-> ((mem e (cdr a)) | (mem e b)))
->
t
<-> {Short Circuit}
t
Q.E.D.