(load-file "general-alloy-lemmas.ath")


;; --------------- FIRST DIRECTION (Soundness) --------------- 

(define lemma1 "ALL n x | [n x] in data ==> [x] in elms(n)")

(!pf lemma1 [scalar-lemma elms-uber-axiom union-axiom])
               
(define ind-lemma "ALL k m n x | [n m] in next^k & [m x] in data ==> [x] in elms(n)")

(define (goal k)
  (forall ?m ?n ?x "[n m] in next^k & [m x] in data ==> [x] in elms(n)"))

(by-induction-on ?k (goal ?k)
  (zero (!pf (goal zero) [lemma1 elms-uber-axiom 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-uber-axiom union-axiom])))))

(define inclusion-1
  (pick-any n
    (!prove-subsets (sbdot (sbdot (scalar n) (rtc next)) data) (elms n)
      [elms-uber-axiom star-pow-lemma sbdot-axiom scalar-lemma ind-lemma])))

;; ---------------  SECOND DIRECTION (Completeness) --------------- 

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

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

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

(define inclusion-2 (!list-induction ind-goal))

;; -------------- FINAL EQUALITY CONCLUSION --------------- 

(!pf "ALL n | elms(n) = ({[n]}.next*).data" [inclusion-1 inclusion-2 set-equality])