(structure Nat 
  zero
  (succ Nat))

(declare less (-> (Nat Nat) Boolean))

(declare plus (-> (Nat Nat) Nat))


(define (if-then-else ?b ?a1 ?a2)
  (the ?x 
     (and (if ?b ?a1)
          (if (not ?b) ?a2))))

  (forall ?b
    (forall ?a1
      (forall ?a2
        (forall ?x
          (iff (equal (if-then-else ?b ?a1 ?a2) ?x)
               (and (if ?b (equal ?x ?a1))
                    (if (not ?b) (equal ?x ?a2)))))))))

(define eq-symmetry
  (method (t1 t2) 
    (dlet ((t1=t2 $(equal t1 t2))
           (v (fresh-var t1 t2))
           (property (equal v t1))
           (t1=t1<==>t2=t1 (!leibniz t1 t2 property v))
           (t1=t1==>t2=t1 (!left-iff t1=t1<==>t2=t1))
           (t1=t1 (!eq-reflex t1)))
      (!mp t1=t1==>t2=t1 t1=t1))))



(assume (equal ?x zero)
  (!eq-symmetry ?x zero))

(define eq-tran
;; This method takes three terms t1, t2, and t3 such that
;; t1 = t2 and t2 = t3 hold, and derives the equality t1 = t3.
;;

(define eq-tran
  (method (t1 t2 t3)
    (dlet ((t1=t2 $(equal t1 t2))
           (t2=t3 $(equal t2 t3))
           (v (fresh-var t1 t2 t3))
           (prop (equal v t3))
           (t1=t3<==>t2=t3 (!leibniz t1 t2 prop v))
           (t2=t3==>t1=t3 (!right-iff t1=t3<==>t2=t3)))
      (!mp t2=t3==>t1=t3 t2=t3))))
           

(define eq-congruence
  (method (t1 t2 t v)
    (dlet ((t1=t2 $(equal t1 t2))
           (v' (fresh-var t1 t2 v))
           (new-t (term-replace v v' t))
           (newt{t2/v'} (term-replace v' t2 new-t))
           (prop (equal new-t newt{t2/v'}))
           (newt{t1/v'}=newt{t2/v'}<==>newt{t2/v'}=newt{t2/v'} (!leibniz t1 t2 prop v'))
           (newt{t2/v'}=newt{t2/v'}==>newt{t1/v'}=newt{t2/v'}
                (!right-iff newt{t1/v'}=newt{t2/v'}<==>newt{t2/v'}=newt{t2/v'}))
           (newt{t2/v'}=newt{t2/v'} (!eq-reflex newt{t2/v'})))
      (!mp newt{t2/v'}=newt{t2/v'}==>newt{t1/v'}=newt{t2/v'}
           newt{t2/v'}=newt{t2/v'}))))
           

(assert (equal ?x ?y)
        (equal ?y ?z))

(!eq-tran ?x ?y ?z)
