(def-language state-machine-language (base-types state action) (constants (tr (state action state prop)) (initial (state prop)) (accepting (state prop))))

(def-theory state-machines (language state-machine-language) (component-theories h-o-real-arithmetic))

(def-constant historyRemark: This entry is multiply defined. See: [1] [2]"lambda(s_seq:[nn,state], a_seq:[nn,action], (#(s_seq(0)) implies initial(s_seq(0))) and forall(i:nn, #(s_seq(i+1)) implies tr(s_seq(i),a_seq(i),s_seq(i+1))))"(theory state-machines) (usages transportable-macete))

(def-constant state%historyRemark: This entry is multiply defined. See: [1] [2]"lambda(s_seq:[nn,state], forsome(a_seq:[nn,action], history(s_seq, a_seq)))"(theory state-machines) (usages transportable-macete))

(def-constant action%history"lambda(a_seq:[nn,action], forsome(s_seq:[nn,state], history(s_seq, a_seq)))"(theory state-machines) (usages transportable-macete))

(def-constant accessibleRemark: This entry is multiply defined. See: [1] [2]"lambda(s:state, forsome(s_seq:[nn,state], a_seq:[nn,action], i:nn, history(s_seq, a_seq) and s_seq(i)=s))"(theory state-machines) (usages transportable-macete))

(def-constant in%language"lambda(a_seq:[nn,action], forsome(s_seq:[nn,state], history(s_seq, a_seq) and accepting(s_seq(length(s_seq)-1))))"(theory state-machines) (usages transportable-macete)) (theory-import-transportable-rewrite-rules (name->theory 'state-machines) (list sequences))

(def-theorem histories-defined-on-state-segment"forall(s_seq:[nn,state], a_seq:[nn,action], i,j:zz, history(s_seq, a_seq) and #(s_seq(j)) and i<=j and 0<=i implies #(s_seq(i)))"(theory state-machines) (usages tranportable-macete) (proof"$theories/state-machines/proofs/histories-defined-on-state-segment.t"))

(def-theorem histories-defined-on-action-segment"forall(s_seq:[nn,state], a_seq:[nn,action], i,j:zz, history(s_seq, a_seq) and #(s_seq(j+1)) and i<=j and 0<=i implies #(a_seq(i)))"(theory state-machines) (usages tranportable-macete) (proof"$theories/state-machines/proofs/histories-defined-on-action-segment.t"))

(def-theorem histories-defined-at-0"forall(s_seq:[nn,state], a_seq:[nn,action], j:zz, history(s_seq, a_seq) and #(s_seq(j)) implies #(s_seq(0)))"(theory state-machines) (usages ) (proof"$theories/state-machines/proofs/histories-defined-at-0.t"))

(def-theorem fundamental-sm-thm"forall(p:[state,prop], (forall(s:state, initial(s) implies p(s)) and forall(s_1, s_2:state, a:action, (p(s_1) and tr(s_1, a, s_2)) implies p(s_2))) implies forall(s:state, accessible(s) implies p(s)))"(theory state-machines) (usages ) (proof"$theories/state-machines/proofs/fundamental-sm-thm.t"))

(def-theorem initial-implies-accessible"forall(s:state, initial(s) implies accessible(s))"(theory state-machines) (usages transportable-macete) (proof"$theories/state-machines/proofs/initial-implies-accessible.t"))

(def-theorem tr-preserves-accessible"forall(s_1,s_2:state, a:action, accessible(s_1) and tr(s_1,a,s_2) implies accessible(s_2))"(theory state-machines) (usages transportable-macete) (proof"$theories/state-machines/proofs/tr-preserves-accessible.t"))

(def-theorem converse-sm-induction"forall(p:[state,prop], forall(s:state, accessible(s) implies p(s)) implies forall(s:state, initial(s) implies p(s)) and forall(s_1,s_2:state,a:action, accessible(s_1) and p(s_1) and tr(s_1,a,s_2) implies p(s_2)))"(theory state-machines) (usages ) (proof"$theories/state-machines/proofs/converse-sm-induction.t"))

(def-theorem sm-induction"forall(p:[state,prop], forall(s:state, initial(s) implies p(s)) and forall(s_1,s_2:state,a:action, accessible(s_1) and p(s_1) and tr(s_1,a,s_2) implies p(s_2)) implies forall(s:state, accessible(s) implies p(s)))"(theory state-machines) (usages ) (proof"$theories/state-machines/proofs/sm-induction.t"))

(def-theorem sm-induction-biconditional"forall(p:[state,prop], (forall(s:state, initial(s) implies p(s)) and forall(s_1, s_2:state, a:action, (accessible(s_1) and p(s_1) and tr(s_1, a, s_2)) implies p(s_2))) iff forall(s:state, accessible(s) implies p(s)))"(theory state-machines) (usages ) (proof"$theories/state-machines/proofs/sm-induction-biconditional.t"))

(def-theorem sm-induction-biconditional-conv"forall(p:[state,prop], forall(s:state, accessible(s) implies p(s)) iff (forall(s:state, initial(s) implies p(s)) and forall(s_1, s_2:state, a:action, (accessible(s_1) and p(s_1) and tr(s_1, a, s_2)) implies p(s_2))))"(theory state-machines) (usages ) (proof"$theories/state-machines/proofs/sm-induction-biconditional-conv.t"))

(def-inductor sm-induct sm-induction-biconditional-conv (theory state-machines) (base-case-hook eliminate-nonrecursive-definitions-and-simplify))

(def-theory-ensemble state-machines) (pop-current-theory)