CS313K
J Moore
March 4, 2010
-----------------------------------------------------------------

Given:

(defun rev (x)
  (if (endp x)
      nil
      (app (rev (rest x))
           (cons (first x) nil))))

T1:
(true-listp (app x y)) <--> (true-listp y)

T2:
(true-listp (if x y z)) = (if x (true-listp y) (true-listp z))

Prove:
(true-listp (rev a))

Proof:
(true-listp (rev a))
= {def rev}
(true-listp
 (if (endp a)
     nil
     (app (rev (rest a))
          (cons (first a) nil))))
= {by T2}
(if (endp a)
    (true-listp nil)
    (true-listp
     (app (rev (rest a))
          (cons (first a) nil))))
= {comp}
(if (endp a)
    T
    (true-listp
     (app (rev (rest a))
          (cons (first a) nil))))
<--> {T1}
(if (endp a)
    T
    (true-listp (cons (first a) nil)))
= {def true-listp}
(if (endp a)
    T
    T)
= {if-x-y-y}
T
Q.E.D.