(def-constant prefix"lambda(m,n:uu, forsome(p:uu, n=m**p))"(theory monoid-theory))

(def-theorem prefix-is-transitive"forall(x,y,z:uu, x prefix y and y prefix z implies x prefix z)"(theory monoid-theory) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (backchain"with(p,y,z:uu,z=y**p);") (backchain"with(p_$0,x,y:uu,y=x**p_$0);") (instantiate-existential ("p_$0**p")) simplify )))

(def-theorem prefix-is-reflexive"forall(x:uu, x prefix x)"(theory monoid-theory) (proof ( (unfold-single-defined-constant-globally prefix) direct-and-antecedent-inference-strategy (instantiate-existential ("e")) simplify )))

(def-constant init%eqv"lambda(a,b:uu, a=e and b=e or not a=e and not b=e and forsome(x:uu, not x=e and x prefix a and x prefix b))"(theory monoid-theory))

(def-theory directed-monoid-theory (component-theories monoid-theory) (axioms (directed-property"forall(x,y,z:uu, not x=e and not z=e and x prefix y and z prefix y implies forsome(u:uu, not u=e and u prefix x and u prefix z))") (no-units"forall(x:uu, x prefix e implies x=e)") ))

(def-theorem init%eqv-reflexive-property"forall(x:uu, x init%eqv x)"(theory monoid-theory) (proof ( (unfold-single-defined-constant-globally init%eqv) (unfold-single-defined-constant-globally prefix) direct-and-antecedent-inference-strategy auto-instantiate-existential (instantiate-existential ("e")) simplify )))

(def-theorem init%eqv-symmetric-property"forall(x,y:uu,x init%eqv y iff y init%eqv x)"(theory monoid-theory) (proof ( (unfold-single-defined-constant-globally init%eqv) direct-and-antecedent-inference-strategy auto-instantiate-existential auto-instantiate-existential )))

(def-theorem init%eqv-transitive-property"forall(x,y,z:uu, x init%eqv y and y init%eqv z implies x init%eqv z)"(theory directed-monoid-theory) (proof ( unfold-defined-constants direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(z:uu, not z=e and z prefix x_$1 and z prefix x_$0)") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises directed-property) auto-instantiate-existential) (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(z:uu,p));") (instantiate-existential ("z_$0")) (block (script-comment"`instantiate-existential' at (0 1)") (apply-macete-with-minor-premises prefix-is-transitive) (instantiate-existential ("x_$1"))) (block (script-comment"`instantiate-existential' at (0 2)") (apply-macete-with-minor-premises prefix-is-transitive) (instantiate-existential ("x_$0")))) )))

(def-translation generic-theory-to-directed-monoid (source generic-theory-1) (target directed-monoid-theory) (fixed-theories h-o-real-arithmetic) (sort-pairs (ind_1 uu)) (theory-interpretation-check using-simplification))

(def-transported-symbols quotient (translation generic-theory-to-directed-monoid) (renamer gt-to-dm-renamer) )

(def-overloading quotient (generic-theory-1 quotient) (directed-monoid-theory quotient%uu))

(def-theorem ()"#(quotient(init%eqv))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally quotient%uu) )))

(def-constant germ"quotient(init%eqv)"(theory directed-monoid-theory))

(def-theorem totality-of-germ"forall(x:uu, #(germ(x)))"(theory directed-monoid-theory) (usages d-r-convergence) (proof ( insistent-direct-inference (unfold-single-defined-constant-globally germ) (unfold-single-defined-constant (0) quotient%uu) )))

(def-theorem germ-equality-condition"forall(m,n:uu, germ(m)=germ(n) iff (m=e and n=e or forsome(u:uu, not u=e and u prefix m and u prefix n)))"(theory directed-monoid-theory) (proof ( (unfold-single-defined-constant-globally germ) (apply-macete-with-minor-premises tr%rev%quotient-map-for-equivalence-relations) (move-to-sibling 1) (block (script-comment"`apply-macete-with-minor-premises' at (1)") direct-and-antecedent-inference-strategy (apply-macete-with-minor-premises init%eqv-reflexive-property) (apply-macete-with-minor-premises init%eqv-symmetric-property) (block (script-comment"`direct-and-antecedent-inference-strategy' at (2 0 0 0 0)") (apply-macete-with-minor-premises init%eqv-transitive-property) (instantiate-existential ("y_$0")))) (block (script-comment"`apply-macete-with-minor-premises' at (0)") (unfold-single-defined-constant-globally init%eqv) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0 1 1 0 0)") (contrapose"with(m,u:uu,u prefix m);") (backchain"with(m:uu,m=e);") (contrapose"with(u:uu,not(u=e));") (instantiate-theorem no-units ("u"))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 1 0 1 0 0)") (contrapose"with(n,u:uu,u prefix n);") (backchain"with(n:uu,n=e);") (contrapose"with(u:uu,not(u=e));") (instantiate-theorem no-units ("u")))) )))

(def-theorem ()"nonempty_indic_q{ran{germ}}"(theory directed-monoid-theory) (proof ( (instantiate-existential ("germ(x)")) simplify-insistently (instantiate-existential ("x")) )))

(def-atomic-sort action"lambda(s:sets[uu], s in ran{germ})"(theory directed-monoid-theory))

(def-language language-for-monoid-transition-system (embedded-languages monoid-theory) (base-types state) (constants (act"[state,uu,state -> prop]")))

(def-theory monoid-transition-system (component-theories directed-monoid-theory) (language language-for-monoid-transition-system) (axioms (monoid-operation-behaves-as-composition"forall(s,t:uu, p,r:state, act(p, s**t, r) iff forsome(q:state, act(p,s,q) and act(q,t,r)))") (monoid-identity-behaves-as-identity"forall(p:state, act(p,e,p))")))

(def-constant accepted%transitions"lambda(p:state, indic{m:uu, forsome(q:state, act(p,m,q))})"(theory monoid-transition-system))

(def-constant refused%transitions"lambda(p:state, indic{m:uu, forall(q:state, not act(p,m,q))})"(theory monoid-transition-system))

(def-theorem accepted%transitions-is-prefix-closed"forall(p:state, m,n:uu, m in accepted%transitions(p) and n prefix m implies n in accepted%transitions(p))"(theory monoid-transition-system) (proof ( unfold-defined-constants simplify-insistently direct-and-antecedent-inference-strategy (contrapose"with(q_$1:state,m:uu,p:state,act(p,m,q_$1));") (backchain"with(u,m:uu,m=u);") (apply-macete-with-minor-premises monoid-operation-behaves-as-composition) simplify )))

(def-constant accepted%actions"lambda(p:state, indic{a:action, forsome(m:uu, germ(m)=a and m in accepted%transitions(p))})"(theory monoid-transition-system))

(def-constant refused%actions"lambda(p:state, indic{a:action, forall(m:uu, germ(m)=a implies not m in accepted%transitions(p))})"(theory monoid-transition-system))

(def-theorem refused%actions-is-total"forall(p:state, #(refused%actions(p)))"(usages d-r-convergence) (theory monoid-transition-system) (proof ( insistent-direct-inference (unfold-single-defined-constant-globally refused%actions) )))

(def-theorem accepted%actions-is-complement-of-refused%actions"forall(p:state, x:action, accepted%actions(p)^^=refused%actions(p))"lemma (theory monoid-transition-system) reverse (proof ( (apply-macete-with-minor-premises tr%subseteq-antisymmetry) unfold-defined-constants simplify-insistently )))

(def-constant failures"lambda(p:state, lambda(u:uu, indic{s:sets[action], forsome(q:state, act(p,u,q) and s subseteq refused%actions(q))}))"(theory monoid-transition-system))

(def-constant may%refuse%after"lambda(x:sets[action],u:uu,p:state, forsome(q:state, act(p,u,q) and x subseteq refused%actions(q)))"(theory monoid-transition-system))

(def-constant <_may%refuse"lambda(p,q:state, forall(x:sets[action],u:uu, may%refuse%after(x,u,p) implies may%refuse%after(x,u,q)))"(theory monoid-transition-system))

(def-theorem failures-characterization-of-<_may%refuse"forall(p,q:state, p <_may%refuse q iff forall(u:uu, failures(p)(u) subseteq failures(q)(u)))"(theory monoid-transition-system) (proof ( unfold-defined-constants (unfold-single-defined-constant-globally may%refuse%after) simplify-insistently (prove-by-logic-and-simplification 0) )))

(def-constant must%refuse%after"lambda(x:sets[action],u:uu,p:state, forall(q:state, act(p,u,q) implies x subseteq refused%actions(q)))"(theory monoid-transition-system))

(def-theorem must%refuse%after-characterization-lemma"forall(x:sets[action],u:uu,p:state, must%refuse%after(x,u,p) iff x subseteq big_i{lambda(q:state, if(act(p,u,q), refused%actions(q),sort_to_indic{action}))})"(theory monoid-transition-system) lemma (proof ( (unfold-single-defined-constant-globally must%refuse%after) simplify-insistently direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0)") (case-split ("act(p,u,i_$0)")) simplify simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0)") simplify-insistently insistent-direct-inference direct-and-antecedent-inference-strategy simplify (auto-instantiate-universal-antecedent"with(u:uu,p:state,x_$1:sets[action], forall(x_$0:action, x_$0 in x_$1 implies forall(i_$0:state, x_$0 in if(act(p,u,i_$0), refused%actions(i_$0), sort_to_indic{action}))));") (instantiate-universal-antecedent"with(p:prop,forall(i_$0:state,p));"("q")) (simplify-antecedent"with(x_$0:action,f:sets[action],p:prop,x_$0 in if(p, f, f));")) )))

(def-constant successors%after"lambda(p:state, lambda(u:uu, indic{a:action, forsome(q:state, act(p,u,q) and a in accepted%actions(q))}))"(theory monoid-transition-system))

(def-theorem successors%after-complement"forall(p:state, u:uu, big_i{lambda(q:state, if(act(p,u,q), refused%actions(q),sort_to_indic{action}))}= successors%after(p)(u)^^)"(theory monoid-transition-system) (proof ( (apply-macete-with-minor-premises tr%subseteq-antisymmetry) (unfold-single-defined-constant-globally successors%after) simplify-insistently (apply-macete-with-minor-premises rev%accepted%actions-is-complement-of-refused%actions) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(i_$0:state,p));"("q")) (simplify-antecedent"with(x_$2:action,f:sets[action],x_$2 in f);")) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(q:state,p));"("i_$1")) simplify (block (script-comment"`instantiate-universal-antecedent' at (0 0 1)") (case-split ("act(p,u,i_$1)")) simplify simplify)) )))

(def-theorem must%refuse%after-characterization"forall(x:sets[action],u:uu,p:state, must%refuse%after(x,u,p) iff x subseteq successors%after(p)(u)^^)"(theory monoid-transition-system) (proof ( (apply-macete-with-minor-premises must%refuse%after-characterization-lemma) (apply-macete-with-minor-premises successors%after-complement) )))

(def-constant <_must%refuse"lambda(p,q:state, forall(x:sets[action],u:uu, must%refuse%after(x,u,p) implies must%refuse%after(x,u,q)))"(theory monoid-transition-system))

(def-theorem characterization-of-<_must%refuse"forall(p,q:state, q <_must%refuse p iff forall(u:uu,successors%after(p)(u) subseteq successors%after(q)(u)));"(theory monoid-transition-system) (proof ( (unfold-single-defined-constant-globally <_must%refuse) (apply-macete-with-minor-premises must%refuse%after-characterization) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0)") (cut-with-single-formula"successors%after(q)(u)^^ subseteq successors%after(p)(u)^^") (move-to-sibling 1) (instantiate-universal-antecedent"with(p:prop,p);"("successors%after(q)(u)^^""u")) (block (script-comment"`cut-with-single-formula' at (0)") (weaken (1)) (incorporate-antecedent"with(p:prop,p);") simplify-insistently)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0)") (cut-with-single-formula"successors%after(q)(u_$0)^^ subseteq successors%after(p)(u_$0)^^") (block (script-comment"`cut-with-single-formula' at (0)") (weaken (2)) (incorporate-antecedent"with(u_$0:uu,q:state,x_$1:sets[action], x_$1 subseteq successors%after(q)(u_$0)^^);") (incorporate-antecedent"with(p:prop,p);") simplify-insistently direct-and-antecedent-inference-strategy simplify) (block (script-comment"`cut-with-single-formula' at (1)") (weaken (0)) (incorporate-antecedent"with(p:prop,p);") simplify-insistently)) )))

(def-constant must%accept%after"lambda(x:sets[action],u:uu,p:state, forall(q:state, act(p,u,q) implies not(x disj accepted%actions(q))))"(theory monoid-transition-system))

(def-constant may%accept%after"lambda(x:sets[action],u:uu,p:state, forsome(q:state, act(p,u,q) and not(x disj accepted%actions(q))))"(theory monoid-transition-system))

(def-theorem must%accept%after-negation-of-may%refuse%after"forall(p:state, x:sets[action],u:uu, must%accept%after(x,u,p) iff not may%refuse%after(x,u,p))"(theory monoid-transition-system) (proof ( unfold-defined-constants (apply-macete-with-minor-premises rev%accepted%actions-is-complement-of-refused%actions) simplify-insistently direct-and-antecedent-inference-strategy simplify simplify )))

(def-theorem testing-characterization-of-<_may%refuse"forall(p,q:state, p <_may%refuse q iff forall(x:sets[action],u:uu, must%accept%after(x,u,q) implies must%accept%after(x,u,p)))"(theory monoid-transition-system) (proof ( (unfold-single-defined-constant-globally <_may%refuse) (apply-macete-with-minor-premises must%accept%after-negation-of-may%refuse%after) simplify direct-and-antecedent-inference-strategy simplify simplify )))

(def-theorem may%accept%after-negation-of-must%refuse%after"forall(p:state, x:sets[action],u:uu, may%accept%after(x,u,p) iff not must%refuse%after(x,u,p))"(theory monoid-transition-system) (proof ( unfold-defined-constants (apply-macete-with-minor-premises rev%accepted%actions-is-complement-of-refused%actions) simplify-insistently direct-and-antecedent-inference-strategy simplify simplify )))

(def-theorem testing-characterization-of-<_must%refuse"forall(p,q:state, p <_must%refuse q iff forall(x:sets[action],u:uu, may%accept%after(x,u,q) implies may%accept%after(x,u,p)))"(theory monoid-transition-system) (proof ( (unfold-single-defined-constant-globally <_must%refuse) (apply-macete-with-minor-premises may%accept%after-negation-of-must%refuse%after) simplify direct-and-antecedent-inference-strategy simplify simplify )))

(def-theorem accepted%transitions-characterization-of-<_must%refuse"forall(p,q:state, q <_must%refuse p iff accepted%transitions(p) subseteq accepted%transitions(q))"(theory monoid-transition-system) (proof ( (apply-macete-with-minor-premises characterization-of-<_must%refuse) (unfold-single-defined-constant-globally successors%after) (unfold-single-defined-constant-globally accepted%actions) simplify-insistently direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0)") insistent-direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(u:uu,p));"("x")) (incorporate-antecedent"with(x:uu,f:sets[uu],x in f);") (unfold-single-defined-constant-globally accepted%transitions) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(x_$0:action,p));"("germ(e)")) (block (script-comment"`instantiate-universal-antecedent' at (0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(q_$3:state,p));"("q_$0")) (instantiate-universal-antecedent"with(p:prop,forall(m_$1:uu,p));"("e")) (simplify-antecedent"with(p:prop,not(p));") (block (script-comment"`instantiate-universal-antecedent' at (0 0 1)") (contrapose"with(p:prop,not(p));") (unfold-single-defined-constant-globally accepted%transitions) simplify-insistently (instantiate-existential ("q_$0")) (apply-macete-with-minor-premises monoid-identity-behaves-as-identity))) (instantiate-existential ("q_$2")) (block (script-comment"`instantiate-universal-antecedent' at (1 1)") (apply-macete-with-minor-premises action-defining-axiom_directed-monoid-theory) simplify-insistently (instantiate-existential ("e")))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0 0 0 0 0 0)") (incorporate-antecedent"with(f:sets[uu],f subseteq f);") (incorporate-antecedent"with(m_$0:uu,f:sets[uu],m_$0 in f);") (unfold-single-defined-constant-globally accepted%transitions) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-theorem monoid-operation-behaves-as-composition ("u""m_$0""p""q_$1")) (block (script-comment"`instantiate-theorem' at (0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(x:uu,p));"("u**m_$0")) (instantiate-universal-antecedent"with(p:prop,forall(q_$0:state,p));"("q_$1")) (block (script-comment"`instantiate-universal-antecedent' at (0 0 1 0)") (incorporate-antecedent"with(q_$3:state,m_$0,u:uu,q:state,act(q,u**m_$0,q_$3));") (apply-macete-with-minor-premises monoid-operation-behaves-as-composition) direct-and-antecedent-inference-strategy (instantiate-existential ("q_$4")) (instantiate-existential ("m_$0")) (instantiate-existential ("q_$3")))) (instantiate-universal-antecedent"with(p:prop,forall(q:state,p));"("q_$0"))) )))

(def-constant support"lambda(f:[uu->sets[sets[action]]], indic{u:uu, nonempty_indic_q{f(u)}})"(theory directed-monoid-theory))

(def-constant failure_q"lambda(f:[uu, sets[sets[action]]], forall(u:uu,x,y:sets[action], y in f(u) and x subseteq y implies x in f(u)) and e in support(f) and forall(u,v:uu, u in support(f) and v prefix u implies v in support(f)) and forall(u:uu, a:action, u in support(f) implies (forsome(m:uu, germ(m)=a and (u**m) in support(f)) or forall(x:sets[action], x in f(u) implies (x union singleton{a}) in f(u)))) and total_q{f,[uu -> sets[sets[action]]]} and forall(u:uu,s:sets[action], s in f(u) implies not (germ(e)) in s))"(theory directed-monoid-theory))

(def-theorem e-is-never-refused"forall(p:state, not(germ(e) in refused%actions(p)))"lemma (theory monoid-transition-system) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(x:action, germ(e) =x)") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,p);") (backchain"with(p:prop,p);") (unfold-single-defined-constant-globally refused%actions) (unfold-single-defined-constant-globally accepted%transitions) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly (backchain-backwards"with(p:prop,p);") (weaken (0)) simplify (instantiate-existential ("e")) (instantiate-existential ("p")) (apply-macete-with-minor-premises monoid-identity-behaves-as-identity)) (block (script-comment"`cut-with-single-formula' at (1)") (instantiate-existential ("germ(e)")) (apply-macete-with-minor-premises action-defining-axiom_directed-monoid-theory) simplify-insistently (instantiate-existential ("e"))) )))

(def-theorem range-of-failures"forall(p:state, failure_q(failures(p)))"(theory monoid-transition-system) (proof ( unfold-defined-constants (unfold-single-defined-constant-globally support) simplify-insistently direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0 0 0)") auto-instantiate-existential (apply-macete-with-minor-premises tr%subseteq-transitivity) auto-instantiate-existential ) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0)") (instantiate-universal-antecedent"with(p:prop,p);"("p")) (instantiate-universal-antecedent"with(p:prop,p);"("e""empty_indic{action}")) (block (script-comment"`instantiate-universal-antecedent' at (0 0 0)") (contrapose"with(p:prop,p);") (instantiate-existential ("empty_indic{action}")) (instantiate-existential ("p")) (apply-macete-with-minor-premises monoid-identity-behaves-as-identity) simplify-insistently ) (block (script-comment"`instantiate-universal-antecedent' at (0 0 1 0 0)") (instantiate-existential ("empty_indic{action}")) (instantiate-existential ("p")) (apply-macete-with-minor-premises monoid-identity-behaves-as-identity) simplify-insistently ) ) (block (script-comment"`direct-and-antecedent-inference-strategy' at (2 0 0 0 0 0 0 0 0)") (instantiate-existential ("empty_indic{action}")) (incorporate-antecedent"with(u_$0,v_$0:uu,v_$0 prefix u_$0);") (unfold-single-defined-constant (0) prefix) direct-and-antecedent-inference-strategy (incorporate-antecedent"with(q_$0:state,u_$0:uu,p:state,act(p,u_$0,q_$0));") (backchain"with(u,u_$0:uu,u_$0=u);") (apply-macete-with-minor-premises monoid-operation-behaves-as-composition) direct-and-antecedent-inference-strategy (instantiate-existential ("q")) simplify-insistently ) (block (script-comment"`direct-and-antecedent-inference-strategy' at (3 0 0 0 0 0 0 0 0 0 0 0 0)") auto-instantiate-existential (antecedent-inference"with(p:prop,p or p);") simplify (block (script-comment"`antecedent-inference' at (1)") (cut-with-single-formula"forsome(m:uu, germ(m)=a_$0)") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (cut-with-single-formula"#(a_$0, action)") (incorporate-antecedent"with(a_$0:action,#(a_$0,action));") (apply-macete-with-minor-premises action-defining-axiom_directed-monoid-theory) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-existential ("x_$0")) ) (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(m:uu,p));") (unfold-single-defined-constant-globally refused%actions) simplify-insistently (backchain"with(a_$0,x:action,x=a_$0);") (backchain-backwards"with(a_$0:action,m:uu,germ(m)=a_$0);") (apply-macete-with-minor-premises germ-equality-condition) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(m_$0:uu,p));"("m")) (instantiate-universal-antecedent"with(p:prop,forall(x_$5:sets[action],p));"("x_$5") ) (instantiate-universal-antecedent"with(p:prop,forall(q_$0:state,p or p));"("q_$0")) (contrapose"with(p:prop,not(p));") simplify ) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)") (instantiate-universal-antecedent"with(p:prop,forall(m_$0:uu,p));"("u")) (block (script-comment"`instantiate-universal-antecedent' at (0 0 0)") (contrapose"with(a_$0:action,f:sets[uu],not(f=a_$0));") (backchain-backwards"with(a_$0:action,m:uu,germ(m)=a_$0);") (apply-macete-with-minor-premises germ-equality-condition) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0)") (instantiate-existential ("u")) (apply-macete-with-minor-premises prefix-is-reflexive) ) (instantiate-existential ("u")) ) (block (script-comment"`instantiate-universal-antecedent' at (0 0 1)") (instantiate-universal-antecedent"with(p:prop,forall(x_$5:sets[action],p));"("empty_indic{action}") ) (contrapose"with(p:prop,forall(q_$0:state,p or p));") (apply-macete-with-minor-premises monoid-operation-behaves-as-composition) direct-and-antecedent-inference-strategy (cut-with-single-formula"u in accepted%transitions(q)") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises accepted%transitions-is-prefix-closed) (instantiate-existential ("m_$0")) ) (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(u:uu,q:state,u in accepted%transitions(q));") (unfold-single-defined-constant-globally accepted%transitions) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-existential ("q_$1")) (instantiate-existential ("q")) ) ) ) ) ) ) (block (script-comment"`direct-and-antecedent-inference-strategy' at (4 0 0 0 0 0 0)") (cut-with-single-formula"not(germ(e) in refused%actions(q))") (block (script-comment"`cut-with-single-formula' at (0)") (contrapose"with(p:prop,not(p));") simplify ) (apply-macete-with-minor-premises e-is-never-refused) ) )))

(def-theorem not-everything-is-a-failure"not(failure_q(lambda(x:uu, empty_indic{sets[action]})))"(theory directed-monoid-theory) lemma (proof ( (unfold-single-defined-constant-globally failure_q) simplify-insistently (unfold-single-defined-constant-globally support) simplify-insistently )))

(def-constant stop_ff"lambda(x:uu, if(x=e, indic{s:sets[action], not (germ(e) in s)}, empty_indic{sets[action]}))"(theory directed-monoid-theory))

(def-theorem stop-is-a-failure"failure_q(stop_ff)"(theory directed-monoid-theory) (proof ( unfold-defined-constants (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)") (case-split ("u_$0=e")) (block (script-comment"`case-split' at (1)") (incorporate-antecedent"with(y_$0:sets[action],f:sets[sets[action]],y_$0 in f);") simplify direct-and-antecedent-inference-strategy (contrapose"with(p:prop,not(p));") simplify) (block (script-comment"`case-split' at (2)") (incorporate-antecedent"with(y_$0:sets[action],f:sets[sets[action]],y_$0 in f);") simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1)") simplify (instantiate-existential ("empty_indic{action}")) simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (2 0 0 0 0 0)") (cut-with-single-formula"v_$0=e") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (instantiate-theorem no-units ("v_$0")) (contrapose"with(p:prop,not(p));") (cut-with-single-formula"u_$0=e") simplify (block (script-comment"`cut-with-single-formula' at (1)") (contrapose"with(x_$1:sets[action],u_$0:uu, x_$1 in if(u_$0=e, indic{s:sets[action], not(germ(e) in s)}, empty_indic{sets[action]}));") simplify)) simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (3 0 0 0 0 0 0 0)") (cut-with-single-formula"u_$0=e") (block (script-comment"`cut-with-single-formula' at (0)") simplify (incorporate-antecedent"with(x_$8:sets[action],u_$0:uu, x_$8 in if(u_$0=e, indic{s:sets[action], not(germ(e) in s)}, empty_indic{sets[action]}));") simplify (apply-macete-with-minor-premises tr%union-disjunction-conversion) (cut-with-single-formula"forsome(x:action, germ(e)=x)") (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(x:action,p));") (backchain"with(x:action,f:sets[uu],f=x);") (backchain"with(x:action,f:sets[uu],f=x);") (apply-macete-with-minor-premises tr%union-disjunction-conversion) simplify direct-and-antecedent-inference-strategy (backchain-backwards"with(x:action,f:sets[uu],f=x);") (weaken (1)) (instantiate-universal-antecedent"with(p:prop,forall(m_$0:uu,p));"("e")) (contrapose"with(f:sets[sets[action]],empty_indic_q{f});") (apply-macete-with-minor-premises right-multiplicative-identity-for-monoids) simplify (instantiate-existential ("empty_indic{action}")) simplify) (block (script-comment"`cut-with-single-formula' at (1)") (instantiate-existential ("germ(e)")) (apply-macete-with-minor-premises action-defining-axiom_directed-monoid-theory) simplify (instantiate-existential ("e")))) (block (script-comment"`cut-with-single-formula' at (1)") (contrapose"with(x_$1:sets[action],u_$0:uu, x_$1 in if(u_$0=e, indic{s:sets[action], not(germ(e) in s)}, empty_indic{sets[action]}));") simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (4 0)") insistent-direct-inference beta-reduce-repeatedly) (block (script-comment"`direct-and-antecedent-inference-strategy' at (5 0 0 0)") (cut-with-single-formula"u_$0=e") (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(s_$0:sets[action],u_$0:uu, s_$0 in if(u_$0=e, indic{s:sets[action], not(germ(e) in s)}, empty_indic{sets[action]}));") simplify) (block (script-comment"`cut-with-single-formula' at (1)") (contrapose"with(s_$0:sets[action],u_$0:uu, s_$0 in if(u_$0=e, indic{s:sets[action], not(germ(e) in s)}, empty_indic{sets[action]}));") simplify)) )))

(def-atomic-sort ff"failure_q"(witness"stop_ff") (theory directed-monoid-theory))

(def-language language-for-graded-monoid (embedded-language directed-monoid-theory) (constants (lngth"[uu,rr]")))

(def-theory graded-monoid (language language-for-graded-monoid) (component-theories directed-monoid-theory) (axioms (divisibility"forall(a:uu, not a=e implies forsome(b:uu, not b=e and b prefix a and 0<=lngth(b) and lngth(b)<=1))") (length-non-negative"forall(a:uu, 0<=lngth(a))") (length-of-product"forall(a,b:uu, lngth(a**b)=lngth(a)+lngth(b))")))

(def-theorem ()"forall(a:uu, #(lngth(a)))"(theory graded-monoid) (usages d-r-convergence) (proof ( insistent-direct-inference (assume-theorem length-of-product) )))

(def-theorem lngth-of-e"lngth(e)=0"(theory graded-monoid) (proof ( (cut-with-single-formula"lngth(e**e)=lngth(e)+lngth(e)") (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(p:prop,p);") simplify) (apply-macete-with-minor-premises length-of-product) )))

(def-theorem action-representatives-can-have-norm-le-1"forall(a:action, forsome(u:uu, germ(u)=a and 0<=lngth(u) and lngth(u)<=1))"(theory graded-monoid) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"#(a,action)") (incorporate-antecedent"with(p:prop,p);") (apply-macete-with-minor-premises action-defining-axiom_directed-monoid-theory) simplify-insistently direct-and-antecedent-inference-strategy (case-split ("x=e")) (block (script-comment"`case-split' at (1)") (instantiate-existential ("e")) simplify (block (script-comment"`instantiate-existential' at (0 2)") (apply-macete-with-minor-premises lngth-of-e) simplify)) (block (script-comment"`case-split' at (2)") (instantiate-theorem divisibility ("x")) (instantiate-existential ("b")) (backchain"with(f:sets[uu],a:action,a=f);") (apply-macete-with-minor-premises germ-equality-condition) direct-and-antecedent-inference-strategy (instantiate-existential ("b")) (apply-macete-with-minor-premises prefix-is-reflexive)) )))

(def-theory graded-monoid-transition-system (component-theories graded-monoid monoid-transition-system))

(def-constant eqv%may%refuse"lambda(p,q:state, n:zz, forall(x:sets[action],u:uu, lngth(u)<=n implies may%refuse%after(x,u,p) iff may%refuse%after(x,u,q)))"(theory graded-monoid-transition-system))

(def-theorem failures-characterization-of-eqv%may%refuse"forall(p,q:state, n:zz, eqv%may%refuse(p,q,n) iff forall(u:uu, lngth(u)<=n implies failures(p)(u)= failures(q)(u)))"(theory graded-monoid-transition-system) (proof ( unfold-defined-constants (unfold-single-defined-constant-globally may%refuse%after) (apply-macete-with-minor-premises tr%subseteq-antisymmetry) simplify-insistently (prove-by-logic-and-simplification 0) )))

(def-constant =_may%refuse"lambda(p,q:state, forall(x:sets[action],u:uu, may%refuse%after(x,u,p) iff may%refuse%after(x,u,q)))"(theory monoid-transition-system))

(def-theorem failures-characterization-of-=%may%refuse"forall(p,q:state, p =_may%refuse q iff failures(p)=failures(q))"(theory graded-monoid-transition-system) (proof ( (unfold-single-defined-constant (0) =_may%refuse) direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0)") extensionality (block (script-comment"`extensionality' at (0)") direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(p:state, x:uu, #(failures(p)(x)))") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") direct-and-antecedent-inference-strategy (unfold-single-defined-constant (0) failures)) (block (script-comment"`cut-with-single-formula' at (0)") simplify (instantiate-universal-antecedent-multiply"with(p:prop,forall(p:state,x:uu,with(p:prop,p)));"(("p""x_0") ("q""x_0"))) simplify (cut-with-single-formula"eqv%may%refuse(p,q,1+floor(lngth(x_0)))") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (unfold-single-defined-constant (0) eqv%may%refuse) direct-and-antecedent-inference-strategy (backchain-backwards"with(p:prop,forall(x:sets[action],u:uu,p));") (backchain"with(p:prop,forall(x:sets[action],u:uu,p));")) (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(r:rr,q,p:state,eqv%may%refuse(p,q,r));") (apply-macete-with-minor-premises failures-characterization-of-eqv%may%refuse) direct-and-antecedent-inference-strategy simplify))) (unfold-single-defined-constant (0) failures) (unfold-single-defined-constant (0) failures)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 0)") (instantiate-theorem failures-characterization-of-eqv%may%refuse ("p""q""1+floor(lngth(u))")) (block (script-comment"`instantiate-theorem' at (0 0)") (incorporate-antecedent"with(r:rr,q,p:state,eqv%may%refuse(p,q,r));") (unfold-single-defined-constant (0) eqv%may%refuse) direct-and-antecedent-inference-strategy (backchain-backwards"with(p:prop,forall(x_$0:sets[action],u_$0:uu,p));") simplify) (block (script-comment"`instantiate-theorem' at (0 1 0 0)") (contrapose"with(f:sets[sets[action]],not(f=f));") (cut-with-single-formula"forall(p:state, x:uu, #(failures(p)(x)))") (move-to-sibling 1) (unfold-single-defined-constant (0) failures) simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 1)") (instantiate-theorem failures-characterization-of-eqv%may%refuse ("p""q""1+floor(lngth(u))")) (block (script-comment"`instantiate-theorem' at (0 0)") (incorporate-antecedent"with(r:rr,q,p:state,eqv%may%refuse(p,q,r));") (unfold-single-defined-constant (0) eqv%may%refuse) direct-and-antecedent-inference-strategy (backchain"with(p:prop,forall(x_$0:sets[action],u_$0:uu,p));") simplify) (block (script-comment"`instantiate-theorem' at (0 1 0 0)") (contrapose"with(f:sets[sets[action]],not(f=f));") (cut-with-single-formula"forall(p:state, x:uu, #(failures(p)(x)))") (move-to-sibling 1) (unfold-single-defined-constant (0) failures) simplify)) )))