Question Z:
 Z1:
(implies (and (endp x)
	      (tlp y))
         (tlp (app x y)))

------------
Context:   |
A1: (endpx)|
A2: (tlp y)|
___________

proof: 
	(tlp (app x y))
	<= { def app, A1, if-true}
	(tlp y)
	<= {A2}
	t
QED

===============================================================
Z2:
(implies (and (consp x) 
	      (tlp (app (cdr) y))
	 (tlp (app x y)))

--------------
Context:     
A1: (consp x)
A2: (tlp (app (cdr x) y))  
___________

	(tlp (app x y))
	<= { def app, if-false, A1}
	(tlp (cons (car x) app (cdr x) y)
	<= {def tlp ,def endp, A1, consp-cons}
	(tlp (app (cdr x) y))
	<= {A2}
	t
QED
===============================================================
Z3:
(implies (endp x)
	 (tlp (rev x)))
 
--------------
Context:     
A1: (endp x)
___________
Proof:
	(tlp (rev x))
	<={ def rev, A1, if-true}
	(tlp nil)
	<={ def tlp A1 , evaluate}
	t

QED
===============================================================
Z4:
(tlp (consp x)
     (tlp (rev x)))

-----------------
Context: 
A1: (consp x)
----------------

Proof:
	(tlp (rev x))
	<= { def rev ,A1, if-false, def. endp}
	(tlp (app (rev (cdr x))
 	          (cons (car x) nil)))
	<= { lemma tlp-app instantiated with subsititution ((x (rev (cdr x))) (y (cons (car x) nil))) 
    	(tlp (cons (car x) nil))
	<= {def tlp, consp-cons , endp, A1, if-false, cdr-cons}
	(tlp nil)
        <= {def tlp, evaluate, endpf}
	t

QED
=============================================================================
Z5:
(tlp (rev x))
We will prove this using case-analysis, i.e we use the tautology p =: q /\ ~p =: q =: q
i.e We will prove q assuming p, then we will prove q assuming (not p) and if both proofs
are successfull, that is they are true statements, then we can deduce that q is a true statement.
Case 1: (endp x)

Context:
A1: (endp x)

Proof:
	(tlp (rev x))
	<={ Z3 }
	t 

Case 2: (not (endp x))

Context
A1: (not (endp x))
D1: (consp x) {Def. endp}

Proof:
	(tlp (rev X))
	<={ D1, Z4}
	t
Since we proved both cases, this completes the proof of (tlp (rev x)). i.e we can
deduce that (tlp (rev x)) is true by Prop deduction(case-analysis tautology).
=============================================================================

PART Y

Y2:
(and (implies (endpx X)
	      (booleanp (in a X)))
     (implies (and (consp X)
                   (booleanp (in a (cdr X))))
	      (booleanp (in a X) 

Since we have the form  (AND  P1 P2)
for this to be true both P1 and P2 should be true.
So we will prove both, lets name P1 and P2 as Subgoal 1
and Subgoal 2.

Subgoal 1: 
(implies (endpx X)
	 (booleanp (in a X)))

Context 
A1: (endp x)

Proof:
	(booleanp (in a x))
	<= {def in, A1, if-true}
	(booleanp nil)
	<={Evaluation}
	t

Subgoal 2: 
     (implies (and (consp X)
                   (booleanp (in a (cdr X))))
	      (booleanp (in a X) 

Context:
A1: (consp x)
A2: (booleanp (in (a cdr X)))

Proof:
	(booleanp (in a  X))
	<= {def in, A1, endp, if-false}
	(booleanp (or (= a (car x))
	           (in a (cdr x))))

Recall "or" returns the first non-nil argument, we
dont know if (= a (car X)) is true or not, in such a
situation, we simply do case-analysis, in one case assume
its true, and in another assume its not true and & if we
in both cases reduce to t, then we know by Prop Deduction(case-analysis)
the original formula we started out is true(can be derived

Case 1: (= a (car X))
Extended Context1 
A1: (consp X)
A2: (booleanp (in (a cdr X)))
CA1: (= a (car X)) {case assumption} 

Continuing the first subproof from the original goal:
	(booleanp (OR (= a (car x))
	           (in a (cdr x))))
	<= {def OR, CA1}
	(booleanp t)
	<= {evaluation}
	t

Case 2: (not ((= a (car X)))
Extended Context2 
A1: (consp X)
A2: (booleanp (in (a cdr X)))
CA2: (not (= a (car X))
Continuing the second subproof from the original goal:
	(booleanp (OR (= a (car x))
	           (in a (cdr x))))
	<= { def. OR , CA2 }
	(booleanp (in a (cdr x)))
	<={ A2 }
	t
So by case-analysis(prop deduction) we can deduce(=>)
(booleanp (or (= a (car x))
	      (in a (cdr x))))
from which we can deduce(=>)
(booleanp (in a  X))
Thus completing our proof of showing that (booleanp (in a X)) is true.