(def-theorem complete-induction-schema
Remark: This entry is multiply defined. See: [1] [2]
"forall(p:[zz,prop],n:zz,
forall(k:zz,n<=k implies p(k))
iff
(truth
and
forall(m:zz,
n<=m and forall(k:zz,n<=k and k<m implies p(k))
implies
p(m))))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(backchain "with(p:[zz,prop],n:zz,forall(k:zz,n<=k implies p(k)));")
(apply-macete-with-minor-premises complete-induction)
(instantiate-existential ("n"))
)))
(def-inductor complete-inductor
complete-induction-schema
(theory h-o-real-arithmetic))
(def-theorem omega-n-as-domain-lemma
"forall(f:[nn->nn],n:nn, dom{f}=omega(n) iff forall(x:nn, #(f(x)) iff x<n))"
(theory h-o-real-arithmetic)
lemma
(proof
(
(unfold-single-defined-constant (0) omega)
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-and-antecedent-inference-strategy
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 0
0 0)")
(instantiate-universal-antecedent "with(f:[nn,nn],dom{f})
subseteq with(f:[nn,prop],pred_to_indic(f));"
("x"))
(simplify-antecedent "with(p:prop,not(p));")
(simplify-antecedent "with(x:nn,f:sets[nn],x in f);"))
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 0 0
1 0)")
(instantiate-universal-antecedent "with(f:[nn,prop],pred_to_indic(f))
subseteq with(f:[nn,nn],dom{f});"
("x"))
(simplify-antecedent "with(p:prop,not(p));")
(simplify-antecedent "with(x:nn,f:sets[nn],x in f);"))
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 1 0)")
insistent-direct-inference
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(x:nn,p));"
("x_$2"))
simplify
(simplify-antecedent "with(x_$2:nn,f:sets[nn],x_$2 in f);"))
(block
(script-comment "node added by `direct-and-antecedent-inference-strategy' at (0 1 1)")
insistent-direct-inference
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:prop,forall(x:nn,p iff p));"
("x_$1"))
simplify
(block
(script-comment "node added by `instantiate-universal-antecedent' at (0 0 1)")
simplify))
)))
(def-theorem not-in-range-condition
"forall(f,g:[nn,nn], m:nn, dom{f}=dom{g} and
forall(k,l:nn, #(f(k)) and #(f(l)) and #(g(k)) and #(g(l)) and k<l
implies
f(k) < f(l) and g(k)<g(l))
and
forall(x:nn, x<m implies f(x)==g(x))
and
f(m)<g(m)
implies not(f(m) in ran{g}))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(contrapose "with(f:sets[nn],f=f);")
(antecedent-inference "with(p:prop,forsome(x:nn,p));")
(contrapose "with(n:nn,n=n);")
(cut-with-single-formula "x<m or x=m or m<x")
(move-to-sibling 1)
simplify
(block
(script-comment "node added by `cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p or p);")
(block
(script-comment "node added by `antecedent-inference' at (0)")
(case-split ("#(f(x)) and #(f(m))"))
(block
(script-comment "node added by `case-split' at (1)")
(cut-with-single-formula "f(x)=g(x) and f(x)<f(m)")
(move-to-sibling 1)
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
(backchain-backwards "with(p:prop,forall(x:nn,p));")
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,forall(k,l:nn,p));")
direct-and-antecedent-inference-strategy
(backchain-backwards "with(p:prop,forall(x:nn,p));")
direct-and-antecedent-inference-strategy)
simplify)
(block
(script-comment "node added by `case-split' at (2)")
(contrapose "with(p:prop,not(p));")
direct-inference
simplify))
simplify
(block
(script-comment "node added by `antecedent-inference' at (2)")
(case-split ("#(g(x))"))
(block
(script-comment "node added by `case-split' at (1)")
(cut-with-single-formula "g(m)<g(x)")
simplify
(block
(script-comment "node added by `cut-with-single-formula' at (1)")
simplify
simplify
(backchain "with(p:prop,forall(k,l:nn,p));")
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%rev%domain-membership-iff-defined)
(backchain "with(f:sets[nn],f=f);")
(apply-macete-with-minor-premises tr%domain-membership-iff-defined)))
simplify))
)))
(def-theorem characterization-of-omega-embedding-lemma
"forall(f,g:[nn -> nn], n:nn, dom{f}= dom{g}
and ran{f}=ran{g} and
forall(k,l:nn, k<l and l in dom{g} implies f(k) < f(l) and g(k)<g(l))
implies
g=f)"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forall(k:zz, 0<=k implies g(k)==f(k))")
(block
(script-comment "`cut-with-single-formula' at (0)")
extensionality
direct-inference
simplify)
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction complete-inductor ())
(case-split ("m in dom{g}"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "#(f(m)) and #(g(m))")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(incorporate-antecedent "with(m:zz,f:sets[nn],m in f);")
(backchain-backwards "with(g,f:[nn,nn],dom{f}=dom{g});")
simplify)
(simplify-antecedent "with(m:zz,f:sets[nn],m in f);"))
(block
(script-comment "`cut-with-single-formula' at (0)")
(cut-with-single-formula "g(m)<f(m) or g(m)=f(m) or f(m)<g(m)")
(move-to-sibling 1)
simplify
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(cut-with-single-formula "not(g(m) in ran{f})")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises not-in-range-condition)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 0
0 0)")
(backchain "with(p:prop,forall(k,l:nn,p));")
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 0
1 0)")
(backchain "with(p:prop,forall(k,l:nn,p));")
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0)")
(backchain "with(p:prop,forall(k:zz,p));")
simplify))
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(p:prop,not(p));")
(backchain "with(g,f:[nn,nn],ran{f}=ran{g});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(instantiate-existential ("m"))))
(block
(script-comment "`antecedent-inference' at (2)")
(cut-with-single-formula "not(f(m) in ran{g})")
(move-to-sibling 1)
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises not-in-range-condition)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 0
0 0)")
(backchain "with(p:prop,forall(k,l:nn,p));")
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 0 0
1 0)")
(backchain "with(p:prop,forall(k,l:nn,p));")
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0)")
(backchain "with(p:prop,forall(k:zz,p));")
simplify))
(block
(script-comment "`cut-with-single-formula' at (0)")
(contrapose "with(p:prop,not(p));")
(backchain-backwards "with(g,f:[nn,nn],ran{f}=ran{g});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(instantiate-existential ("m")))))))
(block
(script-comment "`case-split' at (2)")
(cut-with-single-formula "not(#(g(m))) and not(#(f(m)))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
direct-inference
(simplify-antecedent "with(p:prop,not(p));")
(block
(script-comment "`direct-inference' at (1)")
(contrapose "with(m:zz,f:sets[nn],not(m in f));")
(backchain-backwards "with(g,f:[nn,nn],dom{f}=dom{g});")
simplify))))
)))
(def-theorem characterization-of-omega-embedding
"forall(f:[nn -> nn], s:sets[nn],
(omega%embedding(s)=f
iff
(dom{f}=dom(omega%embedding(s))
and ran{f}=s and
forall(k,l:nn, k<l and l in dom{f} implies f(k) < f(l)))))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1)")
(backchain-backwards "with(f:[nn,nn],f=f);")
(apply-macete-with-minor-premises ran-of-omega%embedding))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 2
0 0 0)")
(backchain-backwards "with(f:[nn,nn],f=f);")
(backchain-backwards "with(f:[nn,nn],f=f);")
(apply-macete-with-minor-premises strong-monotonicity-of-omega%embedding)
(backchain "with(f:[nn,nn],f=f);")
direct-inference
(simplify-antecedent "with(l:nn,f:sets[nn],l in f);"))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0)")
(apply-macete-with-minor-premises characterization-of-omega-embedding-lemma)
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises ran-of-omega%embedding)
simplify
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0
1 0)")
(apply-macete-with-minor-premises strong-monotonicity-of-omega%embedding)
direct-and-antecedent-inference-strategy
(simplify-antecedent "with(l:nn,f:sets[nn],l in f);")))
)))
(def-theorem upper-bound-of-finite-sequences
"forall(f:[nn->rr],n:nn,
forsome(r:rr, forall(k:nn, k<=n and #(f(k))implies f(k)<=r)))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula
"forall(n:zz,0<=n implies
forsome(r:rr,forall(k:nn,k<=n and #(f(k)) implies f(k)<=r)))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction integer-inductor ())
(block
(script-comment "`induction' at (0 0 0)")
(case-split ("#(f(0))"))
(block
(script-comment "`case-split' at (1)")
(instantiate-existential ("f(0)"))
(cut-with-single-formula "k_$0=0")
simplify
simplify)
(block
(script-comment "`case-split' at (2)")
(instantiate-existential ("0"))
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "k=0")
simplify
simplify))
(block
(script-comment "`induction' at (0 1 0 0 0 0 0)")
(case-split ("#(f(1+t))"))
(block
(script-comment "`case-split' at (1)")
(instantiate-existential ("max(r,f(1+t))"))
(case-split ("k_$0<=t"))
(block
(script-comment "`case-split' at (1)")
(cut-with-single-formula "f(k_$0)<=r and r<=max(r,f(1+t))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises maximum-1st-arg)
simplify))
(block
(script-comment "`case-split' at (2)")
(cut-with-single-formula "f(1+t)<=max(r,f(1+t)) and f(k_$0)=f(1+t)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises maximum-2nd-arg)
(cut-with-single-formula "k_$0=1+t")
simplify)))
(block
(script-comment "`case-split' at (2)")
(instantiate-existential ("r"))
(backchain "with(p:prop,forall(k:nn,p));")
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not(k=1+t)")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(contrapose "with(p:prop,not(p));")
simplify))))
)))
(def-theorem upper-bound-of-finite-sequences-of-nn
"forall(f:[nn->nn],n:nn,
forsome(m:nn, forall(k:nn, k<=n and #(f(k))implies f(k)<=m)))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(r:rr, forall(k:nn, k<=n and #(f(k))implies f(k)<=r))")
(move-to-sibling 1)
(apply-macete-with-minor-premises upper-bound-of-finite-sequences)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p);")
(cut-with-single-formula "forsome(n:zz, max(0,r)<n)")
(move-to-sibling 1)
(apply-macete-with-minor-premises archimedean)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(n:zz,p));")
(instantiate-existential ("n_$0"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(cut-with-single-formula "r<=max(0,r) and f(k)<=r")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises maximum-2nd-arg)
simplify))
(block
(script-comment "`instantiate-existential' at (1)")
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
beta-reduce-repeatedly
(cut-with-single-formula "0<=max(0,r)")
simplify
(apply-macete-with-minor-premises maximum-1st-arg))))
)))
(def-theorem finite-sets-in-nn-are-bounded
"forall(s:sets[nn], f_indic_q{s} implies forsome(n:nn, s subseteq omega(n)))"
(theory h-o-real-arithmetic)
lemma
(proof
(
direct-and-antecedent-inference-strategy
(cut-with-single-formula "forsome(n:nn, omega(n) equinumerous s)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(n:nn,p));")
(antecedent-inference "with(s,f:sets[nn],f equinumerous s);")
(antecedent-inference "with(s:sets[nn],
bijective_on_q{with(f:[nn,nn],f),with(f:sets[nn],f),s});")
(cut-with-single-formula
"forsome(r:nn, forall(k:nn, k<=n and #(f(k)) implies f(k)<=r))")
(move-to-sibling 1)
(apply-macete-with-minor-premises upper-bound-of-finite-sequences-of-nn)
(block
(script-comment "`cut-with-single-formula' at (0)")
(weaken (1))
(antecedent-inference "with(s:sets[nn],
surjective_on_q{with(f:[nn,nn],f),with(f:sets[nn],f),s});")
(incorporate-antecedent "with(s:sets[nn],f:[nn,nn],ran{f}=s);")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
(antecedent-inference "with(p:prop,p and p);")
(instantiate-existential ("r+1"))
insistent-direct-inference
(instantiate-universal-antecedent
"with(f:[nn,nn],s:sets[nn],s subseteq ran{f});"
("x"))
(move-to-ancestor 3)
direct-inference
(instantiate-universal-antecedent "with(f:[nn,nn],s:sets[nn],s subseteq ran{f});"
("x"))
(contrapose "with(x:nn,f:[nn,nn],x in ran{f});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(contrapose "with(p:prop,not(p));")
(unfold-single-defined-constant (0) omega)
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
(antecedent-inference "with(p:prop,forsome(x_$1:nn,p));")
(backchain "with(n,x:nn,x=n);")
(instantiate-universal-antecedent "with(r,n:nn,p:prop,forall(k:nn,p and p implies n<=r));"
("x_$1"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 0 0)")
(contrapose "with(f:sets[nn],f=f);")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
(contrapose "with(n,x_$1:nn,not(x_$1<=n));")
(antecedent-inference "with(p:prop,p and p);")
(instantiate-universal-antecedent "with(n:nn,f:[nn,nn],dom{f} subseteq omega(n));"
("x_$1"))
(simplify-antecedent "with(x_$1:nn,f:sets[nn],not(x_$1 in f));")
(block
(script-comment "`instantiate-universal-antecedent' at (0 0 1)")
(incorporate-antecedent "with(x_$1,n:nn,x_$1 in omega(n));")
(unfold-single-defined-constant (0) omega)
(apply-macete-with-minor-premises indicator-facts-macete)
simplify))
simplify))
(block
(script-comment "`cut-with-single-formula' at (1)")
(incorporate-antecedent "with(p:prop,p);")
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-card)
direct-and-antecedent-inference-strategy
(move-to-ancestor 3)
(instantiate-existential ("n"))
(apply-macete-with-minor-premises tr%equinumerous-is-symmetric))
)))
(def-theorem subset-of-nn-finite-iff-bounded
"forall(s:sets[nn], f_indic_q{s} iff forsome(n:nn, s subseteq omega(n)))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises finite-sets-in-nn-are-bounded)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0)")
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(cut-with-single-formula "forsome(m:nn, m<=n and f_card{s}=m)")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:nn,p));")
(instantiate-existential ("m")))
(apply-macete-with-minor-premises subset-of-finite-cardinal-has-f-card))
)))
(def-theorem domain-of-omega-embedding-for-finite-sets
"forall(s:sets[nn], f_indic_q{s} implies dom{omega%embedding(s)}=omega(f_card{s}))"
(theory h-o-real-arithmetic)
(proof
(
(apply-macete-with-minor-premises subset-of-nn-finite-iff-bounded)
direct-and-antecedent-inference-strategy
(cut-with-single-formula
"forsome(m:nn, m<=n and dom{omega%embedding(s)}=omega(m))")
(move-to-sibling 1)
(apply-macete-with-minor-premises dom-of-omega%embedding-at-finite-set)
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(m:nn,p));")
(backchain "with(p:prop,p and p);")
(cut-with-single-formula "f_card{s}=m")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-card)
(antecedent-inference "with(p:prop,p and p);")
(apply-macete-with-minor-premises tr%equinumerous-is-symmetric)
(instantiate-existential ("omega%embedding(s)"))
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises ran-of-omega%embedding))
(block
(script-comment "`insistent-direct-inference' at (1)")
(apply-macete-with-minor-premises tr%injective-implies-injective-on)
(apply-macete-with-minor-premises injectiveness-of-omega%embedding))))
)))
(def-theorem characterization-of-omega-embedding-for-finite-sets
"forall(f:[nn -> nn], s:sets[nn],
f_indic_q{s}
implies
(omega%embedding(s)=f
iff
(dom{f}=omega(f_card{s})
and ran{f}=s and
forall(k,l:nn, k<l and l in dom{f} implies f(k) < f(l)))))"
(theory h-o-real-arithmetic)
(proof
(
(force-substitution "omega(f_card{s})" "dom(omega%embedding(s))" (0))
(move-to-sibling 1)
(apply-macete-with-minor-premises domain-of-omega-embedding-for-finite-sets)
(apply-macete-with-minor-premises characterization-of-omega-embedding)
)))
(def-theorem domain-of-omega-embedding-for-infinite-sets
"forall(s:sets[nn],
not(f_indic_q{s})
implies
dom{omega%embedding(s)}=sort_to_indic{nn})"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
simplify-insistently
(block
(script-comment "`direct-inference' at (1)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,not(p));")
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-indic-q)
(apply-macete-with-minor-premises tr%iota-free-definition-of-f-card)
(cut-with-single-formula "forsome(n:nn, dom{omega%embedding(s)}=omega(n))")
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,forsome(n:nn,p));")
(instantiate-existential ("n"))
(backchain-backwards "with(f:sets[nn],f=f);")
(apply-macete-with-minor-premises tr%equinumerous-is-symmetric)
(instantiate-existential ("omega%embedding(s)"))
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises ran-of-omega%embedding))
(block
(script-comment "`insistent-direct-inference' at (1)")
(apply-macete-with-minor-premises tr%injective-implies-injective-on)
(apply-macete-with-minor-premises injectiveness-of-omega%embedding)))
(block
(script-comment "`cut-with-single-formula' at (1)")
(weaken (2 1))
(contrapose "with(p:prop,p);")
(cut-with-single-formula "forall(k:zz, 0<=k implies #(omega%embedding(s)(k)))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction complete-inductor ("k"))
(move-to-ancestor 3)
(antecedent-inference "with(p:prop,p and p);")
(incorporate-antecedent "with(p:prop,forall(n:nn,not(p)));")
(apply-macete-with-minor-premises omega-n-as-domain-lemma)
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,forall(n:nn,not(p)));")
(instantiate-existential ("m"))
(block
(script-comment "`instantiate-existential' at (0 0 0)")
(contrapose "with(n:nn,#(n));")
(case-split ("m=x or m<x"))
(antecedent-inference "with(p:prop,p or p);")
simplify
(instantiate-theorem strong-monotonicity-of-omega%embedding
("s" "m" "x")))
simplify)))
)))
(def-theorem characterization-of-omega-embedding-for-infinite-sets
"forall(f:[nn -> nn], s:sets[nn],
not(f_indic_q{s})
implies
(omega%embedding(s)=f
iff
(dom{f}=sort_to_indic{nn}
and ran{f}=s and
forall(k,l:nn, k<l and l in dom{f} implies f(k) < f(l)))))"
(theory h-o-real-arithmetic)
(proof
(
(force-substitution "sort_to_indic{nn}" "dom(omega%embedding(s))" (0))
(move-to-sibling 1)
(apply-macete-with-minor-premises domain-of-omega-embedding-for-infinite-sets)
(apply-macete-with-minor-premises characterization-of-omega-embedding)
)))
(def-theorem compositionality-of-omega-embedding
"forall(s:sets[nn], f:[nn -> nn],
s subseteq dom{f} and
forall(a,b:nn, a<b and a in s and b in s implies f(a)<f(b))
implies
omega%embedding(image{f,s})=f oo (omega%embedding(s)))"
(theory h-o-real-arithmetic)
(proof
(
direct-and-antecedent-inference-strategy
(case-split ("f_indic_q{s}"))
(block
(script-comment "`case-split' at (1)")
(apply-macete-with-minor-premises characterization-of-omega-embedding-for-finite-sets)
(move-to-sibling 1)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(cut-with-single-formula "f_card{image{f,s}}<=f_card{s}")
(apply-macete-with-minor-premises tr%image-of-a-finite-set-is-finite))
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises tr%domain-composition)
(move-to-sibling 1)
(apply-macete-with-minor-premises ran-of-omega%embedding)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
(apply-macete-with-minor-premises domain-of-omega-embedding-for-finite-sets)
(cut-with-single-formula "f_card{s}=f_card{image{f,s}}")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%f-card-equal-iff-finite-and-equinumerous)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1 1 0)")
(instantiate-existential ("restrict{f,s}"))
insistent-direct-inference
(block
(script-comment "`insistent-direct-inference' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises tr%domain-of-a-restriction)
(block
(script-comment "`insistent-direct-inference' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
(block
(script-comment "`direct-inference' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly)
(block
(script-comment "`direct-inference' at (1)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly)))
(block
(script-comment "`insistent-direct-inference' at (1)")
insistent-direct-inference
direct-and-antecedent-inference-strategy
(contrapose "with(p:prop,forall(a,b:nn,p));")
(cut-with-single-formula "x_$1<x_$2 or x_$2<x_$1")
(move-to-sibling 1)
simplify
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(instantiate-existential ("x_$1" "x_$2"))
(contrapose "with(n:nn,n=n);")
simplify-insistently)
(block
(script-comment "`antecedent-inference' at (1)")
(instantiate-existential ("x_$2" "x_$1"))
(contrapose "with(n:nn,n=n);")
simplify-insistently))))
(weaken (0)))))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
(block
(script-comment "`direct-inference' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "omega%embedding(s)(x_$9) in s")
auto-instantiate-existential
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%membership-in-a-range)
(instantiate-existential ("x_$9" "omega%embedding(s)"))
(apply-macete-with-minor-premises ran-of-omega%embedding)))
(block
(script-comment "`direct-inference' at (1)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "s=ran{omega%embedding(s)}")
(move-to-sibling 1)
(apply-macete-with-minor-premises ran-of-omega%embedding)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(x:nn,s:sets[nn],x in s);")
(backchain "with(f:[nn,nn],s:sets[nn],s=ran{f});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential ("x_$0"))
simplify)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0 0)")
simplify-insistently
(backchain "with(p:prop,forall(a,b:nn,p));")
(block
(script-comment "`backchain' at (0)")
(apply-macete-with-minor-premises strong-monotonicity-of-omega%embedding)
simplify
(cut-with-single-formula "s=ran{omega%embedding(s)}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(force-substitution "s"
"ran{omega%embedding(s)}"
(2 4))
(apply-macete-with-minor-premises tr%membership-in-a-range)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(incorporate-antecedent "with(l_$0:nn,f:sets[nn],l_$0 in f);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(instantiate-existential ("k_$0" "omega%embedding(s)"))
simplify
(apply-macete-with-minor-premises omega%embedding-strong-definedness)
(instantiate-existential ("l_$0"))
simplify)
(instantiate-existential ("l_$0" "omega%embedding(s)")))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises omega%embedding-strong-definedness)
(instantiate-existential ("l_$0"))
simplify))
(apply-macete-with-minor-premises ran-of-omega%embedding))
direct-inference)))
(block
(script-comment "`case-split' at (2)")
(apply-macete-with-minor-premises characterization-of-omega-embedding-for-infinite-sets)
(move-to-sibling 1)
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "f_card{s}<=f_card{image{f,s}}")
(apply-macete-with-minor-premises tr%f-card-leq-iff-finite-and-embeds)
direct-inference
(instantiate-existential ("restrict{f,s}"))
(apply-macete-with-minor-premises tr%domain-of-a-restriction)
(block
(script-comment "`instantiate-existential' at (0 1)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly)
(block
(script-comment "`instantiate-existential' at (0 2)")
(apply-macete-with-minor-premises tr%injective-implies-injective-on)
insistent-direct-inference
direct-and-antecedent-inference-strategy
(contrapose "with(n:nn,n=n);")
(cut-with-single-formula "x_$0<x_$1 or x_$1<x_$0")
(move-to-sibling 1)
simplify
(block
(script-comment "`cut-with-single-formula' at (0)")
(antecedent-inference "with(p:prop,p or p);")
(block
(script-comment "`antecedent-inference' at (0)")
(contrapose "with(p:prop,forall(a,b:nn,p));")
auto-instantiate-existential
(block
(script-comment "`auto-instantiate-existential' at (0 1)")
(contrapose "with(n:nn,n=n);")
simplify-insistently)
(block
(script-comment "`auto-instantiate-existential' at (0 2)")
(contrapose "with(n:nn,n=n);")
simplify-insistently)
(block
(script-comment "`auto-instantiate-existential' at (0 3)")
(contrapose "with(n:nn,n=n);")
simplify-insistently))
(block
(script-comment "`antecedent-inference' at (1)")
(contrapose "with(p:prop,forall(a,b:nn,p));")
auto-instantiate-existential
(block
(script-comment "`auto-instantiate-existential' at (0 1)")
(contrapose "with(n:nn,n=n);")
simplify-insistently)
(block
(script-comment "`auto-instantiate-existential' at (0 2)")
(contrapose "with(n:nn,n=n);")
simplify-insistently)
(block
(script-comment "`auto-instantiate-existential' at (0 3)")
(contrapose "with(n:nn,n=n);")
simplify-insistently)))))
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(apply-macete-with-minor-premises tr%domain-composition)
(move-to-sibling 1)
(apply-macete-with-minor-premises ran-of-omega%embedding)
(apply-macete-with-minor-premises domain-of-omega-embedding-for-infinite-sets))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(apply-macete-with-minor-premises tr%subseteq-antisymmetry)
direct-inference
(block
(script-comment "`direct-inference' at (0)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "omega%embedding(s)(x) in s")
(block
(script-comment "`cut-with-single-formula' at (0)")
auto-instantiate-existential
(instantiate-existential ("omega%embedding(s)(x)")))
(block
(script-comment "`cut-with-single-formula' at (1)")
(apply-macete-with-minor-premises tr%membership-in-a-range)
(instantiate-existential ("x_$2" "omega%embedding(s)"))
(apply-macete-with-minor-premises ran-of-omega%embedding)
(move-to-ancestor 2)
(instantiate-existential ("x" "omega%embedding(s)"))))
(block
(script-comment "`direct-inference' at (1)")
insistent-direct-inference
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(cut-with-single-formula "s=ran{omega%embedding(s)}")
(move-to-sibling 1)
(apply-macete-with-minor-premises ran-of-omega%embedding)
(block
(script-comment "`cut-with-single-formula' at (0)")
(incorporate-antecedent "with(x:nn,s:sets[nn],x in s);")
(backchain "with(f:[nn,nn],s:sets[nn],s=ran{f});")
(apply-macete-with-minor-premises indicator-facts-macete)
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(instantiate-existential ("x_$0"))
simplify)))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (2 0 0
0)")
simplify-insistently
(backchain "with(p:prop,forall(a,b:nn,p));")
(block
(script-comment "`backchain' at (0)")
(apply-macete-with-minor-premises strong-monotonicity-of-omega%embedding)
simplify
(cut-with-single-formula "s=ran{omega%embedding(s)}")
(block
(script-comment "`cut-with-single-formula' at (0)")
(force-substitution "s"
"ran{omega%embedding(s)}"
(2 4))
(apply-macete-with-minor-premises tr%membership-in-a-range)
(block
(script-comment "`apply-macete-with-minor-premises' at (0)")
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0)")
(incorporate-antecedent "with(l:nn,f:sets[nn],l in f);")
simplify-insistently)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (1)")
(instantiate-existential ("k" "omega%embedding(s)"))
simplify
(apply-macete-with-minor-premises omega%embedding-strong-definedness)
(instantiate-existential ("l"))
simplify)
(instantiate-existential ("l" "omega%embedding(s)")))
(block
(script-comment "`apply-macete-with-minor-premises' at (1)")
(apply-macete-with-minor-premises omega%embedding-strong-definedness)
(instantiate-existential ("l"))
simplify))
(apply-macete-with-minor-premises ran-of-omega%embedding))
direct-inference)))
)))