(def-language det-state-machine-language
    (base-types state action)
    (constants 
      (next (state action state))))
            

(def-theory det-state-machines 
    (language det-state-machine-language)
    (component-theories state-machines)
    (axioms
      (tr-means-next
        "forall(s:state, a:action, s_1:state, tr(s,a,s_1) iff next(s,a)=s_1)"
        rewrite)))
(language-from-definition
  '(start-det-state-machine-language
      (base-types state action)
      (constants 
        (s_init state))))

(def-theorem next-preserves-accessible 
  "forall(s,s_1:state, a:action, accessible(s) and next(s,a)=s_1 implies accessible(s_1))"
  (theory det-state-machines)
  (usages )
  (proof "$theories/state-machines/proofs/next-preserves-accessible.t"))

(def-theorem run-next 
  "forall(s_1:state,a:action,a_seq:[nn,action], 
 	 run(next(s_1,a),a_seq)==run(s_1,cons(a,a_seq)))"
  (theory det-state-machines)
  (usages transportable-macete)
  (proof "$theories/state-machines/proofs/run-next.t"))

(def-theorem det-fun-sm-thm 
  "forall(p:[state,prop],
	(forall(s:state, initial(s) implies p(s))
	and
	  forall(s:state, a:action,
		p(s)
		implies
		p(next(s,a))))
	implies
	  forall(s:state, accessible(s) implies p(s)))"
  (theory det-state-machines)
  (usages transportable-macete)
  (proof "$theories/state-machines/proofs/det-fun-sm-thm.t"))

(def-theorem dsm-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:state,a:action, 
	    accessible(s_1) and p(s_1) and #(next(s_1,a))
	    implies
	    p(next(s_1,a)))))"
  (theory det-state-machines)
  (usages transportable-macete)
  (proof "$theories/state-machines/proofs/dsm-induction-biconditional-conv.t"))

(def-theorem dsm-induction-biconditional 
    "forall(p:[state,prop],
	(forall(s:state,  initial(s) implies p(s))
 	 and 
	  forall(s_1:state,a:action, 
	    accessible(s_1) and p(s_1) and #(next(s_1,a))
	    implies
	    p(next(s_1,a))))
 	 iff
 	 forall(s:state, accessible(s) implies p(s)))"
    (theory det-state-machines)
    (usages transportable-macete)
    (proof;just cite the preceding and simplify.
      ""))

(def-theorem run-run-lemma 
  "forall(a_seq_1:[nn,action], 
          f_seq_q(a_seq_1) implies
                forall(s_1:state, a_seq_2:[nn,action],
	run(run(s_1,a_seq_1),a_seq_2)==run(s_1, append(a_seq_1,a_seq_2))))"
  (theory det-state-machines)
  (usages )
  (proof "$theories/state-machines/proofs/run-run-lemma.t"))
(qr "forall(a_seq_1:[nn,action], 
          f_seq_q(a_seq_1) implies
                forall(s_1:state, a_seq_2:[nn,action],
	run(s_1, append(a_seq_1,a_seq_2))==run(run(s_1,a_seq_1),a_seq_2)))")

(def-theorem run-run 
  "forall(s_1:state, a_seq_1, a_seq_2:[nn,action], 
          f_seq_q(a_seq_1) implies
	run(run(s_1,a_seq_1),a_seq_2)==run(s_1, append(a_seq_1,a_seq_2)))"
  (theory det-state-machines)
  (usages transportable-macete)
  (proof "$theories/state-machines/proofs/run-run.t"))

(def-constant after 
    "lambda(a_seq:[nn,action], run(s_init, a_seq))"
    (theory det-state-machines-with-start)
    (usages transportable-macete))
(language-from-definition
  '(det-state-machine-sublanguage
      (embedded-languages det-state-machine-language start-det-state-machine-language)))