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


(define lemma-2 "ALL n: Node | n.data in elms(n)")

(!pf lemma-2 [elms-axiom-1 elms-axiom-2 union-axiom subset-axiom])

(define ind-lemma "ALL k m: Node n: Node x: Element | m in n.next^k & x in m.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: Node | n.next*.data in 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: Node | ~(EXISTS m: Node | [n m] in next) ==> elms(n) in (n.next*).data)")
(!pf base-step [elms-axiom-1 empty-axiom scalar-lemma lemma-L1])

(define (ind-goal n)
  (in "elms(n)" "n.next*.data"))

(define ind-step
  (pick-any x: Node y: Node
      (assume-let ((hyp "y in x.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* in x.next*" [hyp comp-monotonicity scalar-lemma first-power-lemma-2]))
               (P3 (!pf "y.next*.data in x.next*.data" [P2 dot-theorem]))
               (P4 (!pf "elms(y) in x.next*.data" [P3 ihyp subset-trans])))
          (!pf "elms(x) in 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])