(def-language fts-language
    (embedded-language det-state-machines-with-start)
    (constants 
      (secure%state (state prop))))

(def-theory fts-theory 
    (language fts-language)
    (component-theories det-state-machines-with-start))

(def-theorem fun-sec 
    "secure%state(s_init) 
            and
          forall(s:state,a:action, 
	secure%state(s) and #(next(s,a))
              implies secure%state(next(s,a)))
      implies forall(s:state, accessible(s) implies secure%state(s)) "
    (theory fts-theory)
    (proof "$theories/state-machines/proofs/fun-sec.t"))

(def-theory fts+invariant 
    (component-theories fts-theory)
    (axioms
      (fts+init-secure "secure%state(s_init)" rewrite)
      (fts+next-secure
            "forall(s:state,a:action, 
	secure%state(s) and #(next(s,a))
              implies secure%state(next(s,a)))")))
            

(def-theorem fts+secure 
    "forall(s:state, accessible(s) implies secure%state(s))"
    (theory fts+invariant)
    (usages transportable-macete)
    (proof "$theories/state-machines/proofs/fts+secure.t.z"))
    
    
(pop-current-theory)
(pop-current-syntax)