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