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

(define lemma-1 "ALL n x | [n x] in data ==> (ALL S | elms({[n]},S) ==> [x] in S)")

(!pf lemma-1 [scalar-lemma elms-semantics union-axiom])

(define ind-lemma "ALL k m n x S | [n m] in next^k & [m x] in data & elms({[n]},S) ==> [x] in S")

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

(by-induction-on ?k (goal ?k)
  (zero (!pf (goal zero) [lemma-1 pow-axiom-1 id-axiom]))
  ((succ k) (pick-any m n x S
	      (assume-let ((hyp "[n m] in next^k+1 & [m x] in data & elms({[n]},S)"))
                (dlet ((P (!pf "EXISTS z S' | [n z] in next & [z m] in next^k & elms({[z]},S') & S = S' union {[n]}.data" 
	                    [hyp elms-semantics next-is-partial-fun empty-axiom scalar-lemma  pow-axiom-2])))
		  (!pf "[x] in S" [P hyp (goal k) union-axiom]))))))
;scalar-lemma

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

(Elms-Soundness BY 
  (pick-any n S
    (assume-let ((hyp "elms({[n]},S)"))
      (!prove-subsets  (sbdot (sbdot (scalar n) (rtc next)) data) S
         [hyp elms-semantics star-pow-lemma sbdot-axiom scalar-lemma ind-lemma]))))

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