(def-language sequences-language
(embedded-language h-o-real-arithmetic)
(base-types ind_1))
(def-theory sequences
(language sequences-language)
(component-theories h-o-real-arithmetic))
(def-quasi-constructor length
"lambda(s:[nn,ind_1],
iota(n:nn,
forall(m:nn, m<n iff #(s(m)))))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor f-seq?
"lambda(s:[nn,ind_1], #(length(s)))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor nil
"lambda(e:ind_1, lambda(n:nn, ?ind_1))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor cons
"lambda(e:ind_1, s:[nn,ind_1], lambda(n:nn, if(n<1, e, s(n-1))))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor drop
"lambda(s:[nn,ind_1], n:ind, lambda(m:nn, if(#(n,nn), s(n+m), ?ind_1)))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor takefirst
"lambda(s:[nn,ind_1], n:ind,
lambda(m:nn, if(m<n, s(m), ?ind_1)))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor append
"lambda(s_1,s_2:[nn,ind_1],
lambda(m:nn, if(length(s_1)<=m, s_2(m-length(s_1)), s_1(m))))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-quasi-constructor in_seq
"lambda(x:ind_1, s_1:[nn,ind_1],
forsome(i:nn, s_1(i)=x))"
(language sequences)
(fixed-theories h-o-real-arithmetic))
(def-theorem meaning-of-zero
"forall([[[z],nn]], forall([[[x],nn]], not(x<z)) iff z=0)"
(theory h-o-real-arithmetic)
(proof
(direct-and-antecedent-inference-strategy
(contrapose "with(z:nn,forall(x:nn,not(x<z)));")
(instantiate-existential ("0"))
simplify
simplify)))
(def-theorem iota-free-definition-of-length
"forall([[[n],nn],[[s],[nn,ind_1]]], length(s) = n iff
forall([[[m],nn]], m < n iff #(s(m))))"
(theory sequences)
(usages transportable-macete)
(proof
(
(disable-quasi-constructor length)
direct-and-antecedent-inference-strategy
(contrapose "with(n:nn,s:[nn,ind_1],
iota(n:nn,forall(m:nn,m<n iff #(s(m))))=n);")
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(s:[nn,ind_1],n:nn,forall(m:nn,m<n iff #(s(m))));" ("m"))
(contrapose "with(n:nn,s:[nn,ind_1],
iota(n:nn,forall(m:nn,m<n iff #(s(m))))=n);")
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify
direct-and-antecedent-inference-strategy
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(s:[nn,ind_1],n:nn,forall(m:nn,m<n iff #(s(m))));" ("m"))
(apply-macete-with-minor-premises eliminate-iota-macete)
simplify
direct-and-antecedent-inference-strategy
(instantiate-theorem trichotomy ("b" "n"))
(instantiate-universal-antecedent "with(s:[nn,ind_1],b:nn,forall(m:nn,m<b iff #(s(m))));" ("n"))
(instantiate-universal-antecedent "with(s:[nn,ind_1],n:nn,forall(m:nn,m<n iff #(s(m))));" ("n"))
simplify
(instantiate-universal-antecedent "with(s:[nn,ind_1],n:nn,forall(m:nn,m<n iff #(s(m))));" ("b"))
(auto-instantiate-universal-antecedent "with(s:[nn,ind_1],b:nn,forall(m:nn,m<b iff #(s(m))));")
(instantiate-universal-antecedent "with(s:[nn,ind_1],b:nn,forall(m:nn,m<b iff #(s(m))));" ("b"))
simplify)))
(def-theorem meaning-of-length
"forall([[[k],nn],[[s],[nn,ind_1]]], f_seq_q(s) implies
k<length(s) iff #(s(k)))"
(theory sequences)
(usages transportable-macete)
(proof
(direct-inference
direct-inference
(instantiate-theorem iota-free-definition-of-length ("length(s)" "s"))
(backchain "with(s:[nn,ind_1],forall(m:nn,m<length{s} iff #(s(m))));"))))
(def-theorem meaning-of-length-rev
"forall([[[k],nn],[[s],[nn,ind_1]]], f_seq_q(s) implies
#(s(k)) iff k<length(s))"
(theory sequences)
(usages transportable-macete)
(proof
(direct-inference
(instantiate-theorem meaning-of-length ("k" "s"))
simplify
simplify
simplify)))
(def-theorem iota-free-definition-of-length-conv
"forall([[[n],nn],[[s],[nn,ind_1]]], forall([[[m],nn]], m < n iff #(s(m))) iff
length(s) = n)"
(theory sequences)
(usages transportable-macete)
(proof
((assume-theorem iota-free-definition-of-length)
simplify)))
(def-theorem sequence-defined-up-to-length
"forall(s_1:[nn,ind_1],m:nn,
m<length(s_1)
implies
#(s_1(m)))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises meaning-of-length-rev))))
(def-theorem length-characterizes-definedness
"forall([[[s],[nn,ind_1]]], #(length(s)) implies
forall([[[m],nn]], m < length(s) iff #(s(m))))"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises meaning-of-length))))
(def-theorem sequence-not-defined-at-length
"forall([[[s],[nn,ind_1]]], not(#(s(length(s)))))"
(theory sequences)
(usages transportable-macete)
(proof
(direct-and-antecedent-inference-strategy
(case-split ("f_seq_q{s}"))
(apply-macete-with-minor-premises meaning-of-length-rev)
simplify
simplify)))
(def-theorem sequences-same-length-same-domain
"forall(s_1,s_2:[nn,ind_1],
f_seq_q(s_1) and f_seq_q(s_2)
implies
forall(m:nn, #(s_1(m)) iff #(s_2(m)))
iff
length(s_1)=length(s_2))"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises iota-free-definition-of-length)
(apply-macete-with-minor-premises meaning-of-length-rev)
direct-and-antecedent-inference-strategy-with-simplification)))
(def-theorem length-existence-implies-uniqueness
"forall(t:[nn,ind_1],
forall(i:nn,
forall(m:nn,m<i iff #(t(m)))
implies
forall(j:nn,forall(m:nn,m<j iff #(t(m))) implies j=i)))"
(theory sequences)
(proof
(direct-and-antecedent-inference-strategy
(instantiate-theorem trichotomy ("i" "j"))
(instantiate-universal-antecedent
"with(t:[nn,ind_1],i:nn,forall(m:nn,m<i iff #(t(m))));" ("j"))
(instantiate-universal-antecedent
"with(t:[nn,ind_1],j:nn,forall(m:nn,m<j iff #(t(m))));" ("j"))
simplify
(instantiate-universal-antecedent
"with(t:[nn,ind_1],j:nn,forall(m:nn,m<j iff #(t(m))));" ("i"))
(instantiate-universal-antecedent
"with(t:[nn,ind_1],i:nn,forall(m:nn,m<i iff #(t(m))));" ("i"))
simplify)))
(def-theorem length-non-negative
Remark: This entry is multiply defined. See: [1] [2]
"forall(s:[nn,ind_1], f_seq_q{s} implies 0<=length{s})"
(theory sequences)
(usages transportable-macete)
(proof (simplify-insistently)))
(def-theorem sequence-defined-monotonically
"forall(s:[nn,ind_1], m,n:nn, f_seq_q{s} and m<=n and #(s(n)) implies #(s(m)))"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises sequence-defined-up-to-length)
(apply-macete-with-minor-premises meaning-of-length-rev)
direct-and-antecedent-inference-strategy
simplify)))
(def-theorem f_seq_q-characterization
"forall(s:[nn->ind_1],
f_seq_q{s}
iff
(forall(i,j:nn, i<j and #(s(j)) implies #(s(i)))
and forsome(k:nn, not(#(s(k))))))"
(theory sequences)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 0 0 0 0)")
(apply-macete-with-minor-premises sequence-defined-monotonically)
auto-instantiate-existential
simplify)
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0 1)")
(instantiate-existential ("length{s}"))
(apply-macete-with-minor-premises sequence-not-defined-at-length))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1 0 0)")
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "forall(m:zz, 0<=m implies #(s(m)))")
simplify
(block
(script-comment "`cut-with-single-formula' at (1)")
(induction integer-inductor ("m"))
(block
(script-comment "`induction' at (0 0 0)")
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "length{s}=0")
(apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
direct-inference
(case-split ("0<m"))
(auto-instantiate-universal-antecedent "with(s:[nn,ind_1],
forall(i,j:nn,i<j and #(s(j)) implies #(s(i))));")
(block
(script-comment "`case-split' at (2)")
simplify
(cut-with-single-formula "0=m")
simplify
simplify))
(block
(script-comment "`induction' at (0 1 0 0 0 0)")
(contrapose "with(p:prop,not(p));")
(cut-with-single-formula "length{s}=1+t")
(apply-macete-with-minor-premises iota-free-definition-of-length)
direct-and-antecedent-inference-strategy
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 0)")
(case-split ("m=t"))
simplify
(block
(script-comment "`case-split' at (2)")
(instantiate-universal-antecedent "with(p:prop,forall(i,j:nn,p));"
("m" "t"))
(contrapose "with(t:zz,m:nn,not(m<t));")
simplify))
(block
(script-comment "`direct-and-antecedent-inference-strategy' at (0 1)")
(contrapose "with(p:prop,not(p));")
(case-split ("(m=1+t)"))
simplify
(block
(script-comment "`case-split' at (2)")
(instantiate-universal-antecedent "with(p:prop,forall(i,j:nn,p));"
("1+t" "m"))
(contrapose "with(m:nn,t:zz,not(1+t<m));")
simplify))))))))
(transportable-rewrite-usage-simplog1st
(def-theorem length-of-nil
"length(nil(ind_1)) = 0"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (simplify-insistently
(eliminate-iota 0)
(instantiate-existential ("0"))
simplify
(instantiate-universal-antecedent
"with(z%iota:nn,forall(m_$0:nn,not(m_$0<z%iota)));" ("0"))
simplify))))
(transportable-rewrite-usage-simplog1st
(def-theorem length-0-iff-nil
"forall(s:[nn,ind_1], length(s) = 0 iff s=nil(ind_1))"
reverse
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof ((apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
direct-and-antecedent-inference-strategy
extensionality
simplify
simplify
))))
(def-theorem length-0-implies-nil
"forall(s:[nn,ind_1], length(s) = 0 implies s=nil(ind_1))"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises length-0-iff-nil))))
(def-theorem nil-is-fseq
"f_seq_q(nil(ind_1))"
(theory sequences)
(usages transportable-macete)
(proof ((assume-theorem length-0-iff-nil)
simplify)))
(def-theorem non-nil-fseq-defined-at-0
"forall(s:[nn,ind_1], f_seq_q(s) and not(s=nil{ind_1}) implies #(s(0)))"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises meaning-of-length-rev)
direct-and-antecedent-inference-strategy
(instantiate-theorem length-0-implies-nil ("s"))
simplify)))
(transportable-rewrite-usage-simplog1st
(def-theorem car-of-cons
"forall([[[x],ind_1],[[s],[nn,ind_1]]], cons(x,s)(0) = x)"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (simplify))))
(transportable-rewrite-usage-simplog1st
(def-theorem cdr-of-cons
"forall([[[x],ind_1],[[s],[nn,ind_1]]], drop(cons(x,s),1) = s)"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (simplify-insistently
(apply-macete-with-minor-premises tr%unary-eta-reduction)))))
(def-theorem length-of-cons
"forall(x:ind_1,s:[nn,ind_1],
f_seq_q{s} implies length{cons{x,s}}=length{s}+1)"
(theory sequences)
(usages transportable-macete)
(proof
(
(apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
(apply-macete-with-minor-premises meaning-of-length-rev)
simplify
direct-and-antecedent-inference-strategy
(cut-with-single-formula "0<=length{s}")
simplify
(apply-macete-with-minor-premises length-non-negative)
)))
(def-theorem cons-is-fseq
"forall(x:ind_1,s:[nn,ind_1],
f_seq_q{s} implies f_seq_q{cons{x,s}})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem length-of-cons ("x" "s")))))
(def-theorem length-of-pre-cons
"forall(x:ind_1,s:[nn,ind_1],
f_seq_q{cons{x,s}} implies length{s}=length{cons{x,s}}-1)"
(theory sequences)
(usages transportable-macete)
(proof
((apply-macete-with-minor-premises iota-free-definition-of-length)
direct-and-antecedent-inference-strategy
(incorporate-antecedent "with(s:[nn,ind_1],x:ind_1,m:nn,m<length{cons{x,s}}-1);")
simplify
(apply-macete-with-minor-premises length-characterizes-definedness)
simplify
simplify
(apply-macete-with-minor-premises meaning-of-length)
(cut-with-single-formula "0<length{cons{x,s}}")
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
(apply-macete-with-minor-premises meaning-of-length)
simplify)))
(def-theorem cons-fseq-implies-fseq
"forall(x:ind_1,s:[nn,ind_1],
f_seq_q{cons{x,s}} implies f_seq_q{s})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem length-of-pre-cons ("x" "s")))))
(transportable-rewrite-usage-simplog1st
(def-theorem length-of-cons-rew ; proof (no history)
"forall(x:ind_1,s:[nn,ind_1],length{cons{x,s}}==length{s}+1)"
(theory sequences)
(usages transportable-rewrite)
(proof (insistent-direct-inference-strategy
(antecedent-inference
"with(s:[nn,ind_1],x:ind_1, f_seq_q{cons{x,s}} or #(length{s}+1));")
(instantiate-theorem length-of-pre-cons ("x" "s"))
simplify
(apply-macete-with-minor-premises length-of-cons)))))
(def-theorem length-of-cons-alt-1
"forall(s:[nn,ind_1],x:ind_1,
f_seq_q{cons{x,s}}
implies
length{s}=length{cons{x,s}}-1);"
(theory sequences)
(usages )
(proof ((apply-macete-with-minor-premises length-of-pre-cons)
simplify
(apply-macete-with-minor-premises cons-fseq-implies-fseq))))
(def-theorem length-of-cons-alt
"forall(x:ind_1,s:[nn,ind_1],
f_seq_q{cons{x,s}} implies length{cons{x,s}}=length{s}+1)"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem length-of-pre-cons ("x" "s"))
simplify)))
(transportable-rewrite-usage-simplog1st
(def-theorem cons-fseq-biconditional
"forall(x:ind_1,s:[nn,ind_1],
f_seq_q{cons{x,s}} iff f_seq_q{s});"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises cons-fseq-implies-fseq)
auto-instantiate-existential
(apply-macete-with-minor-premises cons-is-fseq)))))
(def-theorem cons-to-nil-is-fseq
"forall(e:ind_1,f_seq_q{cons{e,nil{ind_1}}})"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises cons-is-fseq)
(apply-macete-with-minor-premises nil-is-fseq))))
(transportable-rewrite-usage-simplog1st
(def-theorem cons-non-nil-2
"forall(e:ind_1,s:[nn,ind_1], not(cons(e,s)=nil{ind_1}))"
(theory sequences)
(usages transportable-rewrite transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
(instantiate-existential ("0"))
simplify))))
(transportable-rewrite-usage-simplog1st
(def-theorem take-none
"forall(s:[nn,ind_1], takefirst(s,0) = nil(ind_1))"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify))))
(def-theorem take-all
"forall(s:[nn,ind_1], f_seq_q(s) implies
takefirst(s,length(s)) = s)"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises meaning-of-length-rev))))
(def-theorem length-of-takefirst
"forall(s:[nn,ind_1],k:nn, f_seq_q(s) implies
length(takefirst(s,k)) = if(k<=length(s),k,length(s)))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises sequence-defined-up-to-length)
simplify
(apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises sequence-defined-up-to-length)
(apply-macete-with-minor-premises length-characterizes-definedness))))
(def-theorem takefirst-is-fseq
"forall(s:[nn,ind_1],k:nn, f_seq_q(s) implies
f_seq_q(takefirst(s,k)))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem length-of-takefirst ("s" "k")))))
(transportable-rewrite-usage-simplog1st
(def-theorem drop-none
"forall(s:[nn,ind_1], drop(s,0) = s)"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (simplify-insistently
(apply-macete-with-minor-premises tr%unary-eta-reduction)))))
(def-theorem drop-all-or-more
"forall([[[m],nn],[[s],[nn,ind_1]]], (f_seq_q(s) and length(s)<=m) implies
drop(s,m) = nil(ind_1))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify
(apply-macete-with-minor-premises meaning-of-length-rev)
simplify)))
(def-theorem drop-all
"forall(s:[nn,ind_1],
f_seq_q{s} implies drop{s,length{s}}=nil{ind_1})"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises drop-all-or-more)
direct-and-antecedent-inference-strategy)))
(def-theorem length-of-drop
"forall(s:[nn,ind_1],k:nn,
f_seq_q{s}
implies
length{drop{s,k}}=if(k<=length{s}, length{s}-k, 0));"
(theory sequences)
(usages transportable-macete)
(proof
(direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(force-substitution "k+length{drop{s,k}}=length{s}" "length{drop{s,k}}=length{s}-k" (0))
(apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
(apply-macete-with-minor-premises length-characterizes-definedness)
direct-inference
simplify
(apply-macete-with-minor-premises drop-all-or-more)
(apply-macete-with-minor-premises length-of-nil))))
(def-theorem drop-is-fseq
"forall(s:[nn,ind_1],k:nn,
f_seq_q{s} implies f_seq_q{drop{s,k}})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem length-of-drop ("s" "k")))))
(def-theorem cons-car-cdr-lemma
"forall(s:[nn,ind_1], #(s(0)) implies cons{s(0),drop{s,1}}=s)"
(theory sequences)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
extensionality
beta-reduce-repeatedly
direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(cut-with-single-formula "x_0=0")
simplify
)))
(def-theorem cons-car-cdr
"forall(s:[nn,ind_1],
1<=length(s)
implies
cons(s(0),drop(s,1))=s)"
(theory sequences)
(usages transportable-macete)
(proof
(
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises cons-car-cdr-lemma)
(apply-macete-with-minor-premises sequence-defined-up-to-length)
simplify
)))
(def-theorem existential-cons-car-cdr
"forall(s:[nn,ind_1], 0<length{s}
implies
forsome(i:ind_1, s_1:[nn,ind_1], s=cons(i,s_1)))"
(theory sequences)
(usages )
(proof (direct-and-antecedent-inference-strategy
(instantiate-existential ("s(0)" "drop{s,1}"))
(apply-macete-with-minor-premises cons-car-cdr)
(apply-macete-with-minor-premises sequence-defined-up-to-length))))
(def-theorem drop-cons
"forall(s:[nn,ind_1], n:nn, e:ind_1,
1<=n implies
drop{cons(e,s),n}=drop{s,n-1})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
direct-and-antecedent-inference-strategy
simplify
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify)))
(def-compound-macete drop-cons-and-simplify
(series
(repeat (without-minor-premises tr%drop-cons))
simplify))
(def-theorem drop-from-nil
"forall(n:nn, drop{nil{ind_1},n}=nil{ind_1})"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof ((apply-macete-with-minor-premises drop-all-or-more)
(apply-macete-with-minor-premises length-of-nil)
simplify
simplify)))
(def-theorem takefirst-of-cons
"forall(a:ind_1, s:[nn,ind_1], n:nn,
0<n implies takefirst{cons{a,s},n} = cons{a,takefirst{s,n-1}})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify-with-minor-premises
direct-inference
(case-split-on-conditionals (1))
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify)))
(def-theorem takefirst-of-append-at-length
"forall(s,t:[nn,ind_1], f_seq_q(s) implies
takefirst(append(s,t),length(s)) = s)"
(theory sequences)
(usages transportable-macete)
(proof (
direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises meaning-of-length-rev)
)))
(def-theorem takefirst-of-append
"forall(s,t:[nn,ind_1], n:nn, length{s}<n implies
takefirst{append{s,t},n} = append{s,takefirst{t,n-length{s}}})"
(theory sequences)
(usages transportable-macete)
(proof (
direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(case-split-on-conditionals (0))
insistent-direct-and-antecedent-inference-strategy
simplify
simplify)))
(def-theorem drop-of-append
"forall(s,t:[nn,ind_1],
f_seq_q{s} implies drop{append{s,t},length{s}}=t)"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify)))
(def-theorem drop-some-from-append
"forall(s_0,s_1:[nn,ind_1], m:nn,
m<=length{s_0}
implies
drop{append{s_0,s_1},m}=append{drop{s_0,m},s_1})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises length-of-drop)
simplify)))
(def-theorem length-of-append
"forall(s,t:[nn,ind_1],
f_seq_q{s} and f_seq_q{t}
implies
length{append{s,t}}=length{s}+length{t})"
(theory sequences)
(usages transportable-macete)
(proof
((apply-macete-with-minor-premises iota-free-definition-of-length)
simplify
direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises sequence-defined-up-to-length)
simplify
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify
(apply-macete-with-minor-premises sequence-defined-up-to-length)
simplify
(incorporate-antecedent
"with(t:[nn,ind_1],m:nn,s:[nn,ind_1],
#(if(length{s}<=m, t(m+[-1]*length{s}), s(m))));")
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises meaning-of-length-rev)
simplify
(apply-macete-with-minor-premises nn-defining-axiom_h-o-real-arithmetic)
simplify)))
(def-theorem infinite-append
"forall(s,t:[nn,ind_1],not(f_seq_q{s}) implies append{s,t}=s)"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(cut-with-single-formula "not(length{s}<=x_0)")
simplify
simplify)))
(def-theorem append-is-fseq
"forall(s,t:[nn,ind_1],
f_seq_q{s} and f_seq_q{t} implies f_seq_q{append{s,t}})"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem length-of-append ("s" "t")))))
(def-theorem append-shifts-second-arg
"forall(s,t:[nn,ind_1],
#(length(s))
implies
forall(m:nn,
length(s)<=m
implies
append(s,t)(m)==t(m-length(s))))"
(theory sequences)
(proof (simplify)))
(def-theorem append-fseq-implies-first-fseq
"forall(s,t:[nn,ind_1],
f_seq_q{append{s,t}} implies f_seq_q{s})"
(theory sequences)
(proof (direct-and-antecedent-inference-strategy
(contrapose "with(t,s:[nn,ind_1],f_seq_q{append{s,t}});")
(apply-macete-with-minor-premises infinite-append)
)))
(def-theorem append-fseq-implies-second-fseq
"forall(s,t:[nn,ind_1],
f_seq_q{append{s,t}} implies f_seq_q{t})"
(theory sequences)
(proof (direct-and-antecedent-inference-strategy
(force-substitution "t" "drop{append{s,t},length{s}}" (0))
(apply-macete-with-minor-premises drop-is-fseq)
(apply-macete-with-minor-premises append-fseq-implies-first-fseq)
auto-instantiate-existential
(apply-macete-with-minor-premises drop-of-append))))
(def-theorem append-fseq-macete ; ;; short proof
"forall(s,t:[nn,ind_1],
f_seq_q{append{s,t}} iff (f_seq_q{s} and f_seq_q{t}))"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises append-fseq-implies-first-fseq)
auto-instantiate-existential
(apply-macete-with-minor-premises append-fseq-implies-second-fseq)
auto-instantiate-existential
(apply-macete-with-minor-premises append-is-fseq)
simplify)))
(def-theorem length-of-append-quasi-eq
"forall(x,y:[nn,ind_1],
length{append{x,y}}==length{x}+length{y})"
(theory sequences)
(usages transportable-macete)
(proof (insistent-direct-inference-strategy
(antecedent-inference "with(y,x:[nn,ind_1],
f_seq_q{append{x,y}} or #(length{x}+length{y}));")
(apply-macete-with-minor-premises length-of-append)
simplify
(instantiate-theorem append-fseq-macete ("x" "y"))
(apply-macete-with-minor-premises append-fseq-implies-second-fseq)
auto-instantiate-existential
(apply-macete-with-minor-premises append-fseq-implies-first-fseq)
auto-instantiate-existential
(apply-macete-with-minor-premises length-of-append))))
(transportable-rewrite-usage-simplog1st
(def-theorem append-nil ; proof ( history)
"forall(s:[nn,ind_1], append(nil(ind_1),s)=s)"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify
(apply-macete-with-minor-premises length-of-nil)
simplify))))
(transportable-rewrite-usage-simplog1st
(def-theorem append-nil-right
"forall(s:[nn,ind_1], append(s,nil(ind_1))=s)"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
extensionality
simplify
direct-and-antecedent-inference-strategy
(case-split-on-conditionals (0))
(apply-macete-with-minor-premises meaning-of-length-rev)
simplify))))
(def-theorem append-is-nil-implies-left-is-nil ; proof ( history)
"forall(s_0,s_1:[nn,ind_1], append(s_0,s_1)=nil(ind_1) implies s_0=nil(ind_1))"
(theory sequences)
(usages transportable-macete)
(proof
((force-substitution "s_0=nil{ind_1}" "length{s_0}=0" (0))
(force-substitution "append{s_0,s_1}=nil{ind_1}" "length{append{s_0,s_1}}=0" (0))
direct-and-antecedent-inference-strategy
(case-split ("f_seq_q{append{s_0,s_1}}"))
(cut-with-single-formula "length{s_0}<=length{append{s_0,s_1}}")
simplify
(apply-macete-with-minor-premises length-of-append)
(instantiate-theorem length-non-negative ("s_1"))
(contrapose "with(s_1:[nn,ind_1],not(f_seq_q{s_1}));")
(weaken (0 2))
(apply-macete-with-minor-premises append-fseq-implies-second-fseq)
auto-instantiate-existential
simplify
(weaken (0 2))
(apply-macete-with-minor-premises append-fseq-implies-first-fseq)
auto-instantiate-existential
(weaken (1))
(weaken (1))
(apply-macete-with-minor-premises length-0-iff-nil)
(apply-macete-with-minor-premises length-0-iff-nil))))
(def-theorem append-cons-not-fseq
"forall(t,u:[nn,ind_1],e:ind_1,
not(f_seq_q{t})
implies
append{cons{e,t},u}=cons{e,append{t,u}})"
(theory sequences)
(usages )
(proof ((apply-macete-with-minor-premises infinite-append)
(apply-macete-with-minor-premises cons-fseq-biconditional))))
(def-theorem append-cons
"forall(t,u:[nn,ind_1],e:ind_1,
append{cons{e,t},u}=cons{e,append{t,u}})"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
(case-split ("f_seq_q{t}"))
(apply-macete-with-minor-premises append-cons-fseq)
(apply-macete-with-minor-premises append-cons-not-fseq)
)))
(def-theorem cons-append
"forall(t,u:[nn,ind_1],e:ind_1,
cons{e,append{t,u}}=append{cons{e,t},u})"
(theory sequences)
(usages transportable-macete)
(proof ((apply-macete-with-minor-premises append-cons))))
(def-theorem last-of-append-single
"forall(s:[nn,ind_1],s_f:ind_1,
f_seq_q{s}
implies
append{s,seq{s_f,ind_1}}(length{append{s,seq{s_f,ind_1}}}-1)=s_f)"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(apply-macete-with-minor-premises length-of-append)
(apply-macete-with-minor-premises length-of-cons)
(apply-macete-with-minor-premises length-of-nil)
(apply-macete-with-minor-premises append-shifts-second-arg)
simplify
(apply-macete-with-minor-premises nil-is-fseq)
(apply-macete-with-minor-premises nil-is-fseq)
(apply-macete-with-minor-premises cons-to-nil-is-fseq))))
(def-theorem append-agrees-with-first-below-length
"forall(s_0,s_1:[nn,ind_1],i:nn, i<length{s_0} implies append{s_0,s_1}(i)=s_0(i))"
(theory sequences)
(usages transportable-macete)
(proof (beta-reduce-with-minor-premises
simplify
(apply-macete-with-minor-premises sequence-defined-up-to-length))))
(def-theorem sequence-induction
"forall(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],
f_seq_q(s) implies p(s))
iff
(p(nil(ind_1))
and
forall(s:[nn,ind_1], e:ind_1,
f_seq_q(s) and p(s) implies p(cons{e,s}))))"
(theory sequences)
(usages transportable-macete)
(proof
(direct-inference
direct-inference
direct-and-antecedent-inference-strategy
(backchain "with(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],f_seq_q{s} implies p(s)));")
(apply-macete-with-minor-premises nil-is-fseq)
(backchain "with(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],f_seq_q{s} implies p(s)));")
(apply-macete-with-minor-premises cons-is-fseq)
(cut-with-single-formula "forall(j:zz, 0<=j implies forall(s:[nn,ind_1], length{s}<=j implies p(s)))")
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent "with(p:[[nn,ind_1],prop],
forall(j:zz,
0<=j
implies
forall(s:[nn,ind_1],length{s}<=j implies p(s))));" ("length{s}"))
(contrapose "with(s:[nn,ind_1],not(0<=length{s}));")
(apply-macete-with-minor-premises length-non-negative)
(instantiate-universal-antecedent "with(p:[[nn,ind_1],prop],s:[nn,ind_1],
forall(s_$0:[nn,ind_1],
length{s_$0}<=length{s} implies p(s_$0)));" ("s"))
(contrapose "with(s:[nn,ind_1],not(length{s}<=length{s}));")
simplify
(induction integer-inductor ("j"))
direct-and-antecedent-inference-strategy
(cut-with-single-formula "s=nil{ind_1}")
simplify
(instantiate-theorem length-non-negative ("s"))
(instantiate-theorem length-0-implies-nil ("s"))
(contrapose "with(s:[nn,ind_1],not(length{s}=0));")
simplify
(case-split ("length{s}=1+t"))
(instantiate-theorem existential-cons-car-cdr ("s"))
(contrapose "with(s:[nn,ind_1],not(0<length{s}));")
simplify
(cut-with-single-formula "length{s_1}=t")
(instantiate-universal-antecedent "with(p:[[nn,ind_1],prop],t:zz,
forall(s:[nn,ind_1],length{s}<=t implies p(s)));" ("s_1"))
(contrapose "with(t:zz,s_1:[nn,ind_1],not(length{s_1}<=t));")
simplify
(backchain "with(s_1:[nn,ind_1],i:ind_1,s:[nn,ind_1],s=cons{i,s_1});")
(backchain "with(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],e:ind_1,
f_seq_q{s} and p(s) implies p(cons{e,s})));")
simplify
(incorporate-antecedent "with(t:zz,s:[nn,ind_1],length{s}=1+t);")
(backchain "with(s_1:[nn,ind_1],i:ind_1,s:[nn,ind_1],s=cons{i,s_1});")
(apply-macete-with-minor-premises length-of-cons)
simplify
(apply-macete-with-minor-premises cons-fseq-implies-fseq)
(instantiate-existential ("i"))
simplify
(backchain "with(p:[[nn,ind_1],prop],t:zz, forall(s:[nn,ind_1],length{s}<=t implies p(s)));")
simplify)))
(def-inductor sequence-inductor
sequence-induction
(theory sequences)
(base-case-hook simplify))
(transportable-rewrite-usage-simplog1st
(def-theorem associativity-of-append
"forall(s,t,u:[nn,ind_1],
append{append{s,t},u}=append{s,append{t,u}})"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
(case-split ("f_seq_q{s}"))
(block (script-comment "main case: first arg is finite.")
(let-macete
append-macete
(series (repeat append-nil append-cons) simplify))
(label-node main-case)
(induction sequence-inductor ())
(jump-to-node main-case)
(for-nodes
(unsupported-descendents)
(apply-macete-with-minor-premises $append-macete)))
(block (script-comment "supplementary case: first arg infinite.")
(let-macete inf-app-repeat
(repeat infinite-append))
(apply-macete-with-minor-premises $inf-app-repeat)
(contrapose "with(s:[nn,ind_1],not(f_seq_q{s}));")
(apply-macete-with-minor-premises append-fseq-implies-first-fseq)
auto-instantiate-existential)))))
(def-theorem sequence-cases
"forall(s:[nn,ind_1],
f_seq_q{s}
implies
(s=nil{ind_1}
or
forsome(x:ind_1, s_0:[nn,ind_1], s=cons{x,s_0} and f_seq_q{s_0}))) "
(theory sequences)
(usages transportable-macete)
(proof ((induction sequence-inductor ("s"))
direct-and-antecedent-inference-strategy
(instantiate-existential ("s"))
(instantiate-existential ("e")))))
(def-theorem sequence-cases-on-right
"forall(s:[nn,ind_1], s=nil{ind_1} or
forsome(e:ind_1, s_1:[nn,ind_1], s=append{s_1,cons{e,nil{ind_1}}}))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(case-split ("f_seq_q{s}"))
(induction sequence-inductor ("s"))
(antecedent-inference "with(s:[nn,ind_1],
not(s=nil{ind_1})
implies
forsome(e:ind_1,s_1:[nn,ind_1],
s=append{s_1,seq{e,ind_1}}));")
(instantiate-existential ("e" "nil{ind_1}"))
(apply-macete-with-minor-premises append-nil)
(backchain "with(s:[nn,ind_1],s=nil{ind_1});")
(antecedent-inference "with(s:[nn,ind_1],
forsome(e:ind_1,s_1:[nn,ind_1],
s=append{s_1,seq{e,ind_1}}));")
(instantiate-existential ("e_$0" "cons{e,s_1}"))
(backchain "with(e_$0:ind_1,s_1,s:[nn,ind_1],
s=append{s_1,seq{e_$0,ind_1}});")
(apply-macete-with-minor-premises append-cons)
(instantiate-existential ("e" "s"))
(apply-macete-with-minor-premises infinite-append))))
(def-theorem sequence-decomposition-on-right
"forall(s:[nn,ind_1], 0<length{s} implies
forsome(e:ind_1, s_1:[nn,ind_1], s=append{s_1,cons{e,nil{ind_1}}}))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(instantiate-theorem sequence-cases-on-right ("s"))
(contrapose "with(n:nn,0<n);")
(backchain "with(f,s:[nn,ind_1],s=f);")
(apply-macete-with-minor-premises length-of-nil)
simplify)))
(def-theorem sequence-induction-on-right
"forall(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],
f_seq_q(s) implies p(s))
iff
(p(nil(ind_1))
and
forall(s:[nn,ind_1], e:ind_1,
f_seq_q(s) and p(s) implies p(append{s,cons{e,nil{ind_1}}}))))"
(theory sequences)
(usages transportable-macete)
(proof
(
direct-inference
direct-inference
(block (script-comment "first prove easy direction: =>")
direct-and-antecedent-inference-strategy
(backchain "with(p:prop,p);")
(apply-macete-with-minor-premises nil-is-fseq)
(backchain "with(p:prop,forall(s:[nn,ind_1],p));")
(apply-macete-with-minor-premises append-is-fseq)
(apply-macete-with-minor-premises cons-to-nil-is-fseq))
(block (script-comment "next prove other direction: =>.
requires induction on length.")
(cut-with-single-formula "forall(j:zz, 0<=j implies forall(s:[nn,ind_1], length(s)=j implies p(s)))")
(instantiate-universal-antecedent "with(p:prop,forall(j:zz,p));"
("length{s}"))
(block (script-comment "observe that (0<=length{s}).")
(contrapose "with(p:prop,not(p));")
simplify)
(block (script-comment "consider s_$0=s.")
(instantiate-universal-antecedent
"with(p:prop,forall(s_$0:[nn,ind_1],p));" ("s"))
(contrapose "with(p:prop,not(p));"))
(script-comment "now prove the induction formula.")
(induction integer-inductor ("j"))
(block (script-comment "base case.")
(apply-macete-with-minor-premises length-0-iff-nil)
simplify)
(block (script-comment "induction step: decompose seq on right.")
(instantiate-theorem sequence-cases-on-right ("s"))
simplify
(backchain "with(f,s:[nn,ind_1],s=f);")
(backchain "with(p:prop,forall(s:[nn,ind_1],e:ind_1,p));")
(apply-macete-with-minor-premises append-fseq-implies-first-fseq)
direct-inference
(instantiate-existential ("seq{e,ind_1}"))
simplify
(backchain "with(p:prop,forall(s:[nn,ind_1],p));")
(cut-with-single-formula "f_seq_q{s} and f_seq_q{s_1}")
(contrapose "with(r:rr,n:nn,n=r);")
(backchain "with(f,s:[nn,ind_1],s=f);")
(let-macete fseq-macetes
(series
(repeat length-of-append length-of-cons length-of-nil
nil-is-fseq cons-to-nil-is-fseq )
simplify
append-fseq-implies-first-fseq
simplify))
(while (progresses?
(block (jump-to-node induction-step )
(for-nodes
(unsupported-descendents)
(apply-macete-with-minor-premises $fseq-macetes))))
(skip)))))))
(def-inductor sequence-right-inductor
sequence-induction-on-right
(theory sequences)
(base-case-hook simplify))
(def-theorem in_seq-car
"forall(x:ind_1, s:[nn,ind_1], in_seq{x, cons{x,s}})"
(theory sequences)
(usages transportable-macete transportable-rewrite)
(proof (direct-and-antecedent-inference-strategy
(instantiate-existential ("0"))
simplify)))
(def-theorem in_seq-cdr
"forall(x,y:ind_1, s:[nn,ind_1], not(x=y)
implies (in_seq{x, cons{y,s}} iff in_seq{x,s}))"
(theory sequences)
(usages transportable-macete)
(proof (simplify-insistently
direct-and-antecedent-inference-strategy
(case-split ("i<1"))
(incorporate-antecedent "with(x:ind_1,s:[nn,ind_1],y:ind_1,i:nn,
if(i<1, y, s([-1]+i))=x);")
simplify
(incorporate-antecedent "with(x:ind_1,s:[nn,ind_1],y:ind_1,i:nn,
if(i<1, y, s([-1]+i))=x);")
simplify
direct-and-antecedent-inference-strategy
(instantiate-existential ("[-1]+i"))
(instantiate-existential ("i+1"))
simplify)))
(def-theorem in_seq-nil
"forall(x:ind_1, not(in_seq{x,nil{ind_1}}))"
(theory sequences)
(usages transportable-rewrite transportable-macete)
(proof (simplify-insistently)))
(def-compound-macete in_seq-macete
(series
(repeat
tr%in_seq-nil
tr%in_seq-car
tr%in_seq-cdr)
simplify))
(def-compound-macete sequence-length
(series
(repeat tr%length-of-nil
tr%length-of-cons
tr%length-of-append
tr%length-of-drop
tr%length-of-takefirst)
simplify))
(def-theorem sequence-bird-induction
"forall(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],f_seq_q{s} implies p(s))
iff
((p(nil{ind_1})
and
forall(e:ind_1,p(seq{e,ind_1})))
and
forall(s_0,s_1:[nn,ind_1],
f_seq_q{s_0} and f_seq_q{s_1} and p(s_0) and p(s_1)
implies
p(append{s_0,s_1}))))"
(theory sequences)
(usages transportable-macete)
(proof (direct-and-antecedent-inference-strategy
(backchain "with(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],f_seq_q{s} implies p(s)));")
(apply-macete-with-minor-premises nil-is-fseq)
(backchain "with(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],f_seq_q{s} implies p(s)));")
(apply-macete-with-minor-premises cons-to-nil-is-fseq)
(backchain "with(p:[[nn,ind_1],prop],
forall(s:[nn,ind_1],f_seq_q{s} implies p(s)));")
(apply-macete-with-minor-premises append-is-fseq)
simplify
(induction sequence-right-inductor ("s"))
(backchain "with(p:[[nn,ind_1],prop],
forall(s_0,s_1:[nn,ind_1],
f_seq_q{s_0} and f_seq_q{s_1} and p(s_0) and p(s_1)
implies
p(append{s_0,s_1})));")
simplify
(apply-macete-with-minor-premises cons-to-nil-is-fseq))))
(def-inductor sequence-bird-inductor
sequence-bird-induction
(theory sequences)
(base-case-hook simplify))
(def-imported-rewrite-rules h-o-real-arithmetic
(source-theories sequences))