(def-constant act_ff"lambda(p:ff, a:uu, q:ff, forall(u:uu, q(u) subseteq p(a**u)))"(theory directed-monoid-theory))

(def-theorem act_ff-is-act"forall(s,t:uu,p,r:ff, act_ff(p,s**t,r) iff forsome(q:ff,act_ff(p,s,q) and act_ff(q,t,r)))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally act_ff) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0)") (instantiate-existential ("lambda(u:uu, p(s**u))")) beta-reduce-repeatedly (block (script-comment"`instantiate-existential' at (0 1 0)") beta-reduce-repeatedly (incorporate-antecedent"with(t,s:uu,p,r:ff,forall(u:uu,r(u) subseteq p((s**t)**u)));") (apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids) simplify) (block (script-comment"`instantiate-existential' at (1)") (cut-with-single-formula"#(p,ff)") (incorporate-antecedent"with(p:ff,#(p,ff));") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally failure_q) (unfold-single-defined-constant-globally support) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 0)") (backchain"with(p:prop,forall(u:uu,x,y:sets[action],p));") (instantiate-existential ("y_$0"))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0)") (backchain"with(p:prop,forall(u,v:uu,p));") (instantiate-existential ("s**t")) (block (script-comment"`instantiate-existential' at (0 0)") (instantiate-universal-antecedent"with(f:sets[sets[action]],forall(u:uu,f subseteq f));"("e")) (cut-with-single-formula"#(r,ff)") (incorporate-antecedent"with(r:ff,#(r,ff));") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally failure_q) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f:sets[uu],e in f);") (unfold-single-defined-constant-globally support) simplify direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(f:sets[sets[action]],f subseteq f);"("x_$0")) (instantiate-existential ("x_$0")) (simplify-antecedent"with(x_$0:sets[action],u:uu,p:ff,x_$0 in p(u**e));")) (block (script-comment"`instantiate-existential' at (0 1)") (unfold-single-defined-constant (0) prefix) simplify (instantiate-existential ("t")))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 2 0 0 0 0 0 0 0)") (backchain"with(p:prop,forall(u,v:uu,p));") (instantiate-existential ("s**u_$0")) (instantiate-existential ("x_$1")) (block (script-comment"`instantiate-existential' at (0 1)") (unfold-single-defined-constant (0) prefix) (incorporate-antecedent"with(u_$0,v_$0:uu,v_$0 prefix u_$0);") (unfold-single-defined-constant (0) prefix) direct-and-antecedent-inference-strategy (backchain"with(u,u_$0:uu,u_$0=u);") (apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids) (instantiate-existential ("p_$0")))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 3 0 0 0 0 0 0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(u:uu,a:action,p));"("s**u_$0""a_$0")) (instantiate-universal-antecedent"with(f:sets[sets[action]],empty_indic_q{f});"("x_$8")) (block (script-comment"`instantiate-universal-antecedent' at (0 0 1 0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(m_$0:uu,p or p));"("m")) (contrapose"with(f:sets[sets[action]],empty_indic_q{f});") (instantiate-existential ("x_$2")) (apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids)) (backchain"with(p:prop,forall(x:sets[action],p));")) simplify-insistently (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 5 0 0 0 0 0)") (apply-macete-with-minor-premises tr%subseteq-transitivity) (backchain"with(p:prop,forall(u:uu,s:sets[action],p));") auto-instantiate-existential))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0 0)") (apply-macete-with-minor-premises tr%subseteq-transitivity) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (instantiate-existential ("q(t**u)")) simplify (block (script-comment"`instantiate-existential' at (0 1)") (force-substitution"(s**t)**u""s**(t**u)"(0)) simplify (apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids)) (block (script-comment"`instantiate-existential' at (1 0)") (cut-with-single-formula"#(q,ff)") (incorporate-antecedent"with(q:ff,#(q,ff));") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally failure_q) direct-and-antecedent-inference-strategy)) (block (script-comment"`apply-macete-with-minor-premises' at (1)") (cut-with-single-formula"#(p,ff)") (incorporate-antecedent"with(p:ff,#(p,ff));") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally failure_q) direct-and-antecedent-inference-strategy) (block (script-comment"`apply-macete-with-minor-premises' at (2)") (cut-with-single-formula"#(r,ff)") (incorporate-antecedent"with(r:ff,#(r,ff));") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally failure_q) direct-and-antecedent-inference-strategy)) )))

(def-theorem e-behaves-as-identity"forall(p:ff,act_ff(p,e,p))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally act_ff) simplify )))

(def-translation monoid-transition-system-to-directed-monoid-theory (source monoid-transition-system) (target directed-monoid-theory) (fixed-theories h-o-real-arithmetic) (sort-pairs (state ff)) (constant-pairs (act act_ff)) (theory-interpretation-check using-simplification))

(def-transported-symbols (failures refused%actions accepted%transitions may%refuse%after <_may%refuse) (translation monoid-transition-system-to-directed-monoid-theory) (renamer mts-to-dmt))

(def-constant transition"lambda(s:ff, r:uu, lambda(v:uu, s(r**v)))"(theory directed-monoid-theory))

(def-theorem transition-maps-into-ff-condition"forall(s:ff, r:uu, #(transition(s,r),ff) iff r in support(s))"(theory directed-monoid-theory) (proof ( direct-inference (cut-with-single-formula"#(s,ff)") (incorporate-antecedent"with(p:prop,p);") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally transition) (unfold-single-defined-constant-globally failure_q) (unfold-single-defined-constant-globally support) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (simplify-antecedent"with(x:sets[action],r:uu,s:ff,x in s(r**e));") (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0 0 0 0 0 0)") (backchain"with(p:prop,forall(u_$0:uu,x_$8,y_$0:sets[action],p));") (instantiate-existential ("y_$0"))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 1 0 0 0)") (instantiate-existential ("x")) simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 2 0 0 0 0 0 0 0 0)") (backchain"with(p:prop,forall(u_$0,v_$0:uu,p));") (instantiate-existential ("r**u_$0")) (instantiate-existential ("x")) (block (script-comment"`instantiate-existential' at (0 1)") (unfold-single-defined-constant (0) prefix) (incorporate-antecedent"with(u_$0,v_$0:uu,v_$0 prefix u_$0);") (unfold-single-defined-constant (0) prefix) direct-and-antecedent-inference-strategy (backchain"with(u,u_$0:uu,u_$0=u);") (apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids) (instantiate-existential ("p")))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 3 0 0 0 0 0 0 0 0 0 0)") (backchain"with(p:prop,forall(u_$0:uu,a_$0:action,p));") direct-and-antecedent-inference-strategy (instantiate-existential ("x")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(m_$0:uu,p or p));"("m_$0")) (incorporate-antecedent"with(f:sets[sets[action]],empty_indic_q{f});") (apply-macete-with-minor-premises associative-law-for-multiplication-for-monoids))) simplify-insistently (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 5 0 0 0 0 0 0)") (backchain"with(p:prop,forall(u_$0:uu,s_$0:sets[action],p));") (instantiate-existential ("r**u_$0"))) )))

(def-constant after_ff"lambda(p:ff, a:uu, iota(x:ff, x=transition(p,a)))"(theory directed-monoid-theory))

(def-theorem iota-free-characterization-of-after_ff"forall(p,q:ff, a:uu, after_ff(p,a)=q iff (a in support(p) and transition(p,a)=q))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally after_ff) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0)") (contrapose"with(p:prop,p);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(p:prop,p);") (antecedent-inference-strategy (0)) (cut-with-single-formula"#(transition(p,a),ff)") (incorporate-antecedent"with(f:[uu,sets[sets[action]]],#(f,ff));") (apply-macete-with-minor-premises transition-maps-into-ff-condition)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1)") (contrapose"with(q,f:ff,f=q);") (apply-macete-with-minor-premises eliminate-iota-macete) (contrapose"with(p:prop,not(p));")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0)") (apply-macete-with-minor-premises eliminate-iota-macete) direct-and-antecedent-inference-strategy) )))

(def-theorem factorization-of-act"forall(p,q:ff, a:uu, act_ff(p,a,q) iff forall(u:uu, q(u) subseteq transition(p,a)(u)))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally act_ff) (unfold-single-defined-constant-globally transition) )))

(def-theorem accepted%transitions_ff-is-support"forall(s:ff, accepted%transitions_ff(s)=support(s))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally accepted%transitions_ff) (unfold-single-defined-constant-globally act_ff) (unfold-single-defined-constant-globally support) (apply-macete-with-minor-premises tr%subseteq-antisymmetry) simplify-insistently direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,p);"("e")) (instantiate-existential ("x_$2")) (cut-with-single-formula"#(q,ff)") (incorporate-antecedent"with(q:ff,#(q,ff));") (apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory) (unfold-single-defined-constant-globally failure_q) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(f:sets[uu],e in f);") (unfold-single-defined-constant-globally support) simplify direct-and-antecedent-inference-strategy (instantiate-existential ("x")) simplify (simplify-antecedent"with(f:sets[sets[action]],f subseteq f);") simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 0 0 0)") (instantiate-existential ("transition(s,x_$1)")) (unfold-single-defined-constant-globally transition) (block (script-comment"`instantiate-existential' at (1)") (apply-macete-with-minor-premises transition-maps-into-ff-condition) (unfold-single-defined-constant-globally support) simplify (instantiate-existential ("x")))) )))