(def-theorem drop-sequence-lemma"forall(s:[nn,ind_1], #(s(0)) and f_seq_q{drop{s,1}} implies f_seq_q{s})"(theory sequences) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"s=cons{s(0),drop{s,1}}") (block (script-comment"`cut-with-single-formula' at (0)") (backchain"with(f,s:[nn,ind_1],s=f);") (apply-macete-with-minor-premises cons-fseq-biconditional)) (apply-macete-with-minor-premises cons-car-cdr-lemma) )))

(def-theorem length-of-drop-one"forall(s:[nn -> ind_1], n:nn, #(s(0)) implies (length{s} <=n+1 iff length{drop{s,1}}<=n))"reverse (usages transportable-macete) (theory sequences) (proof ( direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0)") (apply-macete-with-minor-premises length-of-drop) (case-split-on-conditionals (0))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1)") (cut-with-single-formula"f_seq_q{s}") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises drop-sequence-lemma) direct-inference) (block (script-comment"`cut-with-single-formula' at (0)") (contrapose"with(n:nn,n<=n);") (apply-macete-with-minor-premises length-of-drop) (cut-with-single-formula"0<length{s}") simplify (apply-macete-with-minor-premises meaning-of-length))) ))) (load-section basic-cardinality)

(def-quasi-constructor collapse"lambda(f:[nn,ind_1], lambda(n:nn, f (omega%embedding(dom{f})(n))))"(language sequences) (fixed-theories h-o-real-arithmetic))

(def-theorem length-of-collapse-lemma"forall(s:[nn,ind_1], forall(m:nn, forall(k:nn, m<=k implies not(#(s(k)))) implies length(collapse{s})<=m))"(theory sequences) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"forsome(k:nn, k<=m and dom{omega%embedding(dom{s})}=omega(k))") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises dom-of-omega%embedding-at-finite-set) simplify-insistently direct-and-antecedent-inference-strategy (instantiate-universal-antecedent"with(p:prop,forall(k:nn,p));"("x")) simplify) (block (script-comment"`cut-with-single-formula' at (0)") (antecedent-inference"with(p:prop,forsome(k:nn,p));") (incorporate-antecedent"with(p:prop,p and p);") (unfold-single-defined-constant (0) omega) (force-substitution"dom{omega%embedding(dom{s})}=indic{m:nn, m<k}""forall(p:nn, #(omega%embedding(dom{s})(p)) iff p<k)"(0)) (move-to-sibling 1) (block (script-comment"`force-substitution' at (1)") (force-substitution"p<k""p in indic{m:nn, m<k}"(0)) (move-to-sibling 1) (block (script-comment"`force-substitution' at (1)") (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly) (block (script-comment"`force-substitution' at (0)") direct-inference (backchain-backwards"with(f:sets[nn],f=f);") (apply-macete-with-minor-premises tr%domain-membership-iff-defined))) (block (script-comment"`force-substitution' at (0)") direct-and-antecedent-inference-strategy (cut-with-single-formula"forall(p:nn, #(omega%embedding(dom{s})(p)) iff omega%embedding(dom{s})(p) in ran{omega%embedding(dom{s})})") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises tr%range-domain-membership) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly) (block (script-comment"`cut-with-single-formula' at (0)") (incorporate-antecedent"with(f:sets[nn],n:nn,forall(p:nn,#(n) iff n in f));") (apply-macete-with-minor-premises ran-of-omega%embedding) (force-substitution"#(omega%embedding(dom{s})(p))""p<k"(0)) (move-to-sibling 1) simplify (block (script-comment"`force-substitution' at (0)") (apply-macete-with-minor-premises tr%domain-membership-iff-defined) direct-and-antecedent-inference-strategy (cut-with-single-formula"length{lambda(p:nn, s(omega%embedding(dom{s})(p)))}=k") simplify (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises iota-free-definition-of-length) (incorporate-antecedent"with(i:ind_1,k:nn,forall(p:nn,p<k iff #(i)));") (force-substitution"s(omega%embedding(dom{s})(p))""collapse{s}(p)"(0)) simplify-insistently))))) )))

(def-theorem collapse-of-finite-is-finite-lemma"forall(s:[nn,ind_1], forsome(m:nn, forall(k:nn, m<=k implies not(#(s(k))))) implies f_seq_q{collapse{s}})"(theory sequences) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"length{collapse{s}}<=m") (apply-macete-with-minor-premises length-of-collapse-lemma) )))

(def-quasi-constructor constrict"lambda(f:[nn,ind_1],a:sets[ind_1], collapse(lambda(n:nn, if(f(n) in a, f(n), ?ind_1))))"(language sequences) (fixed-theories h-o-real-arithmetic))

(def-theorem length-of-constrict-of-finite-sequence"forall(s:[nn,ind_1],a:sets[ind_1], f_seq_q{s} implies length{constrict{s,a}}<=length{s})"(theory sequences) (usages transportable-macete) (proof ( (apply-macete-with-minor-premises length-of-collapse-lemma) beta-reduce-repeatedly direct-and-antecedent-inference-strategy (cut-with-single-formula"not(#(s(k)))") simplify (block (script-comment"node added by `cut-with-single-formula' at (1)") (apply-macete-with-minor-premises meaning-of-length-rev) simplify) )))

(def-theorem constrict-of-finite-sequence-is-finite-sequence"forall(s:[nn,ind_1],a:sets[ind_1], f_seq_q{s} implies f_seq_q{constrict{s,a}})"(theory sequences) (usages transportable-macete) (proof ( direct-and-antecedent-inference-strategy (cut-with-single-formula"length{constrict{s,a}}<=length{s}") (apply-macete-with-minor-premises length-of-constrict-of-finite-sequence) )))

(def-theorem omega%embedding-id-condition"forall(s:sets[nn], omega%embedding(s)=id{s} iff (s=sort_to_indic{nn} or forsome(n:nn, s=omega(n))))"(theory h-o-real-arithmetic) (proof ( direct-inference (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) (apply-macete-with-minor-premises tr%ran-of-id) (apply-macete-with-minor-premises tr%dom-of-id) simplify direct-and-antecedent-inference-strategy auto-instantiate-existential (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 0)") (contrapose"with(s:sets[nn],f_indic_q{s});") (apply-macete-with-minor-premises subset-of-nn-finite-iff-bounded) (contrapose"with(p:prop,not(p));") (antecedent-inference"with(p:prop,forsome(n:nn,p));") (contrapose"with(f,s:sets[nn],s subseteq f);") (unfold-single-defined-constant (0) omega) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly (backchain"with(f,s:sets[nn],s=f);") (instantiate-existential ("n+1")) simplify simplify) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 1 0)") (backchain"with(f,s:sets[nn],s=f);") (backchain"with(f,s:sets[nn],s=f);") (apply-macete-with-minor-premises f-card-of-a-finite-cardinal)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 1 0 0 0 0 0)") (backchain"with(s:sets[nn],s=sort_to_indic{nn});") (apply-macete-with-minor-premises tr%meaning-of-indic-from-sort-element)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 1 0 0 0 0 1 0)") (backchain"with(n:nn,s:sets[nn],s=omega(n));") (incorporate-antecedent"with(l:nn,s:sets[nn],l in s);") (backchain"with(n:nn,s:sets[nn],s=omega(n));") (unfold-single-defined-constant-globally omega) (apply-macete-with-minor-premises indicator-facts-macete) beta-reduce-repeatedly simplify)) (block (script-comment"`case-split' at (2)") (apply-macete-with-minor-premises characterization-of-omega-embedding-for-infinite-sets) (apply-macete-with-minor-premises tr%ran-of-id) (apply-macete-with-minor-premises tr%dom-of-id) simplify direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 0 1 0)") (contrapose"with(p:prop,not(p));") (backchain"with(f,s:sets[nn],s=f);") (apply-macete-with-minor-premises finite-cardinal-is-f-indic)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (1 1 0 0 0 0 0)") (backchain"with(f,s:sets[nn],s=f);") (apply-macete-with-minor-premises tr%meaning-of-indic-from-sort-element)) (backchain"with(s:sets[nn],s=sort_to_indic{nn});")))))

(def-theorem collapse-invariance-condition"forall(s:[nn -> ind_1], (dom{s}=sort_to_indic{nn} or f_seq_q{s}) implies collapse{s}=s)"(theory sequences) (proof ( direct-and-antecedent-inference-strategy (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 0)") extensionality simplify (cut-with-single-formula"omega%embedding(dom{s})=id{dom{s}}") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises omega%embedding-id-condition) direct-and-antecedent-inference-strategy) (block (script-comment"`cut-with-single-formula' at (0)") (backchain"with(f:[nn,nn],f=f);") simplify)) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 0 1)") extensionality simplify (cut-with-single-formula"omega%embedding(dom{s})=id{dom{s}}") (move-to-sibling 1) (block (script-comment"`cut-with-single-formula' at (1)") (apply-macete-with-minor-premises omega%embedding-id-condition) direct-and-antecedent-inference-strategy (instantiate-existential ("length{s}")) (unfold-single-defined-constant (0) omega) (apply-macete-with-minor-premises meaning-of-length)) (block (script-comment"`cut-with-single-formula' at (0)") (backchain"with(f:[nn,nn],f=f);") simplify)) )))