(def-language degree-equivalence-language
(embedded-languages h-o-real-arithmetic)
(base-types pp)
(constants
(approx "[pp,pp,zz->prop]")))
(def-theory degree-equivalence
(language degree-equivalence-language)
(component-theories h-o-real-arithmetic)
(axioms
(approx-separation
"forall(x,y:pp, not(x=y) implies forsome(n:zz, not(approx(x,y,n))))")
(approx-monotonicity
"forall(m,n:zz,x,y:pp, approx(x,y,n) and m<=n implies approx(x,y,m))")
(approx-existence
"forall(x,y:pp, forsome(m:zz, approx(x,y,m)))")
(approx-reflexivity
"forall(m:zz,x:pp, approx(x,x,m))")
(approx-symmetry
"forall(m:zz,x,y:pp, approx(x,y,m) implies approx(y,x,m))")
(approx-transitivity
"forall(m:zz,x,y,z:pp, approx(x,y,m) and approx(y,z,m) implies approx(x,z,m))")))
(def-constant sep%deg
"lambda(x,y:pp,
iota(n:zz, not(approx(x,y,n))
and
forall(m:zz, m<n implies approx(x,y,m))))"
(theory degree-equivalence))
(def-theorem iota-free-characterization-of-sep%deg
"forall(x,y:pp, n:zz,
sep%deg(x,y)=n iff
(not(approx(x,y,n))
and
forall(m:zz, m<n implies approx(x,y,m))))"
(theory degree-equivalence)
(proof
(
(unfold-single-defined-constant (0) sep%deg)
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);"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1 0 0)")
(contrapose "with(n:zz,n=n);")
(apply-macete-with-minor-premises eliminate-iota-macete)
(contrapose "with(m:zz,y,x:pp,not(approx(x,y,m)));")
simplify)
(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
(cut-with-single-formula "b<=n and n<=b")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
direct-inference
(block
(script-comment "`direct-inference' at (0)")
(contrapose "with(n:zz,y,x:pp,not(approx(x,y,n)));")
simplify)
(block
(script-comment "`direct-inference' at (1)")
(contrapose "with(b:zz,y,x:pp,not(approx(x,y,b)));")
simplify)))
)))
(def-theorem alternate-iota-free-characterization-of-sep%deg
"forall(x,y:pp, n:zz,
sep%deg(x,y)=n iff
(not(approx(x,y,n)) and approx(x,y,n-1)))"
(theory degree-equivalence)
(proof
(
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 1 0 0 0)")
(apply-macete-with-minor-premises approx-monotonicity)
(instantiate-existential ("n-1"))
simplify)
)))
(def-theorem definedness-of-sep%deg
"forall(x,y:pp, not(x=y) implies #(sep%deg(x,y)))"
(theory degree-equivalence)
(usages d-r-convergence)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(s:zz, sep%deg(x,y)=s)")
(antecedent-inference "with(p:prop,forsome(s:zz,p));")
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
(instantiate-theorem well-ordering-for-integers
("lambda(n:zz, not(approx(x,y,n)))"))
(block
(script-comment "`instantiate-theorem' at (0 0 0)")
(contrapose "with(p:prop,forall(y:zz,p));")
simplify
(apply-macete-with-minor-premises approx-separation))
(block
(script-comment "`instantiate-theorem' at (0 0 1)")
(beta-reduce-antecedent "with(y,x:pp,
forall(n:zz,
forsome(m:zz,
m<=n and lambda(n:zz,not(approx(x,y,n)))(m))));")
(contrapose "with(p:prop,forall(n:zz,p));")
(cut-with-single-formula "forsome(n:zz, approx(x,y,n))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(instantiate-existential ("n"))
(apply-macete-with-minor-premises approx-monotonicity)
auto-instantiate-existential)
(apply-macete-with-minor-premises approx-existence))
(block
(script-comment "`instantiate-theorem' at (0 1 0 0)")
(beta-reduce-antecedent "with(u:zz,y,x:pp,lambda(n:zz,not(approx(x,y,n)))(u));")
(beta-reduce-antecedent "with(y,x:pp,u:zz,
forall(v:zz,
v<u implies not(lambda(n:zz,not(approx(x,y,n)))(v))));")
auto-instantiate-existential
(instantiate-universal-antecedent "with(p:prop,forall(v:zz,p));"
("m"))))
)))
(def-theorem undefinedness-case-of-sep%deg
"forall(x:pp, not(#(sep%deg(x,x))))"
(theory degree-equivalence)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(n:zz, approx(x,x,n))")
(move-to-sibling 1)
(apply-macete-with-minor-premises approx-reflexivity)
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(p:prop,p);")
(cut-with-single-formula "forsome(s:zz, sep%deg(x,x)=s)")
(move-to-sibling 1)
(instantiate-existential ("sep%deg(x,x)"))
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(s:zz,p));")
(incorporate-antecedent "with(s,n:zz,n=s);")
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
auto-instantiate-existential))
)))
(def-theorem sep%deg-upper-bound
"forall(x,y:pp, n:zz, not(x=y)
implies
(sep%deg(x,y)<=n iff not(approx(x,y,n))))"
(theory degree-equivalence)
(proof
(
direct-inference
direct-inference
(cut-with-single-formula "forsome(s:zz, sep%deg(x,y)=s)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(s:zz,p));")
(backchain "with(s,n:zz,n=s);")
(incorporate-antecedent "with(s,n:zz,n=s);")
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(contrapose "with(s:zz,y,x:pp,not(approx(x,y,s)));")
(apply-macete-with-minor-premises approx-monotonicity)
auto-instantiate-existential)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0)")
(contrapose "with(n:zz,y,x:pp,not(approx(x,y,n)));")
simplify))
(block
(script-comment "`cut-with-single-formula' at (1)")
(instantiate-existential ("sep%deg(x,y)"))
simplify)
))
)
(def-theorem symmetry-of-sep%deg
"forall(x,y:pp, not(x=y)
implies
sep%deg(x,y)=sep%deg(y,x))"
(theory degree-equivalence)
lemma
(proof
(
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
direct-inference
direct-inference
(cut-with-single-formula "forsome(s:zz, sep%deg(y,x)=s)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(s:zz,p));")
(backchain-repeatedly ("with(s:zz,x,y:pp,sep%deg(y,x)=s);"))
(incorporate-antecedent "with(s,n:zz,n=s);")
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(contrapose "with(s:zz,x,y:pp,not(approx(y,x,s)));")
(apply-macete-with-minor-premises approx-symmetry))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0 0)")
(apply-macete-with-minor-premises approx-symmetry)
simplify))
(instantiate-existential ("sep%deg(y,x)"))
)))
(def-theorem reverse-ultrametric-lemma
"forall(x,y,z:pp,
not x=y and not y=z and not x=z and sep%deg(x,y)<=sep%deg(y,z)
implies
sep%deg(x,y)<=sep%deg(x,z))"
lemma
(theory degree-equivalence)
(proof
(
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(n:zz,n<=n);")
(apply-macete-with-minor-premises sep%deg-upper-bound)
(cut-with-single-formula "forsome(s,t:zz, sep%deg(y,z)=s and sep%deg(x,z)=t)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(s,t:zz,p));")
(backchain-repeatedly
("with(t:zz,x:pp,s:zz,z,y:pp,
sep%deg(y,z)=s and sep%deg(x,z)=t);"))
(incorporate-antecedent "with(p:prop,p and p);")
(apply-macete-with-minor-premises iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
(contrapose "with(t:zz,z,x:pp,not(approx(x,z,t)));")
(case-split ("t<s"))
(block
(script-comment "`case-split' at (1)")
(apply-macete-with-minor-premises approx-transitivity)
auto-instantiate-existential
(backchain "with(z,y:pp,s:zz,forall(m:zz,m<s implies approx(y,z,m)));"))
(block
(script-comment "`case-split' at (2)")
(contrapose "with(s:zz,y,x:pp,not(approx(x,y,s)));")
(apply-macete-with-minor-premises approx-monotonicity)
auto-instantiate-existential
simplify))
(instantiate-existential ("sep%deg(y,z)" "sep%deg(x,z)"))
)))
(def-theorem reverse-ultrametric-inequality
"forall(x,y,z:pp,
not x=y and not y=z and not x=z
implies
min(sep%deg(x,y),sep%deg(y,z))<=sep%deg(x,z))"
(theory degree-equivalence)
lemma
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) min)
(raise-conditional (0))
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises reverse-ultrametric-lemma)
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(apply-macete-with-minor-premises symmetry-of-sep%deg)
(apply-macete-with-minor-premises reverse-ultrametric-lemma)
(apply-macete-with-minor-premises symmetry-of-sep%deg)
simplify)
)))
(def-constant sep%dist
"lambda(x,y:pp, if(x=y,0,2^(- sep%deg(x,y))))"
(theory degree-equivalence))
(def-theorem sep%dist-reflexive
"forall(x,y:pp, sep%dist(x,y)=0 iff x=y)"
reverse
(theory degree-equivalence)
(proof
(
(unfold-single-defined-constant (0) sep%dist)
direct-and-antecedent-inference-strategy
(move-to-ancestor 1)
(case-split ("x=y"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
(cut-with-single-formula "0<[1/2]^sep%deg(x,y)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify)
simplify)
)))
(def-theorem sep%dist-non-negative
"forall(x,y:pp, 0<=sep%dist(x,y))"
(theory degree-equivalence)
(proof
(
direct-inference
(case-split ("x=y"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "sep%dist(x,y)=0")
simplify
(apply-macete-with-minor-premises sep%dist-reflexive))
(block
(script-comment "`case-split' at (2)")
(unfold-single-defined-constant-globally sep%dist)
simplify
(cut-with-single-formula "0<[1/2]^sep%deg(x,y)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify))
)))
(def-theorem sep%dist-symmetric
"forall(x,y:pp, sep%dist(x,y)=sep%dist(y,x))"
(theory degree-equivalence)
(proof
(
direct-and-antecedent-inference-strategy
(case-split ("x=y"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "sep%dist(x,y)=0 and sep%dist(x,y)=0")
(apply-macete-with-minor-premises sep%dist-reflexive))
(block
(script-comment "`case-split' at (2)")
unfold-defined-constants
simplify
(cut-with-single-formula "sep%deg(x,y)=sep%deg(y,x)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-locally symmetry-of-sep%deg
(0)
"sep%deg(x,y)")
simplify))
)))
(def-theorem min-under-nondecreasing-fn-lemma
"forall(x,y:zz,f:[zz,rr],
forall(x,y:zz, x<=y implies f(y)<=f(x))
implies
f(min(x,y))=max(f(x),f(y)))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
unfold-defined-constants
(case-split ("x<=y"))
(block
(script-comment "`case-split' at (1)")
simplify
(cut-with-single-formula "f(y)<f(x) or f(y)=f(x)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
simplify
(instantiate-universal-antecedent "with(p:prop,forall(x,y:zz,p));"
("x" "y"))
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
simplify
simplify))
(block
(script-comment "`case-split' at (2)")
simplify
(cut-with-single-formula "f(x)<f(y) or f(x)=f(y)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(instantiate-universal-antecedent "with(p:prop,forall(x,y:zz,p));"
("y" "x"))
simplify
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
simplify
simplify))
)))
(def-theorem sep%dist-ultrametric
"forall(x,y,z:pp, sep%dist(x,z)<=max(sep%dist(x,y),sep%dist(y,z)))"
(theory degree-equivalence)
(proof
(
direct-and-antecedent-inference-strategy
(case-split ("x=z"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "sep%dist(x,z)=0")
(block
(script-comment "`cut-with-single-formula' at (0)") simplify
(unfold-single-defined-constant (0) max)
(cut-with-single-formula "0<=sep%dist(x,y) and 0<= sep%dist(y,x)")
(block
(script-comment "`cut-with-single-formula' at (0)") simplify
(case-split-on-conditionals (0))
)
(apply-macete-with-minor-premises sep%dist-non-negative)
)
(apply-macete-with-minor-premises sep%dist-reflexive)
)
(block
(script-comment "`case-split' at (2)") (case-split ("x=y"))
(block
(script-comment "`case-split' at (1)") simplify
(cut-with-single-formula "sep%dist(x,x)=0")
(block
(script-comment "`cut-with-single-formula' at (0)")
(unfold-single-defined-constant (0) max) simplify
)
(apply-macete-with-minor-premises sep%dist-reflexive)
)
(block
(script-comment "`case-split' at (2)") (case-split ("y=z"))
(block
(script-comment "`case-split' at (1)") simplify
(cut-with-single-formula "sep%dist(z,z)=0")
(block
(script-comment "`cut-with-single-formula' at (0)")
(unfold-single-defined-constant (0) max) simplify
(cut-with-single-formula "0<sep%dist(x,z)") simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "0<=sep%dist(x,y) and not sep%dist(x,y)=0")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises sep%dist-non-negative)
(apply-macete-with-minor-premises sep%dist-reflexive)
) ) )
(apply-macete-with-minor-premises sep%dist-reflexive)
)
(block
(script-comment "`case-split' at (2)")
(unfold-single-defined-constant-globally sep%dist) simplify
(instantiate-theorem min-under-nondecreasing-fn-lemma
("sep%deg(x,y)" "sep%deg(y,z)" "lambda(n:zz, [1/2]^n)")
)
(block
(script-comment "`instantiate-theorem' at (0 0 0 0)")
(contrapose "with(r:rr,not(r<=r));") beta-reduce-repeatedly
(apply-macete-with-minor-premises monotonicity-of-exponentiation)
simplify
)
(block
(script-comment "`instantiate-theorem' at (0 1)")
(beta-reduce-antecedent
"with(z,y,x:pp,
lambda(n:zz,[1/2]^n)(min(sep%deg(x,y),sep%deg(y,z)))
=max(lambda(n:zz,[1/2]^n)(sep%deg(x,y)),
lambda(n:zz,[1/2]^n)(sep%deg(y,z))));"
)
(backchain-backwards "with(r:rr,r=r);")
(apply-macete-with-minor-premises monotonicity-of-exponentiation)
(apply-macete-with-minor-premises reverse-ultrametric-inequality)
simplify
) ) ) )
)))
(def-translation ultrametric-to-degree-equivalence
Remark: This entry is multiply defined. See: [1] [2]
force-under-quick-load
(source ultrametric-spaces)
(target degree-equivalence)
(fixed-theories h-o-real-arithmetic)
(constant-pairs (dist sep%dist))
(theory-interpretation-check using-simplification))
(def-theorem sep%dist-is-a-metric
ultrametic-spaces-are-metric
(theory degree-equivalence)
(translation ultrametric-to-degree-equivalence)
(proof existing-theorem))
(def-theory-ensemble-instances metric-spaces
force-under-quick-load
(target-theories degree-equivalence degree-equivalence)
(permutations (0) (0 1))
(theory-interpretation-check using-simplification)
(sorts (pp pp pp))
(constants (dist sep%dist sep%dist)))
(def-translation ultrametric-to-degree-equivalence
Remark: This entry is multiply defined. See: [1] [2]
force-under-quick-load
(source ultrametric-spaces)
(target degree-equivalence)
(fixed-theories h-o-real-arithmetic)
(constant-pairs (dist sep%dist))
(theory-interpretation-check using-simplification))
(def-theory-ensemble-overloadings metric-spaces
(1 2))
(def-theorem small-distance-characterization-lemma
"forall(x,y:pp, n:zz, sep%dist(x,y)<=2^(-n) iff (x=y or n<=sep%deg(x,y)))"
lemma
(theory degree-equivalence)
(proof
(
direct-inference
(case-split ("x=y"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "sep%dist(x,y)=0 ")
(block
(script-comment "`cut-with-single-formula' at (0)")
simplify
(cut-with-single-formula "0<[1/2]^n")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify))
(apply-macete-with-minor-premises sep%dist-reflexive))
(block
(script-comment "`case-split' at (2)")
(unfold-single-defined-constant (0) sep%dist)
simplify
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(contrapose "with(r:rr,r<=r);")
(cut-with-single-formula "[1/2]^n < [1/2]^sep%deg(x,y)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises strict-monotonicity-of-exponentiation)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(apply-macete-with-minor-premises monotonicity-of-exponentiation)
simplify)))))
(def-theorem small-distance-characterization
"forall(x,y:pp, n:zz, sep%dist(x,y)<=2^(-n) iff approx(x,y,n-1))"
(theory degree-equivalence)
lemma
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises small-distance-characterization-lemma)
(force-substitution "n<=sep%deg(x,y)" "not(sep%deg(x,y)<=n-1)" (0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
(cut-with-single-formula "#(sep%deg(x,y))")
(move-to-sibling 1)
(apply-macete-with-minor-premises definedness-of-sep%deg)
(prove-by-logic-and-simplification 0))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises sep%deg-upper-bound)
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises approx-reflexivity))
)))
(def-theorem powers-arbitrarily-small
"forall(r,eps:rr,
0<r and r<1 and 0<eps
implies
forsome(n:zz,1<=n and r^n<=eps))"
(theory h-o-real-arithmetic)
lemma
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "convergent%to%infinity(lambda(n:zz,(r^[-1])^n))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises r^n-convergent-to-infinity)
(apply-macete-with-minor-premises fractional-expression-manipulation)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(f:[zz,rr],convergent%to%infinity(f));")
(unfold-single-defined-constant (0) convergent%to%infinity)
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(m:rr,p));"
("eps^[-1]"))
(instantiate-universal-antecedent "with(p:prop,forall(j:zz,p));"
("max(1,x)"))
(simplify-antecedent "with(p:prop,not(p));")
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(incorporate-antecedent "with(r:rr,r<=r);")
(apply-macete-with-minor-premises fractional-expression-manipulation)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
simplify
direct-and-antecedent-inference-strategy
auto-instantiate-existential
simplify)
(apply-macete-with-minor-premises positivity-for-r^n))))))
(def-theorem cauchy-characterization-for-sep%dist
"forall(f:[zz->pp],
cauchy(f)
iff
forall(m:zz, forsome(n:zz, forall(p:zz, n<=p implies approx(f(p),f(p+1),m)))))"
(theory degree-equivalence)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%cauchy-ultrametric-condition)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(instantiate-universal-antecedent "with(p:prop,p);" ("2^(-(m+1))"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,p);")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1 0)")
(instantiate-existential ("n_$0"))
(incorporate-antecedent "with(p:prop,forall(m_$0:zz,p));")
(apply-macete-with-minor-premises small-distance-characterization)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(cut-with-single-formula "forsome(n:zz,1<=n and 2^(-n)<=eps)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
simplify
(apply-macete-with-minor-premises powers-arbitrarily-small)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"
("n-1"))
(instantiate-existential ("max(n_$0,n)"))
(cut-with-single-formula "sep%dist(f(m_$0),f(m_$0+1))<=2^(-n)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises small-distance-characterization)
(backchain "with(p:prop,forall(p_$0:zz,p));")
(cut-with-single-formula "n_$0<=max(n_$0,n)")
simplify
simplify)))
)))
(def-theorem strong-cauchy-characterization-for-sep%dist
"forall(f:[zz->pp],
cauchy(f)
iff
forall(m:zz, forsome(n:zz, forall(p,q:zz, n<=p and n<=q implies approx(f(p),f(q),m)))))"
(theory degree-equivalence)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%cauchy-double-index-characterization)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(instantiate-universal-antecedent "with(p:prop,p);" ("2^(-(m+1))"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,p);")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1 0)")
(incorporate-antecedent "with(p:prop,p);")
(apply-macete-with-minor-premises small-distance-characterization)
simplify
direct-and-antecedent-inference-strategy
(instantiate-existential ("n"))))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(cut-with-single-formula "forsome(n:zz,1<=n and 2^(-n)<=eps)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
simplify
(apply-macete-with-minor-premises powers-arbitrarily-small)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"
("n-1"))
(instantiate-existential ("max(n_$0,n)"))
(cut-with-single-formula "sep%dist(f(p_$0),f(q_$0))<=2^(-n)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises small-distance-characterization)
(backchain "with(p:prop,forall(p_$0,q_$0:zz,p));")
(cut-with-single-formula "n_$0<=max(n_$0,n)")
simplify
simplify)))
)))
(def-theorem lim-characterization-for-sep%dist
"forall(f:[zz->pp],s:pp,
lim(f)=s
iff
forall(m:zz, forsome(n:zz, forall(p:zz, n<=p implies approx(f(p),s,m)))))"
(theory degree-equivalence)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises tr%characterization-of-limit)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0)")
(instantiate-universal-antecedent "with(p:prop,p);" ("2^(-(m+1))"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0)")
(contrapose "with(p:prop,p);")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify)
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1 0)")
(instantiate-existential ("n_$0"))
(incorporate-antecedent "with(p:prop,forall(p_$0:zz,p));")
(apply-macete-with-minor-premises small-distance-characterization)
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises approx-symmetry)
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(cut-with-single-formula "forsome(n:zz,1<=n and 2^(-n)<=eps_$0)")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
simplify
(apply-macete-with-minor-premises powers-arbitrarily-small)
simplify)
(block
(script-comment "`cut-with-single-formula' at (0)")
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"
("n-1"))
(instantiate-existential ("max(n_$0,n)"))
(cut-with-single-formula "sep%dist(s,f(p_$1))<=2^(-n)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises small-distance-characterization)
(apply-macete-with-minor-premises approx-symmetry)
(backchain "with(p:prop,forall(p_$0:zz,p));")
(cut-with-single-formula "n_$0<=max(n_$0,n)")
simplify
simplify)))
)))
(def-theory-ensemble-instances metric-spaces
force-under-quick-load
(target-theories degree-equivalence degree-equivalence)
(permutations (0) (0 1))
(theory-interpretation-check using-simplification)
(sorts (pp pp pp))
(constants (dist sep%dist sep%dist)))
(def-theory-ensemble-overloadings metric-spaces (1 2))
(def-theorem characterization-of-contractiveness
"forall(x,y,u,v:pp,
forall(m:zz,approx(x,y,m) implies approx(u,v,m+1))
implies
sep%dist(u,v)<=[1/2]*sep%dist(x,y))"
(theory degree-equivalence)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally sep%dist)
(case-split ("x=y"))
(block
(script-comment "`case-split' at (1)")
simplify
(case-split ("u=v"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
(contrapose "with(p:prop,forall(m:zz,p));")
(backchain "with(y,x:pp,x=y);")
(cut-with-single-formula "forsome(m:zz, not(approx(u,v,m+1)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:zz,p));")
(instantiate-existential ("m"))
(apply-macete-with-minor-premises approx-reflexivity))
(block
(script-comment "`cut-with-single-formula' at (1)")
(cut-with-single-formula "forsome(m:zz,not(approx(u,v,m)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:zz,p));")
(instantiate-existential ("m-1"))
simplify)
(apply-macete-with-minor-premises approx-separation))))
(block
(script-comment "`case-split' at (2)")
simplify
(case-split ("u=v"))
(block
(script-comment "`case-split' at (1)")
simplify
(cut-with-single-formula "0<[1/2]^sep%deg(x,y)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify))
(block
(script-comment "`case-split' at (2)")
simplify
simplify
(force-substitution "2*[1/2]^sep%deg(u,v)"
"[1/2]^(sep%deg(u,v)-1)"
(0))
(move-to-sibling 1)
(block
(script-comment "`force-substitution' at (1)")
simplify
(apply-macete-with-minor-premises sum-of-exponents-law))
(block
(script-comment "`force-substitution' at (0)")
(apply-macete-with-minor-premises monotonicity-of-exponentiation)
direct-and-antecedent-inference-strategy
(move-to-sibling 2)
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises sep%deg-upper-bound)
(cut-with-single-formula "forsome(m:zz ,sep%deg(u,v)=m)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:zz,p));")
(backchain "with(m,z:zz,z=m);")
(incorporate-antecedent "with(m,z:zz,z=m);")
(apply-macete-with-minor-premises alternate-iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
(contrapose "with(m:zz,v,u:pp,not(approx(u,v,m)));")
(instantiate-universal-antecedent "with(p:prop,forall(m:zz,p));"
("m-1"))
(simplify-antecedent "with(r:rr,v,u:pp,approx(u,v,r+1));"))
(instantiate-existential ("sep%deg(u,v)")))
simplify)))
)))
(def-theorem contraction-characterization-for-sep%dist
"forall(f:[pp->pp],
forall(x,y:pp, m:zz, approx(x,y,m) implies approx(f(x),f(y),m+1))
implies
contraction(f))"
(theory degree-equivalence)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant (0) contraction)
(instantiate-existential ("[1/2]"))
simplify
simplify
(block
(script-comment "`instantiate-existential' at (0 2 0 0)")
(apply-macete-with-minor-premises characterization-of-contractiveness)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
simplify)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(simplify-antecedent "with(p:prop,p and p);"))
(simplify-antecedent "with(p:prop,p and p);"))
)))
(def-theorem characterization-of-non-expansiveness
"forall(x,y,u,v:pp,
forall(m:zz,approx(x,y,m) implies approx(u,v,m))
implies
sep%dist(u,v)<=sep%dist(x,y))"
(theory degree-equivalence)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(unfold-single-defined-constant-globally sep%dist)
(case-split ("x=y"))
(block
(script-comment "`case-split' at (1)")
simplify
(case-split ("u=v"))
simplify
(block
(script-comment "`case-split' at (2)")
simplify
(contrapose "with(p:prop,forall(m:zz,p));")
(backchain "with(y,x:pp,x=y);")
(cut-with-single-formula "forsome(m:zz, not(approx(u,v,m)))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:zz,p));")
(instantiate-existential ("m"))
(apply-macete-with-minor-premises approx-reflexivity))
(apply-macete-with-minor-premises approx-separation)))
(block
(script-comment "`case-split' at (2)")
simplify
(case-split ("u=v"))
(block
(script-comment "`case-split' at (1)")
simplify
(cut-with-single-formula "0<[1/2]^sep%deg(x,y)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises positivity-for-r^n)
simplify))
(block
(script-comment "`case-split' at (2)")
simplify
(apply-macete-with-minor-premises monotonicity-of-exponentiation)
direct-and-antecedent-inference-strategy
(move-to-sibling 1)
simplify
(move-to-sibling 2)
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises sep%deg-upper-bound)
(cut-with-single-formula "forsome(m:zz, sep%deg(u,v)=m)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:zz,p));")
(backchain "with(m,z:zz,z=m);")
(incorporate-antecedent "with(m,z:zz,z=m);")
(apply-macete-with-minor-premises alternate-iota-free-characterization-of-sep%deg)
direct-and-antecedent-inference-strategy
(contrapose "with(m:zz,v,u:pp,not(approx(u,v,m)));")
simplify)
(instantiate-existential ("sep%deg(u,v)")))))
)))