(load-file "elms-proof.ath")

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;

(define (test1)
(dbegin
(!pf subset-trans [subset-axiom])
(!pf union-lemma-1 [subset-axiom union-axiom])
(!pf dot-theorem [sbdot-axiom cons-axiom subset-axiom])
(!pf scalar-lemma [sbdot-axiom singleton-axiom cons-injectivity id-axiom])
(!pf singleton-subset-lemma [subset-axiom singleton-axiom id-axiom])
(!pf star-pow-lemma [sbdot-axiom scalar-lemma rtc-axiom])
(!pf set-equality [ext-axiom subset-axiom])
(dlet ((goal (function (k) 
               (forall ?k2 ?x ?y ?z ?R
                 "[x y] in R^k & [y z] in R^k2 ==> [x z] in R^k+k2"))))
  (by-induction-on ?k1 (goal ?k1)
    (zero (!pf (goal zero) [plus-axiom-1 pow-axiom-1 id-axiom]))
    ((succ k) (dlet ((ind-hyp (goal k)))
                (!pf (goal (succ k)) [plus-axiom-2 pow-axiom-2 ind-hyp id-axiom])))))
(pick-any x y R
  (assume-let ((hyp "[y] in {[x]}.R*"))
     (dlet ((L (!pf "ALL t | t in {[y]}.R* ==> t in {[x]}.R*" 
		    [hyp power-sum-lemma rtc-axiom scalar-lemma cons-axiom])))
        (!pf "{[y]}.R* subset {[x]}.R*" [L subset-axiom]))))
(!pf rtc-zero-lemma [pow-axiom-1 id-axiom])
(!pf reflex-clos-lemma [pow-axiom-1 rtc-axiom id-axiom])
(!pf first-power-lemma-1 [rtc-zero-lemma id-axiom pow-axiom-2])
(!pf first-power-lemma-2 [rtc-axiom first-power-lemma-1])
(!pf subset-ref-lemma [reflex-clos-lemma scalar-lemma id-axiom singleton-axiom singleton-subset-lemma])
(!pf lemma-L1 [subset-ref-lemma dot-theorem])))


(define (id x) x)

(define (test M n)
  (dcheck ((equal? n 0) (!M))
          (else (dlet ((foo (id (!M)))) (!test M (minus n 1)))))) 

(define (s)
(dlet ((ind-lemma "ALL k m n x | [n m] in next^k & [m x] in data ==> [x] in elms(n)")
        (goal (function (k)
                (forall ?m ?n ?x "[n m] in next^k & [m x] in data ==> [x] in elms(n)")))
        (foo   (by-induction-on ?k (goal ?k)
           (zero (!pf (goal zero) [lemma1 elms-semantics pow-axiom-1 id-axiom]))
            ((succ k) (pick-any m n x 
	            (assume-let ((hyp "[n m] in next^k+1 & [m x] in data"))
 	              (!pf "[x] in elms(n)" [hyp (goal k) pow-axiom-2 elms-semantics 
			     	             union-lemma-1 union-axiom])))))))
           (pick-any n
	    (!prove-subsets (sbdot (sbdot (scalar n) (rtc next)) data) (elms n)
	      [elms-semantics star-pow-lemma sbdot-axiom scalar-lemma ind-lemma]))))


(define (c)
(dlet ((base-step "ALL n | ~(EXISTS m | [n m] in next) ==> elms(n) subset ({[n]}.next*).data)")
       (ind-goal (function (n)
               (subset "elms(n)" "({[n]}.next*).data")))
      (ind-step (pick-any x y
      (assume-let ((hyp "[x y] in next")
                   (ihyp (ind-goal y)))
        (dlet ((P1 (!pf "elms(x) = {[x]}.data union elms(y)" [elms-semantics hyp]))
	       (P2 (!pf "{[y]}.next* subset {[x]}.next*" [hyp comp-monotonicity scalar-lemma first-power-lemma-2]))
               (P3 (!pf "({[y]}.next*).data subset ({[x]}.next*).data" [P2 dot-theorem]))
               (P4 (!pf "elms(y) subset ({[x]}.next*).data" [P3 ihyp subset-trans])))
          (!pf "elms(x) subset ({[x]}.next*).data" [P1 lemma-L1 P4 union-lemma-1 id-axiom]))))))
  (!list-induction ind-goal)))