(defun-sk E-Fz (u v)
  (exists z (equal (app u v) (rev z))))

#|

 This generates the following events, where e-fz-witness is a new
 function symbol, a Skolem function. 

 (defun-nx e-fz (u v)
   (let ((z (e-fz-witness u v)))
        (equal (app u v) (rev z))))

 Since we can't say that there exist a function s.t. ... in FO, we
 instead say that if

 (app u v) = (rev z) for any z, then (app u v) = (rev (e-fz-witness u v))

 So, we add the following constraint so that e-fz-witness is not just
 any function, but one restricted by e-fz-suff.

 (defthm e-fz-suff
   (implies (equal (app u v) (rev z))
            (e-fz u v)))

 Now, we can use ACL2s to reason about quantifiers. Typically, we do
 this by defining a function that provides the z above. Here is an
 example.

|#

:pe e-fz
:pf e-fz
:pe e-fz-suff
:pcb! :x

(definecd fz (u :tl v :tl) :tl ; define a function that generates a witness
  (app (rev v) (rev u)))

(property fz-thm (u :tl v :tl) ; show that fz works
  (== (rev (fz u v))
      (app u v))
  :hints (("Goal" :in-theory (enable fz))))

(property (u :tl v :tl) ; prove an existential
  :check-contracts? nil
  (e-fz u v)
  :hints (("goal" :use ((:instance e-fz-suff (z (fz u v)))))))

; Proof builder version
(verify
 (implies (and (tlp u) (tlp v))
          (e-fz u v)))
 th
 pro
 th
 sr
 (r 1 ((z (fz u v))))
 th
 bash
 (exit t)

(property foo (u :tl v :tl) ; prove an existential
  :check-contracts? nil
  (e-fz u v)
  :INSTRUCTIONS (:PRO (:REWRITE E-FZ-SUFF ((Z (FZ U V))))
                      :BASH))

#|

 Discuss: How do we use a UResolution theorem prover to reason about
 ACL2s?

 Consistency issues: Definitional principle! Termination!

 Induction: Can add induction axioms

 What is needed to reason about associativity of append?
   Definitions
   Equality 
   Induction
   Contract Theorems
   Formalization of cons, car, cdr, tlp, endp, etc.

|#


#|

 Discussed how to turn associativity of append into a conjecture that
 a resolution-based theorem prover can handle. 

 This was the scratch work.

 Axioms for car/cdr/cons/consp:

 [(car (cons a b)) = a]
 [(cdr (cons a b)) = b]
 [(consp (cons a b))]

 Conjecture:
 [~(tlp x) v ~(tlp y) v ~(tlp z) v (A (A x y) z) = (A x (A y z))]

 Turning this into CNF

{{(car (cons a b)) = a}
 {(cdr (cons a b)) = b}
 {(consp (cons a b))}
 {~(consp x) v (tlp x) = (tlp (cdr x))}
 { (consp x) v (tlp x) = (== x nil)}
 {~(tlp x) v ~(tlp y) v ~(tlp z) v (A (A x y) z) = (A x (A y z))}}

 We still need axioms for endp, definition of Append, induction
 schemes, etc and we need to get rid of = and use the equality axioms,
 schemas, so we will wind up with a very complex formula.

|#