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


(define lemma-2 "ALL n | {[n]}.data subset elms({[n]})")

(!pf lemma-2 [elms-axiom-1 elms-axiom-2 union-axiom subset-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) [lemma-2 pow-axiom-1 scalar-lemma subset-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  vv (is-function next) 
					    scalar-lemma empty-axiom elms-axiom-2 union-axiom])))))

(define Elms-Soundness "ALL n | ({[n]}.next*).data subset elms({[n]})")

(Elms-Soundness BY 
  (pick-any n 
    (!prove-subsets (sbdot (sbdot (scalar n) (rtc next)) data) (elms (scalar n))
         [elms-axiom-1 elms-axiom-2 star-pow-lemma scalar-lemma ind-lemma])))

;===============================  COMPLETENESS ==========================

(define base-step "ALL n | ~(EXISTS m | [n m] in next) ==> elms({[n]}) subset ({[n]}.next*).data)")
(!pf base-step [elms-axiom-1 empty-axiom cons-axiom scalar-lemma 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-axiom-2 hyp vv (is-function next) scalar-lemma empty-axiom]))
	       (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 Elm-Completeness (!list-induction ind-goal))

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

(!pf "ALL n | elms({[n]}) = ({[n]}.next*).data" [Elms-Soundness Elm-Completeness set-equality])