(load-file "elm-lemmas.ath")

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

(!pf lemma1 [scalar-lemma elms-semantics 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-semantics 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-semantics union-lemma-1 union-axiom])))))

;; Final inclusion theorem: ALL n | ({[n]}.next*).data  subset elms(n)
      
(pick-any n
  (!prove-subsets "({[n]}.next*).data"  "elms(n)"  [elms-semantics star-pow-lemma sbdot-axiom scalar-lemma ind-lemma]))