Question A

   (= (len (rev (app (rev x)
               (rev y))))
      (len (app (rev y)
           (rev x))))

We will use the LHS = RHS proof format

LHS : 
   (len (rev (app (rev x)
               (rev y))))
={instantiate len-rev-same with ((x (app (rev x) (rev y))}    * 5 points
   (len (app (rev x)
               (rev y)))
={instantiate len-app with ((x (rev x) y (rev y))}            * 5 points
   (+ (len (rev x))
      (len (rev y)))
={instantiate len-rev-same)                                   * 3 points
   (+ (len x)
      (len y))
  
RHS : 
   (len (app (rev y)
        (rev x)))
={instantiate len-app with ((x (rev x)) (y (rev y)))}            * 5 points
   (+ (len (rev y))
      (len (rev x)))
={instantiate len-rev-same with the appropriate substitution}    * 3 points
   (+ (len y)
      (len x))
={arithmetic}                                                    * 4 points
   (+ (len x)
      (len y))

Since both LHS and RHS are equal to the same formula, by transitivity of equality the original 
formula is true (theorem). QED.  
______________________________________________________________________________________
Question B

(= (len (app (rev x)
            (app y (rev z))))
    (+  (len (app x z))
          (len (rev y))))

LHS:
	(len (app (rev x)
             (app y (rev z))))
= {for outer len Instantiate len-app with ((x (rev x)) (y app y (rev z)))}   * 5 points
	(+ (len (rev x))
      (len (app y (rev z))))
= {for second len instantiate len-app with ((x y) (y rev z))}                * 4 points
	(+ (len (rev x)) 
      (+ (len y) (len (rev z))))
={Instantiate len-rev-same with (x (rev x)) in the first len}                * 3 points
	(+ (len x) (+ (len y) (len (rev z))))
={Instantiate len-rev-same with (x (rev z)) in the len}                      * 2 points
	(+ (len x) (+ (len y) (len z)))



RHS:
   (+ (len (app x z))
      (len (rev y))))
= {Instantiate len-app ((x x) (y z))}             * 5 points 
   (+ (+ (len x) (len z))
      (len (rev y)))
= {Instantiate len-rev-same with ((y z))}         * 2 points
   (+ (+ (len x) (len z)) (len y)) 
={arithmetic , (natp (len x))}  ( no marks deducted for natp)  
   (+ (len x) (+ (len y) (len z)))                 * 4 points

Since both LHS and RHS are equal to the same formula, by transitivity of 
equality the original formula is true(theorem). QED.  
______________________________________________________________________________________
Question C
5 points for each

1. The instantiation of the definition-axiom for remove-all is not correct

2. (endp (remove-all 5 (list 5 5 5 5)))
<= { Evaluation}
t

3. Not Possible: p => p /\ q is not a tautology

4. (not ( in a x)
<= { definition of in , context (endp x), if-true, evaluation}
    (endp x)

5.  NOt possible. Here is a Counterexample: X := '(5 5 6) a := 5 


6. (in (remove-all a (cdr X))
<= {NOT POSSIBLE unless we have more information}
(in a (remove-all a X))
______________________________________________________________________________________
PART D

(defun scale (A x)
'' Adds every element of A by x''
   (if (endp A)
        nil
       (cons (+ (car A) x)
             (scale (cdr A) x))))


By Propositional Deduction we will prove the two statements * 1 points
1. 
(implies (endp A)
         (= (scale (scale A x) y)
            (scale A (+ x y))))

Context: 
   A1: (endp A)* 1 points

(= (scale (scale A x) y)
   (scale A (+ x y))))
<={def scale, A1, if-true}    * 1 points
   (= nil nil)   * 1 points
<={evaluate}     * 1 points
   t

Subgoal 2:
(implies (and (consp A)
              (=(scale (scale (cdr A) x) y)
                (scale (cdr A) (+ x y))))
              (=(scale (scale A x) y)
                (scale A (+ x y))))

Context:
A2: (consp A)   * 1 points
A3: (= (scale (scale (cdr A) x) y)
       (scale (cdr A) (+ x y)))   * 1 points

   (= (scale (scale A x) y)
      (scale A (+ x y))))

We will do the simpler LHS=RHS proof format

LHS:
   (scale (scale A x) y)
={def scale, def endp, A2, if-false}   * 1 points each = 4 points
   (scale (cons (+ (car A) x)
                  (scale (cdr A) x)) y)   * 1 points
={def scale, consp-cons, if-false,cons-car, cons-cdr}   * 1 credit each = 5 points
   (cons (+ (+ (car A) x) y)
         (scale (scale (cdr A) x) y))   * 1 points
={A3,arithmetic reasoning, (natp(car A)}   * 1 points ( no marks deducted for natp)
   (cons (+ (car A) (+ x y))
         (scale (cdr A) (+ x y)))   * 1 points
={A2,def endp, if-false, close def scale}   * 1 points each = 4 points
   (scale A ( + x y))   * 1 credit

:RHS 
   (scale A (+ x y))))

Since LHS = RHS, the original formula is true. QED.