(def-theorem ptwise-closure-condition
"forall(s:[zz,total%fns], aa:sets[sets[sets[action]]],
#(lim(s)) and
forall(n:zz,u:uu, #(s(n)) implies s(n)(u) in aa )
implies
forall(u:uu, lim(s)(u) in aa))"
(theory graded-monoid)
lemma
(proof
(
direct-inference
direct-inference
(cut-with-single-formula "forsome(x:total%fns, lim(s)=x)")
(move-to-sibling 1)
(instantiate-existential ("lim(s)"))
(block
(script-comment "`cut-with-single-formula' at (0)")
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,p and p);")
(antecedent-inference "with(p:prop,forsome(x:total%fns,p));")
(backchain "with(x,f:total%fns,f=x);")
(incorporate-antecedent "with(x,f:total%fns,f=x);")
(apply-macete-with-minor-premises characterization-ultrametric-limit-of-fns)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"
("1+floor(lngth(u))"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "lngth(u)<=1+floor(lngth(u)) and 0<=lngth(u)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises length-non-negative)
simplify))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1 0)")
(backchain-backwards "with(p:prop,forall(p_$0:zz,u_$0:uu,p));")
(instantiate-existential ("n_$0"))
simplify
simplify
(block
(script-comment "`instantiate-existential' at (0 1)")
(backchain "with(p:prop,f:total%fns,#(f) and forall(n:zz,u:uu,p));")
(instantiate-universal-antecedent
"with(p:prop,forall(p_$0:zz,u_$0:uu,p));"
("n_$0" "u"))))))))
(def-constant rel%failure_q
"lambda(f:[uu, sets[sets[action]]], aa:sets[sets[action]],
failure_q(f) and forall(u:uu, f(u) subseteq aa))"
(theory directed-monoid-theory))
(def-theorem rel%failure_q-is-closed-under-lim
"forall(s:[zz,total%fns], aa:sets[sets[action]],
#(lim(s)) and
forall(n:zz, #(s(n)) implies rel%failure_q(s(n),aa))
implies
rel%failure_q(lim(s),aa))"
(theory graded-monoid)
(proof
(
(let-script
prove-definedness 1
((cut-with-single-formula (% "#(~a,total%fns)" $1))
(incorporate-antecedent "with(f:total%fns,#(f,total%fns));")
(apply-macete-with-minor-premises total%fns-defining-axiom_graded-monoid)
beta-reduce-with-minor-premises
direct-and-antecedent-inference-strategy)
)
(unfold-single-defined-constant-globally rel%failure_q)
direct-and-antecedent-inference-strategy
(block
(script-comment
"`direct-and-antecedent-inference-strategy' at (0 0 0 0)")
(apply-macete-with-minor-premises failure_q-is-closed-under-lim)
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(n:zz,p));"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)")
(force-substitution "lim(s)(u) subseteq aa"
"lim(s)(u) in indic{b:sets[sets[action]], b subseteq aa}"
(0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-with-minor-premises
($prove-definedness "lim(s)"))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises ptwise-closure-condition)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-with-minor-premises
(backchain "with(p:prop,forall(n:zz,p));")
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
($prove-definedness "s(n)")))))
))
(def-constant rel%part
"lambda(f:ff, aa:sets[sets[action]], lambda(u:uu, f(u) inters aa))"
(theory directed-monoid-theory))
(def-theorem failure-non-empty-condition
"forall(f:ff, u:uu, nonempty_indic_q{f(u)} iff empty_indic{action} in f(u))"
(theory directed-monoid-theory)
lemma
reverse
(proof
(
direct-inference
(cut-with-single-formula "failure_q(f)")
(move-to-sibling 1)
(apply-macete-with-minor-premises ff-in-quasi-sort_directed-monoid-theory)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(p:prop,p);")
(unfold-single-defined-constant-globally failure_q)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0)")
(backchain "with(p:prop,forall(u_$0:uu,x_$8,y_$0:sets[action],p));")
auto-instantiate-existential
simplify-insistently)
auto-instantiate-existential)
)))
(def-theorem rel%part-mapping-property
"forall(aa:sets[sets[action]],
empty_indic{action} in aa and
forall(x:action, a:sets[action],
a in aa implies a union singleton{x} in aa) and
forall(b,a:sets[action], b in aa and a subseteq b implies a in aa)
implies
forall(f:ff, rel%failure_q(rel%part(f,aa),aa)))"
lemma
(theory directed-monoid-theory)
(proof
(
direct-and-antecedent-inference-strategy
unfold-defined-constants
(cut-with-single-formula "failure_q(f)")
(move-to-sibling 1)
(apply-macete-with-minor-premises ff-in-quasi-sort_directed-monoid-theory)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(f:ff,failure_q(f));")
(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 0 0 0)")
(backchain "with(p:prop,forall(u_$0:uu,x_$8,y_$0:sets[action],p));")
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 1 0 0 0 0)")
(backchain "with(p:prop,forall(b,a:sets[action],p));")
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)")
simplify-insistently
(instantiate-existential ("empty_indic{action}"))
(apply-macete-with-minor-premises rev%failure-non-empty-condition)
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2 0 0 0 0 0 0 0)")
(instantiate-universal-antecedent "with(p:prop,forall(u_$0,v_$0:uu,p));"
("u_$0" "v_$0"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 0)")
(instantiate-universal-antecedent "with(f:sets[sets[action]],empty_indic_q{f});"
("x_$1"))
(simplify-antecedent "with(x_$1:sets[action],aa:sets[sets[action]],u_$0:uu,f:ff,
x_$1 in f(u_$0) inters aa);"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1 0)")
simplify-insistently
(instantiate-existential ("empty_indic{action}"))
(apply-macete-with-minor-premises rev%failure-non-empty-condition)
auto-instantiate-existential))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 3 0 0 0 0 0 0 0
0 0 0 0)")
(instantiate-universal-antecedent "with(p:prop,forall(u_$0:uu,a_$0:action,p));"
("u_$0" "a_$0"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(instantiate-universal-antecedent "with(f:sets[sets[action]],empty_indic_q{f});"
("x_$1"))
(simplify-antecedent "with(x_$1:sets[action],aa:sets[sets[action]],u_$0:uu,f:ff,
x_$1 in f(u_$0) inters aa);"))
(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_$0"))
(contrapose "with(f:sets[sets[action]],empty_indic_q{f});")
(instantiate-existential ("empty_indic{action}"))
simplify-insistently
(apply-macete-with-minor-premises rev%failure-non-empty-condition)
auto-instantiate-existential)
(backchain "with(p:prop,forall(x_$8:sets[action],p));"))
(backchain "with(p:prop,forall(x:action,a:sets[action],p));")
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 4 0 0 0)")
insistent-direct-inference
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 5 0 0 0 0 0 0)")
simplify-insistently
(backchain "with(p:prop,forall(u_$0:uu,s_$0:sets[action],p));")
auto-instantiate-existential)
simplify-insistently)
)))
(def-language relativized-graded-monoid
(embedded-languages graded-monoid)
(constants (aa "sets[sets[action]]")))
(def-theory relativized-graded-monoid
(component-theories graded-monoid)
(language relativized-graded-monoid)
(axioms
(non-vacuous "empty_indic{action} in aa")
(closure-under-unions-with-finite-sets
"forall(x:action, a:sets[action],
a in aa implies a union singleton{x} in aa)")
(hereditary-property
"forall(b,a:sets[action], b in aa and a subseteq b implies a in aa)")))
(def-theorem ()
"lambda(f:ff, rel%failure_q(f,aa))(rel%part(stop_ff,aa))"
(theory relativized-graded-monoid)
(proof
(
beta-reduce-with-minor-premises
(move-to-sibling 1)
(apply-macete-with-minor-premises ff-defining-axiom_directed-monoid-theory)
(cut-with-single-formula "rel%failure_q(rel%part(stop_ff,aa),aa)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(p:prop,p);")
(unfold-single-defined-constant (0) rel%failure_q)
direct-and-antecedent-inference-strategy)
(block
(script-comment "`beta-reduce-with-minor-premises' at (1 0 1)")
(apply-macete-with-minor-premises rel%part-mapping-property)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises non-vacuous)
(apply-macete-with-minor-premises closure-under-unions-with-finite-sets)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0 0)")
(apply-macete-with-minor-premises hereditary-property)
auto-instantiate-existential))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises
ff-defining-axiom_directed-monoid-theory)
(apply-macete-with-minor-premises stop-is-a-failure)))
)))
(def-atomic-sort ff_aa
"lambda(f:ff, rel%failure_q(f,aa))"
(theory relativized-graded-monoid)
(witness "rel%part(stop_ff,aa)"))
(def-constant rel_aa
"lambda(f:ff, rel%part(f,aa))"
(theory relativized-graded-monoid))
(def-theorem rel_aa-is-non-expansive
"forall(f,g:ff, fn%dist(rel_aa(f),rel_aa(g))<=fn%dist(f,g))"
lemma
(theory relativized-graded-monoid)
(usages transportable-macete)
(proof
(
direct-inference
(cut-with-single-formula
"forsome(u,v,w,x:total%fns, rel_aa(f)=u and rel_aa(g)=v and f=w and g=x)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p);")
(backchain-repeatedly ("with(x,w,v:total%fns,g:ff,u:total%fns,f:ff,
rel_aa(f)=u and rel_aa(g)=v and f=w and g=x);"))
(apply-macete-with-minor-premises tr%characterization-of-non-expansiveness)
(backchain-backwards "with(p:prop,p);")
(backchain-backwards "with(p:prop,p);")
(backchain-backwards "with(p:prop,p);")
(backchain-backwards "with(p:prop,p);")
(weaken (0))
(unfold-single-defined-constant-globally rel_aa)
(unfold-single-defined-constant-globally rel%part)
(unfold-single-defined-constant-globally fn%approx)
direct-and-antecedent-inference-strategy
beta-reduce-with-minor-premises
(move-to-sibling 1)
(block
(script-comment "`beta-reduce-with-minor-premises' at (1)")
(apply-macete-with-minor-premises total%fns-defining-axiom_graded-monoid)
beta-reduce-repeatedly
insistent-direct-inference
beta-reduce-repeatedly)
(move-to-sibling 2)
(block
(script-comment "`beta-reduce-with-minor-premises' at (2)")
(apply-macete-with-minor-premises total%fns-defining-axiom_graded-monoid)
beta-reduce-repeatedly
insistent-direct-inference
beta-reduce-repeatedly)
(block
(script-comment "`beta-reduce-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
beta-reduce-repeatedly
simplify))
(block
(script-comment "`cut-with-single-formula' at (1)")
(instantiate-existential ("rel_aa(f)" "rel_aa(g)" "f" "g"))
(block
(script-comment "`instantiate-existential' at (0 0)")
simplify
(unfold-single-defined-constant (0) rel_aa)
(unfold-single-defined-constant (0) rel%part))
(block
(script-comment "`instantiate-existential' at (0 1)")
simplify
(unfold-single-defined-constant (0) rel_aa)
(unfold-single-defined-constant (0) rel%part))
(block
(script-comment "`instantiate-existential' at (1)")
(apply-macete-with-minor-premises total%fns-defining-axiom_graded-monoid)
beta-reduce-repeatedly
insistent-direct-inference
(unfold-single-defined-constant (0) rel_aa)
(unfold-single-defined-constant (0) rel%part))
(block
(script-comment "`instantiate-existential' at (2)")
(apply-macete-with-minor-premises total%fns-defining-axiom_graded-monoid)
beta-reduce-repeatedly
insistent-direct-inference))
)))
(load-section basic-cardinality)
(def-constant f_indic_act
"indic{x:sets[action], f_indic_q{x}}"
(theory graded-monoid))
(def-theorem ()
"empty_indic{action} in f_indic_act"
lemma
(theory graded-monoid)
(proof
(
(unfold-single-defined-constant (0) f_indic_act)
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(instantiate-existential ("0"))
(apply-macete-with-minor-premises tr%empty-indic-has-f-card-zero)
)))
(def-theorem finite-closure-under-singleton-lemma
"forall(a:sets[action],
a in f_indic_act
implies
forall(x:action,
a union singleton{x} in f_indic_act))"
lemma
(theory graded-monoid)
(proof
(
(unfold-single-defined-constant-globally f_indic_act)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
direct-and-antecedent-inference-strategy
(case-split ("x in a"))
(block
(script-comment "`case-split' at (1)")
(instantiate-existential ("n"))
(cut-with-single-formula "a union singleton{x}=a")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
simplify-insistently
direct-and-antecedent-inference-strategy
simplify)
simplify-insistently)
simplify)
(block
(script-comment "`case-split' at (2)")
(apply-macete-with-minor-premises tr%f-card-disjoint-union)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(instantiate-existential ("n+1"))
(apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite)
simplify)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(instantiate-existential ("1"))
(apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite))
(block
(script-comment "`apply-macete-with-minor-premises' at (2)")
simplify-insistently
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(backchain-backwards "with(x,x_$0:action,x_$0=x);")))
)))
(def-theorem ()
"forall(a:sets[action],
a in f_indic_act
implies
forall(x:action,
lambda(x_$2:action,
if(x_$2 in a or x_$2=x, an%individual, ?unit%sort))
in f_indic_act))"
lemma
(theory graded-monoid)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "lambda(x_$2:action,
if(x_$2 in a or x_$2=x, an%individual, ?unit%sort))=a union singleton{x}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(backchain "with(f:sets[action],f=f);")
(apply-macete-with-minor-premises finite-closure-under-singleton-lemma))
simplify
)))
(def-theorem ()
"forall(a:sets[action],
forsome(b:sets[action],b in f_indic_act and a subseteq b)
implies
a in f_indic_act)"
lemma
(theory graded-monoid)
(proof
(
(unfold-single-defined-constant-globally f_indic_act)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
direct-and-antecedent-inference-strategy
auto-instantiate-existential
)))
(def-translation finite-specialization-of-rgm
(source relativized-graded-monoid)
(target graded-monoid)
(fixed-theories h-o-real-arithmetic)
(constant-pairs (aa f_indic_act))
(theory-interpretation-check using-simplification))
(def-constant extendable
"lambda(f:[uu -> sets[sets[action]]], u:uu, a:action,
forsome(m:uu, germ(m)=a and (u**m) in support(f)))"
(theory graded-monoid))
(def-theorem failure-property
"forall(f:ff, u:uu, a:action, u in support(f) and not extendable(f,u,a)
implies
forall(x:sets[action], x in f(u) implies (x union singleton{a}) in f(u)))"
lemma
(theory graded-monoid)
(proof
(
(unfold-single-defined-constant-globally extendable)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "failure_q(f)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(f:ff,failure_q(f));")
(unfold-single-defined-constant-globally failure_q)
direct-and-antecedent-inference-strategy
simplify)
(apply-macete-with-minor-premises ff-in-quasi-sort_directed-monoid-theory)
)))
(def-theorem finite-non-extendable-sets-may-be-added-to-refusal-sets
"forall(f:ff, u:uu, s,s_1:sets[action],
u in support(f) and
f_indic_q{s} and
s_1 in f(u) and
forall(a:action, a in s implies not(extendable(f,u,a))) implies
s union s_1 in f(u))"
(theory graded-monoid)
(proof
(
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(n:zz,
0<=n
implies
forall(s:sets[action],
f_card{s}=n and
forall(a:action, a in s implies not(extendable(f_$0,u,a)))
implies s union s_1 in f_$0(u)))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(weaken (3 0))
(induction trivial-integer-inductor ("n"))
(block
(script-comment "`induction' at (0 0)")
beta-reduce-repeatedly
(apply-macete-with-minor-premises tr%empty-indic-has-f-card-zero)
direct-and-antecedent-inference-strategy
(backchain "with(f,s:sets[action],s=f);")
(apply-macete-with-minor-premises tr%union-commutativity)
(apply-macete-with-minor-premises tr%union-with-empty))
(block
(script-comment "`induction' at (0 1 0 0 0 0 0 0 0)")
(cut-with-single-formula "forsome(x:action, x in s )")
(antecedent-inference "with(s:sets[action],nonempty_indic_q{s});")
(cut-with-single-formula "s= (s diff singleton{x}) union singleton{x}")
(cut-with-single-formula "f_card{s diff singleton{x}}=t")
(instantiate-universal-antecedent "with(p:prop,forall(s:sets[action],p));"
("s diff singleton{x}"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 1 0 0)")
(instantiate-universal-antecedent "with(p:prop,forall(a:action,p));"
("a_$0"))
(contrapose "with(p:prop,not(p));")
(incorporate-antecedent "with(a_$0:action,f,s:sets[action],a_$0 in s diff f);")
simplify-insistently)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(backchain "with(f,s:sets[action],s=f);")
(force-substitution "(s diff singleton{x}) union singleton{x} union s_1"
"((s diff singleton{x}) union s_1) union singleton{x} "
(0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises failure-property)
direct-and-antecedent-inference-strategy
simplify)
(move-to-ancestor 6)
(move-to-descendent (1))
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "f_indic_q{s}")
(incorporate-antecedent "with(r:rr,n:nn,n=r);")
(backchain "with(f,s:sets[action],s=f);")
(apply-macete-with-minor-premises tr%f-card-disjoint-union)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite)
simplify)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(apply-macete-with-minor-premises tr%singleton-has-f-card-one-rewrite)
(instantiate-existential ("1")))
(block
(script-comment "`apply-macete-with-minor-premises' at (2)")
(apply-macete-with-minor-premises tr%subset-of-finite-indic-is-finite)
auto-instantiate-existential
simplify-insistently)
simplify-insistently)
(move-to-ancestor 7)
(move-to-descendent (1))
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
simplify-insistently
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
simplify-insistently
direct-and-antecedent-inference-strategy
simplify))
(move-to-ancestor 9)
(move-to-descendent (1))
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%rev%positive-f-card-iff-nonempty)
simplify)
(block
(script-comment "`force-substitution' at (1)")
simplify
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
simplify-insistently
direct-and-antecedent-inference-strategy)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
simplify-insistently
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(backchain "with(x,x_$1:action,x_$1=x);"))))))
)))
(def-theorem finite-non-extendable-sets-may-be-refused
"forall(f:ff, u:uu, s:sets[action],
u in support(f) and
f_indic_q{s} and
forall(a:action, a in s implies not(extendable(f,u,a))) implies
s in f(u))"
(theory graded-monoid)
(proof
(
direct-and-antecedent-inference-strategy
(force-substitution "s" "s union empty_indic{action}" (0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises finite-non-extendable-sets-may-be-added-to-refusal-sets)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises rev%failure-non-empty-condition)
(incorporate-antecedent "with(u:uu,f:sets[uu],u in f);")
(unfold-single-defined-constant (0) support)
simplify)
(apply-macete-with-minor-premises tr%union-with-empty)
)))
(def-transported-symbols (ff_aa rel_aa)
(translation finite-specialization-of-rgm)
(renamer fs-rgm-renamer))
(def-theorem rel_fin-is-non-expansive
"forall(f,g:ff, fn%dist(rel_fin(f),rel_fin(g))<=fn%dist(f,g))"
(theory graded-monoid)
(proof
(
(apply-macete-with-minor-premises tr%rel_aa-is-non-expansive)
)))