;(load-file "elms-lemmas-new-1.ath")

(load-file "parse1.ath")

(define subset-trans "ALL s1 s2 s3 | (s1 subset s2) & (s2 subset s3) ==> s1 subset s3")
(define union-lemma-1 "ALL s1 s2 s | (s1 subset s) & (s2 subset s) ==> (s1 union s2) subset s")
(define dot-theorem "ALL s1 s2 R | s1 subset s2 ==> s1.R subset s2.R")
(define scalar-lemma "ALL x y R | [y] in {[x]}.R <==> [x y] in R")
(define singleton-subset-lemma "ALL x S | {x} subset S <==> x in S")
(define star-pow-lemma "ALL x n R S | [x] in ({[n]}.R*).S ==> (EXISTS m k | [n m] in R^k & [m x] in S)")

(!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])

(define power-sum-lemma "ALL k1 k2 x y z R | [x y] in R^k1 & [y z] in R^k2 ==> [x z] in R^k1+k2")

(define (goal k) 
   (forall ?k2 ?x ?y ?z ?R
     "[x y] in R^k & [y z] in R^k2 ==> [x z] in R^k+k2"))

;; Here's the proof of power-sum-lemma -- a simple induction on k1:

(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]))))

(define comp-monotonicity "ALL x y R | [y] in {[x]}.R* ==> {[y]}.R* subset {[x]}.R*")

(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]))))

(!claim comp-monotonicity)			           

(define rtc-zero-lemma "ALL n R | [n n] in R^0")
(define reflex-clos-lemma  "ALL n R | [n n] in R*")
(define first-power-lemma-1 "ALL x y R | [x y] in R ==> [x y] in R^1")
(define first-power-lemma-2 "ALL x y R | [x y] in R ==> [x y] in R*")
(define subset-ref-lemma "ALL n R | {[n]} subset {[n]}.R*")
(define lemma-L1 "ALL n | {[n]}.data subset ({[n]}.next*).data")

(!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 (exp1 n)
  (sbdot (scalar n) (rtc next)))

(define (exp2 n)
  (sbdot (exp1 n) data))

(define (ind-goal n)
  (subset (elms n) (exp2 n)))

(define (ind-goal n)
  (subset "elms(n)" 
          "({[n]}.next*).data"))

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

(define base-step "ALL n | ~(EXISTS m | [n m] in next) ==> elms(n) subset ({[n]}.next*).data)")

(!pf base-step [elms-semantics lemma-L1])

(define 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])))))


(assert acyclicity)

(define inductive-proof
  (!list-induction ind-goal))