Lemma: sqequal-nil
[T:Type]. ∀[l:T List].  [] supposing [] ∈ (T List)

Lemma: sqequal-null
[T:Type]. ∀[l:T List].  [] 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.
     (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
  ∀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
  ∀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
  ∀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
  ∀eq:EqDecider(T). ∀x:T. ∀u:Unit. ∀L:(T × A) List.
    ((apply-alist(eq;L;x) (inr ) ∈ (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
  ∀ll:T List List. ∀n:ℕ||concat(ll)||.
     ((||concat(firstn(m;ll))|| ≤ n)
     c∧ ||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 and list item b):
   over list:
   with starting value:
    y) accumulate (with value and list item b):
          if P[b] then f[a;b] else fi 
         over list:
         with starting value:

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 <||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 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) ∈ 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
  ∀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 <||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
  ∀L:T List
    ∀[P:ℕ||L|| ⟶ ℙ]
      ((∀x:ℕ||L||. Dec(P x))
       (∀i,j:ℕ||L||.  ((P i)  supposing i < j))
       (∃L_1,L_2:T List. ((L (L_1 L_2) ∈ (T List)) ∧ (∀i:ℕ||L||. (P ⇐⇒ ||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] g[a] (For{T,f,k} x ∈ as. g[x]))

Definition: mapcons
mapcons(f;as) ==  fix((λmapcons,as. case as of [] => [] a::as' => [f 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 mapcons(f;t)])

Lemma: mapcons_wf
[A,B:Type]. ∀[f:A ⟶ (A List) ⟶ B]. ∀[l:A List].  (mapcons(f;l) ∈ 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] 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]) 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 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) ∈ List)

Lemma: list_accum-triangle-inequality
[T:Type]. ∀[L:T List]. ∀[x,y:ℤ]. ∀[f,g:T ⟶ ℤ].
  (|accumulate (with value and list item a):
    over list:
    with starting value:
     x) accumulate (with value and list item a):
          over list:
          with starting value:
           y)| ≤ accumulate (with value and list item a):
                  |f[a] g[a]|
                 over list:
                 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|| ≥ )

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) ∈ 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 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 and list item x):
   f[a; x]
  over list:
  with starting value:

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) ∈ supposing 0 < ||L||

Lemma: accum_list_cons_lemma
  (accum_list(a,x.f[a;x]; y.base[y]; [u L]) accumulate (with value and list item y):
                                                over list:
                                                with starting value:

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].  b ∈ 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 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
  ∀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 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 ∈ 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 y ∈ (A List)} supposing {a:A| (a ∈ x)}  ⊆B

Lemma: test_sqtype1
[X,Y:Type].  (SQType((n:ℕ × {L:𝔹 List| True} ? × (X Y)) List)) supposing ((Y ⊆Base) and (X ⊆Base))

Definition: len
len(as) ==  rec-case(as) of [] => 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' in eval 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 ⊆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 then else 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 then else 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) ∈ 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 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. [] 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) tl(L2)]

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) tl(bs)];(n 1) hd(as))

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
  ∀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. ([] ⊆ ⇐⇒ 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 ⊆ [] ⇐⇒ [] ∈ (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 ⊆  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]] ⊆ 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
==r if null(L) then [] else let a,as 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
before y ∈ ==  [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)  before y ∈ L1 L2  before y ∈ L1 supposing ¬(y ∈ L2))

Lemma: l_before_append_front
[T:Type]. ∀L1,L2:T List. ∀x,y:T.  before y ∈ L1 L2  before y ∈ L1 supposing ¬(y ∈ L2)

Lemma: l_tricotomy
[T:Type]. ∀x,y:T. ∀L:T List.  ((x ∈ L)  (y ∈ L)  (((x y ∈ T) ∨ before y ∈ L) ∨ before x ∈ L))

Lemma: l_before_member
[T:Type]. ∀L:T List. ∀a,b:T.  (a before b ∈  (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)  before y ∈ L1 L2)

Lemma: l_before_member2
[T:Type]. ∀L:T List. ∀a,b:T.  (a before b ∈  (a ∈ L))

Lemma: l_before_sublist
[T:Type]. ∀L1,L2:T List.  (L1 ⊆ L2  {∀x,y:T.  (x before y ∈ L1  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)) ∨ before y ∈ l)

Lemma: before_last
[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ L)  before last(L) ∈ supposing ¬(x last(L) ∈ T))

Lemma: l_before_select
[T:Type]. ∀L:T List. ∀i,j:ℕ||L||.  L[j] before L[i] ∈ supposing j < i

Lemma: before-map
  ∀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 ∈ ⇐⇒ before y ∈ A ∨ before y ∈ B ∨ ((x ∈ A) ∧ (y ∈ B)))

Lemma: append_overlapping_sublists
[T:Type]. ∀L1,L2,L:T List. ∀x:T.  L1 [x] ⊆  [x L2] ⊆  L1 [x L2] ⊆ supposing no_repeats(T;L)

Lemma: l_before_transitivity
[T:Type]. ∀l:T List. ∀x,y,z:T.  before y ∈  before z ∈  before z ∈ 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 before y ∈ l)

Lemma: l_before_antisymmetry
[T:Type]. ∀[l:T List]. ∀[x,y:T].  before x ∈ l) supposing (x before y ∈ 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)) ∧ 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 f;L)))

Lemma: subtype-l_all
[T:Type]. ∀[L:T List]. ∀[P,Q:{x:T| (x ∈ L)}  ⟶ ℙ].
  (∀x∈L.P[x]) ⊆(∀x∈L.Q[x]) supposing ∀x:T. ((x ∈ L)  (P[x] ⊆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 (x 1) else inl <x, λ%.Ax> fi   else (inr x.Ax) i\000Cn
           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
  ∀L:A List. ∀[F:{a:A| (a ∈ L)}  ⟶ ℙ]. ∀dcd:∀k:{a:A| (a ∈ L)} Dec(F[k]). (l-all-decider() 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) => (x 1)
                         else (inr x.Ax) in

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() 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 else 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| 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| 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' ∈ ({x:T| P[x]}  List) supposing 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 ⊆B

Lemma: l_member_subtype2
[A,B:Type].  ∀L:A List. ∀x:A.  {(x ∈ L)  (x ∈ L)} supposing A ⊆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 ⊆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) ∈ 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 then [f y] else fi ;[];L))

Lemma: member_map_filter
  ∀P:T ⟶ 𝔹
      ∀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
  ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹.
      ∀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)}  ⟶ 𝔹.
                                   ∀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
  ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹.
      ∀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 else (r (i 1)) if then else 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,_ 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 ∈  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)) ∧ before y ∈ l)

Lemma: l_before_filter_subtype
  ∀l:T List. ∀P:T ⟶ 𝔹. ∀x,y:T.  ((↑(P x))  (↑(P y))  (x before y ∈ filter(P;l) ⇐⇒ before y ∈ filter(P;l)))

Lemma: l_before_map
  ∀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) ∧ before v ∈ l))

Lemma: l_before_mapfilter
  ∀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) ∧ 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
  ∀P:T ⟶ 𝔹. ∀L:T List.
    (||filter(P;L)|| 1 ∈ ℤ ⇐⇒ ∃i:ℕ||L||. ((↑(P L[i])) ∧ (∀j:ℕ||L||. 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
  ∀l:T List. ∀P:{x:T| (x ∈ l)}  ⟶ 𝔹. ∀x,y:T.  (x before y ∈ filter(P;l) ⇐⇒ 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 ⊆ ==  (∀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 ⊆  {∀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;[]) ⇐⇒ [] ∈ (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 ⊆ supposing B ∈ (T List)

Lemma: l_contains_transitivity
[T:Type]. ∀A,B,C:T List.  (A ⊆  B ⊆  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] ⊆ ⇐⇒ (a ∈ L) ∧ as ⊆ L)

Lemma: l_contains_singleton
[T:Type]. ∀L:T List. ∀a:T.  ([a] ⊆ ⇐⇒ (a ∈ L))

Lemma: l_contains_append
[T:Type]. ∀A,B:T List.  A ⊆ B

Lemma: l_contains-append
[T:Type]. ∀A,B,C:T List.  (A B ⊆ ⇐⇒ A ⊆ C ∧ B ⊆ C)

Lemma: l_contains_append2
[T:Type]. ∀A,B:T List.  A ⊆ A

Lemma: l_contains_append3
[T:Type]. ∀A,B,C:T List.  (A ⊆  A ⊆ C)

Lemma: l_contains-append4
[T:Type]. ∀A,B,C:T List.  (A ⊆  A ⊆ 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 ⊆  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' ⊆ 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 ⊆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) ⇐⇒ x ∈ T)))

Lemma: l_contains-cons
  ∀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 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 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 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) ∈ 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 then f1 (f2 u) else 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
  ∀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|| ≥ )

Definition: tlp
tlp(L) ==  tl(L)

Lemma: tlp_wf
[A:Type]. ∀[L:A List+].  (tlp(L) ∈ 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] ∈ 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
  ∀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
  ∀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
  ∀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 ≤  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  before y ∈ L1  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 ≤  l2 ≤  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].  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) ∨ before last(L) ∈ L))

Lemma: last-cons
[x:Top]. ∀[as:Top List].  (last([x as]) if null(as) then 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
  ∀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
  ∀eq:EqDecider(T). ∀u:T. ∀v,bs:T List.
    (set-equal(T;[u v];bs) ⇐⇒ (u ∈ bs) ∧ set-equal(T;filter(λx.(¬b(eq u));v);filter(λx.(¬b(eq 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. 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 b1)  (R b2)  (b1 b2 ∈ B)))
        ∧ (∀a∈as.(∃b∈bs. b))
        ∧ (∀b∈bs.(∃a∈as. b)))) and 
     no_repeats(A;as) and 

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 and list item x):
   over list:
   with starting value:
    x) accumulate (with value and list item x):
          if then f[a;g x] else fi 
         over list:
         with starting value:

Lemma: list_accum_functionality
[T,A:Type]. ∀[f,g:T ⟶ A ⟶ T]. ∀[L:A List]. ∀[y,z:T].
  (accumulate (with value and list item a):
   over list:
   with starting value:
     accumulate (with value and list item a):
       over list:
       with starting value:
     ∈ T) supposing 
     ((y z ∈ T) and 
     (∀L':A List. ∀a:A.
        (L' [a] ≤ L
         (f[accumulate (with value and list item a):
              over list:
              with starting value:
           g[accumulate (with value and list item a):
               over list:
               with starting value:
           ∈ T))))

Lemma: list_accum_as_reduce
[T,A:Type]. ∀[f:A ⟶ T ⟶ A].
  ∀[L:T List]. ∀[a0:A].
    (accumulate (with value and list item x):
     over list:
     with starting value:
    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 and list item z):
      over list:
        [x L]
      with starting value:
     accumulate (with value and list item z):
       over list:
       with starting value:
     ∈ 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 and list item z):
      over list:
        as bs
      with starting value:
     accumulate (with value and list item z):
       over list:
         bs as
       with starting value:
     ∈ 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].
        (accumulate (with value and list item z):
         over list:
         with starting value:
        accumulate (with value and list item z):
          over list:
          with starting value:
        ∈ 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 and list item b):
      over list:
      with starting value:
     ∈ 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 and list item x):
      over list:
      with starting value:
    G[accumulate (with value and list item x):
        over list:
        with starting value:
    supposing F[a0] G[b0] ∈ 
  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
  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ ℙ]
      ∀L:T List. ∀a:A.
         (∀a:A. ∀x:T.  (P[a]  P[f[a;x]]))
         P[accumulate (with value and list item x):
             over list:
             with starting value:

Lemma: list_accum_invariant2
  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ ℙ]
      ∀L:T List. ∀a:A.
         (∀a:A. ∀x:T.  ((x ∈ L)  P[a]  P[f[a;x]]))
         P[accumulate (with value and list item x):
             over list:
             with starting value:

Lemma: list_accum_invariant3
  ∀f:A ⟶ T ⟶ A
    ∀[P:A ⟶ (T List) ⟶ ℙ]
      ∀L:T List. ∀a:A.
         (∀a:A. ∀x:T. ∀L':T List.  (L' [x] ≤  P[a;L']  P[f[a;x];L' [x]]))
         P[accumulate (with value and list item x):
             over list:
             with starting value:

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) ∈ 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 of inl(z) => inl f[x;z] inr(z) => inl x;inr ⋅ ;L)) ∈ 
     supposing 0 < ||L||) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))

Lemma: combine-combine-list-left
  ∀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 ∈ ⇐⇒ (f[x;y] x ∈ T) ∧ (f[x;z] x ∈ T))))

Lemma: combine-combine-list-right
  ∀f:T ⟶ T ⟶ T. ∀L:T List.
    ((∀x,y,z:T.  (f[x;f[y;z]] f[y;z] ∈ ⇐⇒ (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) ∈ ⇐⇒ (∃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 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 and list item x):
   eval f[x] in
   case of inl(p) => if fst(p) <then inl <n, x> else fi  inr(q) => inl <n, x>
  over list:
  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
  ∀f:T ⟶ ℤ. ∀L:T List.
    ∧ 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
  ∀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
  ∀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), (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) ∈ List)

Definition: eval-mklist
eval-mklist(n;f;offset) ==
  if n=0
  then []
  else eval offset in
       eval offset' offset in
       eval n' in
       eval eval-mklist(n';f;offset') in
         [v L]

Lemma: eval-mklist-sq
  ∀[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) ∈ 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] i)

Lemma: mklist-add
[T:Type]. ∀[n,m:ℕ]. ∀[f:ℕ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 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 ≤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] 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)

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:ℕ1].  (l_interval(l;j;i) ∈ List)

Lemma: length_l_interval
[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕ1].  (||l_interval(l;j;i)|| (i j) ∈ ℤ)

Lemma: select_l_interval
[T:Type]. ∀[l:T List]. ∀[i:ℕ||l||]. ∀[j:ℕ1]. ∀[x:ℕ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
  ∀L:T List. ∀[R:{x:T| (x ∈ L)}  ⟶ {x:T| (x ∈ L)}  ⟶ ℙ]. (sorted-by(R;L)  (∀x,y:T.  (x before y ∈  (R 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 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 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 b) and 
     Trans(T;a,b.R 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))))

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))) and 
     AntiSym(T;a,b.R b) and 
     Trans(T;a,b.R 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
        (∀x:T. ((x ∈ sa) ⇐⇒ (¬↑null(sa)) ∧ (x ∈ sb) ∧ ((x last(sa) ∈ T) ∨ (R last(sa)))))) supposing 
       (AntiSym(T;x,y.R y) and 
       Irrefl(T;x,y.R y))

Lemma: sorted-by-reverse
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].  ∀L:T List. (sorted-by(R;L) ⇐⇒ sorted-by(λx,y. (R 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
  ∀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
  ∀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
  ∀L:T List
    ∀[P:T ⟶ T ⟶ ℙ']
      ((∀x,y:T.  (P[x;y]  P[y;x]))
       ((∀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
  ∀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
  ∀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||.  j[x] > j[y] supposing x < y)
   ∧ (∀j:ℕk. ∀x:ℕ||p j||.  (p j[x] < c∧ ((c j[x]) j ∈ ℤ))))

Lemma: pigeon-hole
[n,m:ℕ]. ∀[f:ℕn ⟶ ℕm].  n ≤ supposing Inj(ℕn;ℕm;f)

Lemma: pigeon-hole-implies
n:ℕ. ∀[m:ℕ]. ∀f:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕ[((f i) (f j) ∈ ℤ)]) supposing m < n

Lemma: pigeon-hole-implies-ext
n:ℕ. ∀[m:ℕ]. ∀f:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕ[((f i) (f j) ∈ ℤ)]) supposing m < n

Lemma: pigeon-hole-implies2
    ∀f:ℕn ⟶ ℕm. ∀g:ℕn ⟶ ℕm. ∃i:ℕn. (∃j:ℕ[((f i) (g j) ∈ ℤ)]) supposing Inj(ℕn;ℕm;g) supposing Inj(ℕn;ℕm;f) 
    supposing m < 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| ≤ ==  ∃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| ≤  |T| ≤ m} supposing n ≤ m

Lemma: cardinality-le-finite
[T:Type]. ∀n:ℕ(|T| ≤  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| ≤  (∃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

Lemma: int_seg-cardinality-le
i,j:ℤ.  |{i..j-}| ≤ if i ≤then else 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)   (∀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) ≤ supposing |{x..y-}| ≤ n

Lemma: int-seg-cardinality-le
x,y:ℤ. ∀n:ℕ.  |{x..y-}| ≤ 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
  ((∀x,y:T.  Dec(x y ∈ T))
   (∀n:ℕ. ∀s:ℕn ⟶ T.  (Surj(ℕn;T;s)  (∀f:T ⟶ T. ∀x:T. ∃m:ℕ+1. ((f^m x) x ∈ T) supposing Inj(T;T;f)))))

Lemma: list-injection
  ((∀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
   (∀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) ∈ 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 and list item y):
   eval in
   eval in
     if x ≤then else fi 
  over list:
  with starting value:

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| 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)|| ≥ 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)) supposing T ⊆Base

Lemma: map-conversion-test
[T:Type]. ∀[L:T List List]. (map(λX.(X []);L) map(λX.X;L)) supposing T ⊆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]. 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|| ≥ 

Lemma: last-map
[as:Top List]. ∀[f:Top].  last(map(f;as)) 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 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 <then [n eval n' 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 <then else 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, k))

Lemma: select-from-upto
[n,m:ℤ]. ∀[k:ℕn].  ([n, m)[k] 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)) 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 (n 1) ∈ ℤ

Lemma: from-upto-single
[n:ℤ]. ([n, 1) [n])

Lemma: from-upto-decomp-last
[n,m:ℤ].  [n, m) ([n, 1) [m 1]) ∈ (ℤ List) supposing n < m

Lemma: l_all_from-upto
n,m:ℤ. ∀P:ℤ ⟶ ℙ.  ((∀x∈[n, m).P[x]) ⇐⇒ ∀x:ℤ((n ≤ x)  x <  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) ∈ ℕ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:ℕ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
    ∀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:ℕ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 ⊆Base

Lemma: firstn_last
[T:Type]. ∀[L:T List].  (firstn(||L|| 1;L) [last(L)]) ∈ (T List) supposing ¬↑null(L)

Lemma: firstn_last_sq
[T:Type]. ∀[L:T List].  firstn(||L|| 1;L) [last(L)] supposing (¬↑null(L)) ∧ (T ⊆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 ⊆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 ≤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 and list item x): pover list:  Lwith starting value: a) ∈ A) 
  supposing ∀x,y:T. ∀a:A.  ((f (f a)) (f (f 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 and list item x):
                    p ∧b P[x]
                   over list:
                   with starting value:

Lemma: bl-exists-as-accum
[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].
  ((∃x∈L.P[x])_b accumulate (with value and list item x):
                    p ∨bP[x]
                   over list:
                   with starting value:

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 1) then else fi 

Lemma: rotate_wf
[k:ℕ]. (rot(k) ∈ ℕk ⟶ ℕk)

Lemma: iterated-rotate
[n,i:ℕ].  rot(n)^i x.if i <then else (x i) fi ) ∈ (ℕn ⟶ ℕn) supposing i ≤ n

Definition: flip
(i, j) ==  λx.if (x =z i) then if (x =z j) then else fi 

Lemma: flip_wf
[k:ℕ]. ∀[i,j:ℕk].  ((i, j) ∈ ℕk ⟶ ℕk)

Lemma: flip-conjugation
[n:ℕ]. ∀[k:ℕn]. ∀[j:ℕk]. ∀[l:ℕk].  ((j, l) ((k, l) ((j, k) (k, l))) ∈ (ℕn ⟶ ℕn))

Lemma: flip-conjugation1
[n:ℕ]. ∀[k:ℕ1]. ∀[j:ℕk].  ((j, 1) ((k, 1) ((j, k) (k, 1))) ∈ (ℕn ⟶ ℕn))

Lemma: flip-conjugate-rotate
[n:ℕ]. ∀[i:ℕ1].  ((i, 1) (rot(n)^i ((0, 1) 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 j ∈ ℤ

Lemma: flip_bijection
k:ℕ. ∀i,j:ℕk.  Bij(ℕk;ℕk;(i, j))

Lemma: flip_inverse
[k:ℤ]. ∀[x,y:ℕk].  (((y, x) (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:ℕList. ((i, j) reduce(λi,g. ((i, 1) g);λx.x;L) ∈ (ℕn ⟶ ℕn))

Lemma: flip-generators
  ∀i,j:ℕn.  ∃L:𝔹 List. ((i, j) reduce(λi,g. (if then rot(n) else (0, 1) fi  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 rem n)) ∈ (ℕn ⟶ ℕn))

Lemma: rotate-order
[n:ℕ]. (rot(n)^n x.x) ∈ (ℕn ⟶ ℕn))

Lemma: rotate-inverse1
[n:ℕ+]. ((rot(n) rot(n)^n 1) x.x) ∈ (ℕn ⟶ ℕn))

Lemma: rotate-surjection

Lemma: rotate-bijection

Lemma: rotate-inverse
[n:ℕ+]. (inv(rot(n)) rot(n)^n 1 ∈ {f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} )

Definition: permute_list
(L f) ==  mklist(||L||;λi.L[f i])

Lemma: permute_list_wf
[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ ℕ||L||].  ((L f) ∈ List)

Lemma: permute_list_select
[T:Type]. ∀[L:T List]. ∀[f:ℕ||L|| ⟶ ℕ||L||]. ∀[i:ℕ||L||].  ((L f)[i] L[f i] ∈ T)

Lemma: permute_list_length
[T:Type]. ∀[L:T List]. ∀[f:Top].  (||(L 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 g) ((L f) g) ∈ (T List))

Lemma: permute_permute_list
[T:Type]. ∀[L:T List]. ∀[f,g:ℕ||L|| ⟶ ℕ||L||].  (((L f) g) (L g) ∈ (T List))

Definition: permutation
permutation(T;L1;L2) ==  ∃f:ℕ||L1|| ⟶ ℕ||L1||. (Inj(ℕ||L1||;ℕ||L1||;f) ∧ (L2 (L1 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 ⊆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) ⇐⇒ [] ∈ (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
  ∀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
  ∀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
  ∀L1:B List. ∀L2:A List.  (permutation(A;L1;L2)  {(L2 ∈ 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
  ((∀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 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
  ((∀x,y:T.  Dec(x y ∈ 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
  ((∀x,y:T.  Dec(x y ∈ 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
  ((∀x,y:T.  Dec(x y ∈ 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
  ((∀x,y:T.  Dec(x y ∈ T))
   (∀f:T ⟶ T
        ∃orbits:T List List
         ∧ (∀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 hd(L) in
              rec-case(L) of
              [] => x
              a::as =>
               r.if (x =z a) then if null(as) then else hd(as) fi  else fi 

Lemma: cycle_wf
[n:ℕ]. ∀[L:ℕList].  (cycle(L) ∈ ℕn ⟶ ℕn)

Lemma: apply-cycle-member
[n:ℕ]. ∀[L:ℕ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:ℕList.  (x ∈ L)  (cycle(L) x ∈ L) supposing no_repeats(ℕn;L)

Lemma: apply-cycle-non-member
[n:ℕ]. ∀[L:ℕList]. ∀[x:ℕn].  (cycle(L) x) x ∈ ℕsupposing ¬(x ∈ L)

Lemma: cycle-conjugate
[n:ℕ]. ∀[L:ℕList].
  ∀[f,g:ℕn ⟶ ℕn].
    ((g (cycle(L) 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:ℕList].  Inj(ℕn;ℕn;cycle(L)) supposing no_repeats(ℕn;L)

Lemma: cycle-transitive1
[n:ℕ]. ∀[L:ℕList].
  ∀[a,b:ℕ].  ((cycle(L)^b L[a]) L[b] ∈ ℕn) supposing ((a ≤ b) and b < ||L||) supposing no_repeats(ℕn;L)

Lemma: cycle-transitive
n:ℕ. ∀L:ℕList.  ∀a,b:ℕ||L||.  ∃m:ℕ||L||. ((cycle(L)^m L[a]) L[b] ∈ ℕn) supposing no_repeats(ℕn;L)

Lemma: cycle-transitive2
n:ℕ. ∀L:ℕ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:ℕList List
   ∧ (∀c1∈cycles.(∀c2∈cycles.(c1 c2 ∈ (ℕList)) ∨ l_disjoint(ℕn;c1;c2)))
   ∧ (∀c∈cycles.0 < ||c|| ∧ no_repeats(ℕn;c))
   ∧ (f reduce(λc,g. (cycle(c) g);λx.x;cycles) ∈ (ℕn ⟶ ℕn)))

Lemma: cycle-flip-lemma
[n:ℕ]. ∀[L:ℕList].
  (cycle(L) ((hd(L), hd(tl(L))) cycle(tl(L))) ∈ (ℕn ⟶ ℕn)) supposing (1 < ||L|| and no_repeats(ℕn;L))

Definition: compose-flips
compose-flips(flips) ==  reduce(λf,g. (f g);λx.x;map(λp.let i,j 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:ℕ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:ℕList].  cycle(as bs) cycle(bs as) ∈ (ℕn ⟶ ℕn) supposing no_repeats(ℕn;as bs)

Lemma: permutation-generators
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
     ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[(0, 1) f]) supposing 1 < n
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[rot(n) f]))
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f]))

Lemma: permutation-generators2
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
     ∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[f (0, 1)]) supposing 1 < n
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} (P[f]  P[f rot(n)]))
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f]))

Lemma: permutation-generators3
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i,j:ℕn.  P[f]  P[f (i, j)] supposing i < j)
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f]))

Lemma: permutation-generators4
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀j:ℕ+n.  (P[f]  P[f (0, j)]))
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} P[f]))

Lemma: permutation-generators5
  ∀[P:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)}  ⟶ ℙ]
     (∀f:{f:ℕn ⟶ ℕn| Inj(ℕn;ℕn;f)} . ∀i:ℕ1.  (P[f]  P[f (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) ∈ supposing permutation(A;as;bs)) supposing 
     (Comm(A;λx,y. f[x;y]) and 
     Assoc(A;λx,y. f[x;y]))

Lemma: permutation-cons
  ∀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
  ∀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
  ∀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 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
  ∀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
  ∀L1,L2:A List.
     (∀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 and list item y):
                     over list:
                     with starting value:

Lemma: sum-as-accum2
[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
  (f[x] x < n) accumulate (with value and list item y):
                     over list:
                     with starting value:

Lemma: sum-as-accum-filter
[n:ℕ]. ∀[f:ℕn ⟶ ℤ].
  (f[x] x < n) accumulate (with value and list item y):
                     over list:
                       filter(λx.(¬b(x =z 0));map(λx.f[x];upto(n)))
                     with starting value:

Definition: insert-by
insert-by(eq;r;x;l) ==
  rec-case(l) of
  [] => [x]
  a::as =>
   v.if eq then [a as]
  if then [x; [a as]]
  else [a v]

Lemma: insert-by_wf
[T:Type]. ∀[eq,r:T ⟶ T ⟶ 𝔹]. ∀[x:T]. ∀[L:T List].  (insert-by(eq;r;x;L) ∈ List)

Lemma: member-insert-by
  ∀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 b) ⇐⇒ b ∈ T)

Definition: comparison
comparison(T) ==
  {cmp:T ⟶ T ⟶ ℤ
   (∀x,y:T.  ((cmp y) (-(cmp x)) ∈ ℤ))
   ∧ (∀x,y:T.  (((cmp y) 0 ∈ ℤ (∀z:T. ((cmp z) (cmp z) ∈ ℤ))))
   ∧ (∀x,y,z:T.  ((0 ≤ (cmp y))  (0 ≤ (cmp z))  (0 ≤ (cmp z))))} 

Lemma: comparison_wf
T:Type. (comparison(T) ∈ Type)

Lemma: subtype_rel_comparison
[A,B:Type].  comparison(B) ⊆comparison(A) supposing A ⊆B

Lemma: comparison-equiv
[T:Type]. ∀cmp:comparison(T). EquivRel(T;x,y.(cmp y) 0 ∈ ℤ)

Lemma: comparison-reflexive
[T:Type]. ∀cmp:comparison(T). ∀x:T.  ((cmp x) 0 ∈ ℤ)

Lemma: comparison-anti
[T:Type]. ∀[cmp:comparison(T)]. ∀[x,y:T].  ((cmp y) (-(cmp x)) ∈ ℤ)

Definition: int-minus-comparison
int-minus-comparison(f) ==  λx,y. ((f x) 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) 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 then if then else fi  if then -1 else fi 

Lemma: bool-cmp_wf
bool-cmp() ∈ comparison(𝔹)

Lemma: bool-cmp-zero
[x,y:𝔹].  uiff((bool-cmp() 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 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 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 y))

Lemma: strict-comparison-trans
[T:Type]. ∀cmp:comparison(T). Trans(T;x,y.0 < cmp y)

Lemma: comparison-connex
[T:Type]. ∀cmp:comparison(T). Connex(T;x,y.0 ≤ (cmp y))

Lemma: comparison-antisym
[T:Type]. ∀cmp:comparison(T). AntiSym(T;x,y.0 ≤ (cmp y)) supposing ∀x,y:T.  (((cmp y) 0 ∈ ℤ (x y ∈ T))

Lemma: comparison-refl
[T:Type]. ∀cmp:comparison(T). Refl(T;x,y.0 ≤ (cmp 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 in if answer1=0 then c2 else answer1

Lemma: comparison-seq_wf
[T:Type]. ∀[c1:comparison(T)]. ∀[c2:⋂a:T. comparison({b:T| (c1 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 b) 0 ∈ ℤ)]. ∀[x,y:T].
  uiff((comparison-seq(c1; c2) y) 0 ∈ ℤ;((c1 y) 0 ∈ ℤ) ∧ ((c2 y) 0 ∈ ℤ))

Lemma: comparison-seq-zero-simple
[T:Type]. ∀[c1,c2:comparison(T)]. ∀[x,y:T].
  uiff((comparison-seq(c1; c2) y) 0 ∈ ℤ;((c1 y) 0 ∈ ℤ) ∧ ((c2 y) 0 ∈ ℤ))

Definition: find-combine
find-combine(cmp;l) ==
  rec-case(l) of
  [] => inr ⋅ 
  a::as =>
   v.eval tst cmp in
     if (tst =z 0) then inl a
     if 0 <tst then inr ⋅ 
     else v

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
  (find-combine(cmp;[x l]) eval tst cmp in
                               if (tst =z 0) then inl x
                               if 0 <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 in
     if (tst =z 0) then [f as]
     if 0 <tst then [x; [a as]]
     else [a v]

Lemma: insert-combine_wf
T:Type. ∀cmp:comparison(T). ∀f:T ⟶ T ⟶ T. ∀x:T. ∀L:T List.  (insert-combine(cmp;f;x;L) ∈ List)

Lemma: insert-combine-cons
  (insert-combine(cmp;f;x;[a as]) eval tst cmp in
                                      if (tst =z 0) then [f as]
                                      if 0 <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 y) 0 ∈ ℤ) ∧ (z (f 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 y < 0) ∧ cmp z < 0))
      ∨ (∃l,l':T List
           (((l [a l']) v ∈ (T List))
           ∧ (∀y∈l.cmp y < 0)
           ∧ ((0 < cmp a ∧ (z ∈ [x; [a l']])) ∨ (((cmp a) 0 ∈ ℤ) ∧ (z ∈ [f l'])))))
      ∨ ((z x ∈ T) ∧ (∀y∈v.cmp y < 0)))

Lemma: insert-combine-sorted-by
T:Type. ∀cmp:comparison(T).
  ((∀u,x,z:T.  (0 < cmp  0 < cmp  0 < cmp z))
   (∀f:T ⟶ T ⟶ T
        ((∀u,x:T.  (((cmp u) 0 ∈ ℤ ((cmp (f u)) 0 ∈ ℤ)))
         (∀L:T List. ∀x:T.  (sorted-by(λx,y. 0 < cmp y;L)  sorted-by(λx,y. 0 < cmp 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 in
     if (tst =z 0) then as
     if 0 <tst then [a as]
     else [a v]

Lemma: remove-combine_wf
T:Type. ∀cmp:T ⟶ ℤ. ∀l:T List.  (remove-combine(cmp;l) ∈ 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 =z 0) then l
  if 0 <cmp 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 ≤cmp 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) ∈ 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
    ((∀u,x,z:T.  ((0 ≤ (cmp u))  (0 ≤ (cmp z))  (0 ≤ (cmp z))))
     (∀L:T List. ∀x:T.  (sorted-by(λx,y. (0 ≤ (cmp y));L)  sorted-by(λx,y. (0 ≤ (cmp 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 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 ≤cmp mx then mx else 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 mx))} suppos\000Cing valueall-type(T)

Lemma: insert-by-sorted-by
  ∀eq,r:T ⟶ T ⟶ 𝔹.
    Linorder(T;a,b.↑(r b))
     (∀x:T. ∀L:T List.  (sorted-by(λx,y. (↑(r y));L)  sorted-by(λx,y. (↑(r y));insert-by(eq;r;x;L)))) 
    supposing ∀a,b:T.  (↑(eq b) ⇐⇒ 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 ⊆\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 y));L))) supposing 
     (Linorder(T;a,b.↑(r b)) and 
     (∀a,b:T.  (↑(eq b) ⇐⇒ b ∈ T)))

Lemma: sorted-by-exists
  ∀eq,r:T ⟶ T ⟶ 𝔹.
    Linorder(T;a,b.↑(r b))
     (∀L:T List. ∃L':T List. (sorted-by(λx,y. (↑(r y));L') ∧ no_repeats(T;L') ∧ L ⊆ L' ∧ L' ⊆ L)) 
    supposing ∀a,b:T.  (↑(eq b) ⇐⇒ b ∈ T)

Lemma: sorted-by-exists2
[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀a,b:T.  Dec(a b ∈ T))
   (∀a,b:T.  Dec(R b))
   Linorder(T;a,b.R 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 then as else [a r] fi 

Lemma: remove-first_wf
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  (remove-first(P;L) ∈ List)

Lemma: length-remove-first
  ∀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:ℕ1. (¬↑(P L[j]))
  ∧ remove-first(P;L)[i] L[i 1] supposing ∃j:ℕ1. (↑(P L[j])))

Lemma: remove-first-cons
[L,x,P:Top].  (remove-first(P;[x L]) if then 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
  ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹. ∀x:T.
     (∀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
  ∀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  before y ∈ L1))) supposing 
       (no_repeats(T;L2) and 

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  before y ∈ L1))) and 

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. (f x) 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. (f x) x

Lemma: no-member-sq-nil
[T:Type]. ∀[L:T List].  [] supposing ∀x:T. (x ∈ L))

Lemma: equal-nil-sq-nil
[T:Type]. ∀[L:T List].  [] supposing [] ∈ (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 L[i] then L[i] else fi  i < ||L||) ∈ ℤ)

Lemma: l_sum-mapfilter-upto
[n:ℕ]. ∀[P:ℕn ⟶ 𝔹]. ∀[f:{x:ℕn| ↑(P x)}  ⟶ ℤ].
  (l_sum(mapfilter(f;P;upto(n))) = Σ(if then else fi  i < n) ∈ ℤ)

Lemma: l_sum_nil_lemma
l_sum([]) 0

Lemma: l_sum_cons_lemma
L,a:Top.  (l_sum([a L]) 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 and list item a):
   over list:
   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 then else 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 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) ∈ 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
  ∀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
  ∀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].
                                  ∧ (∀j:{j:ℕ||ll||| ¬(i j ∈ ℤ)} . ∀k:ℕ||ll[i]||.  (ll[i][k] ∈ ll[j])))))

Lemma: map-is-permutation-on-list-of-all
  ∀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 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))

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 then [x] else [] fi )

Lemma: length-zero-implies-sq-nil
l:Top List. [] 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} in let L,a in <x, L>

Lemma: list_decomp_rev_wf
[T:Type]. ∀[l:T List].  list_decomp_rev{i:l}(l) ∈ {p:T × (T List)| ((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 (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
  ∀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 b)  (P (L [x]) (F x))))
     (∀L:A List. (P list_ind_reverse(L;nilcase;F))))

Lemma: list_ind_reverse_unfold1
  ∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.
    (list_ind_reverse(L;nilcase;F) if (||L|| =z 0)
    then nilcase
    else list_ind_reverse(firstn(||L|| 1;L);nilcase;F) firstn(||L|| 1;L) last(L)
    fi )

Lemma: list_ind_reverse_unfold
  ∀nilcase:B. ∀F:B ⟶ (A List) ⟶ A ⟶ B. ∀L:A List.
    ((||L|| > 0)
     (list_ind_reverse(L;nilcase;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[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) ∈ List)

Lemma: append_iseg
[T:Type]. ∀as,bs,cs:T List.  (as bs ≤ as cs ⇐⇒ bs ≤ cs)

Lemma: iseg_append_iff
  ∀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] ≤ ⇐⇒ 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 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 ∈ 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) ∈ ⇐⇒ False)) supposing (no_repeats(T;L) and 0 < ||L||)

Lemma: last-not-before
[T:Type]. ∀L:T List. (∀x:T. (last(L) before x ∈ ⇐⇒ 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
  ∀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
  ∀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 ∈ i))

Lemma: concat-decomp
  ∀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
  ∀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) ⇐⇒ before x ∈ L)

Comment: map-index-comment
No doubt this function has already been defined elsewhere, but
can't find it:

   map-index(f; [x0; x1; ...]) [f x0 x1 ...]⋅

Definition: map-index_aux
map-index_aux(f;L) ==  rec-case(L) of [] => λn.[] hd::tl => aux.λn.[f 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 ∈ 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] (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) ∈ 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] 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.<x, 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) ∈ List)

Lemma: length-shuffle
[T:Type]. ∀[ps:(T × T) List].  (||shuffle(ps)|| ||ps||)

Lemma: select-shuffle
[T:Type]. ∀[ps:(T × T) List].
  ∀i:ℕ||shuffle(ps)||. (shuffle(ps)[i] if (i rem =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|| <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.<(2 i), ((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.<(2 i), ((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 
     in if ||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) ∈ 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))]))

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))])))

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
                    b];x,a.g[x; a];x,b.h[x; b];y;as;bs)
==r if as is pair then let a,as' as 
                         in if bs is pair then let b,bs' bs 
                                                 in eval y' f[y;
                                                                b] in
                                                                        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
                                                                          b];x,a.g[x; a];x,b.h[x; b];y';as';Ax) otherwis\000Ce ⊥
    otherwise if as Ax then if bs is pair then let b,bs' bs 
                                                   in eval y' h[y; b] in
                                                                          b];x,a.g[x; a];x,b.h[x; b];y';Ax;bs')
                              otherwise if bs Ax then otherwise ⊥ otherwise ⊥

Lemma: list_accum2_wf
  ∀[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
==r eval aa as in
    if aa is pair then let a,more aa 
                         in eval 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) ∈ List) supposing value-type(B)

Lemma: rev-map-append-sq
  ∀[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) ∈ 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 Ax then otherwise let a,x 
                             in if Ax then otherwise let b,y 
                                                           in eval 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) ∈ List) supposing value-type(T)

Lemma: length-interpolate-list
  ∀[f:T ⟶ T ⟶ T]. ∀[L:T List].  (||interpolate-list(x,y.f[x;y];L)|| if null(L) then else (2 ||L||) 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∈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) ==
      x.(l-all-decider() (f x) 
           z.letrec list_ind(L)=eval in
                                  if is pair then let a,L 
                                                      in case list_ind L
                                                          of inl(%2) =>
                                                          if a
                                                          then inl <0, Ax, Ax>
                                                          else inl let i,%4,%5 %2 in 
                                                               <1, Ax, Ax>
                                                          inr(%2) =>
                                                          if then inl <0, Ax, Ax> else inr %.Ax)  fi 
                                  otherwise if Ax then inr %.Ax)  otherwise fix((λx.x)) in

Lemma: list-closed-test_wf
[T:Type]. ∀L:T List. ∀f:T ⟶ (T List). ∀d:EqDecider(T).  (list-closed-test(f;d;L) ∈ {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) ∈ 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 and list item b):
   let f[L; b] in [<a, b, g[a; b]>]
  over list:
  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