(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)