Lemma: sqequal-nil
∀[T:Type]. ∀[l:T List]. l ~ [] supposing l = [] ∈ (T List)
Lemma: sqequal-null
∀[T:Type]. ∀[l:T List]. l ~ [] supposing ↑null(l)
Lemma: reverse_append
∀[T:Type]. ∀[as,bs:T List]. (rev(as @ bs) = (rev(bs) @ rev(as)) ∈ (T List))
Lemma: reverse_append_sq
∀[as:Top List]. ∀[bs:Top]. (rev(as @ bs) ~ rev(bs) @ rev(as))
Lemma: map-map-trivial
∀[L:Top List]. ∀[X:Top ⟶ Top]. (map(λp.(fst(p));map(λx.<x, X[x]>;L)) ~ L)
Lemma: filter_is_nil3
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. filter(P;L) ~ [] supposing (∀x∈L.¬↑P[x])
Lemma: first-success-is-inl
∀[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List]. ∀[j:ℕ||L||]. ∀[a:A[L[j]]].
(first-success(f;L) = (inl <j, a>) ∈ (i:ℕ||L|| × A[L[i]]?)
⇐⇒ j < ||L|| ∧ ((f L[j]) = (inl a) ∈ (A[L[j]]?)) ∧ (∀x∈firstn(j;L).↑isr(f x)))
Lemma: isl-first-success
∀[T:Type]. ∀[A:T ⟶ Type].
∀f:x:T ⟶ (A[x]?). ∀L:T List.
((↑isl(first-success(f;L)))
⇒ (fst(outl(first-success(f;L))) < ||L||
∧ ((f L[fst(outl(first-success(f;L)))])
= (inl (snd(outl(first-success(f;L)))))
∈ (A[L[fst(outl(first-success(f;L)))]]?))
∧ (∀x∈firstn(fst(outl(first-success(f;L)));L).↑isr(f x))))
Lemma: combine-list-rel-or
∀[T:Type]
∀f:T ⟶ T ⟶ T. ∀R:T ⟶ T ⟶ ℙ.
((∀x,y,z:T. (R[x;f[y;z]] ⇐⇒ R[x;y] ∨ R[x;z]))
⇒ (∀L:T List. ∀a:T. R[a;combine-list(x,y.f[x;y];L)] ⇐⇒ (∃b∈L. R[a;b]) supposing 0 < ||L|| ∧ Assoc(T;λx,y. f[x;y])\000C))
Lemma: imax-list-ub
∀L:ℤ List. ∀a:ℤ. a ≤ imax-list(L) ⇐⇒ (∃b∈L. a ≤ b) supposing 0 < ||L||
Lemma: select-le-imax-list
∀L:ℤ List. ∀i:ℕ||L||. (L[i] ≤ imax-list(L))
Lemma: imax-list-cons-is-nat
∀L:ℤ List. ∀[x:ℕ]. (imax-list([x / L]) ∈ ℕ)
Lemma: imax-list-is-nat
∀L:ℤ List. (imax-list([0 / L]) ∈ ℕ)
Lemma: imax-list-nat
∀L:ℕ List+. (imax-list(L) ∈ ℕ)
Lemma: fresh-nat-exists
∀L:ℕ List. ∃n:ℕ. ∀i:ℕ||L||. L[i] < n
Lemma: fresh-nat-exists2
∀L:ℕ List. ∃n:ℕ. (¬(n ∈ L))
Lemma: combine-list-rel-and
∀[T:Type]
∀f:T ⟶ T ⟶ T. ∀R:T ⟶ T ⟶ ℙ.
((∀x,y,z:T. (R[x;f[y;z]] ⇐⇒ R[x;y] ∧ R[x;z]))
⇒ (∀L:T List. ∀a:T. R[a;combine-list(x,y.f[x;y];L)] ⇐⇒ (∀b∈L.R[a;b]) supposing 0 < ||L|| ∧ Assoc(T;λx,y. f[x;y]))\000C)
Lemma: imax-list-lb
∀[L:ℤ List]. ∀[a:ℤ]. uiff(imax-list(L) ≤ a;(∀b∈L.b ≤ a)) supposing 0 < ||L||
Lemma: imax-list-unique
∀[L:ℤ List]. ∀[a:ℤ]. uiff(imax-list(L) = a ∈ ℤ;(∀b∈L.b ≤ a)) supposing (a ∈ L)
Lemma: imax-list-member
∀L:ℤ List. (imax-list(L) ∈ L) supposing 0 < ||L||
Lemma: imax-list-cons
∀[as:ℤ List]. ∀[a:ℤ]. imax-list([a / as]) = imax(a;imax-list(as)) ∈ ℤ supposing 0 < ||as||
Lemma: isl-apply-alist
∀[A,T:Type].
∀eq:EqDecider(T). ∀x:T. ∀L:(T × A) List.
((↑isl(apply-alist(eq;L;x)) ⇐⇒ (x ∈ map(λp.(fst(p));L)))
∧ (<x, outl(apply-alist(eq;L;x))> ∈ L) supposing ↑isl(apply-alist(eq;L;x)))
Lemma: apply-alist-inl
∀[A,T:Type]. ∀eq:EqDecider(T). ∀x:T. ∀L:(T × A) List. ∀z:A. ((apply-alist(eq;L;x) = (inl z) ∈ (A?)) ⇒ (<x, z> ∈ L))
Lemma: apply-alist-inr
∀[A,T:Type].
∀eq:EqDecider(T). ∀x:T. ∀u:Unit. ∀L:(T × A) List.
((apply-alist(eq;L;x) = (inr u ) ∈ (A?)) ⇒ (¬(∃z:A. (<x, z> ∈ L))))
Lemma: sort-int-sorted
∀[T:Type]. ∀[as:T List]. sorted(sort-int(as)) supposing T ⊆r ℤ
Lemma: select_concat
∀[T:Type]
∀ll:T List List. ∀n:ℕ||concat(ll)||.
∃m:ℕ||ll||
((||concat(firstn(m;ll))|| ≤ n)
c∧ n - ||concat(firstn(m;ll))|| < ||ll[m]||
c∧ (concat(ll)[n] = ll[m][n - ||concat(firstn(m;ll))||] ∈ T))
Lemma: concat-map-single
∀[f,L:Top]. (concat(map(λx.[f[x]];L)) ~ map(λx.f[x];L))
Lemma: length-concat-map-single
∀[f,L:Top]. (||concat(map(λx.[f[x]];L))|| ~ ||L||)
Lemma: concat-map-assoc
∀[f,g:Top]. ∀[L:Top List]. (concat(map(g;concat(map(f;L)))) ~ concat(map(λx.concat(map(g;f x));L)))
Lemma: map-concat
∀[f:Top]. ∀[L:Top List]. (map(f;concat(L)) ~ concat(map(λl.map(f;l);L)))
Lemma: filter_append_sq
∀[P,A,B:Top]. (filter(P;A @ B) ~ filter(P;A) @ filter(P;B))
Lemma: filter-concat
∀[P:Top]. ∀[L:Top List]. (filter(P;concat(L)) ~ concat(map(λl.filter(P;l);L)))
Lemma: list_accum_filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. ∀[f,y:Top].
(accumulate (with value a and list item b):
f[a;b]
over list:
filter(λb.P[b];l)
with starting value:
y) ~ accumulate (with value a and list item b):
if P[b] then f[a;b] else a fi
over list:
l
with starting value:
y))
Lemma: firstn-filter
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀n:ℕ. ∃m:ℕ||L|| + 1. (firstn(n;filter(P;L)) = filter(P;firstn(m;L)) ∈ (T List))
Lemma: last_lemma
∀[T:Type]. ∀L:T List. ∃L':T List. (L = (L' @ [last(L)]) ∈ (T List)) supposing ¬↑null(L)
Lemma: select_append
∀[T:Type]. ∀[as,bs:T List]. ∀[i:ℕ||as|| + ||bs||]. (as @ bs[i] = if i <z ||as|| then as[i] else bs[i - ||as||] fi ∈ T)
Lemma: hd-map-spread
∀[f:Top]. ∀[L:Top List]. (hd(map(λx.let a,b = x in f[a;b];L)) ~ let a,b = hd(L) in f[a;b])
Lemma: non-null-list-tactic-test
∀T:Type. ∀L:T List. ∀x:T.
(((((((((0 < ||L|| ∨ (1 ≤ ||L||)) ∨ null(L) = ff) ∨ null(L) = ff) ∨ (¬↑null(L))) ∨ (¬(L = [] ∈ (T List))))
∨ (¬([] = L ∈ (T List))))
∨ (¬null(L) = tt))
∨ (∃x:T. (x ∈ L))
∨ (x ∈ L)
∨ (L = [x / L] ∈ (T List)))
⇒ (((((((1 ≤ ||L||) ∧ null(L) = ff) ∧ (null(L) ~ ff)) ∧ (¬↑null(L))) ∧ (¬(L = [] ∈ (T List)))) ∧ (∃x:T. (x ∈ L)))
∧ (0 ≤ ||L||)))
Lemma: l_member_decidable
∀[T:Type]. ∀x:T. ∀l:T List. ((∀y:T. Dec(x = y ∈ T)) ⇒ Dec((x ∈ l)))
Lemma: map-wf2
∀[A,B:Type]. ∀[L:A List]. ∀[f:{x:A| (x ∈ L)} ⟶ B]. (map(f;L) ∈ B List)
Lemma: list_extensionality_iff
∀[T:Type]. ∀[a,b:T List]. (a = b ∈ (T List) ⇐⇒ (||a|| = ||b|| ∈ ℤ) ∧ (∀i:ℕ||a||. (a[i] = b[i] ∈ T)))
Lemma: member-update-alist1
∀[A,T:Type].
∀eq:EqDecider(T). ∀x:T. ∀L:(T × A) List. ∀z:A. ∀f:A ⟶ A. ∀y:T.
((y ∈ map(λp.(fst(p));update-alist(eq;L;x;z;v.f[v]))) ⇐⇒ (y ∈ map(λp.(fst(p));L)) ∨ (y = x ∈ T))
Lemma: nth_tl-append
∀[as:Top List]. ∀[bs:Top].
∀n:ℕ. (nth_tl(n;as @ bs) ~ if n <z ||as|| then nth_tl(n;as) @ bs else nth_tl(n - ||as||;bs) fi )
Lemma: nth_tl_nil
∀[n:ℤ]. (nth_tl(n;[]) ~ [])
Lemma: nth_tl_append
∀[T:Type]. ∀[as,bs:T List]. (nth_tl(||as||;as @ bs) ~ bs)
Lemma: nth_tl_decomp
∀[T:Type]. ∀[m:ℕ]. ∀[L:T List]. nth_tl(m;L) ~ [L[m] / nth_tl(1 + m;L)] supposing m < ||L||
Lemma: nth_tl_decomp_eq
∀[T:Type]. ∀[m:ℕ]. ∀[L:T List]. nth_tl(m;L) = [L[m] / nth_tl(1 + m;L)] ∈ (T List) supposing m < ||L||
Lemma: append_firstn_lastn
∀[T:Type]. ∀[L:T List]. ∀[n:{0...||L||}]. ((firstn(n;L) @ nth_tl(n;L)) = L ∈ (T List))
Lemma: append_firstn_lastn_sq
∀[L:Top List]. ∀[n:ℕ||L|| + 1]. (L ~ firstn(n;L) @ nth_tl(n;L))
Lemma: append_split2
∀[T:Type]
∀L:T List
∀[P:ℕ||L|| ⟶ ℙ]
((∀x:ℕ||L||. Dec(P x))
⇒ (∀i,j:ℕ||L||. ((P i) ⇒ P j supposing i < j))
⇒ (∃L_1,L_2:T List. ((L = (L_1 @ L_2) ∈ (T List)) ∧ (∀i:ℕ||L||. (P i ⇐⇒ ||L_1|| ≤ i)))))
Lemma: list_decomp_member
∀[T:Type]. ∀L:T List. ∀i:ℕ||L||. ∃as,bs:T List. (L = (as @ [L[i]] @ bs) ∈ (T List))
Lemma: select_nth_tl
∀[T:Type]. ∀[as:T List]. ∀[n:{0...||as||}]. ∀[i:ℕ||as|| - n]. (nth_tl(n;as)[i] = as[i + n] ∈ T)
Lemma: map_id
∀[A:Type]. ∀[as:A List]. (map(Id{A};as) = as ∈ (A List))
Lemma: ispair_wf_list
∀[T:Type]. ∀[L:T List]. (ispair(L) ∈ 𝔹)
Lemma: non-pair-list
∀[T:Type]. ∀[L:T List]. L ∈ Unit supposing ispair(L) = ff
Lemma: pair-list
∀[T:Type]. ∀[L:T List]. L ∈ T × (T List) supposing ispair(L) = tt
Lemma: isaxiom_wf_list
∀[T:Type]. ∀[L:T List]. (isaxiom(L) ∈ 𝔹)
Lemma: axiom-list
∀[T:Type]. ∀[L:T List]. L ∈ Unit supposing isaxiom(L) = tt
Lemma: non-axiom-list
∀[T:Type]. ∀[L:T List]. L ∈ T × (T List) supposing isaxiom(L) = ff
Lemma: reduce-append
∀[f,k,as,bs:Top]. (reduce(f;k;as @ bs) ~ reduce(f;reduce(f;k;bs);as))
Lemma: nth_tl_nth_tl
∀[m,n:ℕ]. ∀[L:Top List]. (nth_tl(m;nth_tl(n;L)) ~ nth_tl(m + n;L))
Lemma: tl_nth_tl
∀[n:ℕ]. ∀[L:Top List]. (tl(nth_tl(n;L)) ~ nth_tl(n;tl(L)))
Lemma: reverse_singleton
∀[x:Top]. (rev([x]) ~ [x])
Lemma: for_nil_lemma
∀g,k,f,T:Top. (For{T,f,k} x ∈ []. g[x] ~ k)
Lemma: for_cons_lemma
∀g,as,a,k,f,T:Top. (For{T,f,k} x ∈ [a / as]. g[x] ~ f g[a] (For{T,f,k} x ∈ as. g[x]))
Definition: mapcons
mapcons(f;as) == fix((λmapcons,as. case as of [] => [] | a::as' => [f a as' / (mapcons as')] esac)) as
Lemma: mapcons_nil_lemma
∀f:Top. (mapcons(f;[]) ~ [])
Lemma: mapcons_cons_lemma
∀t,h,f:Top. (mapcons(f;[h / t]) ~ [f h t / mapcons(f;t)])
Lemma: mapcons_wf
∀[A,B:Type]. ∀[f:A ⟶ (A List) ⟶ B]. ∀[l:A List]. (mapcons(f;l) ∈ B List)
Definition: for_hdtl
ForHdTl{A,f,k} h::t ∈ as. g[h; t] == reduce(f;k;mapcons(λh,t. g[h; t];as))
Lemma: for_hdtl_wf
∀[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ (A List) ⟶ B]. (ForHdTl{A,f,k} h::t ∈ as. g[h;t] ∈ C)
Lemma: for_hdtl_nil_lemma
∀g,k,f,T:Top. (ForHdTl{T,f,k} h::t ∈ []. g[h;t] ~ k)
Lemma: for_hdtl_cons_lemma
∀g,as,a,k,f,T:Top. (ForHdTl{T,f,k} h::t ∈ [a / as]. g[h;t] ~ f g[a;as] (ForHdTl{T,f,k} h::t ∈ as. g[h;t]))
Lemma: strict4-concat
strict4(λx,y,z,s. concat(x))
Lemma: concat-cons2
∀[l,ll:Top]. (concat([l / ll]) ~ l @ concat(ll))
Lemma: concat-nil
concat([]) ~ []
Lemma: strict4-concat-map
strict4(λx,y,z,w. concat(map(λb.y[b];x)))
Definition: product-map
product-map(F;as;bs) == concat(map(λa.map(λb.(F a b);bs);as))
Lemma: product-map_wf
∀[A,B,C:Type]. ∀[F:A ⟶ B ⟶ C]. ∀[as:A List]. ∀[bs:B List]. (product-map(F;as;bs) ∈ C List)
Lemma: list_accum-triangle-inequality
∀[T:Type]. ∀[L:T List]. ∀[x,y:ℤ]. ∀[f,g:T ⟶ ℤ].
(|accumulate (with value s and list item a):
s + f[a]
over list:
L
with starting value:
x) - accumulate (with value s and list item a):
s + g[a]
over list:
L
with starting value:
y)| ≤ accumulate (with value s and list item a):
s + |f[a] - g[a]|
over list:
L
with starting value:
|x - y|))
Lemma: filter-nil
∀[P:Top]. (filter(P;[]) ~ [])
Lemma: filter_is_nil_implies2
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. (∀x∈L.¬↑P[x]) supposing filter(P;L) = [] ∈ ({x:T| (x ∈ L)} List)
Lemma: filter_is_nil_implies
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. (∀x∈L.¬↑P[x]) supposing filter(P;L) = [] ∈ (T List)
Lemma: pos_length2
∀[A:Type]. ∀[l:A List]. uiff(¬↑null(l);0 < ||l||)
Lemma: pos_length3
∀[A:Type]. ∀[l:A List]. uiff(¬↑null(l);||l|| ≥ 1 )
Lemma: length_zero
∀[T:Type]. ∀[l:T List]. uiff(||l|| = 0 ∈ ℤ;l = [] ∈ (T List))
Lemma: hd-wf-not-null
∀[A:Type]. ∀[l:A List]. hd(l) ∈ A supposing ¬↑null(l)
Lemma: general-append-cancellation
∀[T:Type]. ∀[as,bs,cs,ds:T List].
({(as = bs ∈ (T List)) ∧ (cs = ds ∈ (T List))}) supposing
(((||as|| = ||bs|| ∈ ℤ) ∨ (||cs|| = ||ds|| ∈ ℤ)) and
((as @ cs) = (bs @ ds) ∈ (T List)))
Lemma: append-cancellation
∀[T:Type]. ∀[as,as',bs,cs:T List].
(cs = bs ∈ (T List)) supposing (((as @ cs) = (as' @ bs) ∈ (T List)) and (||as|| = ||as'|| ∈ ℤ))
Lemma: append-cancellation-right
∀[T:Type]. ∀[as,as',bs,cs:T List].
(cs = bs ∈ (T List)) supposing (((cs @ as) = (bs @ as') ∈ (T List)) and (||as|| = ||as'|| ∈ ℤ))
Lemma: append-impossible
∀[T:Type]. ∀[as,bs:T List]. ∀[b:T]. uiff(as = (as @ [b / bs]) ∈ (T List);False)
Lemma: hd-map
∀[f:Top]. ∀[L:Top List]. (hd(map(f;L)) ~ if null(L) then ⊥ else f hd(L) fi )
Lemma: list_append_ind
Alternative Induction Principle for Lists
Used for multiset induction.
∀[T:Type]. ∀[Q:(T List) ⟶ ℙ].
(Q[[]] ⇒ (∀x:T. Q[[x]]) ⇒ (∀ys,ys':T List. (Q[ys] ⇒ Q[ys'] ⇒ Q[ys @ ys'])) ⇒ {∀zs:T List. Q[zs]})
Lemma: null_member
∀[T:Type]. ∀[L:T List]. ∀[x:T]. ¬(x ∈ L) supposing ↑null(L)
Lemma: member_null
∀[T:Type]. ∀[L:T List]. ∀[x:T]. ¬↑null(L) supposing (x ∈ L)
Lemma: member_not_nil
∀[T:Type]. ∀[L:T List]. ¬(L = [] ∈ (T List)) supposing ∃x:T. (x ∈ L)
Lemma: l_member_non_nil
∀[T:Type]. ∀[x:T]. ∀[L:T List]. ¬(L = [] ∈ (T List)) supposing (x ∈ L)
Lemma: list-eq-subtype2
∀[A:Type]. ∀[B:A ⟶ ℙ]. ∀[d1:{a:A| B[a]} List]. ∀[d2:A List]. d2 ∈ {a:A| B[a]} List supposing d1 = d2 ∈ (A List)
Lemma: list-eq-subtype1
∀[A:Type]. ∀[B:A ⟶ ℙ]. ∀[d1,d2:{a:A| B[a]} List]. d1 = d2 ∈ ({a:A| B[a]} List) supposing d1 = d2 ∈ (A List)
Lemma: list-eq-subtype
∀[A:Type]. ∀[d1,d2:A List]. d1 = d2 ∈ ({a:A| (a ∈ d1)} List) supposing d1 = d2 ∈ (A List)
Lemma: decidable__equal_list
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀xs,ys:T List. Dec(xs = ys ∈ (T List))))
Definition: accum_list
accum_list(a,x.f[a; x];x.base[x];L) ==
accumulate (with value a and list item x):
f[a; x]
over list:
tl(L)
with starting value:
base[hd(L)])
Lemma: accum_list_wf
∀[T,A:Type]. ∀[base:T ⟶ A]. ∀[f:A ⟶ T ⟶ A]. ∀[L:T List]. accum_list(a,x.f[a;x];x.base[x];L) ∈ A supposing 0 < ||L||
Lemma: accum_list_cons_lemma
∀L,u,base,f:Top.
(accum_list(a,x.f[a;x]; y.base[y]; [u / L]) ~ accumulate (with value a and list item y):
f[a;y]
over list:
L
with starting value:
base[u]))
Lemma: rev-append-property-top-sqle
∀[as,bs,cs:Top]. (rev(as) + bs @ cs ≤ rev(as) + bs @ cs)
Lemma: list-if-has-value-rev-append
∀[as,bs:Base]. as ∈ Base List supposing (rev(as) + bs)↓
Lemma: eq_cons_imp_eq_hds
∀[A:Type]. ∀[a,b:A]. ∀[as,bs:A List]. a = b ∈ A supposing [a / as] = [b / bs] ∈ (A List)
Lemma: filter-filter
∀[P1,P2,L:Top]. (filter(P2;filter(P1;L)) ~ filter(λt.((P1 t) ∧b (P2 t));L))
Lemma: filter-map
∀[f,Q,L:Top]. (filter(Q;map(f;L)) ~ map(f;filter(Q o f;L)))
Lemma: list_n_properties
∀[A:Type]. ∀[n:ℤ]. ∀[as:A List(n)]. (||as|| = n ∈ ℤ)
Lemma: mono-list
∀A:Type. (mono(A) ⇒ mono(A List))
Lemma: member-product-map
∀[A,B,C:Type].
∀F:A ⟶ B ⟶ C. ∀as:A List. ∀bs:B List. ∀c:C.
((c ∈ product-map(F;as;bs)) ⇐⇒ ∃a:A. ((a ∈ as) ∧ (∃b:B. ((b ∈ bs) ∧ (c = (F a b) ∈ C)))))
Lemma: strong-subtype-list
∀[A,B:Type]. strong-subtype(A List;B List) supposing strong-subtype(A;B)
Lemma: strong-subtype-l_member-type
∀[A,B:Type]. ∀[L:A List]. ∀[x:B]. x ∈ A supposing (x ∈ L) supposing strong-subtype(A;B)
Lemma: strong-subtype-l_member
∀[A,B:Type]. ∀L:A List. ∀x:B. ((x ∈ L) ⇒ (x ∈ L)) supposing strong-subtype(A;B)
Lemma: strong-subtype-equal-lists
∀[A,B:Type]. ∀[L1:A List]. ∀[L2:B List]. L1 = L2 ∈ (A List) supposing L1 = L2 ∈ (B List) supposing strong-subtype(A;B)
Lemma: l_member_length
∀[T:Type]. ∀[L:T List]. ∀[x:T]. 0 < ||L|| supposing (x ∈ L)
Lemma: list-equal-subsume
∀[A,B:Type]. ∀[x,y:A List]. {x = y ∈ (B List) supposing x = y ∈ (A List)} supposing {a:A| (a ∈ x)} ⊆r B
Lemma: test_sqtype1
∀[X,Y:Type]. (SQType((n:ℕ × {L:𝔹 List| True} ? × (X + Y)) List)) supposing ((Y ⊆r Base) and (X ⊆r Base))
Definition: len
len(as) == rec-case(as) of [] => 0 | a::bs => lenbs.lenbs + 1
Lemma: len_wf
∀[as:Top List]. (len(as) ∈ ℕ)
Lemma: len_nil_lemma
len([]) ~ 0
Lemma: len_cons_lemma
∀as,a:Top. (len([a / as]) ~ len(as) + 1)
Lemma: len-length
∀[as:Top List]. (||as|| ~ len(as))
Definition: norm-list
norm-list(N) == λL.rec-case(L) of [] => [] | a::as => r.eval a' = N a in eval r' = r in [a' / r']
Lemma: norm-list_wf
∀[T:Type]. ∀[N:id-fun(T)]. (norm-list(N) ∈ id-fun(T List)) supposing value-type(T)
Lemma: norm-list_wf_sq
∀[T:Type]. (∀[N:sq-id-fun(T)]. (norm-list(N) ∈ sq-id-fun(T List))) supposing (value-type(T) and (T ⊆r Base))
Definition: eval-list
eval-list(L) == norm-list(λx.x) L
Lemma: eval-list_wf
∀[L:ℤ List]. (eval-list(L) ∈ {L':ℤ List| L' = L ∈ (ℤ List)} )
Lemma: eval-list-sq
∀[L:ℤ List]. (eval-list(L) ~ L)
Definition: count
count(P;L) == reduce(λa,n. (if P a then 1 else 0 fi + n);0;L)
Lemma: count_wf
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. (count(P;L) ∈ ℕ)
Lemma: count-append
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L1,L2:A List]. (count(P;L1 @ L2) ~ count(P;L1) + count(P;L2))
Lemma: count-single
∀[P,x:Top]. (count(P;[x]) ~ if P x then 1 else 0 fi + 0)
Definition: l-last-default
l-last-default(l;d) == rec-case(l) of [] => λx.x | h::t => r.λx.(r h) d
Lemma: l-last-default_wf
∀[T:Type]. ∀[L:T List]. ∀[d:T]. (l-last-default(L;d) ∈ T)
Lemma: has-value-l-last-default-list
∀[l,d:Base]. l ∈ Top List supposing (l-last-default(l;d))↓
Definition: l-last
l-last(l) == l-last-default(l;⊥)
Lemma: l-last_wf
∀[T:Type]. ∀[L:T List]. l-last(L) ∈ T supposing ¬↑null(L)
Lemma: has-value-l-last
∀[l:Base]. l ∈ Top × Top supposing (l-last(l))↓
Lemma: has-value-l-last-list
∀[l:Base]. l ∈ Top List supposing (l-last(l))↓
Lemma: l-last-nil
l-last([]) ~ ⊥
Lemma: l-last-cons
∀[u,v:Top]. (l-last([u / v]) ~ if null(v) then u else l-last(v) fi )
Lemma: has-value-last
∀[l:Base]. l ∈ Top × Top supposing (last(l))↓
Lemma: has-value-last-list
∀[l:Base]. l ∈ Top List supposing (last(l))↓
Lemma: length-zero-implies-nil
∀l:Base. l ~ [] supposing ||l|| = 0 ∈ ℤ
Lemma: l-last-is-last
∀[l:Top]. (l-last(l) ~ last(l))
Definition: list-at
L1@L2 ==
if null(L2) then []
if null(L1) then []
else if hd(L2)=0 then [hd(L1) / tl(L1)@tl(L2)] else tl(L1)@[hd(L2) - 1 / tl(L2)]
fi
Lemma: list-at_wf
∀[T:Type]. ∀[ns:colist(ℕ)]. ∀[L:colist(T)]. (L@ns ∈ colist(T))
Lemma: list_at_nil2_lemma
∀L:Top. (L@[] ~ [])
Lemma: nil-at
∀[ms:colist(ℕ)]. ([]@ms ~ [])
Definition: combine-skips
combine-skips(as;bs;n) ==
if null(bs) then []
if null(as) then []
else if hd(bs)=0
then [n + hd(as) / combine-skips(tl(as);tl(bs);0)]
else combine-skips(tl(as);[hd(bs) - 1 / tl(bs)];(n + 1) + hd(as))
fi
Lemma: combine-skips_wf
∀[bs,as:colist(ℕ)]. ∀[k:ℕ]. (combine-skips(as;bs;k) ∈ colist(ℕ))
Lemma: list-at-combine-skips
∀[ms,ns:colist(ℕ)]. ∀[k:ℕ]. ∀[T:Type]. ∀[L:colist(T)]. (L@combine-skips(ns;ms;k) = nth_tl(k;L)@ns@ms ∈ colist(T))
Lemma: list-at-at
∀ms,ns:colist(ℕ). ∀[T:Type]. ∀[L:colist(T)]. (L@ns@ms = L@combine-skips(ns;ms;0) ∈ colist(T))
Definition: sub-co-list
sub-co-list(T;s1;s2) == ∃ns:colist(ℕ). (s1 = s2@ns ∈ colist(T))
Lemma: sub-co-list_wf
∀[T:Type]. ∀[s1,s2:colist(T)]. (sub-co-list(T;s1;s2) ∈ ℙ)
Lemma: sub-co-list_transitivity
∀[T:Type]. ∀[s1,s2,s3:colist(T)]. (sub-co-list(T;s1;s2) ⇒ sub-co-list(T;s2;s3) ⇒ sub-co-list(T;s1;s3))
Lemma: nil-sub-co-list
∀[T:Type]. ∀[s:colist(T)]. sub-co-list(T;[];s)
Lemma: cons-sub-co-list-nil
∀[T:Type]. ∀x:T. ∀L:colist(T). (sub-co-list(T;[x / L];[]) ⇐⇒ False)
Lemma: cons-sub-co-list-cons
∀[T:Type]
∀x1,x2:T. ∀L1,L2:colist(T).
(sub-co-list(T;[x1 / L1];[x2 / L2]) ⇐⇒ ((x1 = x2 ∈ T) ∧ sub-co-list(T;L1;L2)) ∨ sub-co-list(T;[x1 / L1];L2))
Definition: sublist
L1 ⊆ L2 == ∃f:ℕ||L1|| ⟶ ℕ||L2||. (increasing(f;||L1||) ∧ (∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T)))
Lemma: sublist_wf
∀[T:Type]. ∀[L1,L2:T List]. (L1 ⊆ L2 ∈ ℙ)
Lemma: sublist_transitivity
∀[T:Type]. ∀L1,L2,L3:T List. (L1 ⊆ L2 ⇒ L2 ⊆ L3 ⇒ L1 ⊆ L3)
Lemma: length_sublist
∀[T:Type]. ∀[L1,L2:T List]. ||L1|| ≤ ||L2|| supposing L1 ⊆ L2
Lemma: cons_sublist_nil
∀[T:Type]. ∀x:T. ∀L:T List. ([x / L] ⊆ [] ⇐⇒ False)
Lemma: proper_sublist_length
∀[T:Type]. ∀[L1,L2:T List]. (L1 = L2 ∈ (T List)) supposing ((||L1|| = ||L2|| ∈ ℤ) and L1 ⊆ L2)
Lemma: sublist_antisymmetry
∀[T:Type]. ∀[L1,L2:T List]. (L1 = L2 ∈ (T List)) supposing (L2 ⊆ L1 and L1 ⊆ L2)
Lemma: nil-sublist
∀[T,x:Top]. [] ⊆ x
Lemma: nil_sublist
∀[T:Type]. ∀L:T List. ([] ⊆ L ⇐⇒ True)
Lemma: cons_sublist_cons
∀[T:Type]. ∀x1,x2:T. ∀L1,L2:T List. ([x1 / L1] ⊆ [x2 / L2] ⇐⇒ ((x1 = x2 ∈ T) ∧ L1 ⊆ L2) ∨ [x1 / L1] ⊆ L2)
Lemma: member_sublist
∀[T:Type]. ∀L1,L2:T List. (L1 ⊆ L2 ⇒ {∀x:T. ((x ∈ L1) ⇒ (x ∈ L2))})
Lemma: sublist_append
∀[T:Type]. ∀L1,L2,L1',L2':T List. (L1 ⊆ L1' ⇒ L2 ⊆ L2' ⇒ L1 @ L2 ⊆ L1' @ L2')
Lemma: comb_for_sublist_wf
λT,L1,L2,z. L1 ⊆ L2 ∈ T:Type ⟶ L1:(T List) ⟶ L2:(T List) ⟶ (↓True) ⟶ ℙ
Lemma: sublist_weakening
∀[T:Type]. ∀L1,L2:T List. L1 ⊆ L2 supposing L1 = L2 ∈ (T List)
Lemma: sublist_nil
∀[T:Type]. ∀L:T List. (L ⊆ [] ⇐⇒ L = [] ∈ (T List))
Lemma: sublist_tl
∀[T:Type]. ∀L1,L2:T List. L1 ⊆ tl(L2) ⇒ L1 ⊆ L2 supposing ¬↑null(L2)
Lemma: sublist_tl2
∀[T:Type]. ∀u:T. ∀v,L1:T List. (L1 ⊆ v ⇒ L1 ⊆ [u / v])
Lemma: sublist_append_front
∀[T:Type]. ∀L,L1,L2:T List. L ⊆ L1 @ L2 ⇒ L ⊆ L1 supposing ¬(last(L) ∈ L2) supposing ¬↑null(L)
Lemma: sublist_pair
∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||. [L[i]; L[j]] ⊆ L supposing i < j
Lemma: member_iff_sublist
∀[T:Type]. ∀x:T. ∀L:T List. ((x ∈ L) ⇐⇒ [x] ⊆ L)
Lemma: sublist_append1
∀[T:Type]. ∀L1,L2:T List. L1 ⊆ L1 @ L2
Lemma: sublist_append2
∀[T:Type]. ∀L1,L2:T List. L2 ⊆ L1 @ L2
Lemma: sublist-iff-sub-co-list
∀[T:Type]. ∀L2,L1:T List. (L1 ⊆ L2 ⇐⇒ sub-co-list(T;L1;L2))
Lemma: sublist_map
∀[A,B:Type]. ∀f:A ⟶ B. ∀as,bs:A List. (as ⊆ bs ⇒ map(f;as) ⊆ map(f;bs))
Lemma: sublist_map_inj
∀[A,B:Type]. ∀f:A ⟶ B. ∀as,bs:A List. (Inj(A;B;f) ⇒ (as ⊆ bs ⇐⇒ map(f;as) ⊆ map(f;bs)))
Definition: exists_sublist
exists_sublist(L;P)
==r if null(L) then P [] else let a,as = L in exists_sublist(as;P) ∨bexists_sublist(as;λl.(P [a / l])) fi
Lemma: exists_sublist_wf
∀[T:Type]. ∀[P:(T List) ⟶ 𝔹]. ∀[L:T List]. (exists_sublist(L;P) ∈ 𝔹)
Lemma: assert-exists_sublist
∀[T:Type]. ∀L:T List. ∀P:(T List) ⟶ 𝔹. (↑exists_sublist(L;P) ⇐⇒ ∃LL:T List. (LL ⊆ L ∧ (↑(P LL))))
Definition: embeddable
embeddable(R;L1;L2) == ∃f:ℕ||L1|| ⟶ ℕ||L2||. (increasing(f;||L1||) ∧ (∀j:ℕ||L1||. (R L1[j] L2[f j])))
Lemma: embeddable_wf
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[L1,L2:T List]. (embeddable(R;L1;L2) ∈ ℙ)
Definition: l_before
x before y ∈ l == [x; y] ⊆ l
Lemma: l_before_wf
∀[T:Type]. ∀[l:T List]. ∀[x,y:T]. (x before y ∈ l ∈ ℙ)
Lemma: weak_l_before_append_front
∀[T:Type]. ∀L1,L2:T List. ∀x,y:T. ((y ∈ L1) ⇒ x before y ∈ L1 @ L2 ⇒ x before y ∈ L1 supposing ¬(y ∈ L2))
Lemma: l_before_append_front
∀[T:Type]. ∀L1,L2:T List. ∀x,y:T. x before y ∈ L1 @ L2 ⇒ x before y ∈ L1 supposing ¬(y ∈ L2)
Lemma: l_tricotomy
∀[T:Type]. ∀x,y:T. ∀L:T List. ((x ∈ L) ⇒ (y ∈ L) ⇒ (((x = y ∈ T) ∨ x before y ∈ L) ∨ y before x ∈ L))
Lemma: l_before_member
∀[T:Type]. ∀L:T List. ∀a,b:T. (a before b ∈ L ⇒ (b ∈ L))
Lemma: singleton_before
∀[T:Type]. ∀a,x,y:T. (x before y ∈ [a] ⇐⇒ False)
Lemma: nil_before
∀[T:Type]. ∀x,y:T. (x before y ∈ [] ⇐⇒ False)
Lemma: l_before_append
∀[T:Type]. ∀L1,L2:T List. ∀x,y:T. ((x ∈ L1) ⇒ (y ∈ L2) ⇒ x before y ∈ L1 @ L2)
Lemma: l_before_member2
∀[T:Type]. ∀L:T List. ∀a,b:T. (a before b ∈ L ⇒ (a ∈ L))
Lemma: l_before_sublist
∀[T:Type]. ∀L1,L2:T List. (L1 ⊆ L2 ⇒ {∀x,y:T. (x before y ∈ L1 ⇒ x before y ∈ L2)})
Lemma: cons_before
∀[T:Type]. ∀l:T List. ∀a,x,y:T. (x before y ∈ [a / l] ⇐⇒ ((x = a ∈ T) ∧ (y ∈ l)) ∨ x before y ∈ l)
Lemma: before_last
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ x before last(L) ∈ L supposing ¬(x = last(L) ∈ T))
Lemma: l_before_select
∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||. L[j] before L[i] ∈ L supposing j < i
Lemma: before-map
∀[T,T':Type].
∀f:T ⟶ T'. ∀L:T List. ∀x',y':T'.
(x' before y' ∈ map(f;L) ⇐⇒ ∃x,y:T. (x before y ∈ L ∧ ((f x) = x' ∈ T') ∧ ((f y) = y' ∈ T')))
Lemma: l_before_append_iff
∀[T:Type]. ∀A,B:T List. ∀x,y:T. (x before y ∈ A @ B ⇐⇒ x before y ∈ A ∨ x before y ∈ B ∨ ((x ∈ A) ∧ (y ∈ B)))
Lemma: append_overlapping_sublists
∀[T:Type]. ∀L1,L2,L:T List. ∀x:T. L1 @ [x] ⊆ L ⇒ [x / L2] ⊆ L ⇒ L1 @ [x / L2] ⊆ L supposing no_repeats(T;L)
Lemma: l_before_transitivity
∀[T:Type]. ∀l:T List. ∀x,y,z:T. x before y ∈ l ⇒ y before z ∈ l ⇒ x before z ∈ l supposing no_repeats(T;l)
Lemma: no_repeats_iff
∀[T:Type]. ∀[l:T List]. uiff(no_repeats(T;l);∀[x,y:T]. ¬(x = y ∈ T) supposing x before y ∈ l)
Lemma: l_before_antisymmetry
∀[T:Type]. ∀[l:T List]. ∀[x,y:T]. (¬y before x ∈ l) supposing (x before y ∈ l and no_repeats(T;l))
Lemma: l_before_no_repeats
∀[T:Type]. ∀L:T List. ∀i,j:ℕ||L||. uiff(j < i;L[j] before L[i] ∈ L) supposing no_repeats(T;L)
Lemma: filter_sublist
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L_1,L_2:T List. (L_1 ⊆ L_2 ⇒ filter(P;L_1) ⊆ filter(P;L_2))
Lemma: filter_is_sublist
∀[T:Type]. ∀L:T List. ∀P:T ⟶ 𝔹. filter(P;L) ⊆ L
Lemma: length_filter
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. (||filter(P;L)|| = count(P;L) ∈ ℕ)
Lemma: filter_before
∀[A:Type]. ∀L:A List. ∀P:A ⟶ 𝔹. ∀x,y:A. (x before y ∈ filter(P;L) ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ L)
Lemma: filter_functionality
∀[A:Type]. ∀[L:A List]. ∀[f1,f2:A ⟶ 𝔹]. filter(f1;L) ~ filter(f2;L) supposing f1 = f2 ∈ (A ⟶ 𝔹)
Lemma: filter_append
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l1,l2:T List]. (filter(P;l1 @ l2) ~ filter(P;l1) @ filter(P;l2))
Lemma: filter_filter
∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List]. (filter(P1;filter(P2;L)) ~ filter(λt.((P1 t) ∧b (P2 t));L))
Lemma: filter_filter_reduce
∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List].
filter(P1;filter(P2;L)) ~ filter(P1;L) supposing ∀x:T. ((↑(P1 x)) ⇒ (↑(P2 x)))
Lemma: filter_map
∀[T1,T2:Type]. ∀[f:T1 ⟶ T2]. ∀[Q:T2 ⟶ 𝔹]. ∀[L:T1 List]. (filter(Q;map(f;L)) ~ map(f;filter(Q o f;L)))
Lemma: subtype-l_all
∀[T:Type]. ∀[L:T List]. ∀[P,Q:{x:T| (x ∈ L)} ⟶ ℙ].
(∀x∈L.P[x]) ⊆r (∀x∈L.Q[x]) supposing ∀x:T. ((x ∈ L) ⇒ (P[x] ⊆r Q[x]))
Lemma: decidable__l_all-proof
∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)} ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) ⇒ Dec((∀k∈L.F[k])))
Definition: l-all-decider
l-all-decider() ==
λL,dcd. eval j' = ||L|| in
case letrec G(x)=if (x) < (j') then if dcd L[x] then G (x + 1) else inl <x, λ%.Ax> fi else (inr (λx.Ax) ) i\000Cn
G(0)
of inl(%6) =>
inr let k,%8 = %6
in λ%8.Ax
| inr(%7) =>
inl (λk.case dcd L[k] of inl(%10) => %10 | inr(%11) => Ax)
Lemma: decidable__l_all
∀[A:Type]. ∀L:A List. ∀[F:{a:A| (a ∈ L)} ⟶ ℙ]. ((∀k:{a:A| (a ∈ L)} . Dec(F[k])) ⇒ Dec((∀k∈L.F[k])))
Lemma: l-all-decider_wf
∀[A:Type]
∀L:A List. ∀[F:{a:A| (a ∈ L)} ⟶ ℙ]. ∀dcd:∀k:{a:A| (a ∈ L)} . Dec(F[k]). (l-all-decider() L dcd ∈ Dec((∀k∈L.F[k])))
Lemma: l_all_fwd
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ (∀y∈L.P[y]) ⇒ P[x])
Lemma: decidable__l_exists-proof
∀[A:Type]. ∀[F:A ⟶ ℙ]. ∀L:A List. ((∀k:A. Dec(F[k])) ⇒ Dec((∃k∈L. F[k])))
Definition: l-exists-decider
l-exists-decider() ==
λL,dcd. eval j' = ||L|| in
letrec G(x)=if (x) < (j')
then case dcd L[x] of inl(z) => inl <x, z> | inr(z) => G (x + 1)
else (inr (λx.Ax) ) in
G(0)
Lemma: decidable__l_exists
∀[A:Type]. ∀[F:A ⟶ ℙ]. ∀L:A List. ((∀k:A. Dec(F[k])) ⇒ Dec((∃k∈L. F[k])))
Lemma: l-exists-decider_wf
∀[A:Type]. ∀[F:A ⟶ ℙ]. ∀L:A List. ∀dcd:∀k:A. Dec(F[k]). (l-exists-decider() L dcd ∈ Dec((∃k∈L. F[k])))
Lemma: not-l_all-dec
∀[T:Type]. ∀L:T List. ∀P:T ⟶ ℙ. ((∀x:T. Dec(P[x])) ⇒ (¬(∀x∈L.P[x]) ⇐⇒ (∃x∈L. ¬P[x])))
Definition: l-first
l-first(x.f[x];L) == rec-case(L) of [] => inr (λx.Ax) | x::xs => r.if f[x] then inl x else r fi
Lemma: l-first_wf
∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[L:T List]. (l-first(x.f[x];L) ∈ (∃x:T [((x ∈ L) ∧ (↑f[x]))]) ∨ (∀x∈L.¬↑f[x]))
Lemma: l-first-when-none
∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[L:T List]. l-first(x.f[x];L) ~ inr (λx.Ax) supposing (∀x∈L.¬↑f[x])
Lemma: l_member-settype
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L:{x:T| P[x]} List. ∀x:{x:T| P[x]} . ((x ∈ L) ⇐⇒ (x ∈ L))
Lemma: l_member_type
∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P i} List. ((∀y:T. Dec(P y)) ⇒ (x ∈ d) ⇒ (P x))
Lemma: l_member_type2
∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P[i]} List. ((∀y:T. Dec(P[y])) ⇒ (x ∈ d) ⇒ P[x])
Lemma: l_member_settype
∀[T:Type]. ∀[x:T]. ∀[P:T ⟶ ℙ]. ∀[d:{i:T| P[i]} List]. x ∈ {x:T| P[x]} supposing (x ∈ d)
Lemma: property-from-l_member
∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ((∀x:T. SqStable(P[x])) ⇒ (∀d:{i:T| P[i]} List. ((x ∈ d) ⇒ P[x])))
Lemma: l_member_in_subtype
∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P i} List. ((x ∈ d) ⇒ (x ∈ d))
Lemma: l_member_in_subtype2
∀[T:Type]. ∀x:T. ∀[P:T ⟶ ℙ]. ∀d:{i:T| P[i]} List. ((x ∈ d) ⇒ (x ∈ d))
Lemma: list-set-type-property
∀[T:Type]. ∀[P:T ⟶ ℙ]. ((∀x:T. SqStable(P[x])) ⇒ (∀L:{x:T| P[x]} List. (∀x∈L.P[x])))
Lemma: list-set-type-member
∀[T:Type]. ∀[P:T ⟶ ℙ]. ((∀x:T. SqStable(P[x])) ⇒ (∀L:{x:T| P[x]} List. ∀x:T. {(x ∈ L) ⇒ P[x]}))
Lemma: list-prod-set-type
∀[A,T:Type]. ∀[L:(A × T) List]. ∀[P:T ⟶ ℙ]. L ∈ (A × {x:T| P[x]} ) List supposing (∀p∈L.P[snd(p)])
Lemma: list-set-type3
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ ℙ]. L ∈ {x:T| P[x]} List supposing ∃L':{x:T| P[x]} List. (L = L' ∈ (T List))
Lemma: list-equal-set
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[L,L':T List]. (L = L' ∈ ({x:T| P[x]} List)) supposing ((L = L' ∈ (T List)) and (∀x∈L.P[x]))
Lemma: list-equal-set2
∀[T:Type]. ∀[P:T ⟶ ℙ].
∀[L:{x:T| P[x]} List]. ∀[L':T List]. L = L' ∈ ({x:T| P[x]} List) supposing L = L' ∈ (T List)
supposing ∀x:T. SqStable(P[x])
Lemma: l_member_set
∀[A:Type]. ∀[P:A ⟶ ℙ]. ∀L:A List. ∀x:A. ((∀x∈L.P[x]) ⇒ {(x ∈ L) ⇒ (x ∈ L)})
Lemma: l_member_set2
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L:{x:T| P[x]} List. ∀x:T. ((x ∈ L) ⇒ (x ∈ L))
Lemma: l_member-set
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ (x ∈ L))
Lemma: l_member-set2
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀L:{x:T| P[x]} List. ∀x:T. ((x ∈ L) ⇒ (x ∈ {x:T| P[x]} ))
Lemma: l_member_subtype
∀[A,B:Type]. ∀L:A List. ∀x:A. (x ∈ L) ⇒ (x ∈ L) supposing A ⊆r B
Lemma: l_member_subtype2
∀[A,B:Type]. ∀L:A List. ∀x:A. {(x ∈ L) ⇒ (x ∈ L)} supposing A ⊆r B
Lemma: l_member-alt-def
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇐⇒ ∃i:ℕ||L||. (x = L[i] ∈ T))
Lemma: l_all-nil
∀[P:Top]. ((∀x∈[].P[x]) ⇐⇒ True)
Lemma: l_all-cons
∀[T:Type]. ∀x:T. ∀L:T List. ∀[P:{a:T| (a ∈ [x / L])} ⟶ ℙ]. ((∀a∈[x / L].P[a]) ⇐⇒ P[x] ∧ (∀a∈L.P[a]))
Lemma: l_all_subtype
∀[A,B:Type]. ∀[L:A List]. ∀[P:B ⟶ ℙ]. (∀x∈L.P[x]) ⇒ (∀x∈L.P[x]) supposing A ⊆r B
Lemma: l_all-set
∀[T:Type]. ∀[P:T ⟶ ℙ]. ((∀x:T. SqStable(P[x])) ⇒ (∀L:{x:T| P[x]} List. (∀x∈L.P[x])))
Definition: mapfilter
mapfilter(f;P;L) == map(f;filter(P;L))
Lemma: mapfilter_wf
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[T':Type]. ∀[f:{x:T| ↑(P x)} ⟶ T']. (mapfilter(f;P;L) ∈ T' List)
Lemma: mapfilter-wf2
∀[A,B:Type]. ∀[L:A List]. ∀[P:{x:A| (x ∈ L)} ⟶ 𝔹]. ∀[f:{x:A| (x ∈ L) ∧ (↑(P x))} ⟶ B]. (mapfilter(f;P;L) ∈ B List)
Lemma: mapfilter_nil_lemma
∀P,f:Top. (mapfilter(f;P;[]) ~ [])
Lemma: mapfilter-reduce
∀[f:Top]. ∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹].
(mapfilter(f;P;L) ~ reduce(λx,y. if P x then [f x / y] else y fi ;[];L))
Lemma: member_map_filter
∀[T:Type]
∀P:T ⟶ 𝔹
∀[T':Type]
∀f:{x:T| ↑(P x)} ⟶ T'. ∀L:T List. ∀x:T'.
((x ∈ mapfilter(f;P;L)) ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))
Lemma: member-mapfilter-univ
∀[T:Type]
∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹.
∀[T':Type]
∀f:{x:T| (x ∈ L) c∧ (↑(P x))} ⟶ T'. ∀x:T'.
((x ∈ mapfilter(f;P;L)) ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))
Definition: member-mapfilter-witness
member-mapfilter-witness() == TERMOF{member-mapfilter-univ:o, 1:l, 1:l}
Lemma: member-mapfilter-witness_wf
member-mapfilter-witness() ∈ ∀[T:Type]
∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹.
∀[T':Type]
∀f:{x:T| (x ∈ L) c∧ (↑(P x))} ⟶ T'. ∀x:T'.
((x ∈ mapfilter(f;P;L)) ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))
Lemma: member-mapfilter
∀[T:Type]
∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹.
∀[T':Type]
∀f:{x:T| (x ∈ L) c∧ (↑(P x))} ⟶ T'. ∀x:T'.
((x ∈ mapfilter(f;P;L)) ⇐⇒ ∃y:T. ((y ∈ L) ∧ ((↑(P y)) c∧ (x = (f y) ∈ T'))))
Definition: filter-index
filter-index(P;L) ==
rec-case(L) of
[] => λi.i
u::v =>
r.λi.if (i =z 0) then 0 else (r (i - 1)) + if P u then 1 else 0 fi fi
Lemma: filter-index_wf
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. (filter-index(P;L) ∈ i:{i:ℕ||L||| ↑(P L[i])} ⟶ {j:ℕ||filter(P;L)||| filter(P;L)[\000Cj] = L[i] ∈ T} )
Lemma: member-filter3
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀x:{x:T| ↑(P x)} . ((x ∈ L) ⇒ (x ∈ filter(P;L)))
Definition: member-filter-witness
member-filter-witness(P;L;x) == λt.let i,_ = t in <filter-index(P;L) i, ⋅, ⋅>
Lemma: member-filter-witness_wf
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ∀[x:{x:T| ↑(P x)} ]. (member-filter-witness(P;L;x) ∈ (x ∈ L) ⇒ (x ∈ filter(P;L)))
Lemma: length-filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. (||filter(P;L)|| ≤ ||L||)
Lemma: sublist_filter
∀[T:Type]. ∀L1,L2:T List. ∀P:T ⟶ 𝔹. (L2 ⊆ filter(P;L1) ⇐⇒ L2 ⊆ L1 ∧ (∀x∈L2.↑(P x)))
Lemma: list_set_type
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ ℙ]. L ∈ {x:T| P[x]} List supposing (∀x∈L.P[x])
Lemma: sublist_filter_set_type
∀[T:Type]. ∀L1,L2:T List. ∀P:T ⟶ 𝔹. (L2 ⊆ L1 ⇒ L2 ⊆ filter(P;L1) supposing (∀x∈L2.↑(P x)))
Lemma: l_before_filter_set_type
∀[T:Type]. ∀l:T List. ∀P:T ⟶ 𝔹. ∀x,y:{x:T| ↑(P x)} . (x before y ∈ l ⇒ x before y ∈ filter(P;l))
Lemma: l_before_filter
∀[T:Type]. ∀l:T List. ∀P:T ⟶ 𝔹. ∀x,y:T. (x before y ∈ filter(P;l) ⇐⇒ (↑(P x)) ∧ (↑(P y)) ∧ x before y ∈ l)
Lemma: l_before_filter_subtype
∀[T:Type]
∀l:T List. ∀P:T ⟶ 𝔹. ∀x,y:T. ((↑(P x)) ⇒ (↑(P y)) ⇒ (x before y ∈ filter(P;l) ⇐⇒ x before y ∈ filter(P;l)))
Lemma: l_before_map
∀[A,B:Type].
∀l:A List. ∀f:A ⟶ B. ∀x,y:B.
(x before y ∈ map(f;l) ⇐⇒ ∃u,v:A. ((x = (f u) ∈ B) ∧ (y = (f v) ∈ B) ∧ u before v ∈ l))
Lemma: l_before_mapfilter
∀[A,B:Type].
∀l:A List. ∀P:A ⟶ 𝔹. ∀f:{a:A| ↑(P a)} ⟶ B. ∀x,y:B.
(x before y ∈ mapfilter(f;P;l)
⇐⇒ ∃u,v:A. ((↑(P u)) ∧ (↑(P v)) ∧ (x = (f u) ∈ B) ∧ (y = (f v) ∈ B) ∧ u before v ∈ l))
Lemma: no_repeats_filter
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List]. no_repeats(T;filter(P;l)) supposing no_repeats(T;l)
Lemma: no_repeats_filter2
∀[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)} ⟶ 𝔹]. no_repeats(T;filter(P;l)) supposing no_repeats(T;l)
Lemma: filter_is_empty
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. uiff(↑null(filter(P;L));∀[i:ℕ||L||]. (¬↑(P L[i])))
Definition: l_member!
(x ∈! l) == ∃i:ℕ. (i < ||l|| c∧ ((x = l[i] ∈ T) ∧ (∀j:ℕ. (j < ||l|| ⇒ (x = l[j] ∈ T) ⇒ (j = i ∈ ℕ)))))
Lemma: l_member!_wf
∀[T:Type]. ∀[l:T List]. ∀[x:T]. ((x ∈! l) ∈ ℙ)
Lemma: cons_member!
∀[T:Type]. ∀l:T List. ∀a,x:T. ((x ∈! [a / l]) ⇐⇒ ((x = a ∈ T) ∧ (¬(x ∈ l))) ∨ ((x ∈! l) ∧ (¬(x = a ∈ T))))
Lemma: nil_member!
∀[T:Type]. ∀x:T. ((x ∈! []) ⇐⇒ False)
Lemma: filter_is_singleton
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ∀[x:T].
(filter(P;L) = [x] ∈ (T List)) supposing ((∀y∈L.(↑P[y]) ⇒ (y = x ∈ T)) and (↑P[x]) and (x ∈! L))
Lemma: filter_is_singleton2
∀[T:Type]
∀P:T ⟶ 𝔹. ∀L:T List.
(||filter(P;L)|| = 1 ∈ ℤ ⇐⇒ ∃i:ℕ||L||. ((↑(P L[i])) ∧ (∀j:ℕ||L||. i = j ∈ ℤ supposing ↑(P L[j]))))
Lemma: sublist_filter_2
∀[T:Type]. ∀L1,L2:T List. ∀P:{x:T| (x ∈ L1)} ⟶ 𝔹. (L2 ⊆ filter(P;L1) ⇐⇒ L2 ⊆ L1 ∧ (∀x∈L2.↑(P x)))
Lemma: l_before-filter
∀[T:Type]
∀l:T List. ∀P:{x:T| (x ∈ l)} ⟶ 𝔹. ∀x,y:T. (x before y ∈ filter(P;l) ⇐⇒ x before y ∈ l ∧ (↑(P x)) ∧ (↑(P y)))
Definition: l_subset
l_subset(T;as;bs) == ∀x:T. ((x ∈ as) ⇒ (x ∈ bs))
Lemma: l_subset_wf
∀[T:Type]. ∀[as,bs:T List]. (l_subset(T;as;bs) ∈ ℙ)
Definition: l_contains
A ⊆ B == (∀a∈A.(a ∈ B))
Lemma: l_contains_wf
∀[T:Type]. ∀[A,B:T List]. (A ⊆ B ∈ ℙ)
Lemma: l_contains-member
∀[T:Type]. ∀A,B:T List. (A ⊆ B ⇒ {∀x:T. ((x ∈ A) ⇒ (x ∈ B))})
Lemma: l_contains_pos_length
∀[T:Type]. ∀[A,B:T List]. (0 < ||B||) supposing (0 < ||A|| and A ⊆ B)
Lemma: l_subset-l_contains
∀[T:Type]. ∀A,B:T List. (l_subset(T;A;B) ⇐⇒ A ⊆ B)
Lemma: l_subset_pos_length
∀[T:Type]. ∀[A,B:T List]. (0 < ||B||) supposing (0 < ||A|| and l_subset(T;A;B))
Lemma: l_subset_nil_left_true
∀[T:Type]. ∀[L:T List]. uiff(l_subset(T;[];L);True)
Lemma: l_subset_nil_left
∀[T:Type]. ∀[L:T List]. l_subset(T;[];L)
Lemma: l_subset_cons
∀[T:Type]. ∀x:T. ∀L1:T List. ∀[L2:T List]. (l_subset(T;[x / L1];L2) ⇐⇒ (x ∈ L2) ∧ l_subset(T;L1;L2))
Lemma: l_subset_right_cons_trivial
∀[T:Type]. ∀x:T. ∀L:T List. l_subset(T;L;[x / L])
Lemma: l_subset_nil_right
∀[T:Type]. ∀[L:T List]. (l_subset(T;L;[]) ⇐⇒ L = [] ∈ (T List))
Lemma: l_subset_refl
∀[T:Type]. ∀[L:T List]. l_subset(T;L;L)
Lemma: l_subset_append
∀[T:Type]. ∀[L:T List]. ∀L1,L2:T List. (l_subset(T;L1 @ L2;L) ⇐⇒ l_subset(T;L1;L) ∧ l_subset(T;L2;L))
Lemma: l_subset_append2
∀[T:Type]. ∀L1,L2,L1',L2':T List. ((l_subset(T;L1;L1') ∧ l_subset(T;L2;L2')) ⇒ l_subset(T;L1 @ L2;L1' @ L2'))
Lemma: sq_stable__l_subset
∀[T:Type]. ∀[L1:T List]. ∀L2:T List. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ SqStable(l_subset(T;L1;L2)))
Lemma: decidable__l_contains
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀A,B:T List. Dec(A ⊆ B)))
Lemma: l_contains_weakening
∀[T:Type]. ∀A,B:T List. A ⊆ B supposing A = B ∈ (T List)
Lemma: l_contains_transitivity
∀[T:Type]. ∀A,B,C:T List. (A ⊆ B ⇒ B ⊆ C ⇒ A ⊆ C)
Lemma: l_subset_transitivity
∀[T:Type]. ∀A,B,C:T List. (l_subset(T;A;B) ⇒ l_subset(T;B;C) ⇒ l_subset(T;A;C))
Lemma: l_subset_cons_same
∀[T:Type]. ∀x:T. ∀L1,L2:T List. (l_subset(T;L1;L2) ⇒ l_subset(T;[x / L1];[x / L2]))
Lemma: l_contains_nil
∀[T:Type]. ∀L:T List. [] ⊆ L
Lemma: nil-contains
∀[T:Type]. ∀L:T List. (L ⊆ [] ⇐⇒ ↑null(L))
Lemma: l_contains_cons
∀[T:Type]. ∀L:T List. ∀a:T. ∀as:T List. ([a / as] ⊆ L ⇐⇒ (a ∈ L) ∧ as ⊆ L)
Lemma: l_contains_singleton
∀[T:Type]. ∀L:T List. ∀a:T. ([a] ⊆ L ⇐⇒ (a ∈ L))
Lemma: l_contains_append
∀[T:Type]. ∀A,B:T List. A ⊆ A @ B
Lemma: l_contains-append
∀[T:Type]. ∀A,B,C:T List. (A @ B ⊆ C ⇐⇒ A ⊆ C ∧ B ⊆ C)
Lemma: l_contains_append2
∀[T:Type]. ∀A,B:T List. A ⊆ B @ A
Lemma: l_contains_append3
∀[T:Type]. ∀A,B,C:T List. (A ⊆ B ⇒ A ⊆ B @ C)
Lemma: l_contains-append4
∀[T:Type]. ∀A,B,C:T List. (A ⊆ C ⇒ A ⊆ B @ C)
Lemma: l_all-l_contains
∀[T:Type]. ∀[L1,L2:T List]. (L1 ⊆ L2 ⇒ (∀P:T ⟶ ℙ. ((∀x∈L2.P[x]) ⇒ (∀x∈L1.P[x]))))
Lemma: cons-l_contains
∀[T:Type]. ∀A,B:T List. ∀x:T. (A ⊆ B ⇒ A ⊆ [x / B])
Definition: l_disjoint
l_disjoint(T;l1;l2) == ∀x:T. (¬((x ∈ l1) ∧ (x ∈ l2)))
Lemma: l_disjoint_wf
∀[T:Type]. ∀[l,l':T List]. (l_disjoint(T;l;l') ∈ ℙ)
Lemma: l_disjoint_member
∀[T:Type]. ∀[l1,l2:T List]. ∀[x:T]. (¬(x ∈ l2)) supposing ((x ∈ l1) and l_disjoint(T;l1;l2))
Lemma: l_contains_disjoint
∀[T:Type]. ∀[A,B,C:T List]. (l_disjoint(T;B;C)) supposing (l_disjoint(T;A;C) and B ⊆ A)
Lemma: l_disjoint_append
∀[T:Type]. ∀[a,b,c:T List]. uiff(l_disjoint(T;a;b @ c);l_disjoint(T;a;b) ∧ l_disjoint(T;a;c))
Lemma: l_disjoint_append2
∀[T:Type]. ∀[a,b,c:T List]. uiff(l_disjoint(T;b @ c;a);l_disjoint(T;b;a) ∧ l_disjoint(T;c;a))
Lemma: l_disjoint-symmetry
∀[T:Type]. ∀[a,b:T List]. uiff(l_disjoint(T;b;a);l_disjoint(T;a;b))
Lemma: l_disjoint_singleton
∀[T:Type]. ∀[a:T List]. ∀[x:T]. uiff(l_disjoint(T;a;[x]);¬(x ∈ a))
Lemma: l_disjoint_singleton2
∀[T:Type]. ∀[a:T List]. ∀[x:T]. uiff(l_disjoint(T;[x];a);¬(x ∈ a))
Lemma: l_disjoint_nil
∀[A:Type]. ∀[L:A List]. l_disjoint(A;[];L)
Lemma: l_disjoint_nil2
∀[A:Type]. ∀[L:A List]. l_disjoint(A;L;[])
Lemma: l_disjoint_nil_iff
∀[A:Type]. ∀[L:A List]. (l_disjoint(A;L;[]) ⇐⇒ True)
Lemma: l_disjoint_cons
∀[T:Type]. ∀[a,b:T List]. ∀[x:T]. uiff(l_disjoint(T;a;[x / b]);(¬(x ∈ a)) ∧ l_disjoint(T;a;b))
Lemma: l_disjoint_cons2
∀[T:Type]. ∀[a,b:T List]. ∀[x:T]. uiff(l_disjoint(T;[x / b];a);(¬(x ∈ a)) ∧ l_disjoint(T;b;a))
Lemma: no_repeats_append
∀[T:Type]. ∀[l1,l2:T List]. l_disjoint(T;l1;l2) supposing no_repeats(T;l1 @ l2)
Lemma: no_repeats-sublist
∀[T:Type]. ∀[L,L':T List]. (no_repeats(T;L')) supposing (L' ⊆ L and no_repeats(T;L))
Lemma: no_repeats-subtype
∀[T,S:Type]. ∀[L:S List]. no_repeats(S;L) supposing no_repeats(T;L) supposing S ⊆r T
Lemma: no_repeats-strong-subtype
∀[T,S:Type]. ∀[L:S List]. (no_repeats(T;L)) supposing (no_repeats(S;L) and strong-subtype(S;T))
Lemma: no_repeats-settype
∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[L:{x:T| P[x]} List]. uiff(no_repeats(T;L);no_repeats({x:T| P[x]} ;L))
Lemma: no_repeats-l_member!
∀[T:Type]. ∀l:T List. ∀x:T. ((x ∈ l) ⇐⇒ (x ∈! l)) supposing no_repeats(T;l)
Lemma: member-firstn-implies-member
∀[T:Type]. ∀x:T. ∀L:T List. ∀n:ℤ. ((x ∈ firstn(n;L)) ⇒ (x ∈ L))
Lemma: member-nth-tl-implies-member
∀[T:Type]. ∀x:T. ∀n:ℕ. ∀L:T List. ((x ∈ nth_tl(n;L)) ⇒ (x ∈ L))
Lemma: no_repeats-firstn
∀[T:Type]. ∀[l:T List]. ∀[n:ℤ]. no_repeats(T;firstn(n;l)) supposing no_repeats(T;l)
Lemma: no_repeats_append_iff
∀[T:Type]. ∀[l1,l2:T List]. uiff(no_repeats(T;l1 @ l2);l_disjoint(T;l1;l2) ∧ no_repeats(T;l1) ∧ no_repeats(T;l2))
Lemma: no_repeats-append
∀[T:Type]. ∀[L1,L2:T List]. uiff(no_repeats(T;L1 @ L2);{no_repeats(T;L1) ∧ no_repeats(T;L2) ∧ l_disjoint(T;L1;L2)})
Lemma: no_repeats-single
∀[T:Type]. ∀[x:T]. no_repeats(T;[x])
Lemma: length-one-member
∀[T:Type]. ∀[L:T List]. ∀[x,y:T]. (x = y ∈ T) supposing ((y ∈ L) and (x ∈ L)) supposing ||L|| = 1 ∈ ℤ
Lemma: length-one-iff
∀[T:Type]. ∀[L:T List].
uiff(||L|| = 1 ∈ ℤ;(∀[x,y:T]. (x = y ∈ T) supposing ((y ∈ L) and (x ∈ L))) ∧ no_repeats(T;L) ∧ 0 < ||L||)
Lemma: list-is-singleton-iff
∀[T:Type]. ∀L:T List. ∀x:T. (L = [x] ∈ (T List) ⇐⇒ no_repeats(T;L) ∧ (∀f:T. ((f ∈ L) ⇐⇒ f = x ∈ T)))
Lemma: l_contains-cons
∀[T:Type]
∀u:T. ∀v,bs:T List.
([u / v] ⊆ bs ⇐⇒ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ v ⊆ cs @ ds)) supposing
(no_repeats(T;bs) and
no_repeats(T;[u / v]))
Lemma: l_contains-no_repeats-length
∀[T:Type]. ∀[as,bs:T List]. (||as|| ≤ ||bs||) supposing (as ⊆ bs and no_repeats(T;as))
Lemma: no_repeats-same-length-l_contains
∀[T:Type]. ∀as,bs:T List. (no_repeats(T;as) ⇒ (||as|| = ||bs|| ∈ ℤ) ⇒ as ⊆ bs ⇒ bs ⊆ as)
Lemma: mapfilter-nil
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ∀[f:Top]. mapfilter(f;P;L) ~ [] supposing (∀x∈L.¬↑(P x))
Lemma: mapfilter-not-nil
∀[T,B:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ∀[f:{x:{x:T| (x ∈ L)} | ↑(P x)} ⟶ B].
¬(mapfilter(f;P;L) = [] ∈ (B List)) supposing (∃x∈L. ↑(P x))
Lemma: mapfilter-pos-length
∀[T,B:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ∀[f:{x:{x:T| (x ∈ L)} | ↑(P x)} ⟶ B].
0 < ||mapfilter(f;P;L)|| supposing (∃x∈L. ↑(P x))
Lemma: mapfilter-singleton
∀[x,P,f:Top]. (mapfilter(f;P;[x]) ~ map(f;if P x then [x] else [] fi ))
Lemma: mapfilter-append
∀[as,bs,P,f:Top]. (mapfilter(f;P;as @ bs) ~ mapfilter(f;P;as) @ mapfilter(f;P;bs))
Lemma: mapfilter-cons
∀[u,v,P,f:Top]. (mapfilter(f;P;[u / v]) ~ mapfilter(f;P;[u]) @ mapfilter(f;P;v))
Lemma: mapfilter-contains
∀[T,S:Type]. ∀as,bs:T List. ∀P:T ⟶ 𝔹. ∀f:{x:T| ↑(P x)} ⟶ S. (as ⊆ bs ⇒ mapfilter(f;P;as) ⊆ mapfilter(f;P;bs))
Lemma: filter-contains
∀[T:Type]. ∀as:T List. ∀P:T ⟶ 𝔹. filter(P;as) ⊆ as
Lemma: mapfilter-mapfilter1
∀[f1,P2,f2,P1,as:Top]. (mapfilter(f1;P1;mapfilter(f2;P2;as)) ~ mapfilter(f1 o f2;λa.((P2 a) ∧b (P1 (f2 a)));as))
Lemma: mapfilter-mapfilter
∀[f1,as,P2,f2,P1:Top]. (mapfilter(f1;P1;mapfilter(f2;P2;as)) ~ mapfilter(f1 o f2;λa.((P2 a) ∧b (P1 (f2 a)));as))
Lemma: mapfilter-wf
∀[T,U:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ L) ∧ (↑P[x])} ⟶ U]. (mapfilter(f;P;L) ∈ U List)
Lemma: map-as-mapfilter
∀[f:Top]. ∀[L:Top List]. (map(f;L) ~ mapfilter(f;λx.tt;L))
Lemma: filter-as-mapfilter
∀[L,P:Top]. (filter(P;L) ~ mapfilter(λx.x;P;L))
Lemma: reduce-mapfilter
∀[f1,x:Top]. ∀[T,A:Type]. ∀[as:T List]. ∀[P:{a:T| (a ∈ as)} ⟶ 𝔹]. ∀[f2:{a:T| (a ∈ as) ∧ (↑(P a))} ⟶ A].
(reduce(f1;x;mapfilter(f2;P;as)) ~ reduce(λu,z. if P u then f1 (f2 u) z else z fi ;x;as))
Lemma: null-mapfilter
∀P,f,L:Top. (null(mapfilter(f;P;L)) ~ null(filter(P;L)))
Lemma: length-mapfilter
∀[l,f,P:Top]. (||mapfilter(f;P;l)|| ~ ||filter(P;l)||)
Lemma: l_all-map
∀[T,A:Type]. ∀as:T List. ∀f:T ⟶ A. ∀P:A ⟶ ℙ. ((∀x∈map(f;as).P[x]) ⇐⇒ (∀x∈as.P[f x]))
Lemma: l_all-mapfilter
∀[T,A:Type].
∀as:T List. ∀p:{a:T| (a ∈ as)} ⟶ 𝔹. ∀f:{a:T| (a ∈ as) ∧ (↑(p a))} ⟶ A. ∀P:A ⟶ ℙ.
((∀x∈mapfilter(f;p;as).P[x]) ⇐⇒ (∀x∈as.(↑(p x)) ⇒ P[f x]))
Lemma: listp-not-nil
∀[A:Type]. ∀[L:A List+]. (¬(L = [] ∈ (A List)))
Lemma: listp_properties
∀[A:Type]. ∀[l:A List+]. (||l|| ≥ 1 )
Definition: tlp
tlp(L) == tl(L)
Lemma: tlp_wf
∀[A:Type]. ∀[L:A List+]. (tlp(L) ∈ A List)
Definition: hdp
hdp(L) == hd(L)
Lemma: hdp_wf
∀[a:Type]. ∀[L:a List+]. (hdp(L) ∈ a)
Lemma: member-exists
∀[T:Type]. ∀L:T List. (∃x:T. (x ∈ L) ⇐⇒ ¬(L = [] ∈ (T List)))
Lemma: member-exists2
∀[T:Type]. ∀L:T List. (∃x:T. (x ∈ L) ⇐⇒ 0 < ||L||)
Lemma: hd_wf_listp
∀[A:Type]. ∀[l:A List+]. (hd(l) ∈ A)
Lemma: comb_for_hd_wf_listp
λA,l,z. hd(l) ∈ A:Type ⟶ l:A List+ ⟶ (↓True) ⟶ A
Definition: iseg
l1 ≤ l2 == ∃l:T List. (l2 = (l1 @ l) ∈ (T List))
Lemma: iseg_wf
∀[T:Type]. ∀[l1,l2:T List]. (l1 ≤ l2 ∈ ℙ)
Lemma: cons_iseg
∀[T:Type]. ∀a,b:T. ∀l1,l2:T List. ([a / l1] ≤ [b / l2] ⇐⇒ (a = b ∈ T) ∧ l1 ≤ l2)
Lemma: cons_iseg_not_null
∀[T:Type]. ∀u:T. ∀L,v:T List. (L ≤ [u / v] ⇒ (¬↑null(L)) ⇒ (∃K:T List. ((L = [u / K] ∈ (T List)) ∧ K ≤ v)))
Lemma: iseg_transitivity
∀[T:Type]. ∀l1,l2,l3:T List. (l1 ≤ l2 ⇒ l2 ≤ l3 ⇒ l1 ≤ l3)
Lemma: iseg_append
∀[T:Type]. ∀l1,l2,l3:T List. (l1 ≤ l2 ⇒ l1 ≤ l2 @ l3)
Lemma: iseg_extend
∀[T:Type]. ∀l1:T List. ∀v:T. ∀l2:T List. (l1 ≤ l2 ⇒ l1 @ [v] ≤ l2 supposing ||l1|| < ||l2|| c∧ (l2[||l1||] = v ∈ T))
Lemma: firstn_is_iseg
∀[T:Type]. ∀L1,L2:T List. (L1 ≤ L2 ⇐⇒ ∃n:ℕ||L2|| + 1. (L1 = firstn(n;L2) ∈ (T List)))
Lemma: iseg-iff-firstn
∀[T:Type]. ∀L1,L2:T List. (L1 ≤ L2 ⇐⇒ (||L1|| ≤ ||L2||) ∧ (L1 = firstn(||L1||;L2) ∈ (T List)))
Lemma: decidable__iseg
∀[T:Type]. ((∀x,y:T. Dec(x = y ∈ T)) ⇒ (∀L1,L2:T List. Dec(L1 ≤ L2)))
Lemma: iseg_transitivity2
∀[T:Type]. ∀l1,l2,l3:T List. (l2 ≤ l3 ⇒ l1 ≤ l2 ⇒ l1 ≤ l3)
Lemma: comb_for_iseg_wf
λT,l1,l2,z. l1 ≤ l2 ∈ T:Type ⟶ l1:(T List) ⟶ l2:(T List) ⟶ (↓True) ⟶ ℙ
Lemma: iseg_weakening
∀[T:Type]. ∀l:T List. l ≤ l
Lemma: iseg_weakening2
∀[T:Type]. ∀l1,l2:T List. l1 ≤ l2 supposing l1 = l2 ∈ (T List)
Lemma: nil_iseg
∀[T:Type]. ∀l:T List. [] ≤ l
Lemma: iseg_select
∀[T:Type]. ∀l1,l2:T List. (l1 ≤ l2 ⇐⇒ (||l1|| ≤ ||l2||) c∧ (∀i:ℕ. l1[i] = l2[i] ∈ T supposing i < ||l1||))
Lemma: iseg_implies_member
∀[T:Type]. ∀l1,l2:T List. (l1 ≤ l2 ⇒ {∀x:T. ((x ∈ l1) ⇒ (x ∈ l2))})
Lemma: iseg_member
∀[T:Type]. ∀l1,l2:T List. ∀x:T. (l1 ≤ l2 ⇒ (x ∈ l1) ⇒ (x ∈ l2))
Lemma: iseg_nil
∀[T:Type]. ∀L:T List. (L ≤ [] ⇐⇒ ↑null(L))
Lemma: filter_iseg
∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L2,L1:T List. (L1 ≤ L2 ⇒ filter(P;L1) ≤ filter(P;L2))
Lemma: filter_iseg2
∀[T:Type]. ∀L2,L1:T List. ∀P:{x:T| (x ∈ L2)} ⟶ 𝔹. (L1 ≤ L2 ⇒ filter(P;L1) ≤ filter(P;L2))
Lemma: iseg_filter
∀[T:Type]
∀P:T ⟶ 𝔹. ∀L_1,L_2:T List. (L_2 ≤ filter(P;L_1) ⇒ (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
Lemma: iseg_filter_last
∀[T:Type]
∀P:T ⟶ 𝔹. ∀L_1,L_2:T List.
(0 < ||L_2||
⇒ L_2 ≤ filter(P;L_1)
⇒ (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 = filter(P;L_3) ∈ (T List)) ∧ 0 < ||L_3|| ∧ (last(L_2) = last(L_3) ∈ T))))
Lemma: iseg_filter2
∀[T:Type]
∀L_1,L_2:T List. ∀P:{x:T| (x ∈ L_1)} ⟶ 𝔹.
(L_2 ≤ filter(P;L_1) ⇒ (∃L_3:T List. (L_3 ≤ L_1 ∧ (L_2 = filter(P;L_3) ∈ (T List)))))
Lemma: iseg_append0
∀[T:Type]. ∀l1,l2:T List. l1 ≤ l1 @ l2
Lemma: iseg_length
∀[T:Type]. ∀[l1,l2:T List]. ||l1|| ≤ ||l2|| supposing l1 ≤ l2
Lemma: iseg_is_sublist
∀[T:Type]. ∀L_1,L_2:T List. (L_1 ≤ L_2 ⇒ L_1 ⊆ L_2)
Lemma: iseg-l_contains
∀[T:Type]. ∀x,y:T List. (x ≤ y ⇒ x ⊆ y)
Lemma: sublist_iseg
∀[T:Type]. ∀L1,L2:T List. (L1 ≤ L2 ⇒ L1 ⊆ L2)
Lemma: l_before_iseg
∀[T:Type]. ∀L1,L2:T List. ∀x,y:T. (L1 ≤ L2 ⇒ x before y ∈ L1 ⇒ x before y ∈ L2)
Lemma: select-nthtl
∀[n:ℕ]. ∀[L:Top List]. (L[n] ~ hd(nth_tl(n;L)))
Lemma: iseg_select2
∀[T:Type]. ∀[l1,l2:T List]. {∀[i:ℕ||l1||]. (l1[i] = l2[i] ∈ T)} supposing l1 ≤ l2
Definition: compat
l1 || l2 == l1 ≤ l2 ∨ l2 ≤ l1
Lemma: compat_wf
∀[T:Type]. ∀[l1,l2:T List]. (l1 || l2 ∈ ℙ)
Lemma: common_iseg_compat
∀[T:Type]. ∀l,l1,l2:T List. (l1 ≤ l ⇒ l2 ≤ l ⇒ l1 || l2)
Lemma: iseg_same_length
∀[T:Type]. ∀[L1,L2:T List]. (L1 = L2 ∈ (T List)) supposing ((||L1|| = ||L2|| ∈ ℤ) and L1 ≤ L2)
Lemma: iseg_ge_length
∀[T:Type]. ∀[L1,L2:T List]. (L1 = L2 ∈ (T List)) supposing ((||L1|| ≥ ||L2|| ) and L1 ≤ L2)
Definition: fseg
fseg(T;L1;L2) == ∃L:T List. (L2 = (L @ L1) ∈ (T List))
Lemma: fseg_wf
∀[T:Type]. ∀[L1,L2:T List]. (fseg(T;L1;L2) ∈ ℙ)
Lemma: nth_tl_is_fseg
∀[T:Type]. ∀L1,L2:T List. (fseg(T;L1;L2) ⇐⇒ ∃n:ℕ||L2|| + 1. (L1 = nth_tl(n;L2) ∈ (T List)))
Lemma: last-lemma-sq
∀[T:Type]. ∀[L:T List]. L ~ firstn(||L|| - 1;L) @ [last(L)] supposing ¬↑null(L)
Lemma: last_induction
∀[T:Type]. ∀[Q:(T List) ⟶ ℙ]. (Q[[]] ⇒ (∀ys:T List. ∀y:T. (Q[ys] ⇒ Q[ys @ [y]])) ⇒ {∀zs:T List. Q[zs]})
Lemma: last_induction_accum
∀[T:Type]. ∀[Q:(T List) ⟶ ℙ]. (Q[[]] ⇒ (∀[ys:T List]. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))) ⇒ {∀zs:T List. Q[zs]})
Lemma: filter-split-length
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ((||filter(λx.P[x];L)|| + ||filter(λx.(¬bP[x]);L)||) = ||L|| ∈ ℤ)
Lemma: filter-length-less
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ||filter(λx.P[x];L)|| < ||L|| supposing ∃x:T. ((x ∈ L) ∧ (¬↑P[x]))
Lemma: accum_induction
∀[T:Type]. ∀[Q:(T List) ⟶ ℙ]. ((∀[ys:T List]. (Q[ys] ⇒ (∀y:T. Q[ys @ [y]]))) ⇒ Q[[]] ⇒ {∀zs:T List. Q[zs]})
Lemma: non_null_iff_length
∀[L:Top List]. uiff(¬↑null(L);0 < ||L||)
Lemma: null-length-zero
∀[L:Top List]. null(L) = (||L|| =z 0)
Lemma: null-segment
∀[T:Type]. ∀[as:T List]. ∀[i:{0...||as||}]. ∀[j:{i...||as||}]. null(as[i..j-]) = (i =z j)
Lemma: before_last_or
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ ((x = last(L) ∈ T) ∨ x before last(L) ∈ L))
Lemma: last-cons
∀[x:Top]. ∀[as:Top List]. (last([x / as]) ~ if null(as) then x else last(as) fi )
Lemma: last_append
∀[A,B:Top List]. last(A @ B) ~ last(B) supposing ¬↑null(B)
Lemma: last_append2
∀[A,B:Top List]. last(A @ B) ~ last(B) supposing 0 < ||B||
Lemma: last_singleton
∀[T:Type]. ∀[x:T]. (last([x]) = x ∈ T)
Lemma: last_singleton2
∀[x:Top]. (last([x]) ~ x)
Lemma: last_singleton_append
∀[x:Top]. ∀y:Top List. (last(y @ [x]) ~ x)
Definition: set-equal
set-equal(T;x;y) == ∀t:T. ((t ∈ x) ⇐⇒ (t ∈ y))
Lemma: set-equal_wf
∀[T:Type]. ∀[x,y:T List]. (set-equal(T;x;y) ∈ ℙ)
Lemma: set-equal-reflex
∀[T:Type]. ∀[x:T List]. set-equal(T;x;x)
Lemma: set-equal-equiv
∀[T:Type]. EquivRel(T List;x,y.set-equal(T;x;y))
Lemma: set-equal-permute
∀[T:Type]. ∀as,bs:T List. set-equal(T;as @ bs;bs @ as)
Lemma: set-equal-nil
∀[T:Type]. ∀bs:T List. (set-equal(T;[];bs) ⇐⇒ ↑null(bs))
Lemma: set-equal-nil2
∀[T:Type]. ∀bs:T List. (set-equal(T;bs;[]) ⇐⇒ ↑null(bs))
Lemma: set-equal-l_contains
∀[T:Type]. ∀x,y:T List. (set-equal(T;x;y) ⇐⇒ x ⊆ y ∧ y ⊆ x)
Lemma: set-equal-cons
∀[T:Type]
∀u:T. ∀v,bs:T List.
(set-equal(T;[u / v];bs) ⇐⇒ ∃cs,ds:T List. ((bs = (cs @ [u / ds]) ∈ (T List)) ∧ set-equal(T;v;cs @ ds))) supposing
(no_repeats(T;bs) and
no_repeats(T;[u / v]))
Lemma: set-equal-cons2
∀[T:Type]
∀eq:EqDecider(T). ∀u:T. ∀v,bs:T List.
(set-equal(T;[u / v];bs) ⇐⇒ (u ∈ bs) ∧ set-equal(T;filter(λx.(¬b(eq x u));v);filter(λx.(¬b(eq x u));bs)))
Lemma: set-equal-no_repeats-length
∀[T:Type]. ∀[as,bs:T List].
(||as|| = ||bs|| ∈ ℤ) supposing (set-equal(T;as;bs) and no_repeats(T;bs) and no_repeats(T;as))
Lemma: no_repeats-length-le-by-relation
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
∀[as:A List]. ∀[bs:B List]. (||as|| ≤ ||bs||) supposing ((∀a∈as.(∃b∈bs. R a b)) and no_repeats(A;as))
supposing ∀a1,a2:A. ∀b:B. ((R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A))
Lemma: no_repeats-length-equal-by-relation
∀[A,B:Type]. ∀[as:A List]. ∀[bs:B List].
(||as|| = ||bs|| ∈ ℤ) supposing
((∃R:A ⟶ B ⟶ ℙ
((∀a1,a2:A. ∀b:B. ((a1 ∈ as) ⇒ (a2 ∈ as) ⇒ (b ∈ bs) ⇒ (R a1 b) ⇒ (R a2 b) ⇒ (a1 = a2 ∈ A)))
∧ (∀b1,b2:B. ∀a:A. ((b1 ∈ bs) ⇒ (b2 ∈ bs) ⇒ (a ∈ as) ⇒ (R a b1) ⇒ (R a b2) ⇒ (b1 = b2 ∈ B)))
∧ (∀a∈as.(∃b∈bs. R a b))
∧ (∀b∈bs.(∃a∈as. R a b)))) and
no_repeats(A;as) and
no_repeats(B;bs))
Lemma: list_accum-mapfilter
∀[T,U,A:Type]. ∀[f:A ⟶ U ⟶ A]. ∀[L:T List]. ∀[p:{a:T| (a ∈ L)} ⟶ 𝔹]. ∀[g:{a:T| (a ∈ L) ∧ (↑(p a))} ⟶ U]. ∀[x:A].
(accumulate (with value a and list item x):
f[a;x]
over list:
mapfilter(g;p;L)
with starting value:
x) ~ accumulate (with value a and list item x):
if p x then f[a;g x] else a fi
over list:
L
with starting value:
x))
Lemma: list_accum_functionality
∀[T,A:Type]. ∀[f,g:T ⟶ A ⟶ T]. ∀[L:A List]. ∀[y,z:T].
(accumulate (with value x and list item a):
f[x;a]
over list:
L
with starting value:
y)
= accumulate (with value x and list item a):
g[x;a]
over list:
L
with starting value:
z)
∈ T) supposing
((y = z ∈ T) and
(∀L':A List. ∀a:A.
(L' @ [a] ≤ L
⇒ (f[accumulate (with value x and list item a):
f[x;a]
over list:
L'
with starting value:
y);a]
= g[accumulate (with value x and list item a):
f[x;a]
over list:
L'
with starting value:
y);a]
∈ T))))
Lemma: list_accum_as_reduce
∀[T,A:Type]. ∀[f:A ⟶ T ⟶ A].
∀[L:T List]. ∀[a0:A].
(accumulate (with value a and list item x):
f[a;x]
over list:
L
with starting value:
a0)
= reduce(λx,a. f[a;x];a0;L)
∈ A)
supposing ∀a:A. ∀x1,x2:T. (f[f[a;x1];x2] = f[f[a;x2];x1] ∈ A)
Lemma: list_accum_permute1
∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
(∀[L:T List]. ∀[x:T]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
[x / L]
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
L @ [x]
with starting value:
n)
∈ A)) supposing
(Assoc(A;λx,y. f[x;y]) and
Comm(A;λx,y. f[x;y]))
Lemma: list_accum_permute
∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
(∀[as,bs:T List]. ∀[n:A].
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as @ bs
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs @ as
with starting value:
n)
∈ A)) supposing
(Assoc(A;λx,y. f[x;y]) and
Comm(A;λx,y. f[x;y]))
Lemma: list_accum_set-equal
∀[T,A:Type]. ∀[g:T ⟶ A]. ∀[f:A ⟶ A ⟶ A].
(∀[as,bs:T List].
(∀[n:A]
(accumulate (with value a and list item z):
f[a;g[z]]
over list:
as
with starting value:
n)
= accumulate (with value a and list item z):
f[a;g[z]]
over list:
bs
with starting value:
n)
∈ A)) supposing
(no_repeats(T;bs) and
no_repeats(T;as) and
set-equal(T;as;bs))) supposing
(Assoc(A;λx,y. f[x;y]) and
Comm(A;λx,y. f[x;y]))
Lemma: list_accum_is_reduce
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
(∀[as:A List]. ∀[n:A].
(accumulate (with value a and list item b):
f[a;b]
over list:
as
with starting value:
n)
= reduce(f;n;as)
∈ A)) supposing
(Assoc(A;λx,y. f[x;y]) and
Comm(A;λx,y. f[x;y]))
Lemma: list_accum_equality
∀[T,A,B,C:Type]. ∀[f:A ⟶ T ⟶ A]. ∀[g:B ⟶ T ⟶ B]. ∀[F:A ⟶ C]. ∀[G:B ⟶ C].
∀[L:T List]. ∀[a0:A]. ∀[b0:B].
F[accumulate (with value a and list item x):
f[a;x]
over list:
L
with starting value:
a0)]
= G[accumulate (with value b and list item x):
g[b;x]
over list:
L
with starting value:
b0)]
∈ C
supposing F[a0] = G[b0] ∈ C
supposing ∀a:A. ∀b:B. ∀x:T. (((F a) = (G b) ∈ C) ⇒ (F[f[a;x]] = G[g[b;x]] ∈ C))
Lemma: list_accum_invariant
∀[T,A:Type].
∀f:A ⟶ T ⟶ A
∀[P:A ⟶ ℙ]
∀L:T List. ∀a:A.
(P[a]
⇒ (∀a:A. ∀x:T. (P[a] ⇒ P[f[a;x]]))
⇒ P[accumulate (with value a and list item x):
f[a;x]
over list:
L
with starting value:
a)])
Lemma: list_accum_invariant2
∀[T,A:Type].
∀f:A ⟶ T ⟶ A
∀[P:A ⟶ ℙ]
∀L:T List. ∀a:A.
(P[a]
⇒ (∀a:A. ∀x:T. ((x ∈ L) ⇒ P[a] ⇒ P[f[a;x]]))
⇒ P[accumulate (with value a and list item x):
f[a;x]
over list:
L
with starting value:
a)])
Lemma: list_accum_invariant3
∀[T,A:Type].
∀f:A ⟶ T ⟶ A
∀[P:A ⟶ (T List) ⟶ ℙ]
∀L:T List. ∀a:A.
(P[a;[]]
⇒ (∀a:A. ∀x:T. ∀L':T List. (L' @ [x] ≤ L ⇒ P[a;L'] ⇒ P[f[a;x];L' @ [x]]))
⇒ P[accumulate (with value a and list item x):
f[a;x]
over list:
L
with starting value:
a);L])
Lemma: combine-list-flip
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
(∀[as:A List]. ∀[a1,a2:A].
(combine-list(x,y.f[x;y];[a1; [a2 / as]]) = combine-list(x,y.f[x;y];[a2; [a1 / as]]) ∈ A)) supposing
(Comm(A;λx,y. f[x;y]) and
Assoc(A;λx,y. f[x;y]))
Lemma: combine-list-append
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
(∀[as,bs:A List].
combine-list(x,y.f[x;y];as @ bs) = combine-list(x,y.f[x;y];bs @ as) ∈ A supposing 0 < ||as @ bs||) supposing
(Comm(A;λx,y. f[x;y]) and
Assoc(A;λx,y. f[x;y]))
Lemma: combine-list-as-reduce
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
(∀[L:A List]
combine-list(x,y.f[x;y];L) = outl(reduce(λx,y. case y of inl(z) => inl f[x;z] | inr(z) => inl x;inr ⋅ ;L)) ∈ A
supposing 0 < ||L||) supposing
(Comm(A;λx,y. f[x;y]) and
Assoc(A;λx,y. f[x;y]))
Lemma: combine-combine-list-left
∀[T:Type]
∀f:T ⟶ T ⟶ T. ∀L:T List.
(∀a:T. uiff(f[a;combine-list(x,y.f[x;y];L)] = a ∈ T;(∀b∈L.f[a;b] = a ∈ T))) supposing
(0 < ||L|| and
(∀x,y,z:T. (f[x;f[y;z]] = x ∈ T ⇐⇒ (f[x;y] = x ∈ T) ∧ (f[x;z] = x ∈ T))))
Lemma: combine-combine-list-right
∀[T:Type]
∀f:T ⟶ T ⟶ T. ∀L:T List.
((∀x,y,z:T. (f[x;f[y;z]] = f[y;z] ∈ T ⇐⇒ (f[x;y] = y ∈ T) ∨ (f[x;z] = z ∈ T)))
⇒ 0 < ||L||
⇒ (∀a:T. (f[a;combine-list(x,y.f[x;y];L)] = combine-list(x,y.f[x;y];L) ∈ T ⇐⇒ (∃b∈L. f[a;b] = b ∈ T))))
Lemma: combine_list_single_lemma
∀u,f:Top. (combine-list(x,y.f[x;y];[u]) ~ u)
Lemma: imax-list-append
∀[as,bs:ℤ List]. imax-list(as @ bs) = imax-list(bs @ as) ∈ ℤ supposing 0 < ||as @ bs||
Lemma: imax-list-strict-lb
∀[L:ℤ List]. ∀[a:ℤ]. uiff(imax-list(L) < a;(∀b∈L.b < a)) supposing 0 < ||L||
Lemma: imax-list-subset
∀[L,L':ℤ List]. (imax-list(L) ≤ imax-list(L')) supposing (l_subset(ℤ;L;L') and 0 < ||L||)
Lemma: imax-list_functionality
∀[L,L':ℤ List]. (imax-list(L) = imax-list(L') ∈ ℤ) supposing (set-equal(ℤ;L;L') and 0 < ||L||)
Lemma: imax-list-append2
∀[as,bs:ℤ List]. (imax-list(as @ bs) = imax(imax-list(as);imax-list(bs)) ∈ ℤ) supposing (0 < ||bs|| and 0 < ||as||)
Lemma: imax-list-as-reduce
∀[L:ℤ List]
imax-list(L) = outl(reduce(λx,y. case y of inl(z) => inl imax(x;z) | inr(z) => inl x;inr ⋅ ;L)) ∈ ℤ supposing 0 < ||L|\000C|
Lemma: imax-list-eq-implies
∀L:ℤ List. ∀a:ℤ. ((a ∈ L)) supposing ((imax-list(L) = a ∈ ℤ) and 0 < ||L||)
Lemma: imax-list-unique2
∀L:ℤ List. ∀a:ℤ. uiff((||L|| > 0) ∧ (imax-list(L) = a ∈ ℤ);(∀b∈L.b ≤ a) ∧ (a ∈ L))
Lemma: imax-list-filter-member
∀L:ℤ List. ∀P:ℤ ⟶ 𝔹. (imax-list(filter(P;L)) ∈ L) supposing ¬(filter(P;L) = [] ∈ (ℤ List))
Definition: list-max-aux
list-max-aux(x.f[x];L) ==
accumulate (with value a and list item x):
eval n = f[x] in
case a of inl(p) => if fst(p) <z n then inl <n, x> else a fi | inr(q) => inl <n, x>
over list:
L
with starting value:
inr ⋅ )
Lemma: list-max-aux_wf
∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. (list-max-aux(x.f[x];L) ∈ i:ℤ × {x:T| f[x] = i ∈ ℤ} + Top)
Lemma: list-max-aux-property
∀[T:Type]
∀f:T ⟶ ℤ. ∀L:T List.
(↑isl(list-max-aux(x.f[x];L)))
∧ let n,x = outl(list-max-aux(x.f[x];L))
in (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n)
supposing 0 < ||L||
Definition: list-max
list-max(x.f[x];L) == outl(list-max-aux(x.f[x];L))
Lemma: list-max_wf
∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. list-max(x.f[x];L) ∈ i:ℤ × {x:T| f[x] = i ∈ ℤ} supposing 0 < ||L||
Lemma: list-max-property
∀[T:Type]
∀f:T ⟶ ℤ. ∀L:T List. let n,x = list-max(x.f[x];L) in (x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n) supposing 0 < ||L||
Lemma: list-max-property2
∀[T:Type]
∀f:T ⟶ ℤ. ∀L:T List.
∀n:ℤ. ∀x:T. {(x ∈ L) ∧ (f[x] = n ∈ ℤ) ∧ (∀y∈L.f[y] ≤ n)} supposing list-max(x.f[x];L) = <n, x> ∈ (ℤ × T)
supposing 0 < ||L||
Lemma: list-max-map
∀[T,A:Type]. ∀[g:A ⟶ T]. ∀[f:T ⟶ ℤ]. ∀[L:A List].
list-max(x.f[x];map(g;L)) = ((λp.<fst(p), g (snd(p))>) list-max(x.f[g x];L)) ∈ (i:ℤ × {x:T| f[x] = i ∈ ℤ} )
supposing 0 < ||L||
Lemma: list-max-imax-list
∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. (fst(list-max(x.f[x];L))) = imax-list(map(λx.f[x];L)) ∈ ℤ supposing 0 < ||L||
Lemma: maximal-in-list
∀[A:Type]. ∀f:A ⟶ ℤ. ∀L:A List. (∃a∈L. (∀x∈L.(f x) ≤ (f a))) supposing 0 < ||L||
Definition: mklist-general
mklist-general(n;h) == primrec(n;[];λm,rl. (rl @ [h rl]))
Lemma: mklist-general_wf
∀[T3:Type]. ∀[n:ℕ]. ∀[h:(T3 List) ⟶ T3]. (mklist-general(n;h) ∈ T3 List)
Lemma: mklist-general-length
∀[h:Top]. ∀[n:ℕ]. (||mklist-general(n;h)|| ~ n)
Lemma: mklist-general-add1
∀[n:ℕ]. ∀[f:Top]. (mklist-general(n + 1;f) ~ mklist-general(n;f) @ [f mklist-general(n;f)])
Lemma: mklist-general_add1
∀[n:ℕ+]. ∀[f:Top]. (mklist-general(n;f) ~ mklist-general(n - 1;f) @ [f mklist-general(n - 1;f)])
Definition: mklist
mklist(n;f) == primrec(n;[];λi,l. (l @ [f i]))
Lemma: mklist_wf
∀[T:Type]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. (mklist(n;f) ∈ T List)
Definition: eval-mklist
eval-mklist(n;f;offset) ==
if n=0
then []
else eval v = f offset in
eval offset' = offset + 1 in
eval n' = n - 1 in
eval L = eval-mklist(n';f;offset') in
[v / L]
Lemma: eval-mklist-sq
∀[T:Type]
∀[n,offset:ℕ]. ∀[f:{offset..n + offset-} ⟶ T]. (eval-mklist(n;f;offset) ~ mklist(n;λi.(f (i + offset))))
supposing value-type(T)
Lemma: eval-mklist_wf
∀[T:Type]. ∀[n,offset:ℕ]. ∀[f:{offset..n + offset-} ⟶ T]. (eval-mklist(n;f;offset) ∈ T List) supposing value-type(T)
Lemma: mklist_defn2
∀[f:Top]. ∀[n:ℕ]. (mklist(n;f) ~ mklist-general(n;λl.(f ||l||)))
Lemma: mklist_length
∀[f:Top]. ∀[n:ℕ]. (||mklist(n;f)|| ~ n)
Lemma: mklist_select
∀[T:Type]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[i:ℕn]. (mklist(n;f)[i] = (f i) ∈ T)
Lemma: select-mklist
∀[n:ℕ]. ∀[f:ℕn ⟶ Top]. ∀[i:ℕn]. (mklist(n;f)[i] ~ f i)
Lemma: mklist-add
∀[T:Type]. ∀[n,m:ℕ]. ∀[f:ℕn + m ⟶ T]. (mklist(n + m;f) = (mklist(n;f) @ mklist(m;λi.(f (n + i)))) ∈ (T List))
Lemma: mklist-prepend1
∀[f:Top]. ∀[m:ℕ]. (mklist(1 + m;f) ~ [f 0] @ mklist(m;λi.(f (1 + i))))
Lemma: mklist-add1
∀[n:ℕ]. ∀[f:Top]. (mklist(n + 1;f) ~ mklist(n;f) @ [f n])
Lemma: mklist-add1-cons
∀[n:ℕ]. ∀[f:Top]. (mklist(n + 1;f) ~ [f 0 / mklist(n;λi.(f (i + 1)))])
Lemma: mklist_add1
∀[n:ℕ+]. ∀[f:Top]. (mklist(n;f) ~ mklist(n - 1;f) @ [f (n - 1)])
Lemma: mklist-single
∀[f:Top]. (mklist(1;f) ~ [f 0])
Lemma: null-mklist
∀[n:ℤ]. ∀[f:Top]. (null(mklist(n;f)) ~ n ≤z 0)
Lemma: map-sq-mklist
∀[L:Top List]. ∀[f:Top]. (map(f;L) ~ mklist(||L||;λi.(f L[i])))
Lemma: listfun_mklist
∀A,B:Type. ∀G:(A List) ⟶ (B List).
((∀L:A List. (||L|| = ||G L|| ∈ ℕ))
⇒ (∀L1,L2:A List. ∀i:ℕ.
((i ≤ ||L1||) ⇒ (i ≤ ||L2||) ⇒ (∀j:ℕi. (L1[j] = L2[j] ∈ A)) ⇒ (∀j:ℕi. (G L1[j] = G L2[j] ∈ B))))
⇒ (∀f:ℕ ⟶ A. ∀x:ℕ. ((G mklist(x;f)) = mklist(x;λn.G mklist(n + 1;f)[n]) ∈ (B List))))
Lemma: mklist-eq
∀[n:ℕ]. ∀[f,g:ℕ ⟶ Base]. mklist(n;f) ~ mklist(n;g) supposing ∀[i:ℕn]. (f i ~ g i)
Lemma: has-value-mklist
∀[n,f:Base]. n ∈ ℤ supposing (mklist(n;f))↓
Lemma: nth_tl-mklist
∀[n:ℕ]. ∀[f:Top]. ∀[k:ℕ]. (nth_tl(k;mklist(n;f)) ~ mklist(n - k;λi.(f (i + k))))
Lemma: trivial-mklist
∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ T]. mklist(||L||;f) = L ∈ (T List) supposing ∀i:ℕ||L||. ((f i) = L[i] ∈ T)
Definition: l_interval
l_interval(l;j;i) == mklist(i - j;λx.l[j + x])
Lemma: l_interval_wf
∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi + 1]. (l_interval(l;j;i) ∈ T List)
Lemma: length_l_interval
∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi + 1]. (||l_interval(l;j;i)|| = (i - j) ∈ ℤ)
Lemma: select_l_interval
∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi + 1]. ∀[x:ℕi - j]. (l_interval(l;j;i)[x] = l[j + x] ∈ T)
Lemma: hd_l_interval
∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi]. (hd(l_interval(l;j;i)) = l[j] ∈ T)
Lemma: last_l_interval
∀[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕi]. (last(l_interval(l;j;i)) = l[i - 1] ∈ T)
Lemma: swap-filter-filter
∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List]. (filter(P2;filter(P1;L)) ~ filter(P1;filter(P2;L)))
Definition: sorted-by
sorted-by(R;L) == ∀i:ℕ||L||. ∀j:ℕi. (R L[j] L[i])
Lemma: sorted-by_wf
∀[T:Type]. ∀[L:T List]. ∀[R:{x:T| (x ∈ L)} ⟶ {x:T| (x ∈ L)} ⟶ ℙ]. (sorted-by(R;L) ∈ ℙ)
Lemma: sorted-by_wf_nil
∀[R:Top]. (sorted-by(R;[]) ∈ ℙ)
Lemma: sorted-by-nil
∀[R:Top]. uiff(sorted-by(R;[]);True)
Lemma: l_before-sorted-by
∀[T:Type]
∀L:T List. ∀[R:{x:T| (x ∈ L)} ⟶ {x:T| (x ∈ L)} ⟶ ℙ]. (sorted-by(R;L) ⇒ (∀x,y:T. (x before y ∈ L ⇒ (R x y))))
Lemma: sorted-by-cons
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x:T. ∀L:T List. (sorted-by(R;[x / L]) ⇐⇒ sorted-by(R;L) ∧ (∀z∈L.R x z))
Lemma: sorted-by-single
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x:T. sorted-by(R;[x])
Lemma: sorted-by-append
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀as,bs:T List. (sorted-by(R;as @ bs) ⇐⇒ sorted-by(R;as) ∧ sorted-by(R;bs) ∧ (∀a∈as.(∀b∈bs.R a b)))
Lemma: sorted-by-filter
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀P:T ⟶ 𝔹. ∀L:T List. (sorted-by(R;L) ⇒ sorted-by(R;filter(P;L)))
Lemma: sorted-by-unique
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[sa,sb:T List].
(sa = sb ∈ (T List)) supposing
(no_repeats(T;sa) and
sorted-by(R;sa) and
no_repeats(T;sb) and
sorted-by(R;sb) and
set-equal(T;sa;sb))) supposing
(AntiSym(T;a,b.R a b) and
Trans(T;a,b.R a b))
Lemma: sorted-by-strict-no_repeats
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[L:T List]. (no_repeats(T;L)) supposing (sorted-by(R;L) and (∀a:T. (¬(R a a))))
Lemma: sorted-by-strict-unique
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
(∀[sa,sb:T List].
(sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and set-equal(T;sa;sb))) supposing
((∀a:T. (¬(R a a))) and
AntiSym(T;a,b.R a b) and
Trans(T;a,b.R a b))
Lemma: sublist-sorted-by
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀sa,sb:T List. (sa ⊆ sb ⇒ sorted-by(R;sb) ⇒ sorted-by(R;sa))
Lemma: iseg-sorted-by
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀sa,sb:T List. (sa ≤ sb ⇒ sorted-by(R;sb) ⇒ sorted-by(R;sa))
Lemma: member-iseg-sorted-by
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀sa,sb:T List.
(sa ≤ sb
⇒ sorted-by(R;sb)
⇒ (∀x:T. ((x ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x = last(sa) ∈ T) ∨ (R x last(sa)))))) supposing
(AntiSym(T;x,y.R x y) and
Irrefl(T;x,y.R x y))
Lemma: sorted-by-reverse
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀L:T List. (sorted-by(R;L) ⇐⇒ sorted-by(λx,y. (R y x);rev(L)))
Lemma: reverse-append
∀[T:Type]. ∀[as,bs:T List]. (rev(as @ bs) ~ rev(bs) @ rev(as))
Lemma: reverse-reverse
∀[L:Top List]. (rev(rev(L)) ~ L)
Definition: pairwise
(∀x,y∈L. P[x; y]) == ∀i:ℕ||L||. ∀j:ℕi. P[L[j]; L[i]]
Lemma: pairwise_wf
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L. P[x;y]) ∈ ℙ')
Lemma: sq_stable__pairwise
∀[T:Type]. ∀L:T List. ∀P:T ⟶ T ⟶ ℙ'. ((∀x,y:T. SqStable(P[x;y])) ⇒ SqStable((∀x,y∈L. P[x;y])))
Lemma: pairwise_wf2
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ T ⟶ ℙ]. ((∀x,y∈L. P[x;y]) ∈ ℙ)
Lemma: pairwise-implies
∀[T:Type]
∀L:T List
∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L. P[x;y]) ⇒ (∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ ((x = y ∈ T) ∨ P[x;y] ∨ P[y;x]))))
Lemma: pairwise-iff
∀[T:Type]
∀L:T List
∀[P:T ⟶ T ⟶ ℙ']
((∀x,y:T. (P[x;y] ⇒ P[y;x]))
⇒ (∀x:T. P[x;x])
⇒ ((∀x,y∈L. P[x;y]) ⇐⇒ ∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ P[x;y])))
Lemma: pairwise-iff2
∀[T:Type]
∀L:T List
∀[P:T ⟶ T ⟶ ℙ']
((∀x,y:T. (P[x;y] ⇒ P[y;x]))
⇒ no_repeats(T;L)
⇒ ((∀x,y∈L. P[x;y]) ⇐⇒ ∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ (¬(x = y ∈ T)) ⇒ P[x;y])))
Lemma: pairwise-nil
∀[P:Top]. ((∀x,y∈[]. P[x;y]) ⇐⇒ True)
Lemma: pairwise-singleton
∀P,v:Top. ((∀x,y∈[v]. P[x;y]) ⇐⇒ True)
Lemma: pairwise-cons
∀[T:Type]. ∀x:T. ∀L:T List. ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈[x / L]. P[x;y]) ⇐⇒ (∀x,y∈L. P[x;y]) ∧ (∀y∈L.P[x;y]))
Lemma: pairwise-append
∀[T:Type]
∀L1,L2:T List.
∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L1 @ L2. P[x;y]) ⇐⇒ ((∀x,y∈L1. P[x;y]) ∧ (∀x,y∈L2. P[x;y])) ∧ (∀x∈L1.(∀y∈L2.P[x;y])))
Lemma: pairwise-map
∀[T,T2:Type].
∀L:T List. ∀[P:T2 ⟶ T2 ⟶ ℙ']. ∀[f:{x:T| (x ∈ L)} ⟶ T2]. ((∀x,y∈map(f;L). P[x;y]) ⇐⇒ (∀x,y∈L. P[f x;f y]))
Lemma: pairwise-sublist
∀[T:Type]. ∀L1,L2:T List. ∀[P:T ⟶ T ⟶ ℙ']. (L1 ⊆ L2 ⇒ (∀x,y∈L2. P[x;y]) ⇒ (∀x,y∈L1. P[x;y]))
Lemma: pairwise-filter
∀[T:Type]. ∀L:T List. ∀[P:T ⟶ T ⟶ ℙ']. ((∀x,y∈L. P[x;y]) ⇒ (∀Q:T ⟶ 𝔹. (∀x,y∈filter(Q;L). P[x;y])))
Definition: finite-type
finite-type(T) == ∃n:ℕ. ∃f:ℕn ⟶ T. Surj(ℕn;T;f)
Lemma: finite-type_wf
∀[T:Type]. (finite-type(T) ∈ Type)
Lemma: finite-partition
∀n,k:ℕ. ∀c:ℕn ⟶ ℕk.
∃p:ℕk ⟶ (ℕ List)
((Σ(||p j|| | j < k) = n ∈ ℤ)
∧ (∀j:ℕk. ∀x,y:ℕ||p j||. p j[x] > p j[y] supposing x < y)
∧ (∀j:ℕk. ∀x:ℕ||p j||. (p j[x] < n c∧ ((c p j[x]) = j ∈ ℤ))))
Lemma: pigeon-hole
∀[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm]. n ≤ m supposing Inj(ℕn;ℕm;f)
Lemma: pigeon-hole-implies
∀n:ℕ. ∀[m:ℕ]. ∀f:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕi [((f i) = (f j) ∈ ℤ)]) supposing m < n
Lemma: pigeon-hole-implies-ext
∀n:ℕ. ∀[m:ℕ]. ∀f:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕi [((f i) = (f j) ∈ ℤ)]) supposing m < n
Lemma: pigeon-hole-implies2
∀n:ℕ
∀[m:ℕ]
∀f:ℕn ⟶ ℕm. ∀g:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕn [((f i) = (g j) ∈ ℤ)]) supposing Inj(ℕn;ℕm;g) supposing Inj(ℕn;ℕm;f)
supposing m < 2 * n
Lemma: decidable-exists-finite-type
∀[T:Type]. (finite-type(T) ⇒ (∀[P:T ⟶ ℙ]. ((∀t:T. Dec(P[t])) ⇒ Dec(∃t:T. P[t]))))
Lemma: sq_stable-finite-type-onto
∀[A,B:Type]. (finite-type(A) ⇒ (∀x,y:B. Dec(x = y ∈ B)) ⇒ (∀f:A ⟶ B. ∀b:B. SqStable(∃a:A. ((f a) = b ∈ B))))
Definition: cardinality-le
|T| ≤ n == ∃f:ℕn ⟶ T. Surj(ℕn;T;f)
Lemma: cardinality-le_wf
∀[T:Type]. ∀[n:ℕ]. (|T| ≤ n ∈ ℙ)
Lemma: cardinality-le_functionality
∀[T:Type]. ∀n:ℕ+. ∀[m:ℕ]. {|T| ≤ n ⇒ |T| ≤ m} supposing n ≤ m
Lemma: cardinality-le-finite
∀[T:Type]. ∀n:ℕ. (|T| ≤ n ⇒ finite-type(T))
Lemma: list-cardinality-le
∀[T:Type]. ∀L:T List. ((∀x:T. (x ∈ L)) ⇒ |T| ≤ ||L||)
Lemma: cardinality-le-list
∀[T:Type]. ∀n:ℕ. (|T| ≤ n ⇒ (∃L:T List. ((||L|| = n ∈ ℤ) ∧ (∀x:T. (x ∈ L)))))
Lemma: cardinality-le-no_repeats-length
∀[T:Type]. ∀[k:ℕ]. ∀[L:T List]. (||L|| ≤ k) supposing (no_repeats(T;L) and |T| ≤ k)
Lemma: finite-type-iff-list
∀[T:Type]. (finite-type(T) ⇐⇒ ∃L:T List. ∀x:T. (x ∈ L))
Lemma: bool-cardinality-le
|𝔹| ≤ 2
Lemma: finite-type-bool
finite-type(𝔹)
Lemma: int_seg-cardinality-le
∀i,j:ℤ. |{i..j-}| ≤ if i ≤z j then j - i else 0 fi
Lemma: finite-type-int_seg
∀i,j:ℤ. finite-type({i..j-})
Lemma: finite-set-type
∀[T:Type]. ∀[P:T ⟶ ℙ]. ((∀x:T. SqStable(P[x])) ⇒ (finite-type({x:T| P[x]} ) ⇐⇒ ∃L:T List. ∀x:T. (P[x] ⇐⇒ (x ∈ L))))
Lemma: finite-decidable-set
∀[T:Type]. ∀[P:T ⟶ ℙ]. ((∀x:T. Dec(P[x])) ⇒ (finite-type({x:T| P[x]} ) ⇐⇒ ∃L:T List. ∀x:T. (P[x] ⇒ (x ∈ L))))
Lemma: finite-subtype
∀[B:Type]. ∀P:B ⟶ 𝔹. (finite-type(B) ⇒ finite-type({b:B| ↑P[b]} ))
Lemma: finite-max
∀[T:Type]. (finite-type(T) ⇒ T ⇒ (∀g:T ⟶ ℤ. ∃x:T. ∀y:T. ((g y) ≤ (g x))))
Lemma: surject-inverse
∀[A,B:Type]. ∀f:A ⟶ B. (Surj(A;B;f) ⇐⇒ ∃g:B ⟶ A. ∀x:B. ((f (g x)) = x ∈ B))
Lemma: cardinality-le-int_seg
∀[x,y:ℤ]. ∀[n:ℕ]. (y - x) ≤ n supposing |{x..y-}| ≤ n
Lemma: int-seg-cardinality-le
∀x,y:ℤ. ∀n:ℕ. |{x..y-}| ≤ n supposing ((y - x) ≤ n) ∧ x < y
Lemma: biject-iff
∀[A,B:Type]. ∀f:A ⟶ B. (Bij(A;B;f) ⇐⇒ Inj(A;B;f) ∧ (∃g:B ⟶ A. ∀x:B. ((f (g x)) = x ∈ B)))
Definition: bij_inv
bij_inv(bi) == λb.(fst(((snd(bi)) b)))
Lemma: bij_inv_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[bi:Bij(A;B;f)].
(bij_inv(bi) ∈ {g:B ⟶ A| (∀b:B. ((f (g b)) = b ∈ B)) ∧ (∀a:A. ((g (f a)) = a ∈ A))} )
Lemma: biject-inverse
∀[A,B:Type]. ∀[f:A ⟶ B]. (Bij(A;B;f) ⇒ (∃g:B ⟶ A. ((∀b:B. ((f (g b)) = b ∈ B)) ∧ (∀a:A. ((g (f a)) = a ∈ A)))))
Lemma: biject-inverse2
∀[A,B:Type]. ∀f:A ⟶ B. (Bij(A;B;f) ⇒ (∃g:B ⟶ A. InvFuns(A;B;f;g)))
Lemma: biject-iff-inverse
∀[A,B:Type]. ∀f:A ⟶ B. (∃g:B ⟶ A. InvFuns(A;B;f;g) ⇐⇒ Bij(A;B;f))
Lemma: id-biject
∀[T:Type]. Bij(T;T;λx.x)
Lemma: trivial-biject-exists
∀[T:Type]. ∃f:T ⟶ T. Bij(T;T;f)
Lemma: finite-injection
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀n:ℕ. ∀s:ℕn ⟶ T. (Surj(ℕn;T;s) ⇒ (∀f:T ⟶ T. ∀x:T. ∃m:ℕ+n + 1. ((f^m x) = x ∈ T) supposing Inj(T;T;f)))))
Lemma: list-injection
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀L:T List. ∀f:{x:T| (x ∈ L)} ⟶ {x:T| (x ∈ L)} .
∀x:{x:T| (x ∈ L)} . ∃m:ℕ+||L|| + 1. ((f^m x) = x ∈ {x:T| (x ∈ L)} ) supposing Inj({x:T| (x ∈ L)} ;{x:T| (x ∈ L)}\000C ;f)))
Lemma: decidable__inject-finite-type
∀[T:Type]
(finite-type(T)
⇒ (∀x,y:T. Dec(x = y ∈ T))
⇒ (∀[A:Type]. ((∀x,y:A. Dec(x = y ∈ A)) ⇒ (∀f:T ⟶ A. Dec(Inj(T;A;f))))))
Lemma: count-length-filter
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. (count(P;L) ~ ||filter(P;L)||)
Lemma: length-filter-pos
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. 0 < ||filter(P;L)|| supposing (∃x∈L. ↑(P x))
Lemma: length-filter-pos-iff
∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List. ((∃x∈L. ↑(P x)) ⇐⇒ 0 < ||filter(P;L)||)
Lemma: count-pos-iff
∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List. ((∃x∈L. ↑(P x)) ⇐⇒ 0 < count(P;L))
Lemma: length-filter-le
∀[T:Type]. ∀[P1,P2:T ⟶ 𝔹]. ∀[L:T List]. ||filter(P1;L)|| ≤ ||filter(P2;L)|| supposing (∀x∈L.(↑(P1 x)) ⇒ (↑(P2 x)))
Definition: remove-nth
remove-nth(n;L) == <L[n], firstn(n;L) @ nth_tl(n + 1;L)>
Lemma: remove-nth_wf
∀[T:Type]. ∀[L:T List]. ∀[n:ℕ||L||]. (remove-nth(n;L) ∈ T × (T List))
Definition: add-nth
add-nth(n;x;L) == firstn(n;L) @ [x / nth_tl(n;L)]
Lemma: add-nth_wf
∀[T:Type]. ∀[L:T List]. ∀[n:ℕ]. ∀[x:T]. (add-nth(n;x;L) ∈ T List)
Lemma: add-remove-nth
∀[T:Type]. ∀[L:T List]. ∀[n:ℕ||L||]. (let x,L' = remove-nth(n;L) in add-nth(n;x;L') ~ L)
Definition: bigger-int
bigger-int(n;L) ==
accumulate (with value x and list item y):
eval x = x in
eval y = y in
if x ≤z y then y + 1 else x fi
over list:
L
with starting value:
n)
Lemma: bigger-int_wf
∀[n:ℤ]. ∀[L:ℤ List]. (bigger-int(n;L) ∈ ℤ)
Lemma: bigger-int-property
∀[L:ℤ List]. ∀[n:ℤ]. (∀x∈L.x < bigger-int(n;L))
Lemma: bigger-int-property2
∀[L:ℤ List]. ∀[n:ℤ]. (n ≤ bigger-int(n;L))
Lemma: select-nth_tl
∀[n,x:ℕ]. ∀[L:Top List]. (nth_tl(n;L)[x] ~ L[n + x])
Definition: repn
repn(n;x) == primrec(n;[];λi,l. [x / l])
Lemma: repn_wf
∀[T:Type]. ∀[x:T]. ∀[n:ℕ]. (repn(n;x) ∈ {z:T| z = x ∈ T} List)
Lemma: length-repn
∀[x:Top]. ∀[n:ℕ]. (||repn(n;x)|| ~ n)
Lemma: select-repn
∀[x:Top]. ∀[n:ℕ]. ∀[i:ℕn]. (repn(n;x)[i] ~ x)
Lemma: all-but-one
∀[T:Type]. ∀[P:T ⟶ ℙ].
∀L:T List
(∀x,y:T. Dec(x = y ∈ T))
⇒ ((∀x∈L.(∀y∈L.P[x] ∨ P[y] supposing ¬(x = y ∈ T))) ⇐⇒ (∃x∈L. (∀y∈L.P[y] supposing ¬(x = y ∈ T))))
supposing 0 < ||L||
Lemma: no_repeats_member
∀[T:Type]. ∀L:T List. ∀x:T. (x ∈ L) ⇒ (x ∈! L) supposing no_repeats(T;L)
Lemma: filter-for-max
∀[A:Type]. ∀[l:A List]. ∀[m:ℤ]. ∀[g:A ⟶ ℤ].
(||filter(λe.(g[e] =z m);l)|| ≥ 1 ) supposing ((imax-list(map(λe.g[e];l)) = m ∈ ℤ) and 0 < ||l||)
Lemma: max-map-exists
∀[T:Type]. ∀L:T List. ∀f:{x:T| (x ∈ L)} ⟶ ℤ. (∃x∈L. (∀y∈L.(f y) ≤ (f x))) supposing 0 < ||L||
Lemma: subset-map
∀[A,B:Type]. ∀f:A ⟶ B. ∀L1,L2:A List. (l_subset(A;L1;L2) ⇒ l_subset(B;map(f;L1);map(f;L2)))
Lemma: map_functionality_wrt_sq
∀[T:Type]. ∀[f,g:Base]. ∀[L:T List]. map(f;L) ~ map(g;L) supposing ∀x:T. ((x ∈ L) ⇒ (f x ~ g x)) supposing T ⊆r Base
Lemma: map-conversion-test
∀[T:Type]. ∀[L:T List List]. (map(λX.(X @ []);L) ~ map(λX.X;L)) supposing T ⊆r Base
Lemma: map-conversion-test2
∀[L:ℤ List]. (map(λx.(x + 0);L) ~ map(λx.x;L))
Lemma: length-filter-decreases
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ((∃x∈L. ¬↑(P x)) ⇒ ||filter(P;L)|| < ||L||)
Lemma: member_firstn
∀[T:Type]. ∀L:T List. ∀n:ℕ. ∀x:T. ((x ∈ firstn(n;L)) ⇐⇒ ∃i:ℕ. ((i < n ∧ i < ||L||) ∧ (x = L[i] ∈ T)))
Lemma: member-firstn
∀[T:Type]. ∀L:T List. ∀n:ℕ||L|| + 1. ∀x:T. ((x ∈ firstn(n;L)) ⇐⇒ ∃i:ℕn. (x = L[i] ∈ T))
Lemma: firstn_decomp2
∀[T:Type]. ∀[j:ℕ]. ∀[l:T List]. (firstn(j - 1;l) @ [l[j - 1]] ~ firstn(j;l)) supposing ((j ≤ ||l||) and 0 < j)
Lemma: last-decomp
∀[l:Top List]. l ~ firstn(||l|| - 1;l) @ [last(l)] supposing 0 < ||l||
Lemma: last-decomp2
∀[l:Top List]. (l ~ if (||l|| =z 0) then [] else firstn(||l|| - 1;l) @ [last(l)] fi )
Lemma: length2-decomp
∀[T:Type]. ∀L:T List. ∃a,b:T. ∃L':T List. (L = (L' @ [a; b]) ∈ (T List)) supposing ||L|| ≥ 2
Lemma: last-map
∀[as:Top List]. ∀[f:Top]. last(map(f;as)) ~ f last(as) supposing ¬↑null(as)
Lemma: last-mapfilter
∀[T:Type]. ∀[f:Top]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].
(last(mapfilter(f;P;L)) ~ if null(filter(P;L)) then ⊥ else f last(filter(P;L)) fi )
Lemma: last-mapfilter2
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].
(last(mapfilter(f;P;L)) = (f last(L)) ∈ B) supposing ((↑(P last(L))) and (¬↑null(mapfilter(f;P;L))))
Lemma: last-filter1
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List].
(last(filter(P;L)) = last(L) ∈ A) supposing ((↑(P last(L))) and (¬↑null(filter(P;L))))
Lemma: nth_tl_is_nil
∀[n:ℕ]. ∀[L:Top List]. nth_tl(n;L) ~ [] supposing ||L|| ≤ n
Definition: from-upto
[n, m) == fix((λfrom-upto,n. if n <z m then [n / eval n' = n + 1 in from-upto n'] else [] fi )) n
Lemma: from-upto_wf
∀[n,m:ℤ]. ([n, m) ∈ {x:ℤ| (n ≤ x) ∧ x < m} List)
Lemma: length-from-upto
∀[n,m:ℤ]. (||[n, m)|| ~ if n <z m then m - n else 0 fi )
Lemma: from-upto-is-nil
∀[n,m:ℤ]. uiff([n, m) ~ [];m ≤ n)
Lemma: from-upto-nil
∀[n,m:ℤ]. [n, m) ~ [] supposing m ≤ n
Lemma: from-upto-split
∀[n,m,k:ℤ]. ([n, m) ~ [n, k) @ [k, m)) supposing ((k ≤ m) and (n ≤ k))
Lemma: from-upto-shift
∀[n,m,k:ℤ]. (map(λx.(x + k);[n, m)) ~ [n + k, m + k))
Lemma: select-from-upto
∀[n,m:ℤ]. ∀[k:ℕm - n]. ([n, m)[k] ~ n + k)
Lemma: select-filter-from-upto-order-preserving
∀[n,m:ℤ]. ∀[P:{n..m-} ⟶ 𝔹]. ∀[i,j:ℕ||filter(P;[n, m))||]. uiff(i < j;filter(P;[n, m))[i] < filter(P;[n, m))[j])
Lemma: select-filter-from-upto-increasing
∀[n,m:ℤ]. ∀[P:{n..m-} ⟶ 𝔹]. ∀[i,j:ℕ||filter(P;[n, m))||]. filter(P;[n, m))[i] < filter(P;[n, m))[j] supposing i < j
Lemma: last-from-upto
∀[n,m:ℤ]. last([n, m)) ~ m - 1 supposing n < m
Lemma: member-from-upto
∀n,m:ℤ. ∀k:{x:ℤ| (n ≤ x) ∧ x < m} . (k ∈ [n, m))
Lemma: from-upto-member
∀n,m,k:ℤ. uiff((k ∈ [n, m));(n ≤ k) ∧ k < m)
Lemma: from-upto-member-nat
∀n,m,k:ℕ. uiff((k ∈ [n, m));(n ≤ k) ∧ k < m)
Lemma: l_disjoint_from-upto
∀[L:ℤ List]. ∀n1:ℤ. ∀[n2:ℤ]. uiff(∀x:ℤ. ((x ∈ L) ⇒ (x < n1 ∨ (x ≥ n2 )));l_disjoint(ℤ;L;[n1, n2)))
Lemma: no_repeats_from-upto
∀[n1,n2:ℤ]. no_repeats(ℤ;[n1, n2))
Lemma: from-upto-singleton
∀[n,m,k:ℤ]. uiff([n, m) = [k] ∈ (ℤ List);(m = (n + 1) ∈ ℤ) ∧ (k = n ∈ ℤ))
Lemma: from-upto-is-singleton
∀[n,m:ℤ]. [n, m) = [n] ∈ (ℤ List) supposing m = (n + 1) ∈ ℤ
Lemma: from-upto-single
∀[n:ℤ]. ([n, n + 1) ~ [n])
Lemma: from-upto-decomp-last
∀[n,m:ℤ]. [n, m) = ([n, m - 1) @ [m - 1]) ∈ (ℤ List) supposing n < m
Lemma: l_all_from-upto
∀n,m:ℤ. ∀P:ℤ ⟶ ℙ. ((∀x∈[n, m).P[x]) ⇐⇒ ∀x:ℤ. ((n ≤ x) ⇒ x < m ⇒ P[x]))
Lemma: from-upto-sorted
∀a,b:ℤ. sorted-by(λx,y. x < y;[a, b))
Definition: upto
upto(n) == [0, n)
Lemma: upto_wf
∀[n:ℤ]. (upto(n) ∈ ℕn List)
Lemma: length_upto
∀[n:ℕ]. (||upto(n)|| ~ n)
Lemma: upto_is_nil
∀[n:ℕ]. uiff(upto(n) ~ [];n = 0 ∈ ℤ)
Lemma: null-upto
∀[n:ℕ]. (null(upto(n)) ~ (n =z 0))
Lemma: upto_equal_nil
∀[n:ℕ]. uiff(upto(n) = [] ∈ (ℤ List);n = 0 ∈ ℤ)
Lemma: upto_decomp
∀[m:ℕ]. ∀[n:ℕm + 1]. (upto(m) ~ upto(n) @ map(λx.(x + n);upto(m - n)))
Lemma: upto_decomp1
∀[n:ℕ+]. (upto(n) ~ upto(n - 1) @ [n - 1])
Lemma: last-upto
∀n:ℕ+. (upto(n) ~ upto(n - 1) @ [n - 1])
Lemma: upto_decomp2
∀[n:ℕ+]. (upto(n) ~ [0 / map(λi.(i + 1);upto(n - 1))])
Lemma: upto_add_1
∀[n:ℕ]. (upto(n + 1) ~ upto(n) @ [n])
Lemma: upto_iseg
∀i,j:ℕ. upto(i) ≤ upto(j) supposing i ≤ j
Lemma: select_upto
∀[m:ℕ]. ∀[n:ℕm]. (upto(m)[n] = n ∈ ℤ)
Lemma: select-upto
∀[m:ℕ]. ∀[n:ℕm]. (upto(m)[n] ~ n)
Lemma: member_upto
∀n,i:ℕ. ((i ∈ upto(n)) ⇐⇒ i < n)
Lemma: member_upto2
∀n,i:ℕ. (i ∈ upto(n)) supposing i < n
Lemma: before-upto
∀n:ℕ. ∀x,y:ℕn. (x before y ∈ upto(n) ⇐⇒ x < y)
Lemma: no_repeats_upto
∀[n:ℕ]. (no_repeats(ℤ;upto(n)) ∧ no_repeats(ℕn;upto(n)))
Lemma: filter_map_upto
∀[T:Type]. ∀[i,j:ℕ].
∀[f:ℕ ⟶ T]. ∀[P:T ⟶ 𝔹]. ||filter(P;map(f;upto(i)))|| < ||filter(P;map(f;upto(j)))|| supposing ↑(P (f i))
supposing i < j
Lemma: filter_map_upto2
∀t',m:ℕ.
∀[T:Type]
∀f:ℕ ⟶ T. ∀P:T ⟶ 𝔹.
∃t:ℕ. ((↑(P (f t))) ∧ (||filter(P;map(f;upto(t)))|| = m ∈ ℤ)) supposing (m + 1) ≤ ||filter(P;map(f;upto(t')))||
Lemma: firstn_firstn
∀[L:Top List]. ∀[n:ℤ]. ∀[m:ℕn + 1]. (firstn(m;firstn(n;L)) ~ firstn(m;L))
Lemma: list_eq_imp_sqeq
∀T:Type. ∀L1,L2:T List. ((L1 = L2 ∈ (T List)) ⇒ (L1 ~ L2)) supposing T ⊆r Base
Lemma: firstn_last
∀[T:Type]. ∀[L:T List]. L = (firstn(||L|| - 1;L) @ [last(L)]) ∈ (T List) supposing ¬↑null(L)
Lemma: firstn_last_sq
∀[T:Type]. ∀[L:T List]. L ~ firstn(||L|| - 1;L) @ [last(L)] supposing (¬↑null(L)) ∧ (T ⊆r Base)
Lemma: firstn_last_mklist
∀[T:Type]. ∀[F:ℕ ⟶ T]. ∀n:ℕ+. (mklist(n;F) = (firstn(n - 1;mklist(n;F)) @ [last(mklist(n;F))]) ∈ (T List))
Lemma: last_mklist
∀T:Type. ∀f:ℕ ⟶ T. ∀n:ℕ+. (last(mklist(n;f)) = (f (n - 1)) ∈ T)
Lemma: firstn_last_mklist_sq
∀[T:Type]. ∀[F:ℕ ⟶ T]. ∀n:ℕ+. (mklist(n;F) ~ firstn(n - 1;mklist(n;F)) @ [last(mklist(n;F))]) supposing T ⊆r Base
Lemma: firstn_append
∀[L1,L2:Top List]. ∀[n:ℕ||L1|| + 1]. (firstn(n;L1 @ L2) ~ firstn(n;L1))
Lemma: firstn_length
∀[L:Top List]. (firstn(||L||;L) ~ L)
Lemma: firstn_map
∀[f:Top]. ∀[n:ℕ]. ∀[l:Top List]. (firstn(n;map(f;l)) ~ map(f;firstn(n;l)))
Lemma: firstn_upto
∀[n,m:ℕ]. (firstn(n;upto(m)) ~ if n ≤z m then upto(n) else upto(m) fi )
Lemma: firstn_map_upto
∀[L:Top List]. ∀[n:ℕ]. (firstn(n;L) ~ map(λi.L[i];upto(imin(||L||;n))))
Lemma: firstn-mklist
∀[m,n:ℕ]. ∀[f:ℕm ⟶ Top]. (firstn(n;mklist(m;f)) ~ mklist(imin(n;m);f))
Lemma: firstn-mklist1
∀[m,n:ℕ]. ∀[f:ℕm ⟶ Top]. ((n ≤ m) ⇒ (firstn(n;mklist(m;f)) ~ mklist(n;f)))
Lemma: firstn_nth_tl_decomp
∀[T:Type]. ∀[L:T List]. ∀[i:ℕ||L||]. (L ~ firstn(i;L) @ [L[i]] @ nth_tl(1 + i;L))
Lemma: firstn-iseg
∀[T:Type]. ∀L:T List. ∀n:ℕ. firstn(n;L) ≤ L
Lemma: firstn_nth_tl
∀[T:Type]. ∀[L:T List]. ∀[i:ℕ]. (L ~ firstn(i;L) @ nth_tl(i;L))
Lemma: firstn_append_front
∀[L1:Top List]. ∀L2:Top List. (firstn(||L1 @ L2|| - ||L2||;L1 @ L2) ~ L1)
Lemma: firstn_append_front_singleton
∀[L:Top List]. ∀a:Top. (firstn(||L @ [a]|| - 1;L @ [a]) ~ L)
Lemma: whole_segment
∀T:Type. ∀as:T List. ((as[0..||as||-]) = as ∈ (T List))
Lemma: append-segment
∀T:Type. ∀as:T List. ∀i:{0...||as||}. ∀j:{i...||as||}. ∀k:{j...||as||}.
(((as[i..j-]) @ (as[j..k-])) = (as[i..k-]) ∈ (T List))
Lemma: last_append_singleton
∀[T:Type]. ∀L:T List. ∀a:T. (last(L @ [a]) ~ a)
Lemma: last_append_singleton_sq
dumplicate - needes to be removed and references replaced by last_append_singleton⋅
∀[T:Type]. ∀L:T List. ∀a:T. (last(L @ [a]) ~ a)
Lemma: l_contains-firstn
∀[T:Type]. ∀L:T List. ∀n:ℕ. firstn(n;L) ⊆ L
Lemma: l_contains-nth_tl
∀[T:Type]. ∀L:T List. ∀n:ℕ. nth_tl(n;L) ⊆ L
Definition: bl-all
(∀x∈L.P[x])_b == reduce(λx,p. (P[x] ∧b p);tt;L)
Lemma: bl-all_wf
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ((∀x∈L.P[x])_b ∈ 𝔹)
Lemma: assert-bl-all
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. uiff(↑(∀x∈L.P[x])_b;(∀x∈L.↑P[x]))
Lemma: assert-bl-all-2
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. uiff(↑(∀x∈L.P[x])_b;∀x:T. ((x ∈ L) ⇒ (↑P[x])))
Lemma: bl-all-btrue
∀[L:Top List]. ((∀x∈L.tt)_b ~ tt)
Definition: bl-exists
(∃x∈L.P[x])_b == reduce(λx,p. (P[x] ∨bp);ff;L)
Lemma: bl-exists_wf
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ((∃x∈L.P[x])_b ∈ 𝔹)
Lemma: assert-bl-exists
∀[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹. (↑(∃x∈L.P[x])_b ⇐⇒ (∃x∈L. ↑P[x]))
Lemma: assert-bl-exists2
∀[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹. (↑(∃x∈L.P[x])_b ⇐⇒ ∃x:T. ((x ∈ L) ∧ (↑P[x])))
Lemma: bl-exists-bfalse
∀[L:Top List]. ((∃x∈L.ff)_b ~ ff)
Lemma: bl-exists-nil
∀[f:Top]. ((∃x∈[].f[x])_b ~ ff)
Lemma: bl-exists-cons
∀[f,u,v:Top]. ((∃x∈[u / v].f[x])_b ~ f[u] ∨b(∃x∈v.f[x])_b)
Lemma: bl-exists-singleton-top
∀[f,a:Top]. ((∃x∈[a].f[x])_b ~ f[a] ∨bff)
Lemma: not-assert-bl-all
∀[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹. (¬↑(∀x∈L.P[x])_b ⇐⇒ (∃x∈L. ¬↑P[x]))
Lemma: not-assert-bl-exists
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. uiff(¬↑(∃x∈L.P[x])_b;(∀x∈L.¬↑P[x]))
Lemma: not-bl-exists-eq-bl-all
∀[L,P:Top]. (¬b(∃x∈L.P[x])_b ~ (∀x∈L.¬bP[x])_b)
Definition: nonneg-poly
nonneg-poly(p) == (∀m∈p.nonneg-monomial(m))_b
Lemma: nonneg-poly_wf
∀[p:iPolynomial()]. (nonneg-poly(p) ∈ 𝔹)
Lemma: assert-nonneg-poly
∀[p:iPolynomial()]. uiff(↑nonneg-poly(p);(∀m∈p.↑nonneg-monomial(m)))
Lemma: reduce-as-accum
∀[T,A:Type]. ∀[f:T ⟶ A ⟶ A].
∀[L:T List]. ∀[a:A].
(reduce(f;a;L) = accumulate (with value p and list item x): f x pover list: Lwith starting value: a) ∈ A)
supposing ∀x,y:T. ∀a:A. ((f x (f y a)) = (f y (f x a)) ∈ A)
Lemma: reduce-map
∀[f,g,as,x:Top]. (reduce(λa,b. g[a;b];x;map(f;as)) ~ reduce(λa,b. g[f a;b];x;as))
Lemma: bl-all-as-accum
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].
((∀x∈L.P[x])_b ~ accumulate (with value p and list item x):
p ∧b P[x]
over list:
L
with starting value:
tt))
Lemma: bl-exists-as-accum
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].
((∃x∈L.P[x])_b ~ accumulate (with value p and list item x):
p ∨bP[x]
over list:
L
with starting value:
ff))
Lemma: bl-exists-map
∀[f,L,P:Top]. ((∃x∈map(f;L).P[x])_b ~ (∃x∈L.P[f x])_b)
Lemma: bl-exists-append
∀[L1,L2,P:Top]. ((∃x∈L1 @ L2.P[x])_b ~ (∃x∈L1.P[x])_b ∨b(∃x∈L2.P[x])_b)
Lemma: null_append
∀[L1:Top List]. ∀[L2:Top]. (null(L1 @ L2) ~ null(L1) ∧b null(L2))
Lemma: bl-exists-first
∀[A:Type]. ∀P:A ⟶ 𝔹. ∀L:A List. (↑(∃x∈L.P[x])_b ⇐⇒ ∃i:ℕ||L||. ((↑P[L[i]]) ∧ (∀j:ℕi. (¬↑P[L[j]]))))
Lemma: bl-exists-filter
∀[P,Q,L:Top]. ((∃x∈filter(P;L).Q[x])_b ~ (∃x∈L.(P x) ∧b Q[x])_b)
Definition: rotate
rot(n) == λx.if (x =z n - 1) then 0 else x + 1 fi
Lemma: rotate_wf
∀[k:ℕ]. (rot(k) ∈ ℕk ⟶ ℕk)
Lemma: iterated-rotate
∀[n,i:ℕ]. rot(n)^i = (λx.if x + i <z n then x + i else (x + i) - n fi ) ∈ (ℕn ⟶ ℕn) supposing i ≤ n
Definition: flip
(i, j) == λx.if (x =z i) then j if (x =z j) then i else x fi
Lemma: flip_wf
∀[k:ℕ]. ∀[i,j:ℕk]. ((i, j) ∈ ℕk ⟶ ℕk)
Lemma: flip-conjugation
∀[n:ℕ]. ∀[k:ℕn]. ∀[j:ℕk]. ∀[l:ℕn - k]. ((j, k + l) = ((k, k + l) o ((j, k) o (k, k + l))) ∈ (ℕn ⟶ ℕn))
Lemma: flip-conjugation1
∀[n:ℕ]. ∀[k:ℕn - 1]. ∀[j:ℕk]. ((j, k + 1) = ((k, k + 1) o ((j, k) o (k, k + 1))) ∈ (ℕn ⟶ ℕn))
Lemma: flip-conjugate-rotate
∀[n:ℕ]. ∀[i:ℕn - 1]. ((i, i + 1) = (rot(n)^i o ((0, 1) o rot(n)^n - i)) ∈ (ℕn ⟶ ℕn))
Lemma: flip_symmetry
∀[k:ℕ]. ∀[i,j:ℕk]. ((i, j) = (j, i) ∈ (ℕk ⟶ ℕk))
Lemma: flip_identity
∀[k:ℕ]. ∀[i,j:ℕk]. (i, j) = (λx.x) ∈ (ℕk ⟶ ℕk) supposing i = j ∈ ℤ
Lemma: flip_bijection
∀k:ℕ. ∀i,j:ℕk. Bij(ℕk;ℕk;(i, j))
Lemma: flip_inverse
∀[k:ℤ]. ∀[x,y:ℕk]. (((y, x) o (y, x)) = (λx.x) ∈ (ℕk ⟶ ℕk))
Lemma: flip_twice
∀[k:ℤ]. ∀[x,y,i:ℕk]. (((y, x) ((y, x) i)) = i ∈ ℤ)
Lemma: flip-adjacent
∀n:ℕ. ∀i,j:ℕn. ∃L:ℕn - 1 List. ((i, j) = reduce(λi,g. ((i, i + 1) o g);λx.x;L) ∈ (ℕn ⟶ ℕn))
Lemma: flip-generators
∀n:ℕ
∀i,j:ℕn. ∃L:𝔹 List. ((i, j) = reduce(λi,g. (if i then rot(n) else (0, 1) fi o g);λx.x;L) ∈ (ℕn ⟶ ℕn)) supposing 1 <\000C n
Lemma: flip-injection
∀[n:ℕ]. ∀[i,j:ℕn]. Inj(ℕn;ℕn;(i, j))
Lemma: identity-injection
∀[T:Type]. Inj(T;T;λx.x)
Lemma: rotate-injection
∀[n:ℕ]. Inj(ℕn;ℕn;rot(n))
Lemma: iterate-rotate
∀[n,k:ℕ]. (rot(n)^k = (λx.(x + k rem n)) ∈ (ℕn ⟶ ℕn))
Lemma: rotate-order
∀[n:ℕ]. (rot(n)^n = (λx.x) ∈ (ℕn ⟶ ℕn))
Lemma: rotate-inverse1
∀[n:ℕ+]. ((rot(n) o rot(n)^n - 1) = (λx.x) ∈ (ℕn ⟶ ℕn))
Lemma: rotate-surjection
∀n:ℕ+. Surj(ℕn;ℕn;rot(n))
Lemma: rotate-bijection
∀n:ℕ+. Bij(ℕn;ℕn;rot(n))
Lemma: rotate-inverse
∀[n:ℕ+]. (inv(rot(n)) = rot(n)^n - 1 ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )
Definition: permute_list
(L o f) == mklist(||L||;λi.L[f i])
Lemma: permute_list_wf
∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ ℕ||L||]. ((L o f) ∈ T List)
Lemma: permute_list_select
∀[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ ℕ||L||]. ∀[i:ℕ||L||]. ((L o f)[i] = L[f i] ∈ T)
Lemma: permute_list_length
∀[T:Type]. ∀[L:T List]. ∀[f:Top]. (||(L o f)|| ~ ||L||)
Lemma: permute_list-identity
∀[T:Type]. ∀[L:T List]. ((L o λx.x) = L ∈ (T List))
Lemma: permute_list-compose
∀[T:Type]. ∀[L:T List]. ∀[f,g:ℕ||L|| ⟶ ℕ||L||]. ((L o f o g) = ((L o f) o g) ∈ (T List))
Lemma: permute_permute_list
∀[T:Type]. ∀[L:T List]. ∀[f,g:ℕ||L|| ⟶ ℕ||L||]. (((L o f) o g) = (L o f o g) ∈ (T List))
Definition: permutation
permutation(T;L1;L2) == ∃f:ℕ||L1|| ⟶ ℕ||L1||. (Inj(ℕ||L1||;ℕ||L1||;f) ∧ (L2 = (L1 o f) ∈ (T List)))
Lemma: permutation_wf
∀[A:Type]. ∀[L1,L2:A List]. (permutation(A;L1;L2) ∈ ℙ)
Lemma: permutation-subtype
∀[A,B:Type]. ∀[L1,L2:A List]. (permutation(A;L1;L2) ⇒ (A ⊆r B) ⇒ permutation(B;L1;L2))
Lemma: permutation-length
∀[A:Type]. ∀[L1,L2:A List]. ||L1|| = ||L2|| ∈ ℤ supposing permutation(A;L1;L2)
Lemma: permutation-contains
∀[A:Type]. ∀L1,L2:A List. (permutation(A;L1;L2) ⇒ L2 ⊆ L1)
Lemma: permutation-nil
∀[A:Type]. permutation(A;[];[])
Lemma: permutation-nil-iff
∀[A:Type]. ∀L:A List. (permutation(A;[];L) ⇐⇒ L = [] ∈ (A List))
Lemma: permutation-rotate
∀[A:Type]. ∀as,bs:A List. permutation(A;as @ bs;bs @ as)
Lemma: permutation-rotate-cons
∀[A:Type]. ∀a:A. ∀as:A List. permutation(A;[a / as];as @ [a])
Lemma: permutation_weakening
∀[A:Type]. ∀as,bs:A List. permutation(A;as;bs) supposing as = bs ∈ (A List)
Lemma: permutation_transitivity
∀[A:Type]. ∀as,bs,cs:A List. (permutation(A;as;bs) ⇒ permutation(A;bs;cs) ⇒ permutation(A;as;cs))
Lemma: permutation_inversion
∀[A:Type]. ∀as,bs:A List. (permutation(A;as;bs) ⇒ permutation(A;bs;as))
Lemma: permutation-equiv
∀[A:Type]. EquivRel(A List)(permutation(A;_1;_2))
Lemma: append_functionality_wrt_permutation
∀[A:Type]
∀as1,as2,bs1,bs2:A List. (permutation(A;as1;bs1) ⇒ permutation(A;as2;bs2) ⇒ permutation(A;as1 @ as2;bs1 @ bs2))
Lemma: permutation_functionality_wrt_permutation
∀[A:Type]
∀as1,as2,bs1,bs2:A List.
(permutation(A;as1;as2) ⇒ permutation(A;bs1;bs2) ⇒ (permutation(A;as1;bs1) ⇐⇒ permutation(A;as2;bs2)))
Lemma: no_repeats_functionality_wrt_permutation
∀[A:Type]. ∀as1,as2:A List. (permutation(A;as1;as2) ⇒ (no_repeats(A;as1) ⇐⇒ no_repeats(A;as2)))
Lemma: cons_cancel_wrt_permutation
∀[A:Type]. ∀a:A. ∀bs,cs:A List. (permutation(A;[a / bs];[a / cs]) ⇒ permutation(A;bs;cs))
Lemma: append_cancel_wrt_permutation
∀[A:Type]. ∀as,bs,cs:A List. (permutation(A;as @ bs;as @ cs) ⇒ permutation(A;bs;cs))
Lemma: append_cancel
∀[A:Type]. ∀[as,bs,cs:A List]. bs = cs ∈ (A List) supposing (as @ bs) = (as @ cs) ∈ (A List)
Lemma: append_cancel_nil
∀[A:Type]. ∀[as,bs:A List]. bs = [] ∈ (A List) supposing as = (as @ bs) ∈ (A List)
Lemma: l_member-permutation
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ (∃L':T List. permutation(T;L;[x / L'])))
Lemma: member-permutation
∀[A:Type]. ∀as,bs:A List. (permutation(A;as;bs) ⇒ {∀a:A. ((a ∈ as) ⇐⇒ (a ∈ bs))})
Lemma: l_member_functionality_wrt_permutation
∀[A:Type]. ∀as,bs:A List. ∀a:A. (permutation(A;as;bs) ⇒ (a ∈ as) ⇒ (a ∈ bs))
Lemma: permutation-strong-subtype
∀[A,B:Type].
∀L1:B List. ∀L2:A List. (permutation(A;L1;L2) ⇒ {(L2 ∈ B List) ∧ permutation(B;L1;L2)})
supposing strong-subtype(B;A)
Lemma: decidable__l_disjoint
∀[A:Type]. ((∀x,y:A. Dec(x = y ∈ A)) ⇒ (∀L1,L2:A List. Dec(l_disjoint(A;L1;L2))))
Lemma: l_disjoint-representatives
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ (∀L:T List List
∃reps:T List List
(reps ⊆ L ∧ (∀as∈L.(∃rep∈reps. ¬l_disjoint(T;as;rep))) ∧ (∀rep1,rep2∈reps. l_disjoint(T;rep1;rep2)))
supposing (∀as∈L.0 < ||as||)))
Definition: orbit
orbit(T;f;L) ==
0 < ||L|| ∧ no_repeats(T;L) ∧ (∀i:ℕ||L||. ((f L[i]) = if (i =z ||L|| - 1) then L[0] else L[i + 1] fi ∈ T))
Lemma: orbit_wf
∀[T:Type]. ∀[f:T ⟶ T]. ∀[L:T List]. (orbit(T;f;L) ∈ ℙ)
Lemma: orbit-iterates
∀[T:Type]. ∀[f:T ⟶ T]. ∀[L:T List]. ∀[i:ℕ||L||]. ∀[n:ℕ]. ((f^n L[i]) = L[i + n rem ||L||] ∈ T) supposing orbit(T;f;L)
Lemma: orbit-closed
∀[T:Type]. ∀f:T ⟶ T. ∀L:T List. (∀a∈L.∀n:ℕ. (f^n a ∈ L)) supposing orbit(T;f;L)
Lemma: singleton-orbit
∀[T:Type]. ∀[f:T ⟶ T]. ∀[o:T List]. (o ∈ {x:T| (f x) = x ∈ T} List) supposing (orbit(T;f;o) and (||o|| = 1 ∈ ℤ))
Lemma: orbit-of-involution
∀[T:Type]. ∀[f:T ⟶ T].
∀o:T List. (||o|| = 1 ∈ ℤ) ∨ (||o|| = 2 ∈ ℤ) supposing orbit(T;f;o) supposing ∀x:T. ((f (f x)) = x ∈ T)
Lemma: orbit-transitive
∀[T:Type]. ∀f:T ⟶ T. ∀L:T List. (∀a∈L.(∀b∈L.∃n:ℕ. ((f^n a) = b ∈ T))) supposing orbit(T;f;L)
Lemma: orbit-exists
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ finite-type(T)
⇒ (∀f:T ⟶ T. ∀a:T.
∃L:T List
(no_repeats(T;L) ∧ (∀i:ℕ||L||. (L[i] = (f^i a) ∈ T)) ∧ (∀b:T. ((b ∈ L) ⇐⇒ ∃n:ℕ. (b = (f^n a) ∈ T))))))
Lemma: orbit-cover
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ finite-type(T)
⇒ (∀f:T ⟶ T
∃orbits:T List List
((∀orbit∈orbits.0 < ||orbit||
∧ no_repeats(T;orbit)
∧ (∀i:ℕ||orbit||. (orbit[i] = (f^i orbit[0]) ∈ T))
∧ (∀b:T. ((b ∈ orbit) ⇐⇒ ∃n:ℕ. (b = (f^n orbit[0]) ∈ T))))
∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))
∧ (∀o1∈orbits.(∀o2∈orbits.(o1[0] ∈ o2) ⇒ o1 ⊆ o2)))))
Lemma: orbit-decomp
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ finite-type(T)
⇒ (∀f:T ⟶ T
∃orbits:T List List
((∀orbit∈orbits.0 < ||orbit||
∧ no_repeats(T;orbit)
∧ (∀i:ℕ||orbit||. ((f orbit[i]) = if (i =z ||orbit|| - 1) then orbit[0] else orbit[i + 1] fi ∈ T))
∧ (∀x∈orbit.∀n:ℕ. (f^n x ∈ orbit)))
∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))
∧ (∀o1,o2∈orbits. l_disjoint(T;o1;o2)))
supposing Inj(T;T;f)))
Lemma: orbit-decomp2
∀[T:Type]
((∀x,y:T. Dec(x = y ∈ T))
⇒ finite-type(T)
⇒ (∀f:T ⟶ T
∃orbits:T List List
((∀o∈orbits.orbit(T;f;o))
∧ (∀a:T. (∃orbit∈orbits. (a ∈ orbit)))
∧ (∀o1,o2∈orbits. l_disjoint(T;o1;o2))
∧ no_repeats(T List;orbits))
supposing Inj(T;T;f)))
Definition: cycle
cycle(L) ==
λx.if null(L)
then x
else let b = hd(L) in
rec-case(L) of
[] => x
a::as =>
r.if (x =z a) then if null(as) then b else hd(as) fi else r fi
fi
Lemma: cycle_wf
∀[n:ℕ]. ∀[L:ℕn List]. (cycle(L) ∈ ℕn ⟶ ℕn)
Lemma: apply-cycle-member
∀[n:ℕ]. ∀[L:ℕn List].
∀[i:ℕ||L||]. ((cycle(L) L[i]) = if (i =z ||L|| - 1) then L[0] else L[i + 1] fi ∈ ℕn) supposing no_repeats(ℕn;L)
Lemma: cycle-closed
∀n:ℕ. ∀x:ℕn. ∀L:ℕn List. (x ∈ L) ⇒ (cycle(L) x ∈ L) supposing no_repeats(ℕn;L)
Lemma: apply-cycle-non-member
∀[n:ℕ]. ∀[L:ℕn List]. ∀[x:ℕn]. (cycle(L) x) = x ∈ ℕn supposing ¬(x ∈ L)
Lemma: cycle-conjugate
∀[n:ℕ]. ∀[L:ℕn List].
∀[f,g:ℕn ⟶ ℕn].
((g o (cycle(L) o f)) = cycle(map(g;L)) ∈ (ℕn ⟶ ℕn)) supposing
((∀a:ℕn. ((f (g a)) = a ∈ ℕn)) and
(∀a:ℕn. ((g (f a)) = a ∈ ℕn)))
supposing no_repeats(ℕn;L)
Lemma: cycle-injection
∀[n:ℕ]. ∀[L:ℕn List]. Inj(ℕn;ℕn;cycle(L)) supposing no_repeats(ℕn;L)
Lemma: cycle-transitive1
∀[n:ℕ]. ∀[L:ℕn List].
∀[a,b:ℕ]. ((cycle(L)^b - a L[a]) = L[b] ∈ ℕn) supposing ((a ≤ b) and b < ||L||) supposing no_repeats(ℕn;L)
Lemma: cycle-transitive
∀n:ℕ. ∀L:ℕn List. ∀a,b:ℕ||L||. ∃m:ℕ||L||. ((cycle(L)^m L[a]) = L[b] ∈ ℕn) supposing no_repeats(ℕn;L)
Lemma: cycle-transitive2
∀n:ℕ. ∀L:ℕn List. (∀x∈L.(∀y∈L.∃m:ℕ||L||. ((cycle(L)^m x) = y ∈ ℕn))) supposing no_repeats(ℕn;L)
Lemma: cycle-decomp
∀n:ℕ. ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} .
∃cycles:ℕn List List
(no_repeats(ℕn List;cycles)
∧ (∀c1∈cycles.(∀c2∈cycles.(c1 = c2 ∈ (ℕn List)) ∨ l_disjoint(ℕn;c1;c2)))
∧ (∀c∈cycles.0 < ||c|| ∧ no_repeats(ℕn;c))
∧ (f = reduce(λc,g. (cycle(c) o g);λx.x;cycles) ∈ (ℕn ⟶ ℕn)))
Lemma: cycle-flip-lemma
∀[n:ℕ]. ∀[L:ℕn List].
(cycle(L) = ((hd(L), hd(tl(L))) o cycle(tl(L))) ∈ (ℕn ⟶ ℕn)) supposing (1 < ||L|| and no_repeats(ℕn;L))
Definition: compose-flips
compose-flips(flips) == reduce(λf,g. (f o g);λx.x;map(λp.let i,j = p in (i, j);flips))
Lemma: compose-flips_wf
∀k:ℕ. ∀flips:(ℕk × ℕk) List. (compose-flips(flips) ∈ ℕk ⟶ ℕk)
Lemma: compose-flips-injection
∀n:ℕ. ∀L:(ℕn × ℕn) List. Inj(ℕn;ℕn;compose-flips(L))
Lemma: cycle-as-flips
∀n:ℕ. ∀L:ℕn List. ∃flips:(ℕn × ℕn) List. (cycle(L) = compose-flips(flips) ∈ (ℕn ⟶ ℕn)) supposing no_repeats(ℕn;L)
Lemma: rotate-as-flips
∀n:ℕ. ∃flips:(ℕn × ℕn) List. (rot(n) = compose-flips(flips) ∈ (ℕn ⟶ ℕn))
Lemma: cycle-append
∀[n:ℕ]. ∀[as,bs:ℕn List]. cycle(as @ bs) = cycle(bs @ as) ∈ (ℕn ⟶ ℕn) supposing no_repeats(ℕn;as @ bs)
Lemma: permutation-generators
∀n:ℕ
∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ]
(P[λx.x]
⇒ ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[(0, 1) o f]) supposing 1 < n
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[rot(n) o f]))
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
Lemma: permutation-generators2
∀n:ℕ
∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ]
(P[λx.x]
⇒ ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[f o (0, 1)]) supposing 1 < n
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . (P[f] ⇒ P[f o rot(n)]))
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
Lemma: permutation-generators3
∀n:ℕ
∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ]
(P[λx.x]
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn. P[f] ⇒ P[f o (i, j)] supposing i < j)
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
Lemma: permutation-generators4
∀n:ℕ
∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ]
(P[λx.x]
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n. (P[f] ⇒ P[f o (0, j)]))
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
Lemma: permutation-generators5
∀n:ℕ
∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} ⟶ ℙ]
(P[λx.x]
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i:ℕn - 1. (P[f] ⇒ P[f o (i, i + 1)]))
⇒ (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . P[f]))
Lemma: permutation-invariant2
∀[T:Type]. ∀[R:(T List) ⟶ (T List) ⟶ ℙ].
(Trans(T List;as,bs.R[as;bs])
⇒ Refl(T List;as,bs.R[as;bs])
⇒ (∀as:T List. ∀a:T. R[[a / as];as @ [a]])
⇒ (∀as:T List. ∀a1,a2:T. R[[a1; [a2 / as]];[a2; [a1 / as]]])
⇒ (∀as,bs:T List. (permutation(T;as;bs) ⇒ R[as;bs])))
Lemma: permutation-invariant
∀[T:Type]. ∀[P:(T List) ⟶ ℙ].
((∀as:T List. ∀a:T. (P[[a / as]] ⇒ P[as @ [a]]))
⇒ (∀as:T List. ∀a1,a2:T. (P[[a1; [a2 / as]]] ⇒ P[[a2; [a1 / as]]]))
⇒ (∀as,bs:T List. (permutation(T;as;bs) ⇒ (P[as] ⇐⇒ P[bs]))))
Lemma: combine-list-permutation
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
(∀[as,bs:A List].
(combine-list(x,y.f[x;y];as) = combine-list(x,y.f[x;y];bs) ∈ A) supposing
(permutation(A;as;bs) and
0 < ||as||)) supposing
(Comm(A;λx,y. f[x;y]) and
Assoc(A;λx,y. f[x;y]))
Lemma: reduce-as-combine-list
∀[A:Type]. ∀[f:A ⟶ A ⟶ A].
(∀[L:A List]. ∀[z:A]. (reduce(f;z;L) = combine-list(x,y.f[x;y];[z / L]) ∈ A)) supposing
(Comm(A;λx,y. f[x;y]) and
Assoc(A;λx,y. f[x;y]))
Lemma: reduce-permutation
∀[A:Type]. ∀[f:A ⟶ A ⟶ A]. ∀[e:A].
(∀[as,bs:A List]. reduce(f;e;as) = reduce(f;e;bs) ∈ A supposing permutation(A;as;bs)) supposing
(Comm(A;λx,y. f[x;y]) and
Assoc(A;λx,y. f[x;y]))
Lemma: permutation-cons
∀[A:Type]
∀x:A. ∀L1,L2:A List.
(permutation(A;[x / L1];L2) ⇐⇒ ∃as,bs:A List. ((L2 = (as @ [x / bs]) ∈ (A List)) ∧ permutation(A;L1;as @ bs)))
Lemma: permutation-cons2
∀[A:Type]. ∀x:A. ∀L1,L2:A List. (permutation(A;L1;L2) ⇒ permutation(A;[x / L1];[x / L2]))
Lemma: permutation-swap-first2
∀[A:Type]. ∀x,y:A. ∀L:A List. permutation(A;[x; [y / L]];[y; [x / L]])
Lemma: permutation-last
∀[A:Type]
∀x:A. ∀L1,L2:A List.
(permutation(A;L1 @ [x];L2) ⇐⇒ ∃as,bs:A List. ((L2 = (as @ [x / bs]) ∈ (A List)) ∧ permutation(A;L1;as @ bs)))
Lemma: permutation-when-no_repeats
∀[T:Type]
∀sa,sb:T List. ((∀x:T. ((x ∈ sa) ⇐⇒ (x ∈ sb))) ⇒ no_repeats(T;sb) ⇒ no_repeats(T;sa) ⇒ permutation(T;sb;sa))
Lemma: permutation-sorted-by-unique
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
∀[sa,sb:T List]. (sa = sb ∈ (T List)) supposing (sorted-by(R;sa) and sorted-by(R;sb) and permutation(T;sa;sb))
supposing Linorder(T;a,b.R a b)
Lemma: permutation-singleton
∀[T:Type]. ∀[x:T]. ∀[ts:T List]. ts = [x] ∈ (T List) supposing permutation(T;[x];ts)
Lemma: permutation-reverse
∀[A:Type]. ∀L:A List. permutation(A;L;rev(L))
Lemma: permutation-map
∀[A:Type]. ∀L1,L2:A List. (permutation(A;L1;L2) ⇒ (∀[B:Type]. ∀f:A ⟶ B. permutation(B;map(f;L1);map(f;L2))))
Lemma: permutation-filter
∀[A:Type]. ∀L1,L2:A List. (permutation(A;L1;L2) ⇒ (∀p:A ⟶ 𝔹. permutation({a:A| ↑(p a)} ;filter(p;L1);filter(p;L2))))
Lemma: filter_functionality_wrt_permutation
∀[A:Type]. ∀L1,L2:A List. ∀p:A ⟶ 𝔹. (permutation(A;L1;L2) ⇒ permutation(A;filter(p;L1);filter(p;L2)))
Lemma: cons_functionality_wrt_permutation
∀[A:Type]. ∀L1,L2:A List. ∀x:A. (permutation(A;L1;L2) ⇒ permutation(A;[x / L1];[x / L2]))
Lemma: permutation-split
∀[A:Type]. ∀p:A ⟶ 𝔹. ∀L:A List. permutation(A;filter(λx.p[x];L) @ filter(λx.(¬bp[x]);L);L)
Lemma: permutation-split2
∀[A:Type]
∀p,q:A ⟶ 𝔹. ((∀a:A. (↑q[a] ⇐⇒ ¬↑p[a])) ⇒ (∀L:A List. permutation(A;filter(λx.p[x];L) @ filter(λx.q[x];L);L)))
Lemma: permutation-mapfilter
∀[A:Type]
∀L1,L2:A List.
(permutation(A;L1;L2)
⇒ (∀p:A ⟶ 𝔹. ∀[B:Type]. ∀f:{a:A| ↑(p a)} ⟶ B. permutation(B;mapfilter(f;p;L1);mapfilter(f;p;L2))))
Lemma: l_all_functionality_wrt_permutation
∀[A:Type]. ∀P:A ⟶ ℙ. ∀L1,L2:A List. (permutation(A;L1;L2) ⇒ {(∀x∈L1.P[x]) ⇐⇒ (∀x∈L2.P[x])})
Lemma: sum-as-accum
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
(Σ(f[x] | x < n) ~ accumulate (with value x and list item y):
x + y
over list:
map(λx.f[x];upto(n))
with starting value:
0))
Lemma: sum-as-accum2
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
(Σ(f[x] | x < n) ~ accumulate (with value x and list item y):
x + f[y]
over list:
upto(n)
with starting value:
0))
Lemma: sum-as-accum-filter
∀[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
(Σ(f[x] | x < n) ~ accumulate (with value x and list item y):
x + y
over list:
filter(λx.(¬b(x =z 0));map(λx.f[x];upto(n)))
with starting value:
0))
Definition: insert-by
insert-by(eq;r;x;l) ==
rec-case(l) of
[] => [x]
a::as =>
v.if eq x a then [a / as]
if r x a then [x; [a / as]]
else [a / v]
fi
Lemma: insert-by_wf
∀[T:Type]. ∀[eq,r:T ⟶ T ⟶ 𝔹]. ∀[x:T]. ∀[L:T List]. (insert-by(eq;r;x;L) ∈ T List)
Lemma: member-insert-by
∀[T:Type]
∀eq,r:T ⟶ T ⟶ 𝔹.
∀x:T. ∀L:T List. ∀z:T. ((z ∈ insert-by(eq;r;x;L)) ⇐⇒ (z = x ∈ T) ∨ (z ∈ L))
supposing ∀a,b:T. (↑(eq a b) ⇐⇒ a = b ∈ T)
Definition: comparison
comparison(T) ==
{cmp:T ⟶ T ⟶ ℤ|
(∀x,y:T. ((cmp x y) = (-(cmp y x)) ∈ ℤ))
∧ (∀x,y:T. (((cmp x y) = 0 ∈ ℤ) ⇒ (∀z:T. ((cmp x z) = (cmp y z) ∈ ℤ))))
∧ (∀x,y,z:T. ((0 ≤ (cmp x y)) ⇒ (0 ≤ (cmp y z)) ⇒ (0 ≤ (cmp x z))))}
Lemma: comparison_wf
∀T:Type. (comparison(T) ∈ Type)
Lemma: subtype_rel_comparison
∀[A,B:Type]. comparison(B) ⊆r comparison(A) supposing A ⊆r B
Lemma: comparison-equiv
∀[T:Type]. ∀cmp:comparison(T). EquivRel(T;x,y.(cmp x y) = 0 ∈ ℤ)
Lemma: comparison-reflexive
∀[T:Type]. ∀cmp:comparison(T). ∀x:T. ((cmp x x) = 0 ∈ ℤ)
Lemma: comparison-anti
∀[T:Type]. ∀[cmp:comparison(T)]. ∀[x,y:T]. ((cmp x y) = (-(cmp y x)) ∈ ℤ)
Definition: int-minus-comparison
int-minus-comparison(f) == λx,y. ((f x) - f y)
Lemma: int-minus-comparison_wf
∀[T:Type]. ∀[f:T ⟶ ℤ]. (int-minus-comparison(f) ∈ comparison(T))
Definition: int-minus-comparison-inc
int-minus-comparison-inc(f) == λx,y. ((f y) - f x)
Lemma: int-minus-comparison-inc_wf
∀[T:Type]. ∀[f:T ⟶ ℤ]. (int-minus-comparison-inc(f) ∈ comparison(T))
Definition: bool-cmp
bool-cmp() == λx,y. if x then if y then 0 else 1 fi if y then -1 else 0 fi
Lemma: bool-cmp_wf
bool-cmp() ∈ comparison(𝔹)
Lemma: bool-cmp-zero
∀[x,y:𝔹]. uiff((bool-cmp() x y) = 0 ∈ ℤ;x = y)
Definition: compare-fun
compare-fun(cmp;f) == λx,y. (cmp (f x) (f y))
Lemma: compare-fun_wf
∀[A,B:Type]. ∀[cmp:comparison(B)]. ∀[f:A ⟶ B]. (compare-fun(cmp;f) ∈ comparison(A))
Definition: cmp-type
cmp-type(T;cmp) == x,y:T//((cmp x y) = 0 ∈ ℤ)
Lemma: cmp-type_wf
∀[T:Type]. ∀cmp:comparison(T). (cmp-type(T;cmp) ∈ Type)
Definition: cmp-le
cmp-le(cmp;x;y) == 0 ≤ (cmp x y)
Lemma: cmp-le_wf
∀[T:Type]. ∀[cmp:comparison(T)]. ∀[x,y:cmp-type(T;cmp)]. (cmp-le(cmp;x;y) ∈ ℙ)
Lemma: decidable__cmp-le
∀[T:Type]. ∀cmp:comparison(T). ∀x,y:cmp-type(T;cmp). Dec(cmp-le(cmp;x;y))
Lemma: comparison-trans
∀[T:Type]. ∀cmp:comparison(T). Trans(T;x,y.0 ≤ (cmp x y))
Lemma: strict-comparison-trans
∀[T:Type]. ∀cmp:comparison(T). Trans(T;x,y.0 < cmp x y)
Lemma: comparison-connex
∀[T:Type]. ∀cmp:comparison(T). Connex(T;x,y.0 ≤ (cmp x y))
Lemma: comparison-antisym
∀[T:Type]. ∀cmp:comparison(T). AntiSym(T;x,y.0 ≤ (cmp x y)) supposing ∀x,y:T. (((cmp x y) = 0 ∈ ℤ) ⇒ (x = y ∈ T))
Lemma: comparison-refl
∀[T:Type]. ∀cmp:comparison(T). Refl(T;x,y.0 ≤ (cmp x y))
Lemma: comparison-linear
∀[T:Type]. ∀cmp:comparison(T). Linorder(cmp-type(T;cmp);x,y.cmp-le(cmp;x;y))
Definition: comparison-seq
comparison-seq(c1; c2) == λx,y. eval answer1 = c1 x y in if answer1=0 then c2 x y else answer1
Lemma: comparison-seq_wf
∀[T:Type]. ∀[c1:comparison(T)]. ∀[c2:⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )]. (comparison-seq(c1; c2) ∈ comparison(\000CT))
Lemma: comparison-seq-simple-wf
∀[T:Type]. ∀[c1,c2:comparison(T)]. (comparison-seq(c1; c2) ∈ comparison(T))
Lemma: comparison-seq-zero
∀[T:Type]. ∀[c1:comparison(T)]. ∀[c2:⋂a:T. comparison({b:T| (c1 a b) = 0 ∈ ℤ} )]. ∀[x,y:T].
uiff((comparison-seq(c1; c2) x y) = 0 ∈ ℤ;((c1 x y) = 0 ∈ ℤ) ∧ ((c2 x y) = 0 ∈ ℤ))
Lemma: comparison-seq-zero-simple
∀[T:Type]. ∀[c1,c2:comparison(T)]. ∀[x,y:T].
uiff((comparison-seq(c1; c2) x y) = 0 ∈ ℤ;((c1 x y) = 0 ∈ ℤ) ∧ ((c2 x y) = 0 ∈ ℤ))
Definition: find-combine
find-combine(cmp;l) ==
rec-case(l) of
[] => inr ⋅
a::as =>
v.eval tst = cmp a in
if (tst =z 0) then inl a
if 0 <z tst then inr ⋅
else v
fi
Lemma: find-combine_wf
∀[T:Type]. ∀[cmp:T ⟶ ℤ]. ∀[l:T List]. (find-combine(cmp;l) ∈ T?)
Lemma: find-combine-nil
∀[cmp:Top]. (find-combine(cmp;[]) ~ inr ⋅ )
Lemma: find-combine-cons
∀[cmp,x,l:Top].
(find-combine(cmp;[x / l]) ~ eval tst = cmp x in
if (tst =z 0) then inl x
if 0 <z tst then inr ⋅
else find-combine(cmp;l)
fi )
Definition: insert-combine
insert-combine(cmp;f;x;l) ==
rec-case(l) of
[] => [x]
a::as =>
v.eval tst = cmp x a in
if (tst =z 0) then [f x a / as]
if 0 <z tst then [x; [a / as]]
else [a / v]
fi
Lemma: insert-combine_wf
∀T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x:T. ∀L:T List. (insert-combine(cmp;f;x;L) ∈ T List)
Lemma: insert-combine-cons
∀cmp,f,x,a,as:Top.
(insert-combine(cmp;f;x;[a / as]) ~ eval tst = cmp x a in
if (tst =z 0) then [f x a / as]
if 0 <z tst then [x; [a / as]]
else [a / insert-combine(cmp;f;x;as)]
fi )
Lemma: insert-combine-nil
∀cmp,f,x:Top. (insert-combine(cmp;f;x;[]) ~ [x])
Lemma: member-insert-combine
∀T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x,z:T. ∀v:T List.
((z ∈ insert-combine(cmp;f;x;v)) ⇒ ((z ∈ v) ∨ (z = x ∈ T) ∨ (∃y∈v. ((cmp x y) = 0 ∈ ℤ) ∧ (z = (f x y) ∈ T))))
Lemma: member-insert-combine2
∀T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x,z:T. ∀v:T List.
((z ∈ insert-combine(cmp;f;x;v))
⇐⇒ (∃l:T List. (l @ [z] ≤ v ∧ (∀y∈l.cmp x y < 0) ∧ cmp x z < 0))
∨ (∃l,l':T List
∃a:T
(((l @ [a / l']) = v ∈ (T List))
∧ (∀y∈l.cmp x y < 0)
∧ ((0 < cmp x a ∧ (z ∈ [x; [a / l']])) ∨ (((cmp x a) = 0 ∈ ℤ) ∧ (z ∈ [f x a / l'])))))
∨ ((z = x ∈ T) ∧ (∀y∈v.cmp x y < 0)))
Lemma: insert-combine-sorted-by
∀T:Type. ∀cmp:comparison(T).
((∀u,x,z:T. (0 < cmp x u ⇒ 0 < cmp u z ⇒ 0 < cmp x z))
⇒ (∀f:T ⟶ T ⟶ T
((∀u,x:T. (((cmp x u) = 0 ∈ ℤ) ⇒ ((cmp u (f x u)) = 0 ∈ ℤ)))
⇒ (∀L:T List. ∀x:T. (sorted-by(λx,y. 0 < cmp x y;L) ⇒ sorted-by(λx,y. 0 < cmp x y;insert-combine(cmp;f;x;L)))\000C))))
Definition: remove-combine
remove-combine(cmp;l) ==
rec-case(l) of
[] => []
a::as =>
v.eval tst = cmp a in
if (tst =z 0) then as
if 0 <z tst then [a / as]
else [a / v]
fi
Lemma: remove-combine_wf
∀T:Type. ∀cmp:T ⟶ ℤ. ∀l:T List. (remove-combine(cmp;l) ∈ T List)
Lemma: remove-combine-nil
∀[cmp:Top]. (remove-combine(cmp;[]) ~ [])
Lemma: remove-combine-cons
∀[T:Type]. ∀[cmp:T ⟶ ℤ]. ∀[x:T]. ∀[l:T List].
(remove-combine(cmp;[x / l]) ~ if (cmp x =z 0) then l
if 0 <z cmp x then [x / l]
else [x / remove-combine(cmp;l)]
fi )
Lemma: remove-combine-implies-member
∀[T:Type]. ∀cmp:T ⟶ ℤ. ∀x:T. ∀l:T List. ((x ∈ remove-combine(cmp;l)) ⇒ (x ∈ l))
Lemma: remove-combine-implies-member2
∀[T:Type]. ∀cmp:T ⟶ ℤ. ∀x:T. ∀l:T List. ((¬((cmp x) = 0 ∈ ℤ)) ⇒ (x ∈ l) ⇒ (x ∈ remove-combine(cmp;l)))
Definition: insert-no-combine
insert-no-combine(cmp;x;l) == rec-case(l) of [] => [x] | a::as => v.if 0 ≤z cmp x a then [x; [a / as]] else [a / v] fi
Lemma: insert-no-combine_wf
∀[T:Type]. ∀[cmp:comparison(T)]. ∀[x:T]. ∀[L:T List]. (insert-no-combine(cmp;x;L) ∈ T List)
Lemma: insert-no-combine-permutation
∀T:Type. ∀cmp:comparison(T). ∀L:T List. ∀u:T. permutation(T;insert-no-combine(cmp;u;L);[u] @ L)
Lemma: member-insert-no-combine
∀T:Type. ∀cmp:comparison(T). ∀x,z:T. ∀v:T List. ((z ∈ insert-no-combine(cmp;x;v)) ⇐⇒ (z ∈ [x / v]))
Lemma: insert-no-combine-sorted-by
∀[T:Type]
∀cmp:comparison(T)
((∀u,x,z:T. ((0 ≤ (cmp x u)) ⇒ (0 ≤ (cmp u z)) ⇒ (0 ≤ (cmp x z))))
⇒ (∀L:T List. ∀x:T. (sorted-by(λx,y. (0 ≤ (cmp x y));L) ⇒ sorted-by(λx,y. (0 ≤ (cmp x y));insert-no-combine(cmp;x\000C;L)))))
Definition: comparison-sort
comparison-sort(cmp;L) == eager-accum(srtd,x.insert-no-combine(cmp;x;srtd);[];L)
Lemma: comparison-sort_wf
∀[T:Type]. ∀[cmp:comparison(T)].
∀L:T List. (comparison-sort(cmp;L) ∈ {srtd:T List| sorted-by(λx,y. (0 ≤ (cmp x y));srtd)} ) supposing valueall-type(T)
Lemma: comparison-sort-permutation
∀T:Type. (valueall-type(T) ⇒ (∀cmp:comparison(T). ∀L:T List. permutation(T;comparison-sort(cmp;L);L)))
Definition: comparison-max
comparison-max(cmp;L) == eager-accum(mx,x.if 0 ≤z cmp x mx then mx else x fi ;hd(L);tl(L))
Lemma: comparison-max_wf
∀[T:Type]. ∀[cmp:comparison(T)]. ∀L:T List+. (comparison-max(cmp;L) ∈ {mx:T| (mx ∈ L) ∧ (∀x∈L.0 ≤ (cmp x mx))} ) suppos\000Cing valueall-type(T)
Lemma: insert-by-sorted-by
∀[T:Type]
∀eq,r:T ⟶ T ⟶ 𝔹.
Linorder(T;a,b.↑(r a b))
⇒ (∀x:T. ∀L:T List. (sorted-by(λx,y. (↑(r x y));L) ⇒ sorted-by(λx,y. (↑(r x y));insert-by(eq;r;x;L))))
supposing ∀a,b:T. (↑(eq a b) ⇐⇒ a = b ∈ T)
Lemma: s-insert-no-repeats
∀[T:Type]. ∀[x:T]. ∀[L:T List]. (no_repeats(T;s-insert(x;L))) supposing (no_repeats(T;L) and sorted(L)) supposing T ⊆r \000Cℤ
Lemma: insert-by-no-repeats
∀[T:Type]. ∀[eq,r:T ⟶ T ⟶ 𝔹].
(∀[x:T]. ∀[L:T List].
(no_repeats(T;insert-by(eq;r;x;L))) supposing (no_repeats(T;L) and sorted-by(λx,y. (↑(r x y));L))) supposing
(Linorder(T;a,b.↑(r a b)) and
(∀a,b:T. (↑(eq a b) ⇐⇒ a = b ∈ T)))
Lemma: sorted-by-exists
∀[T:Type]
∀eq,r:T ⟶ T ⟶ 𝔹.
Linorder(T;a,b.↑(r a b))
⇒ (∀L:T List. ∃L':T List. (sorted-by(λx,y. (↑(r x y));L') ∧ no_repeats(T;L') ∧ L ⊆ L' ∧ L' ⊆ L))
supposing ∀a,b:T. (↑(eq a b) ⇐⇒ a = b ∈ T)
Lemma: sorted-by-exists2
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
((∀a,b:T. Dec(a = b ∈ T))
⇒ (∀a,b:T. Dec(R a b))
⇒ Linorder(T;a,b.R a b)
⇒ (∀L:T List. ∃L':T List. (sorted-by(R;L') ∧ no_repeats(T;L') ∧ L ⊆ L' ∧ L' ⊆ L)))
Lemma: l_all_assert_iff_reduce
∀[A:Type]. ∀[P:A ⟶ 𝔹]. ∀[L:A List]. uiff((∀x∈L.↑P[x]);↑reduce(λx,b. (P[x] ∧b b);tt;L))
Lemma: l_all_exists_injection
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ]. ∀[P:B ⟶ ℙ].
∀L:A List
((∀x∈L.∃y:B. (R[x;y] ∧ P[y])) ⇒ (∃f:ℕ||L|| ⟶ {y:B| P[y]} . Inj(ℕ||L||;{y:B| P[y]} ;f))) supposing
(no_repeats(A;L) and
(∀x1,x2:A. ∀y:B. (R[x1;y] ⇒ R[x2;y] ⇒ (x1 = x2 ∈ A))))
Lemma: l_all_exists_max
∀[A:Type]. ∀[R:A ⟶ ℤ ⟶ ℙ].
((∀x:A. ∀n,m:ℤ. (R[x;n] ⇒ R[x;m] supposing n ≤ m)) ⇒ (∀L:A List. ((∀x∈L.∃n:ℤ. R[x;n]) ⇒ (∃n:ℤ. (∀x∈L.R[x;n])))))
Lemma: l_exists_filter
∀[T:Type]. ∀[Q:T ⟶ ℙ]. ∀P:T ⟶ 𝔹. ∀L:T List. ((∃x∈filter(P;L). Q[x]) ⇐⇒ ∃x:T. ((x ∈ L) ∧ (↑(P x)) ∧ Q[x]))
Lemma: l_all_sublist
∀[A:Type]. ∀P:A ⟶ ℙ. ∀as,bs:A List. (as ⊆ bs ⇒ (∀x∈bs.P[x]) ⇒ (∀x∈as.P[x]))
Definition: remove-first
remove-first(P;L) == rec-case(L) of [] => [] | a::as => r.if P a then as else [a / r] fi
Lemma: remove-first_wf
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. (remove-first(P;L) ∈ T List)
Lemma: length-remove-first
∀[T:Type]
∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹.
(((∀x∈L.¬↑(P x)) ∧ (remove-first(P;L) ~ L)) ∨ ((∃x∈L. ↑(P x)) ∧ (||remove-first(P;L)|| = (||L|| - 1) ∈ ℤ)))
Lemma: length-remove-first-le
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. (||remove-first(P;L)|| ≤ ||L||)
Lemma: select-remove-first
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ∀[i:ℕ||remove-first(P;L)||].
(remove-first(P;L)[i] ~ L[i] supposing ∀j:ℕi + 1. (¬↑(P L[j]))
∧ remove-first(P;L)[i] ~ L[i + 1] supposing ∃j:ℕi + 1. (↑(P L[j])))
Lemma: remove-first-cons
∀[L,x,P:Top]. (remove-first(P;[x / L]) ~ if P x then L else [x / remove-first(P;L)] fi )
Lemma: remove-first-member-implies
∀[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹. ∀x:T. ((x ∈ remove-first(P;L)) ⇒ (x ∈ L))
Lemma: no_repeats-remove-first
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. no_repeats(T;remove-first(P;L)) supposing no_repeats(T;L)
Lemma: remove-first-no_repeats-member
∀[T:Type]
∀L:T List. ∀P:{x:T| (x ∈ L)} ⟶ 𝔹. ∀x:T.
(no_repeats(T;L)
⇒ (∀a,b:{x:T| (x ∈ L)} . (((↑(P a)) ∧ (↑(P b))) ⇒ (a = b ∈ T)))
⇒ ((x ∈ remove-first(P;L)) ⇐⇒ (x ∈ L) ∧ (↑¬b(P x))))
Lemma: filter-equals
∀[T:Type]
∀P:T ⟶ 𝔹. ∀L1,L2:T List.
(filter(P;L1) = L2 ∈ (T List)
⇐⇒ (∀x:T. ((x ∈ L2) ⇐⇒ (x ∈ L1) ∧ (↑(P x)))) ∧ (∀x,y:T. (x before y ∈ L2 ⇒ x before y ∈ L1))) supposing
(no_repeats(T;L2) and
no_repeats(T;L1))
Lemma: implies-filter-equal
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List].
(filter(P;L1) = L2 ∈ (T List)) supposing
(((∀x:T. ((x ∈ L2) ⇐⇒ (x ∈ L1) ∧ (↑(P x)))) ∧ (∀x,y:T. (x before y ∈ L2 ⇒ x before y ∈ L1))) and
no_repeats(T;L1))
Lemma: filter-sq
∀[T:Type]. ∀[L:T List]. ∀[P,Q:{x:T| (x ∈ L)} ⟶ 𝔹].
filter(P;L) ~ filter(Q;L) supposing ∀x:{x:T| (x ∈ L)} . (↑(P x) ⇐⇒ ↑(Q x))
Lemma: filter-equal
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L1,L2:T List].
(filter(P;L1) = filter(P;L2) ∈ (T List)) supposing
((∀i:ℕ||L1||. ((L1[i] = L2[i] ∈ T) ∨ ((¬↑(P L1[i])) ∧ (¬↑(P L2[i]))))) and
(||L1|| = ||L2|| ∈ ℤ))
Lemma: filter-le
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. (||filter(P;L)|| ≤ ||L||)
Lemma: filter-less
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. ||filter(P;L)|| < ||L|| supposing ∃x:T. ((x ∈ L) ∧ (¬↑(P x)))
Lemma: filter-upto-length
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List]. (filter(P;L) ~ map(λi.L[i];filter(λi.(P L[i]);upto(||L||))))
Lemma: map-filter
∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].
∀[L:T List]. (map(f;filter(P;L)) ~ filter(Q;map(f;L))) supposing ∀x:T. Q (f x) = P x
Lemma: map-filter-proof2
∀[T,A:Type]. ∀[f:T ⟶ A]. ∀[P:T ⟶ 𝔹]. ∀[Q:A ⟶ 𝔹].
∀[L:T List]. (map(f;filter(P;L)) ~ filter(Q;map(f;L))) supposing ∀x:T. Q (f x) = P x
Lemma: no-member-sq-nil
∀[T:Type]. ∀[L:T List]. L ~ [] supposing ∀x:T. (¬(x ∈ L))
Lemma: equal-nil-sq-nil
∀[T:Type]. ∀[L:T List]. L ~ [] supposing L = [] ∈ (T List)
Lemma: last-mapfilter3
∀[A,B:Type]. ∀[L:A List]. ∀[P:A ⟶ 𝔹]. ∀[f:{x:A| ↑(P x)} ⟶ B].
(last(mapfilter(f;P;L)) = (f last(L)) ∈ B) supposing ((↑(P last(L))) and (¬↑null(mapfilter(f;P;L))))
Definition: l_sum
l_sum(L) == reduce(λx,y. (x + y);0;L)
Lemma: l_sum_wf
∀[L:ℤ List]. (l_sum(L) ∈ ℤ)
Lemma: l_sum-wf-partial-nat
∀[L:partial(ℕ) List]. (l_sum(L) ∈ partial(ℕ))
Lemma: l_sum_filter0
∀[L:ℤ List]. (l_sum(L) = l_sum(filter(λx.(¬b(x =z 0));L)) ∈ ℤ)
Lemma: l_sum-sum
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ]. (l_sum(map(f;L)) = Σ(f L[i] | i < ||L||) ∈ ℤ)
Lemma: sum-l_sum
∀[n:ℕ]. ∀[a:ℕn ⟶ ℤ]. (Σ(a[i] | i < n) = l_sum(map(λi.a[i];upto(n))) ∈ ℤ)
Lemma: summand-le-l_sum
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ].
∀x:{x:T| (x ∈ L)} . (f[x] ≤ l_sum(map(f;L))) supposing ∀x:{x:T| (x ∈ L)} . (0 ≤ f[x])
Lemma: l_sum-lower-bound
∀b:ℤ. ∀[L:ℤ List]. ((∀x∈L.b ≤ x) ⇒ ((b * ||L||) ≤ l_sum(L)))
Lemma: l_sum_nonneg
∀[L:ℤ List]. ((∀x∈L.0 ≤ x) ⇒ (0 ≤ l_sum(L)))
Lemma: l_sum-upper-bound
∀b:ℤ. ∀[L:ℤ List]. ((∀x∈L.x ≤ b) ⇒ (l_sum(L) ≤ (b * ||L||)))
Lemma: l_sum-upper-bound-map
∀[b:ℤ]. ∀[T:Type]. ∀[f:T ⟶ {...b}]. ∀[L:T List]. (l_sum(map(f;L)) ≤ (b * ||L||))
Lemma: l_sum-mapfilter
∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹]. ∀[f:{x:T| (x ∈ L) ∧ (↑(P x))} ⟶ ℤ].
(l_sum(mapfilter(f;P;L)) = Σ(if P L[i] then f L[i] else 0 fi | i < ||L||) ∈ ℤ)
Lemma: l_sum-mapfilter-upto
∀[n:ℕ]. ∀[P:ℕn ⟶ 𝔹]. ∀[f:{x:ℕn| ↑(P x)} ⟶ ℤ].
(l_sum(mapfilter(f;P;upto(n))) = Σ(if P i then f i else 0 fi | i < n) ∈ ℤ)
Lemma: l_sum_nil_lemma
l_sum([]) ~ 0
Lemma: l_sum_cons_lemma
∀L,a:Top. (l_sum([a / L]) ~ a + l_sum(L))
Lemma: l_sum-append
∀[L1,L2:ℤ List]. (l_sum(L1 @ L2) ~ l_sum(L1) + l_sum(L2))
Lemma: l_sum_permute
∀[L1,L2:ℤ List]. l_sum(L1) = l_sum(L2) ∈ ℤ supposing permutation(ℤ;L1;L2)
Lemma: l_sum-mul-left
∀[L:ℤ List]. ∀[m:ℤ]. (m * l_sum(L) ~ l_sum(map(λx.(m * x);L)))
Lemma: l_sum_as_accum
∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. ∀[x:ℤ].
(accumulate (with value s and list item a):
s + f[a]
over list:
L
with starting value:
x) ~ l_sum(map(λx.f[x];L)) + x)
Lemma: l_sum_as_reduce_general
∀[T:Type]. ∀[f:T ⟶ ℤ]. ∀[L:T List]. ∀[x:ℤ]. (reduce(λa,s. (s + f[a]);x;L) ~ l_sum(map(λx.f[x];L)) + x)
Lemma: l_sum_as_reduce
∀[L:ℤ List]. (reduce(λa,s. (s + a);0;L) ~ l_sum(L))
Lemma: l_sum-split
∀[A:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)} ⟶ ℤ]. ∀[P:{a:A| (a ∈ L)} ⟶ 𝔹].
(l_sum(map(f;L)) = (l_sum(map(f;filter(P;L))) + l_sum(map(f;filter(λx.(¬b(P x));L)))) ∈ ℤ)
Lemma: l_sum_functionality_wrt_permutation
∀[L1,L2:ℤ List]. l_sum(L1) = l_sum(L2) ∈ ℤ supposing permutation(ℤ;L1;L2)
Lemma: l_sum-triangle-inequality-general
∀[T:Type]. ∀[L:T List]. ∀[x,y:ℤ]. ∀[f,g:T ⟶ ℤ].
(|(l_sum(map(λa.f[a];L)) + x) - l_sum(map(λa.g[a];L)) + y| ≤ (l_sum(map(λa.|f[a] - g[a]|;L)) + |x - y|))
Lemma: l_sum-triangle-inequality
∀[T:Type]. ∀[L:T List]. ∀[f,g:T ⟶ ℤ].
(|l_sum(map(λa.f[a];L)) - l_sum(map(λa.g[a];L))| ≤ l_sum(map(λa.|f[a] - g[a]|;L)))
Lemma: le-l_sum
∀[T:Type]. ∀[f:T ⟶ ℕ]. ∀[L:T List]. ∀[t:T]. ((t ∈ L) ⇒ ((f t) ≤ l_sum(map(f;L))))
Definition: lsum
Σ(f[x] | x ∈ L) == l_sum(map(λx.f[x];L))
Lemma: lsum_wf
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ]. (Σ(f[x] | x ∈ L) ∈ ℤ)
Lemma: lsum_nil_lemma
∀f:Top. (Σ(f[x] | x ∈ []) ~ 0)
Lemma: lsum_cons_lemma
∀as,a,f:Top. (Σ(f[x] | x ∈ [a / as]) ~ f[a] + Σ(f[x] | x ∈ as))
Lemma: lsum-add
∀[T:Type]. ∀[L:T List]. ∀[f,g:{x:T| (x ∈ L)} ⟶ ℤ]. (Σ(f[x] + g[x] | x ∈ L) = (Σ(f[x] | x ∈ L) + Σ(g[x] | x ∈ L)) ∈ ℤ)
Lemma: lsum-append
∀[T:Type]. ∀[L1,L2:T List]. ∀[f:{x:T| (x ∈ L1 @ L2)} ⟶ ℤ].
(Σ(f[x] | x ∈ L1 @ L2) = (Σ(f[x] | x ∈ L1) + Σ(f[x] | x ∈ L2)) ∈ ℤ)
Lemma: lsum-mul-const
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ]. ∀[c:ℤ]. (Σ(c * f[x] | x ∈ L) = (c * Σ(f[x] | x ∈ L)) ∈ ℤ)
Lemma: lsum-0
∀[T:Type]. ∀[L:T List]. (Σ(0 | x ∈ L) = 0 ∈ ℤ)
Lemma: lsum-constant
∀[T:Type]. ∀[L:T List]. ∀[c:ℤ]. (Σ(c | x ∈ L) = (c * ||L||) ∈ ℤ)
Lemma: lsum-upto
∀[k:ℕ]. ∀[f:ℕk ⟶ ℤ]. (Σ(f[x] | x ∈ upto(k)) = Σ(f[x] | x < k) ∈ ℤ)
Lemma: double-lsum-swap
∀[T,S:Type]. ∀[K:T List]. ∀[L:S List]. ∀[f:T ⟶ S ⟶ ℤ].
(Σ(Σ(f[t;s] | s ∈ L) | t ∈ K) = Σ(Σ(f[t;s] | t ∈ K) | s ∈ L) ∈ ℤ)
Lemma: length-filter-lsum
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. (||filter(P;L)|| = Σ(if P x then 1 else 0 fi | x ∈ L) ∈ ℤ)
Lemma: count-related-pairs
∀[T,S:Type]. ∀[K:T List]. ∀[L:S List]. ∀[R:T ⟶ S ⟶ 𝔹].
(Σ(||filter(R t;L)|| | t ∈ K) = Σ(||filter(λt.(R t s);K)|| | s ∈ L) ∈ ℤ)
Lemma: lsum-split
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ].
(Σ(f[x] | x ∈ L) = (Σ(f[x] | x ∈ filter(λx.P[x];L)) + Σ(f[x] | x ∈ filter(λx.(¬bP[x]);L))) ∈ ℤ)
Lemma: summand-le-lsum
∀[T:Type]. ∀[L:T List]. ∀[f:{x:T| (x ∈ L)} ⟶ ℤ].
∀x:{x:T| (x ∈ L)} . (f[x] ≤ Σ(f[x] | x ∈ L)) supposing ∀x:{x:T| (x ∈ L)} . (0 ≤ f[x])
Definition: l_mul
l_mul(L) == reduce(λx,y. (x * y);1;L)
Lemma: l_mul_wf
∀[L:ℤ List]. (l_mul(L) ∈ ℤ)
Lemma: l_mul_permute
∀[L1,L2:ℤ List]. l_mul(L1) = l_mul(L2) ∈ ℤ supposing permutation(ℤ;L1;L2)
Lemma: length-concat
∀[ll:Top List List]. (||concat(ll)|| = l_sum(map(λl.||l||;ll)) ∈ ℤ)
Lemma: length-concat-lower-bound
∀[ll:Top List+ List]. (||ll|| ≤ ||concat(ll)||)
Lemma: l_disjoint-concat
∀[T:Type]. ∀[LL:T List List]. ∀[L:T List]. uiff(l_disjoint(T;L;concat(LL));(∀l2∈LL.l_disjoint(T;L;l2)))
Lemma: no_repeats-concat-iff
∀[T:Type]. ∀[ll:T List List].
uiff(no_repeats(T;concat(ll));(∀l∈ll.no_repeats(T;l)) ∧ (∀l1,l2∈ll. l_disjoint(T;l1;l2)))
Lemma: no_repeats-concat
∀[T:Type]. ∀[ll:T List List].
(no_repeats(T;concat(ll))) supposing ((∀l∈ll.no_repeats(T;l)) and (∀l1,l2∈ll. l_disjoint(T;l1;l2)))
Definition: mapl
mapl(f;l) == map(f;l)
Lemma: mapl_wf
∀[A,B:Type]. ∀[L:A List]. ∀[f:{a:A| (a ∈ L)} ⟶ B]. (mapl(f;L) ∈ B List)
Lemma: member-mapl
∀[T,T':Type]. ∀L:T List. ∀y:T'. ∀f:{x:T| (x ∈ L)} ⟶ T'. ((y ∈ mapl(f;L)) ⇐⇒ ∃a:T. ((a ∈ L) c∧ (y = (f a) ∈ T')))
Lemma: pairwise-mapl
∀[T,T':Type].
∀L:T List. ∀f:{x:T| (x ∈ L)} ⟶ T'.
∀[P:T' ⟶ T' ⟶ ℙ']. ((∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ P[f x;f y])) ⇒ (∀x,y∈mapl(f;L). P[x;y]))
Lemma: pairwise-mapl-no-repeats
∀[T,T':Type].
∀L:T List. ∀f:{x:T| (x ∈ L)} ⟶ T'.
∀[P:T' ⟶ T' ⟶ ℙ']
(∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ P[f x;f y] supposing ¬(x = y ∈ T))) ⇒ (∀x,y∈mapl(f;L). P[x;y])
supposing no_repeats(T;L)
Lemma: no_repeats_map
∀[T:Type]. ∀[L:T List]. ∀[A:Type]. ∀[f:{x:T| (x ∈ L)} ⟶ A]. no_repeats(A;map(f;L)) supposing Inj({x:T| (x ∈ L)} ;A;f\000C) supposing no_repeats(T;L)
Lemma: no_repeats_map_uiff
∀[T:Type]. ∀[L:T List]. ∀[A:Type]. ∀[f:{x:T| (x ∈ L)} ⟶ A].
uiff(no_repeats(A;map(f;L));no_repeats(T;L)) supposing Inj({x:T| (x ∈ L)} ;A;f)
Lemma: no_repeats_concat
∀[T:Type]. ∀[ll:T List List].
uiff(no_repeats(T;concat(ll));∀i:ℕ||ll||
(no_repeats(T;ll[i])
∧ (∀j:{j:ℕ||ll||| ¬(i = j ∈ ℤ)} . ∀k:ℕ||ll[i]||. (¬(ll[i][k] ∈ ll[j])))))
Lemma: map-is-permutation-on-list-of-all
∀[T:Type]
∀f:T ⟶ T. (Bij(T;T;f) ⇒ (∀as:T List. ((no_repeats(T;as) ∧ (∀t:T. (t ∈ as))) ⇒ permutation(T;as;map(f;as)))))
Lemma: sorted-by-append1
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀x:T. ∀L:T List. (sorted-by(R;L @ [x]) ⇐⇒ sorted-by(R;L) ∧ (∀z∈L.R z x))
Lemma: sorted-by-no_repeats
∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ]. ∀[L:T List]. no_repeats(T;L) supposing sorted-by(R;L) supposing ∀x:T. (¬(R x x))
Lemma: fseg-iseg-reverse
∀[T:Type]. ∀[L1,L2:T List]. (fseg(T;L1;L2) ⇐⇒ rev(L1) ≤ rev(L2))
Lemma: filter-filter2
∀[P1,P2,L:Top]. (filter(P2;filter(P1;L)) ~ filter(λt.((P1 t) ∧b (P2 t));L))
Lemma: filter-singleton
∀[x,P:Top]. (filter(P;[x]) ~ if P x then [x] else [] fi )
Lemma: length-zero-implies-sq-nil
∀l:Top List. l ~ [] supposing ||l|| = 0 ∈ ℤ
Lemma: map_equal
∀[T,T':Type]. ∀[a:T List]. ∀[f,g:T ⟶ T'].
map(f;a) = map(g;a) ∈ (T' List) supposing ∀i:ℕ. (i < ||a|| ⇒ ((f a[i]) = (g a[i]) ∈ T'))
Lemma: select_equal
∀[T:Type]. ∀[a,b:T List]. ∀[i:ℕ]. (a[i] = b[i] ∈ T) supposing (i < ||a|| and (a = b ∈ (T List)))
Lemma: list_decomp_reverse
∀[T:Type]. ∀L:T List. ∃x:T. ∃L':T List. (L = (L' @ [x]) ∈ (T List)) supposing 0 < ||L||
Definition: list_decomp_rev
list_decomp_rev{i:l}(l) == let x,y = TERMOF{list_decomp_reverse:o, 1:l, i:l} l in let L,a = y in <x, L>
Lemma: list_decomp_rev_wf
∀[T:Type]. ∀[l:T List]. list_decomp_rev{i:l}(l) ∈ {p:T × (T List)| l = ((snd(p)) @ [fst(p)]) ∈ (T List)} supposing 0 <\000C ||l||
Lemma: list_append_singleton_ind
∀[T:Type]. ∀[Q:(T List) ⟶ ℙ]. (Q[[]] ⇒ (∀ys:T List. ∀x:T. (Q[ys] ⇒ Q[ys @ [x]])) ⇒ {∀zs:T List. Q[zs]})
Definition: list_ind_reverse
list_ind_reverse(L;nilcase;R) ==
fix((λF,l. if (||l|| =z 0) then nilcase else R (F firstn(||l|| - 1;l)) firstn(||l|| - 1;l) last(l) fi )) L
Lemma: list_ind_reverse_wf
∀[A,B:Type]. ∀[L:A List]. ∀[nilcase:B]. ∀[F:B ⟶ (A List) ⟶ A ⟶ B]. (list_ind_reverse(L;nilcase;F) ∈ B)
Lemma: list_ind_reverse_wf_dependent
∀[A,B:Type].
∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀P:(A List) ⟶ B ⟶ ℙ.
((P [] nilcase)
⇒ (∀L:A List. ∀x:A. ∀b:B. ((b = list_ind_reverse(L;nilcase;F) ∈ B) ⇒ (P L b) ⇒ (P (L @ [x]) (F b L x))))
⇒ (∀L:A List. (P L list_ind_reverse(L;nilcase;F))))
Lemma: list_ind_reverse_unfold1
∀[A,B:Type].
∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.
(list_ind_reverse(L;nilcase;F) ~ if (||L|| =z 0)
then nilcase
else F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)
fi )
Lemma: list_ind_reverse_unfold
∀[A,B:Type].
∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.
((||L|| > 0)
⇒ (list_ind_reverse(L;nilcase;F) ~ F list_ind_reverse(firstn(||L|| - 1;L);nilcase;F) firstn(||L|| - 1;L) last(L)))
Lemma: map_length_nat
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. (||map(f;as)|| = ||as|| ∈ ℕ)
Lemma: list_2_decomp
∀[T:Type]. ∀[z:T List]. z = [z[0]; z[1]] ∈ (T List) supposing ||z|| = 2 ∈ ℕ
Lemma: listp_decomp
∀[T:Type]. ∀L:T List+. ∃x:T. ∃K:T List. (L = (K @ [x]) ∈ (T List))
Lemma: list_decomp_last
∀[T:Type]. ∀L:T List. ∃L':T List. (L = (L' @ [last(L)]) ∈ (T List)) supposing 0 < ||L||
Lemma: listp_decomp_last
∀[T:Type]. ∀L:T List+. ∃K:T List. (L = (K @ [last(L)]) ∈ (T List))
Lemma: list-decomp-nat
∀[T:Type]. ∀L:T List. ∀i:ℕ||L|| + 1. ∃K,J:T List. ((L = (K @ J) ∈ (T List)) ∧ (||K|| = i ∈ ℤ))
Lemma: list-decomp-nat-iseg
∀[T:Type]. ∀L:T List. ∀i:ℕ||L|| + 1. ∃K:T List. (K ≤ L ∧ (||K|| = i ∈ ℤ))
Lemma: mklist_member
∀[T:Type]. ∀n:ℕ. ∀f:ℕn ⟶ T. ∀x:T. ((x ∈ mklist(n;f)) ⇐⇒ ∃i:ℕn. (x = (f i) ∈ T))
Definition: single-valued-list
single-valued-list(L;T) == ∀x,y:T. ((x ∈ L) ⇒ (y ∈ L) ⇒ (x = y ∈ T))
Lemma: single-valued-list_wf
∀T:Type. ∀[L:T List]. (single-valued-list(L;T) ∈ ℙ)
Definition: list-rep
list-rep(n;x) == primrec(n;[];λi,r. [x / r])
Lemma: list-rep_wf
∀[T:Type]. ∀[n:ℕ]. ∀[x:T]. (list-rep(n;x) ∈ T List)
Lemma: append_iseg
∀[T:Type]. ∀as,bs,cs:T List. (as @ bs ≤ as @ cs ⇐⇒ bs ≤ cs)
Lemma: iseg_append_iff
∀[T:Type]
∀l1,l2,l3:T List. (l1 ≤ l2 @ l3 ⇐⇒ l1 ≤ l2 ∨ (∃l:T List. (0 < ||l|| ∧ (l1 = (l2 @ l) ∈ (T List)) ∧ l ≤ l3)))
Lemma: iseg_append_single
∀[T:Type]. ∀l1,l2:T List. ∀x:T. (l1 ≤ l2 @ [x] ⇐⇒ l1 ≤ l2 ∨ (l1 = (l2 @ [x]) ∈ (T List)))
Lemma: iseg_single
∀[T:Type]. ∀L:T List. ∀x:T. (L ≤ [x] ⇐⇒ (↑null(L)) ∨ (L = [x] ∈ (T List)))
Lemma: single_iseg
∀[T:Type]. ∀L:T List. ∀x:T. ([x] ≤ L ⇐⇒ 0 < ||L|| ∧ (L[0] = x ∈ T))
Lemma: iseg_append_length
∀[T:Type]. ∀l1,l2,l3:T List. (l1 ≤ l2 @ l3 ⇒ l1 ≤ l2 supposing ||l1|| ≤ ||l2||)
Lemma: decidable__exists_iseg
∀[T:Type]. ∀[P:(T List) ⟶ ℙ]. ((∀L:T List. Dec(P[L])) ⇒ (∀L:T List. Dec(∃L':T List. (L' ≤ L ∧ P[L']))))
Definition: proper-iseg
L1 < L2 == L1 ≤ L2 ∧ (¬(L1 = L2 ∈ (T List)))
Lemma: proper-iseg_wf
∀[T:Type]. ∀[L1,L2:T List]. (L1 < L2 ∈ ℙ{[1 | i 0]})
Lemma: cons-proper-iseg
∀[T:Type]. ∀L1,L2:T List. ∀a,b:T. ([a / L1] < [b / L2] ⇐⇒ L1 < L2 ∧ (a = b ∈ T))
Lemma: proper-iseg-append
∀[T:Type]. ∀L1,L2,L3,L4:T List. L1 @ L3 < L2 @ L4 ⇐⇒ L3 < L4 ∧ (L1 = L2 ∈ (T List)) supposing ||L1|| = ||L2|| ∈ ℤ
Lemma: proper-iseg-length
∀[T:Type]. ∀L1,L2:T List. (L1 < L2 ⇐⇒ L1 ≤ L2 ∧ ||L1|| < ||L2||)
Lemma: proper-iseg-append-one
∀[T:Type]. ∀L1,L2:T List. ∀x:T. (L1 < L2 @ [x] ⇐⇒ L1 ≤ L2)
Lemma: iseg-append-one
∀[T:Type]. ∀L1,L2:T List. ∀x:T. (L1 ≤ L2 @ [x] ⇐⇒ L1 ≤ L2 ∨ (L1 = (L2 @ [x]) ∈ (T List)))
Lemma: compat-iseg-cases
∀[T:Type]. ∀L1,L2:T List. (L1 || L2 ⇐⇒ L1 < L2 ∨ L2 < L1 ∨ (L1 = L2 ∈ (T List)))
Lemma: hd-before
∀[T:Type]. ∀L:T List. ∀x:T. ((x ∈ L) ⇒ hd(L) before x ∈ L supposing ¬(x = hd(L) ∈ T)) supposing 0 < ||L||
Lemma: hd-append
∀[T:Type]. ∀[L1:T List+]. ∀[L2:T List]. (hd(L1 @ L2) = hd(L1) ∈ T)
Lemma: hd-append-sq
∀[L1:Top List+]. ∀[L2:Top]. (hd(L1 @ L2) ~ hd(L1))
Lemma: before-hd
∀[T:Type]. ∀L:T List. (∀x:T. (x before hd(L) ∈ L ⇐⇒ False)) supposing (no_repeats(T;L) and 0 < ||L||)
Lemma: last-not-before
∀[T:Type]. ∀L:T List. (∀x:T. (last(L) before x ∈ L ⇐⇒ False)) supposing (no_repeats(T;L) and (¬↑null(L)))
Lemma: reject_cons_hd_sq
∀[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ]. [a / as]\[i] ~ as supposing i ≤ 0
Lemma: reject_cons_tl_sq
∀[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ]. ([a / as]\[i] ~ [a / as\[i - 1]]) supposing ((i ≤ ||as||) and 0 < i)
Lemma: reject_eq_firstn_nth_tl
∀[T:Type]. ∀[L:T List]. ∀[i:ℕ||L||]. (L\[i] ~ firstn(i;L) @ nth_tl(1 + i;L))
Lemma: sq_stable__fseg
∀[T:Type]. ∀l1,l2:T List. SqStable(fseg(T;l1;l2))
Lemma: nth_tl_map
∀[f:Top]. ∀[n:ℕ]. ∀[l:Top List]. (nth_tl(n;map(f;l)) ~ map(f;nth_tl(n;l)))
Lemma: continuous-monotone-list
∀[F:Type ⟶ Type]. ContinuousMonotone(T.F[T] List) supposing ContinuousMonotone(T.F[T])
Lemma: member_map2
∀[T,T':Type]. ∀a:T List. ∀x:T'. ∀f:{x:T| (x ∈ a)} ⟶ T'. ((x ∈ map(f;a)) ⇐⇒ ∃y:T. ((y ∈ a) ∧ (x = (f y) ∈ T')))
Lemma: no-repeats-pairwise
∀[T:Type]
∀L:T List
∀[P:{x:T| (x ∈ L)} ⟶ {x:T| (x ∈ L)} ⟶ ℙ']
(∀x,y:{x:T| (x ∈ L)} . P[x;y] supposing ¬(x = y ∈ T)) ⇒ (∀x,y∈L. P[x;y]) supposing no_repeats(T;L)
Lemma: iseg-mapfilter
∀[T:Type]
∀P:T ⟶ 𝔹. ∀[T':Type]. ∀f:{x:T| ↑(P x)} ⟶ T'. ∀L1,L2:T List. (L1 ≤ L2 ⇒ mapfilter(f;P;L1) ≤ mapfilter(f;P;L2))
Lemma: iseg-map
∀[A,B:Type]. ∀f:A ⟶ B. ∀L1,L2:A List. (L1 ≤ L2 ⇒ map(f;L1) ≤ map(f;L2))
Lemma: length_concat
∀[T:Type]. ∀[ll:T List List]. (||concat(ll)|| = Σ(||ll[i]|| | i < ||ll||) ∈ ℤ)
Lemma: select_concat_sum
∀[T:Type]. ∀[ll:T List List]. ∀[i:ℕ||ll||]. ∀[j:ℕ||ll[i]||]. (ll[i][j] = concat(ll)[Σ(||ll[k]|| | k < i) + j] ∈ T)
Lemma: member-concat
∀[T:Type]. ∀ll:T List List. ∀x:T. ((x ∈ concat(ll)) ⇐⇒ ∃l:T List. ((l ∈ ll) ∧ (x ∈ l)))
Lemma: member-concat-mklist
∀[T:Type]. ∀n:ℕ. ∀f:ℕn ⟶ (T List). ∀x:T. ((x ∈ concat(mklist(n;f))) ⇐⇒ ∃i:ℕn. (x ∈ f i))
Lemma: concat-decomp
∀[T:Type]
∀ll:T List List. ∀x:T.
((x ∈ concat(ll))
⇐⇒ ∃ll1,ll2:T List List
∃l1,l2:T List
((concat(ll) = (concat(ll1) @ (l1 @ [x] @ l2) @ concat(ll2)) ∈ (T List))
∧ (ll = (ll1 @ [l1 @ [x] @ l2] @ ll2) ∈ (T List List))))
Lemma: last-concat
∀[T:Type]
∀ll:T List List
∃ll1:T List List
∃l1:T List
((concat(ll) = (concat(ll1) @ l1 @ [last(concat(ll))]) ∈ (T List)) ∧ ll1 @ [l1 @ [last(concat(ll))]] ≤ ll)
supposing ¬(concat(ll) = [] ∈ (T List))
Lemma: last-concat-non-null
∀[T:Type]. ∀[ll:T List List].
((¬↑null(concat(ll))) ∧ (last(concat(ll)) = last(last(ll)) ∈ T)) supposing ((¬↑null(last(ll))) and (¬↑null(ll)))
Lemma: concat_iseg
∀[T:Type]. ∀ll1,ll2:T List List. (ll1 ≤ ll2 ⇒ concat(ll1) ≤ concat(ll2))
Lemma: iseg-append-nth_tl
∀[T:Type]. ∀[as,bs:T List]. (as @ nth_tl(||as||;bs)) = bs ∈ (T List) supposing as ≤ bs
Lemma: concat_map_upto
∀[T:Type]. ∀f:ℕ ⟶ (T List). ∀t,t':ℕ. concat(map(f;upto(t))) @ (f t) ≤ concat(map(f;upto(t'))) supposing t < t'
Lemma: concat-is-nil
∀[T:Type]. ∀[LL:T List List]. uiff(concat(LL) = [] ∈ (T List);(∀L∈LL.L = [] ∈ (T List)))
Lemma: map-reverse
∀[f:Top]. ∀[L:Top List]. (map(f;rev(L)) ~ rev(map(f;L)))
Lemma: filter-reverse
∀[T:Type]. ∀[f:T ⟶ 𝔹]. ∀[L:T List]. (filter(f;rev(L)) ~ rev(filter(f;L)))
Lemma: mapfilter-reverse
∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[f:Top]. ∀[L:T List]. (mapfilter(f;P;rev(L)) ~ rev(mapfilter(f;P;L)))
Lemma: sublist-reverse
∀[T:Type]. ∀L1,L2:T List. (rev(L1) ⊆ rev(L2) ⇐⇒ L1 ⊆ L2)
Lemma: last-reverse
∀[T:Type]. ∀[L:T List]. (last(rev(L)) ~ hd(L))
Lemma: hd-reverse
∀[T:Type]. ∀[L:T List]. (hd(rev(L)) ~ last(L))
Lemma: before-reverse
∀[T:Type]. ∀L:T List. ∀x,y:T. (x before y ∈ rev(L) ⇐⇒ y before x ∈ L)
Comment: map-index-comment
No doubt this function has already been defined elsewhere, but
I can't find it:
map-index(f; [x0; x1; ...]) = [f 0 x0 ; f 1 x1 ; ...]⋅
Definition: map-index_aux
map-index_aux(f;L) == rec-case(L) of [] => λn.[] | hd::tl => aux.λn.[f n hd / (aux (n + 1))]
Lemma: map-index_aux_wf
∀[A,B:Type]. ∀[L:A List]. ∀[x:ℤ]. ∀[f:{x..x + ||L||-} ⟶ A ⟶ B]. (map-index_aux(f;L) x ∈ B List)
Lemma: length-map-index_aux
∀[f:Top]. ∀[L:Top List]. ∀[x:Top]. (||map-index_aux(f;L) x|| ~ ||L||)
Lemma: select-map-index_aux
∀[f:Top]. ∀[L:Top List]. ∀[i:ℕ||L||]. ∀[x:ℤ]. (map-index_aux(f;L) x[i] ~ f (x + i) L[i])
Definition: map-index
map-index(f;L) == map-index_aux(f;L) 0
Lemma: map-index_wf
∀[A,B:Type]. ∀[L:A List]. ∀[f:ℕ||L|| ⟶ {a:A| (a ∈ L)} ⟶ B]. (map-index(f;L) ∈ B List)
Lemma: length-map-index
∀[f:Top]. ∀[L:Top List]. (||map-index(f;L)|| ~ ||L||)
Lemma: select-map-index
∀[f:Top]. ∀[L:Top List]. ∀[i:ℕ||L||]. (map-index(f;L)[i] ~ f i L[i])
Definition: zip
zip(as;bs) ==
fix((λzip,as,bs. case as of [] => [] | a::as' => case bs of [] => [] | b::bs' => [<a, b> / (zip as' bs')] esac esac)) \000Cas bs
Lemma: zip_wf
∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List]. (zip(as;bs) ∈ (T1 × T2) List)
Lemma: length-zip
∀[as,bs:Top List]. ||zip(as;bs)|| ~ ||as|| supposing ||as|| = ||bs|| ∈ ℤ
Lemma: zip_length
∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List]. ((||zip(as;bs)|| ≤ ||as||) ∧ (||zip(as;bs)|| ≤ ||bs||))
Lemma: select_zip
∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List]. ∀[i:ℕ].
zip(as;bs)[i] = <as[i], bs[i]> ∈ (T1 × T2) supposing i < ||zip(as;bs)||
Lemma: length_zip
∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List]. ||zip(as;bs)|| = ||as|| ∈ ℤ supposing ||as|| = ||bs|| ∈ ℤ
Lemma: zip_nil_lemma
∀x:Top. (zip([];x) ~ [])
Lemma: zip_cons_nil_lemma
∀b,a:Top. (zip([a / b];[]) ~ [])
Lemma: zip_cons_cons_lemma
∀d,c,b,a:Top. (zip([a / b];[c / d]) ~ [<a, c> / zip(b;d)])
Lemma: member-zip
∀[A,B:Type]. ∀xs:A List. ∀ys:B List. ∀x:A. ∀y:B. ((<x, y> ∈ zip(xs;ys)) ⇒ {(x ∈ xs) ∧ (y ∈ ys)})
Lemma: zip-append
∀[A,B:Type]. ∀[xs1:A List]. ∀[ys1:B List]. ∀[xs2:A List]. ∀[ys2:B List].
zip(xs1 @ xs2;ys1 @ ys2) ~ zip(xs1;ys1) @ zip(xs2;ys2) supposing ||xs1|| = ||ys1|| ∈ ℤ
Lemma: zip-map
∀[L:Top List]. ∀[f,g:Top]. (zip(map(f;L);map(g;L)) ~ map(λx.<f x, g x>;L))
Definition: unzip
unzip(as) == <map(λp.(fst(p));as), map(λp.(snd(p));as)>
Lemma: unzip_wf
∀[T1,T2:Type]. ∀[as:(T1 × T2) List]. (unzip(as) ∈ T1 List × (T2 List))
Lemma: map-fst-zip
∀[as,bs:Top List]. map(λp.(fst(p));zip(as;bs)) ~ as supposing ||as|| = ||bs|| ∈ ℤ
Lemma: map-snd-zip
∀[as,bs:Top List]. map(λp.(snd(p));zip(as;bs)) ~ bs supposing ||as|| = ||bs|| ∈ ℤ
Lemma: unzip-zip
∀[as,bs:Top List]. unzip(zip(as;bs)) ~ <as, bs> supposing ||as|| = ||bs|| ∈ ℤ
Lemma: unzip_zip
∀[T1,T2:Type]. ∀[as:T1 List]. ∀[bs:T2 List].
unzip(zip(as;bs)) = <as, bs> ∈ (T1 List × (T2 List)) supposing ||as|| = ||bs|| ∈ ℤ
Lemma: zip_unzip
∀[T1,T2:Type]. ∀[as:(T1 × T2) List]. (zip(fst(unzip(as));snd(unzip(as))) = as ∈ ((T1 × T2) List))
Definition: shuffle
shuffle(ps) == concat(map(λp.[fst(p); snd(p)];ps))
Lemma: shuffle_wf
∀[T:Type]. ∀[ps:(T × T) List]. (shuffle(ps) ∈ T List)
Lemma: length-shuffle
∀[T:Type]. ∀[ps:(T × T) List]. (||shuffle(ps)|| ~ 2 * ||ps||)
Lemma: select-shuffle
∀[T:Type]. ∀[ps:(T × T) List].
∀i:ℕ||shuffle(ps)||. (shuffle(ps)[i] ~ if (i rem 2 =z 0) then fst(ps[i ÷ 2]) else snd(ps[i ÷ 2]) fi )
Lemma: select-shuffle2
∀[T:Type]. ∀[ps:(T × T) List].
∀i:ℕ||ps||. ((shuffle(ps)[2 * i] ~ fst(ps[i])) ∧ (shuffle(ps)[(2 * i) + 1] ~ snd(ps[i])))
Definition: unshuffle
unshuffle(L) == fix((λunshuffle,L. if ||L|| <z 2 then [] else [<hd(L), hd(tl(L))> / (unshuffle tl(tl(L)))] fi )) L
Lemma: unshuffle_wf
∀[T:Type]. ∀[L:T List]. (unshuffle(L) ∈ (T × T) List)
Lemma: length-unshuffle
∀[T:Type]. ∀[L:T List]. (||unshuffle(L)|| ~ ||L|| ÷ 2)
Lemma: unshuffle-shuffle
∀[T:Type]. ∀[ps:(T × T) List]. (unshuffle(shuffle(ps)) ~ ps)
Lemma: unshuffle-map
∀[f:ℕ ⟶ Top]. ∀[m:ℕ]. (unshuffle(map(f;upto(2 * m))) ~ map(λi.<f (2 * i), f ((2 * i) + 1)>;upto(m)))
Lemma: unshuffle-odd-length
∀[f:ℕ ⟶ Top]. ∀[m:ℕ]. ∀[L:ℕ List]. ∀[x:ℕ].
unshuffle(map(f;L @ [x])) ~ unshuffle(map(f;L)) supposing ||L|| = (2 * m) ∈ ℤ
Lemma: unshuffle-map'
∀[f:ℕ ⟶ Top]. ∀[m:ℕ]. ∀[r:ℕ2]. (unshuffle(map(f;upto((2 * m) + r))) ~ map(λi.<f (2 * i), f ((2 * i) + 1)>;upto(m)))
Lemma: unshuffle-iseg
∀[T:Type]. ∀as,bs:T List. (as ≤ bs ⇒ unshuffle(as) ≤ unshuffle(bs))
Lemma: select-unshuffle
∀[T:Type]. ∀as:T List. ∀i:ℕ||unshuffle(as)||. (unshuffle(as)[i] = <as[2 * i], as[(2 * i) + 1]> ∈ (T × T))
Lemma: length-filter-bnot
∀[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)} ⟶ 𝔹]. (||filter(λa.(¬bP[a]);L)|| = (||L|| - ||filter(λa.P[a];L)||) ∈ ℤ)
Definition: list-partition
list-partition(f;L) ==
rec-case(L) of
[] => <[], []>
a::as =>
r.let left,right = r
in if f ||as|| then <[a / left], right> else <left, [a / right]> fi
Lemma: list-partition_wf
∀T:Type. ∀L:T List. ∀f:ℕ||L|| ⟶ 𝔹. (list-partition(f;L) ∈ T List × (T List))
Lemma: list-partition-permutation
∀T:Type. ∀L:T List. ∀f:ℕ||L|| ⟶ 𝔹. let as,bs = list-partition(f;L) in permutation(T;L;as @ bs)
Lemma: monotone-upper-bound-function
∀f:ℕ ⟶ ℤ. ∃g:ℕ ⟶ ℤ. ((∀i,j:ℕ. ((i ≤ j) ⇒ ((g i) ≤ (g j)))) ∧ (∀n:ℕ. ((f n) ≤ (g n))))
Lemma: bar-induction
∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ].
((∀s:T List. Dec(R[s]))
⇒ (∀s:T List. (R[s] ⇒ A[s]))
⇒ (∀s:T List. ((∀t:T. A[s @ [t]]) ⇒ A[s]))
⇒ (∀s:T List. ((∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[s @ map(alpha;upto(n))])) ⇒ A[s])))
Lemma: basic-bar-induction
∀[T:Type]. ∀[R,A:(T List) ⟶ ℙ].
((∀s:T List. Dec(R[s]))
⇒ (∀s:T List. (R[s] ⇒ A[s]))
⇒ (∀s:T List. ((∀t:T. A[s @ [t]]) ⇒ A[s]))
⇒ (∀alpha:ℕ ⟶ T. (↓∃n:ℕ. R[map(alpha;upto(n))]))
⇒ A[[]])
Lemma: bool_bar_induction
∀[T:Type]. ∀[A:(T List) ⟶ ℙ].
∀R:(T List) ⟶ 𝔹
((∀s:{s:T List| ↑R[s]} . A[s])
⇒ (∀s:{s:T List| ¬↑R[s]} . ((∀t:T. A[s @ [t]]) ⇒ A[s]))
⇒ (∀alpha:ℕ ⟶ T. (↓∃n:ℕ. (↑R[map(alpha;upto(n))])))
⇒ A[[]])
Lemma: iseg-subtype
∀[A,B:Type]. ∀xs,ys:A List. {xs ≤ ys ⇒ xs ≤ ys} supposing strong-subtype(A;B)
Lemma: squash-list-exists
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
∀as:A List
((∀i:ℕ||as||. (↓∃b:B. R[as[i];b])) ⇒ (↓∃bs:B List. ((||bs|| = ||as|| ∈ ℤ) ∧ (∀i:ℕ||as||. R[as[i];bs[i]]))))
Lemma: sum-partial-list-has-value
∀[T:Type]. ∀[L:T List]. ∀[f:T ⟶ partial(ℕ)]. ∀x:T. (f[x])↓ supposing (x ∈ L) supposing (Σ(f[L[i]] | i < ||L||))↓
Definition: list_accum2
list_accum2(x,a,b.f[x;
a;
b];x,a.g[x; a];x,b.h[x; b];y;as;bs)
==r if as is a pair then let a,as' = as
in if bs is a pair then let b,bs' = bs
in eval y' = f[y;
a;
b] in
list_accum2(x,a,b.f[x;
a;
b];x,a.g[x; a];x,b.h[x; b];y';as';bs')
otherwise if bs = Ax then eval y' = g[y; a] in
list_accum2(x,a,b.f[x;
a;
b];x,a.g[x; a];x,b.h[x; b];y';as';Ax) otherwis\000Ce ⊥
otherwise if as = Ax then if bs is a pair then let b,bs' = bs
in eval y' = h[y; b] in
list_accum2(x,a,b.f[x;
a;
b];x,a.g[x; a];x,b.h[x; b];y';Ax;bs')
otherwise if bs = Ax then y otherwise ⊥ otherwise ⊥
Lemma: list_accum2_wf
∀[A,B,T:Type].
∀[f:T ⟶ A ⟶ B ⟶ T]. ∀[g:T ⟶ A ⟶ T]. ∀[h:T ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List]. ∀[y:T].
(list_accum2(x,a,b.f[x;a;b];x,a.g[x;a];x,b.h[x;b];y;as;bs) ∈ T)
supposing value-type(T)
Definition: rev-map-append
rev-map-append(f;as;bs)
==r eval aa = as in
if aa is a pair then let a,more = aa
in eval b = f a in
rev-map-append(f;more;[b / bs]) otherwise bs
Lemma: rev-map-append_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. ∀[bs:B List]. (rev-map-append(f;as;bs) ∈ B List) supposing value-type(B)
Lemma: rev-map-append-sq
∀[A,B:Type].
∀[f:A ⟶ B]. ∀[as:A List]. ∀[bs:B List]. (rev-map-append(f;as;bs) ~ rev(map(f;as)) @ bs) supposing value-type(B)
Definition: map-rev
map-rev(f;L) == eval L' = rev-map-append(f;L;[]) in rev(L')
Lemma: map-rev_wf
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. map-rev(f;as) ∈ B List supposing value-type(B)
Lemma: map-rev-sq-map
∀[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. map-rev(f;as) ~ map(f;as) supposing value-type(B)
Definition: list-match
list-match(L1;L2;a,b.R[a; b]) == ∃f:ℕ||L1|| ⟶ ℕ||L2|| [(Inj(ℕ||L1||;ℕ||L2||;f) ∧ (∀i:ℕ||L1||. R[L1[i]; L2[f i]]))]
Lemma: list-match_wf
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ]. ∀[as:A List]. ∀[bs:B List]. (list-match(as;bs;a,b.R[a;b]) ∈ ℙ)
Definition: list-match-aux
list-match-aux(L1;L2;used;a,b.R[a; b]) ==
∃f:ℕ||L1|| ⟶ ℕ||L2|| [(Inj(ℕ||L1||;ℕ||L2||;f) ∧ (∀i:ℕ||L1||. ((¬(f i ∈ used)) ∧ R[L1[i]; L2[f i]])))]
Lemma: list-match-aux_wf
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ]. ∀[as:A List]. ∀[bs:B List]. ∀[used:ℤ List]. (list-match-aux(as;bs;used;a,b.R[a;b]) ∈ ℙ)
Lemma: list_match-aux-nil
∀[bs:Top List]. ∀[used,R:Top]. list-match-aux([];bs;used;a,b.R[a;b])
Lemma: list_match-aux-cons
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. SqStable(R[a;b]))
⇒ (∀bs:B List. ∀u:A. ∀v:A List. ∀used:ℤ List.
(list-match-aux([u / v];bs;used;a,b.R[a;b])
⇐⇒ ∃j:ℕ||bs||. ((¬↑j ∈b used) ∧ R[u;bs[j]] ∧ list-match-aux(v;bs;[j / used];a,b.R[a;b])))))
Lemma: decidable__list-match-aux
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀bs:B List. ∀as:A List. ∀used:ℤ List. Dec(list-match-aux(as;bs;used;a,b.R[a;b]))))
Lemma: decidable__squash-list-match-aux
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀bs:B List. ∀as:A List. ∀used:ℤ List. Dec(↓list-match-aux(as;bs;used;a,b.R[a;b]))))
Lemma: decidable__squash-list-match-aux-ext
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀bs:B List. ∀as:A List. ∀used:ℤ List. Dec(↓list-match-aux(as;bs;used;a,b.R[a;b]))))
Lemma: decidable__list-match
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀as:A List. ∀bs:B List. Dec(list-match(as;bs;a,b.R[a;b]))))
Lemma: decidable__list-match-ext
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀as:A List. ∀bs:B List. Dec(list-match(as;bs;a,b.R[a;b]))))
Lemma: decidable__squash-list-match
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀as:A List. ∀bs:B List. Dec(↓list-match(as;bs;a,b.R[a;b]))))
Lemma: decidable__squash-list-match-ext
∀[A,B:Type]. ∀[R:A ⟶ B ⟶ ℙ].
((∀a:A. ∀b:B. Dec(R[a;b])) ⇒ (∀as:A List. ∀bs:B List. Dec(↓list-match(as;bs;a,b.R[a;b]))))
Lemma: test-change-equality
∀[L1:ℕ List]. ∀[L2:ℤ List]. ((L1 = L2 ∈ (ℤ List)) ⇒ (L1 = L2 ∈ (ℕ List)))
Definition: interpolate-list
interpolate-list(x,y.f[x; y];L) ==
if L = Ax then L otherwise let a,x = L
in if x = Ax then L otherwise let b,y = x
in eval z = f[a; b] in
eval L' = interpolate-list(x,y.f[x; y];x) in
[a; [z / L']]
Lemma: interpolate-list_wf
∀[T:Type]. ∀[f:T ⟶ T ⟶ T]. ∀[L:T List]. (interpolate-list(x,y.f[x;y];L) ∈ T List) supposing value-type(T)
Lemma: length-interpolate-list
∀[T:Type]
∀[f:T ⟶ T ⟶ T]. ∀[L:T List]. (||interpolate-list(x,y.f[x;y];L)|| = if null(L) then 0 else (2 * ||L||) - 1 fi ∈ ℤ)
supposing value-type(T)
Definition: equiv-props
equiv-props(L) == ∀i,j:ℕ||L||. (L[i] ⇐⇒ L[j])
Lemma: equiv-props_wf
∀[L:ℙ List]. (equiv-props(L) ∈ ℙ)
Lemma: implies-equiv-props
∀L:ℙ List+. ((∀i:ℕ||L|| - 1. (L[i] ⇒ L[i + 1])) ⇒ (last(L) ⇒ hd(L)) ⇒ equiv-props(L))
Definition: list-closed
list-closed(T;L;f) == (∀x∈L.(∀z∈f x.(z ∈ L)))
Lemma: list-closed_wf
∀[T:Type]. ∀[L:T List]. ∀[f:T ⟶ (T List)]. (list-closed(T;L;f) ∈ ℙ)
Lemma: decidable__list-closed
∀[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ((∀x,y:T. Dec(x = y ∈ T)) ⇒ Dec(list-closed(T;L;f)))
Lemma: decidable__list-closed2
∀[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ∀d:EqDecider(T). Dec(list-closed(T;L;f))
Lemma: decidable__list-closed2-ext
∀[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ∀d:EqDecider(T). Dec(list-closed(T;L;f))
Definition: list-closed-test
list-closed-test(f;d;L) ==
isl(l-all-decider() L
(λx.(l-all-decider() (f x)
(λz.letrec list_ind(L)=eval v = L in
if v is a pair then let a,L = v
in case list_ind L
of inl(%2) =>
if d z a
then inl <0, Ax, Ax>
else inl let i,%4,%5 = %2 in
<i + 1, Ax, Ax>
fi
| inr(%2) =>
if d z a then inl <0, Ax, Ax> else inr (λ%.Ax) fi
otherwise if v = Ax then inr (λ%.Ax) otherwise fix((λx.x)) in
list_ind(L)))))
Lemma: list-closed-test_wf
∀[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ∀d:EqDecider(T). (list-closed-test(f;d;L) ∈ {b:𝔹| ↑b ⇐⇒ list-closed(T;L;f)} )
Lemma: member-union
∀[T:Type]. ∀eq:EqDecider(T). ∀as,bs:T List. ∀x:T. ((x ∈ as ⋃ bs) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))
Definition: alist-map
alist-map(eq;L) == λx.case apply-alist(eq;L;x) of inl(x') => x' | inr(_) => x
Lemma: alist-map_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:(T × T) List]. (alist-map(eq;L) ∈ T ⟶ T)
Definition: l-union-list
l-union-list(eq;ll) == rec-case(ll) of [] => [] | l1::l2 => r.r ⋃ l1
Lemma: l-union-list_wf
∀[T:Type]. ∀[eq:EqDecider(T)]. ∀[ll:T List List]. (l-union-list(eq;ll) ∈ T List)
Lemma: member-l-union-list
∀[T:Type]. ∀eq:EqDecider(T). ∀ll:T List List. ∀x:T. ((x ∈ l-union-list(eq;ll)) ⇐⇒ ∃l:T List. ((l ∈ ll) ∧ (x ∈ l)))
Definition: dep-accum
dep-accum(L,b.f[L; b];a,bb.g[a; bb];bs) ==
accumulate (with value L and list item b):
L @ let a = f[L; b] in [<a, b, g[a; b]>]
over list:
bs
with starting value:
[])
Lemma: dep-accum_wf
∀[A,B:Type]. ∀[C:A ⟶ B ⟶ Type]. ∀[f:very-dep-fun(A;B;a,b.C[a;b])]. ∀[g:a:A ⟶ b:B ⟶ C[a;b]]. ∀[bs:B List].
(dep-accum(L,b.f[L;b];a,b.g[a;b];bs) ∈ {L:(a:A × b:B × C[a;b]) List|
vdf-eq(A;f;L) ∧ (map(λx.(fst(snd(x)));L) = bs ∈ (B List))} )
Comment: list_1_end
********************************⋅
Home
Index