(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  history 
  Remark: 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%history 
  Remark: 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  accessible 
  Remark: 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)