************ LIST_0 ************
The list type used to be primitive, but now
we define it using the rec-type and unit, union, and product types.

The list_ind operator is defined by recursion,
and cons and nil are just pair and Axiom.


Type-checking naturally partial list functions
can be rather onerous. Therefore when possible
I've made functions more total than they need to 
be. Also, to simplify life for type checking
I've made it so that all length restrictions are
spun off as separate subgoals and avoided having 
multiple wf lemmas giving types both in List and 

Lemma: isaxiom_wf_listunion
[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  (isaxiom(L) ∈ 𝔹)

Lemma: axiom-listunion
[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  L ∈ Unit supposing isaxiom(L) tt

Lemma: non-axiom-listunion
[A,B:Type]. ∀[L:Unit ⋃ (A × B)].  L ∈ A × supposing isaxiom(L) ff

Lemma: list-functor
[T:Type]. ContinuousMonotone(L.Unit ⋃ (T × L))

Definition: colist
The co-recursive type of
all terms built from Ax  (= []) and pairs <t, l> (= ⌜[t l]⌝)
where ⌜t ∈ T⌝ and ⌜l ∈ colist(T)⌝It includes both the finite lists and
infinite streams.⋅

colist(T) ==  corec(L.Unit ⋃ (T × L))

Lemma: colist_wf
[T:Type]. (colist(T) ∈ Type)

Lemma: subtype_rel_colist
[A,B:Type].  colist(A) ⊆colist(B) supposing A ⊆B

Lemma: colist-fix-partial
  (∀[T:Type]. ∀[f:⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))].
     (fix(f) ∈ colist(T) ⟶ partial(A))) supposing 
     (mono(A) and 

Lemma: colist-ext
[T:Type]. colist(T) ≡ Unit ⋃ (T × colist(T))

Lemma: unit_subtype_colist
[T:Type]. (Unit ⊆colist(T))

Lemma: product_subtype_colist
[T:Type]. ((T × colist(T)) ⊆colist(T))

Lemma: colist-value-type
[T:Type]. value-type(colist(T))

Definition: co-nil
() ==  ⋅

Lemma: co-nil_wf
[T:Type]. (() ∈ colist(T))

Definition: co-cons
[x L] ==  <x, L>

Lemma: co-cons_wf
[T:Type]. ∀[x:T]. ∀[L:colist(T)].  ([x L] ∈ colist(T))

Lemma: isaxiom-wf-colist
[T:Type]. ∀[x:colist(T)].  (isaxiom(x) ∈ 𝔹)

Lemma: colist-fix-ap-partial
  (∀[T:Type]. ∀[f:⋂L:Type. ((L ⟶ partial(A)) ⟶ (Unit ⋃ (T × L)) ⟶ partial(A))]. ∀[L:colist(T)].
     (fix(f) L ∈ partial(A))) supposing 
     (mono(A) and 

Definition: colength
colength(L)==r if Ax then otherwise let a,b in colength(b)

Lemma: colength_wf
[T:Type]. ∀[L:colist(T)].  (colength(L) ∈ partial(ℕ))

Definition: list
The list type was once primitive in Nuprl. Later, it was defined using
the "Mendler" fixpoint type. Now we define lists as those "co-lists"
for which the length (a partially defined function) has value.
Once we show that the list iterator is well formed (see list_ind_wf)
then we can use list as an abstract type. This "implementation" shows that
we only need induction on ⌜ℕ⌝ to build lists, and do not need the power
of the Mendler fixpoint or general inductive construction.⋅

List ==  {L:colist(T)| (colength(L))↓

Lemma: list_wf
[T:Type]. (T List ∈ Type)

Lemma: list-wf
[A:Type]. (A List ∈ Type)

Lemma: list-ext
[A:Type]. List ≡ Unit ⋃ (A × (A List))

Lemma: colength_wf_list
[T:Type]. ∀[L:T List].  (colength(L) ∈ ℕ)

Definition: nil
[] ==  ⋅

Lemma: nil_wf
[T:Type]. ([] ∈ List)

Lemma: subtype_rel_list
[A,B:Type].  (A List) ⊆(B List) supposing A ⊆B

Lemma: list-value-type
[T:Type]. value-type(T List)

Lemma: product_subtype_list
[T:Type]. ((T × (T List)) ⊆(T List))

Definition: cons
[a b] ==  <a, b>

Lemma: cons_wf
[S:Type]. ∀[a:S]. ∀[b:S List].  ([a b] ∈ List)

Lemma: colength-cons-not-zero
[T:Type]. ∀[v:T List]. ∀[u:Top].  False supposing colength([u v]) 0 ∈ ℕ

Lemma: subtype_rel_list_set
[A,B:Type]. ∀[P:A ⟶ Type]. ∀[Q:B ⟶ Type].
  (({a:A| P[a]}  List) ⊆({b:B| Q[b]}  List)) supposing ((∀x:A. (P[x]  Q[x])) and ({a:A| P[a]}  ⊆B))

Lemma: unit_subtype_list
[T:Type]. (Unit ⊆(T List))

Lemma: evalall_nil_lemma
evalall([]) []

Lemma: colength-zero
[L:Top List]. ((colength(L) 0 ∈ ℤ (L []))

Lemma: colength-positive
[T:Type]. ∀[L:T List].
  (0 < colength(L)
   {(fst(L) ∈ T) ∧ (snd(L) ∈ List) ∧ (colength(L) (1 colength(snd(L))) ∈ ℤ) ∧ (L [fst(L) (snd(L))])})

Lemma: pi1_cons_lemma
b,a:Top.  (fst([a b]) a)

Lemma: spread_cons_lemma
f,y,x:Top.  (let a,b [x y] in f[a;b] f[x;y])

Definition: hd
hd(l) ==  fst(l)

Lemma: reduce_hd_cons_lemma
b,a:Top.  (hd([a b]) a)

Definition: tl
tl(l) ==  if Ax then [] otherwise snd(l)

Lemma: reduce_tl_cons_lemma
b,a:Top.  (tl([a b]) b)

Lemma: reduce_tl_nil_lemma
tl([]) []

Lemma: not-cons-sq-nil
[u,v:Top].  (([u v] []) (0 1) ∈ Type)

Lemma: has-valueall-cons
[a,b:Base].  uiff(has-valueall(a) ∧ has-valueall(b);has-valueall([a b]))

Lemma: has-valueall-single
[a:Base]. uiff(has-valueall(a);has-valueall([a]))

Lemma: evalall-cons
a,b:Top.  (evalall([a b]) eval evalall(a) in eval evalall(b) in   [u v])

Definition: listify
listify(f;m;n) ==  fix((λlistify,m. if n ≤then [] else [f (listify (m 1))] fi )) m

Lemma: listify_wf
[T:Type]. ∀[m,n:ℤ]. ∀[f:{m..n-} ⟶ T].  (listify(f;m;n) ∈ List)

Lemma: colength-positive2
[T:Type]. ∀[L:T List].
    (0 < n
     (colength(L) n ∈ ℤ)
     {(fst(L) ∈ T) ∧ (snd(L) ∈ List) ∧ (colength(L) (1 colength(snd(L))) ∈ ℤ) ∧ (L [fst(L) (snd(L))])})

Lemma: comb_for_listify_wf
λT,m,n,f,z. listify(f;m;n) ∈ T:Type ⟶ m:ℤ ⟶ n:ℤ ⟶ f:({m..n-} ⟶ T) ⟶ (↓True) ⟶ (T List)

Lemma: list-functionality-induction
T,A:Type. ∀F:Base.
  ((F[[]] ∈ A)
   (∀a1,a2,L1,L2:Base.  ((a1 a2 ∈ T)  (F[L1] F[L2] ∈ A)  (F[[a1 L1]] F[[a2 L2]] ∈ A)))
   (∀L:T List. (F[L] ∈ A)))

Lemma: pair-sq-axiom-wf
[a,b:Top].  (<a, b> Ax ∈ Type)

Lemma: colist-cases
[T:Type]. ∀x:colist(T). ((x Ax) ∨ (x ∈ T × colist(T)))

Lemma: list-cases
[T:Type]. ∀x:T List. ((x []) ∨ (x ∈ T × (T List)))

Lemma: list-cases2
[T:Type]. ∀x:T List. ((x []) ∨ (x [hd(x) tl(x)]))

Lemma: tl_wf
[A:Type]. ∀[l:A List].  (tl(l) ∈ List)

Definition: list_ind
rec-case(L) of
[] => nilcase
h::t =>
     r] ==
  fix((λlist_ind,L. eval in
                    if is pair then let h,t 
                                        in F[h;
                                             list_ind t] otherwise if Ax then nilcase otherwise ⊥)) 

Lemma: list_ind_nil_lemma
A,x:Top.  (rec-case([]) of [] => h::t => r.A[h;t;r] x)

Lemma: list_ind_cons_lemma
A,x,b,a:Top.  (rec-case([a b]) of [] => h::t => r.A[h;t;r] A[a;b;rec-case(b) of [] => h::t => r.A[h;t;r]])

Lemma: list_ind-general-wf
[A:Type]. ∀[B:(A List) ⟶ ℙ]. ∀[x:B[[]]]. ∀[F:∀a:A. ∀L:A List.  (B[L]  B[[a L]])]. ∀[L:A List].
  (rec-case(L) of
   [] => x
   h::t =>
    r.F[h;t;r] ∈ B[L])

Lemma: list_ind_wf
[A,B:Type]. ∀[x:B]. ∀[F:A ⟶ (A List) ⟶ B ⟶ B]. ∀[L:A List].  (rec-case(L) of [] => h::t => r.F[h;t;r] ∈ B)

Lemma: list_subtype_base
[A:Type]. (A List) ⊆Base supposing A ⊆Base

Definition: l-ind
==r eval in
    if Ax then nilcase otherwise let h,t 
                                     in F[h;

Lemma: l_ind_nil_lemma
A,x:Top.  (l-ind([];x;h,t,r.A[h;t;r]) x)

Lemma: l_ind_cons_lemma
A,x,b,a:Top.  (l-ind([a b];x;h,t,r.A[h;t;r]) A[a;b;l-ind(b;x;h,t,r.A[h;t;r])])

Lemma: l-ind_wf
[A,B:Type]. ∀[L:A List]. ∀[x:B]. ∀[F:A ⟶ (A List) ⟶ B ⟶ B].  (l-ind(L;x;h,t,r.F[h;t;r]) ∈ B)

Definition: list_accum
accumulate (with value and list item a):
 f[x; a]
over list:
with starting value:
 y) ==
  fix((λlist_accum,y,L. eval in
                        if is pair then let h,t 
                                            in list_accum f[y; h] otherwise if Ax then otherwise ⊥)) 

Lemma: list_accum_wf
[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].
  (accumulate (with value and list item a):
   over list:
   with starting value:
    y) ∈ T')

Lemma: list-valueall-type
[T:Type]. valueall-type(T List) supposing valueall-type(T)

Lemma: list_induction
[T:Type]. ∀[P:(T List) ⟶ ℙ].  (P[[]]  (∀aaaa:T. ∀LLLL:T List.  (P[LLLL]  P[[aaaa LLLL]]))  (∀L:T List. P[L]))

Lemma: cons_neq_nil
[T:Type]. ∀[h:T]. ∀[t:T List].  ([h t] [] ∈ (T List)))

Lemma: sqle-list_ind
        F[rec-case(as) of
          [] => b1
          h::t =>
           r.H[h;t;r]] ≤ G[rec-case(as) of
                           [] => b2
                           h::t =>
        supposing F[b1] ≤ G[b2] 
      supposing ∀x,y,r1,r2:Base.  ((F[r1] ≤ G[r2])  (F[H[x;y;r1]] ≤ G[J[x;y;r2]])) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])

Lemma: l-ind-sqequal-list_ind
[L,x,F:Top].  (l-ind(L;x;h,t,r.F[h;t;r]) rec-case(L) of [] => h::t => r.F[h;t;r])

Definition: eval_list
eval_list(t) ==  rec-case(t) of [] => [] h::t => r.eval in <h, s>

Lemma: eval_list_wf
[T:Type]. ∀[L:T List].  (eval_list(L) ∈ List)

Definition: reduce
Reduce is the foldr operation⋅

reduce(f;k;as) ==  rec-case(as) of [] => a::as' => r.f r

Lemma: reduce_nil_lemma
k,f:Top.  (reduce(f;k;[]) k)

Lemma: reduce_cons_lemma
b,a,k,f:Top.  (reduce(f;k;[a b]) reduce(f;k;b))

Lemma: reduce_wf
[A,B:Type]. ∀[f:A ⟶ B ⟶ B]. ∀[k:B]. ∀[as:A List].  (reduce(f;k;as) ∈ B)

Lemma: list_accum_nil_lemma
z,f:Top.  (accumulate (with value and list item y): f[x;y]over list:  []with starting value: z) z)

Lemma: list_accum_cons_lemma
  (accumulate (with value and list item b):
   over list:
     [x y]
   with starting value:
    z) accumulate (with value and list item b):
         over list:
         with starting value:

Lemma: sqle-list_accum
        F[accumulate (with value and list item a):
          over list:
          with starting value:
           b1)] ≤ G[accumulate (with value and list item a):
                    over list:
                    with starting value:
        supposing F[b1] ≤ G[b2] 
      supposing ∀a,r1,r2:Base.  ((F[r1] ≤ G[r2])  (F[H[r1;a]] ≤ G[J[r2;a]])) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])

Lemma: sqequal-list_accum
        F[accumulate (with value and list item a):
          over list:
          with starting value:
           b1)] G[accumulate (with value and list item a):
                    over list:
                    with starting value:
        supposing F[b1] G[b2] 
      supposing (∀a,r1,r2:Base.  ((F[r1] ≤ G[r2])  (F[H[r1;a]] ≤ G[J[r2;a]])))
      ∧ (∀a,r1,r2:Base.  ((G[r1] ≤ F[r2])  (G[J[r1;a]] ≤ F[H[r2;a]]))) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])

Lemma: sqle-list_accum-list_ind
        F[accumulate (with value and list item a):
          over list:
          with starting value:
           b1)] ≤ G[b1;rec-case(as) of
                       [] => b2
                       h::t =>
        supposing ∀x:Base. (F[x] ≤ G[x;b2]) 
      supposing ∀a,b,c:Base.  (G[H[b;a];c] ≤ G[b;J[a;c]]) 
    supposing ∀z:Base. strict1(λx.G[z;x]) 
  supposing strict1(λx.F[x])

Lemma: sqle-list_ind-list_accum
        G[b1;rec-case(as) of
             [] => b2
             h::t =>
              r.J[h;r]] ≤ F[accumulate (with value and list item a):
                            over list:
                            with starting value:
        supposing ∀x:Base. (G[x;b2] ≤ F[x]) 
      supposing ∀a,b,c:Base.  (G[b;J[a;c]] ≤ G[H[b;a];c]) 
    supposing ∀z:Base. strict1(λx.G[z;x]) 
  supposing strict1(λx.F[x])

Definition: append
as bs ==  rec-case(as) of [] => bs a::as' => r.[a r]

Lemma: append_wf
[T:Type]. ∀[as,bs:T List].  (as bs ∈ List)

Definition: eager-append
eager-append(as;bs) ==  rec-case(as) of [] => bs a::as' => r.eval r' in [a r']

Lemma: eager-append_wf
[T:Type]. ∀[as,bs:T List].  (eager-append(as;bs) ∈ List)

Definition: map
map(f;as) ==  rec-case(as) of [] => [] h::t => r.[f r]

Lemma: map_nil_lemma
f:Top. (map(f;[]) [])

Lemma: map_cons_lemma
b,a,f:Top.  (map(f;[a b]) [f map(f;b)])

Lemma: map_wf
[A,B:Type]. ∀[f:A ⟶ B]. ∀[l:A List].  (map(f;l) ∈ List)

Definition: eager-map
eager-map(f;as) ==  rec-case(as) of [] => [] h::t => r.eval h' in eval r' in   [h' r']

Lemma: eager-map_wf
[A,B:Type].  ∀[f:A ⟶ B]. ∀[l:A List].  (eager-map(f;l) ∈ List) supposing value-type(B)

Lemma: eager_map_nil_lemma
f:Top. (eager-map(f;[]) [])

Lemma: eager_map_cons_lemma
v,u,f:Top.  (eager-map(f;[u v]) eval in eval eager-map(f;v) in   [x r])

Definition: nth_tl
nth_tl(n;as) ==  fix((λnth_tl,n,as. if n ≤then as else nth_tl (n 1) tl(as) fi )) as

Lemma: nth_tl_wf
[A:Type]. ∀[as:A List]. ∀[i:ℤ].  (nth_tl(i;as) ∈ List)

Definition: rev-append
rev(as) bs ==  accumulate (with value and list item a): [a r]over list:  aswith starting value: bs)

Lemma: rev-append_wf
[T:Type]. ∀[as,bs:T List].  (rev(as) bs ∈ List)

Lemma: eq_cons_imp_eq_tls
[A:Type]. ∀[a,b:A]. ∀[as,bs:A List].  as bs ∈ (A List) supposing [a as] [b bs] ∈ (A List)

Definition: reject
as\[i] ==
  fix((λreject,i,as. if i ≤then tl(as) else case as of [] => [] a'::as' => [a' (reject (i 1) as')] esac fi )) \000Ci as

Lemma: reject_wf
[A:Type]. ∀[l:A List]. ∀[n:ℤ].  (l\[n] ∈ List)

Definition: eager-map-append
eager-map-append(f;as;bs) ==
  accumulate (with value and list item a):
   eval in
   eval L' in
     [x L']
  over list:
  with starting value:

Lemma: eager-map-append_wf
  ∀[A:Type]. ∀[f:A ⟶ T]. ∀[as:A List]. ∀[bs:T List].  (eager-map-append(f;as;bs) ∈ List) supposing value-type(T)

Definition: mapc
Illustration of use of add_rec_def for curried function⋅

mapc(f) ==  fix((λmapc,f,as. case as of [] => [] a::as1 => [f (mapc as1)] esac)) f

Lemma: mapc_wf
[A,B:Type]. ∀[f:A ⟶ B].  (mapc(f) ∈ (A List) ⟶ (B List))

Definition: insert-int
insert-int(x;l) ==  rec-case(l) of [] => [x] a::as => v.if (a) < (x)  then eval in [a y]  else [x; [a as]]

Lemma: insert-int_wf
[T:Type]. ∀[x:T]. ∀[l:T List].  (insert-int(x;l) ∈ List) supposing T ⊆r ℤ

Lemma: insert_int_nil_lemma
a:Top. (insert-int(a;[]) [a])

Lemma: insert-int-cons
v:ℤ List. ∀u,a:ℤ.  (insert-int(a;[u v]) if u <then [u insert-int(a;v)] else [a; [u v]] fi )

Definition: update-alist
update-alist(eq;L;x;z;v.f[v]) ==  rec-case(L) of [] => [<x, z>p::ps => r.let a,v in if eq then [<x, f[v]> \000Cps] else [p r] fi 

Lemma: update-alist_wf
[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:(T × A) List]. ∀[z:A]. ∀[f:A ⟶ A].
  (update-alist(eq;L;x;z;v.f[v]) ∈ (T × A) List)

Lemma: sqequal-list_ind
        F[rec-case(as) of
          [] => b1
          h::t =>
           r.H[h;t;r]] G[rec-case(as) of
                           [] => b2
                           h::t =>
        supposing F[b1] G[b2] 
      supposing (∀x,y,r1,r2:Base.  ((F[r1] ≤ G[r2])  (F[H[x;y;r1]] ≤ G[J[x;y;r2]])))
      ∧ (∀x,y,r1,r2:Base.  ((G[r1] ≤ F[r2])  (G[J[x;y;r1]] ≤ F[H[x;y;r2]]))) 
    supposing strict1(λx.G[x]) 
  supposing strict1(λx.F[x])

Lemma: eval_list_nil_lemma
eval_list([]) []

Lemma: eval_list_cons_lemma
b,a:Top.  (eval_list([a b]) eval b' eval_list(b) in [a b'])

Lemma: sqequal-list_accum-list_ind
        F[accumulate (with value and list item a):
          over list:
          with starting value:
           b1)] G[b1;rec-case(as) of
                       [] => b2
                       h::t =>
        supposing ∀x:Base. (F[x] G[x;b2]) 
      supposing ∀a,b,c:Base.  (G[H[b;a];c] G[b;J[a;c]]) 
    supposing ∀z:Base. strict1(λx.G[z;x]) 
  supposing strict1(λx.F[x])

Lemma: comb_for_append_wf
λT,as,bs,z. (as bs) ∈ T:Type ⟶ as:(T List) ⟶ bs:(T List) ⟶ (↓True) ⟶ (T List)

Lemma: list_accum_cons
  (accumulate (with value and list item a):
   over list:
     [A B]
   with starting value:
    y) accumulate (with value and list item a):
         over list:
         with starting value:

Lemma: comb_for_map_wf
λA,B,f,l,z. map(f;l) ∈ A:Type ⟶ B:Type ⟶ f:(A ⟶ B) ⟶ l:(A List) ⟶ (↓True) ⟶ (B List)

Lemma: map-pair
[f,a,b:Top].  (map(f;<a, b>~ <a, map(f;b)>)

Lemma: map-axiom
[f:Top]. (map(f;Ax) Ax)

Lemma: eager-map-is-map
[A,B:Type].  ∀[f:A ⟶ B]. ∀[l:A List].  (eager-map(f;l) map(f;l)) supposing value-type(B)

Lemma: list_accum-map
  (accumulate (with value and list item a):
   over list:
   with starting value:
    y) accumulate (with value and list item a):
          f[x;g a]
         over list:
         with starting value:

Lemma: map-ifthenelse
[f,x,y,b:Top].  (map(f;if then else fi if then map(f;x) else map(f;y) fi )

Lemma: reduce-ifthenelse
[f,k,x,y,b:Top].  (reduce(f;k;if then else fi if then reduce(f;k;x) else reduce(f;k;y) fi )

Lemma: rev-append-pair
[a,b,c:Top].  (rev(<a, b>rev(b) + <a, c>)

Lemma: rev-append-axiom
[c:Top]. (rev(Ax) c)

Lemma: rev_app_nil_lemma
bs:Top. (rev([]) bs bs)

Lemma: rev_app_cons_lemma
bs,as,a:Top.  (rev([a as]) bs rev(as) [a bs])

Definition: reverse
rev(as) ==  rev(as) []

Lemma: reverse_wf
[T:Type]. ∀[as:T List].  (rev(as) ∈ List)

Lemma: reject_cons_hd
[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ].  [a as]\[i] as ∈ (T List) supposing i ≤ 0

Definition: for
For{T,op,id} x ∈ as. f[x] ==  reduce(op;id;map(λx:T. f[x];as))

Lemma: for_wf
[A,B,C:Type]. ∀[f:B ⟶ C ⟶ C]. ∀[k:C]. ∀[as:A List]. ∀[g:A ⟶ B].  (For{A,f,k} x ∈ as. g[x] ∈ C)

Definition: filter
filter(P;l) ==  reduce(λa,v. if then [a v] else fi ;[];l)

Lemma: filter_wf
[T:Type]. ∀[l:T List]. ∀[P:T ⟶ 𝔹].  (filter(P;l) ∈ List)

Definition: concat
concat(ll) ==  reduce(λl,l'. (l l');[];ll)

Lemma: concat_wf
[T:Type]. ∀[ll:T List List].  (concat(ll) ∈ List)

Lemma: strict4-append
strict4(λx,y,z,w. (x y))

Lemma: strict4-map
strict4(λx,y,z,s. map(y;x))

Lemma: eager_map_append_nil_lemma
bs,f:Top.  (eager-map-append(f;[];bs) bs)

Definition: eager-product-map
eager-product-map(f;as;bs) ==  rec-case(as) of [] => [] a::more_as => r.eager-map-append(f a;bs;r)

Lemma: eager-product-map_wf
  ∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].  (eager-product-map(f;as;bs) ∈ List) 
  supposing value-type(T)

Definition: merge-int
merge-int(as;bs) ==  reduce(λb,l. insert-int(b;l);as;bs)

Lemma: merge-int_wf
[T:Type]. ∀[as,bs:T List].  (merge-int(as;bs) ∈ List) supposing T ⊆r ℤ

Definition: deq-member
x ∈b ==  reduce(λa,b. ((eq x) ∨bb);ff;L)

Lemma: deq-member_wf
[A:Type]. ∀[eq:EqDecider(A)]. ∀[L:A List]. ∀[x:A].  (x ∈b L ∈ 𝔹)

Definition: null
null(as) ==  if as is pair then ff otherwise if as Ax then tt otherwise ⊥

Lemma: null_nil_lemma
null([]) tt

Lemma: null_cons_lemma
b,a:Top.  (null([a b]) ff)

Lemma: null_wf
[T:Type]. ∀[as:T List].  (null(as) ∈ 𝔹)

Lemma: null_wf2
null([]) ∈ 𝔹

Lemma: assert_of_null
[T:Type]. ∀[as:T List].  uiff(↑null(as);as [] ∈ (T List))

Lemma: assert-null-base
[as:Base]. uiff(null(as) tt;as [])

Lemma: subtype_rel_list-iff
[A,B:Type].  uiff((A List) ⊆(B List);A ⊆B)

Lemma: map_is_nil
[A,B:Type]. ∀[f:A ⟶ B]. ∀[l:A List].  uiff(map(f;l) [] ∈ (B List);l [] ∈ (A List))

Lemma: null-map
[f,L:Top].  (null(map(f;L)) null(L))

Lemma: append-unroll
[as,bs:Top].  (as bs if as is pair then [fst(as) ((snd(as)) bs)] otherwise if as Ax then bs otherwise ⊥)

Lemma: eager-append-is-append
[as,bs:Top List].  (eager-append(as;bs) as bs)

Lemma: has-value-append
[l,k:Base].  (l)↓ supposing (l k)↓

Lemma: append_assoc
[as,bs,cs:Top].  ((as bs) cs as bs cs)

Lemma: eager-append_assoc
[as,bs,cs:Top List].  (eager-append(eager-append(as;bs);cs) eager-append(as;eager-append(bs;cs)))

Lemma: append_back_nil
[T:Type]. ∀[as:T List].  (as [] as)

Lemma: append-nil
[l:Top List]. (l [] l)

Lemma: append-nil-sqle
[t:Top]. (t [] ≤ t)

Lemma: prod-if-ispair-append-nil
[l:Base]. (l ∈ Top × Top) supposing ((↑ispair(l [])) and (l [])↓)

Lemma: pi1-if-ispair-append-nil
[l:Base]. (fst((l [])) fst(l)) supposing ((↑ispair(l [])) and (l [])↓)

Lemma: pi2-if-ispair-append-nil
[l:Base]. (snd((l [])) (snd(l)) []) supposing ((↑ispair(l [])) and (l [])↓)

Lemma: has-value-append-nil
[l:Base]. (l)↓ supposing (l [])↓

Lemma: ispair-or-isaxiom-append-nil
l:Base. ((l [])↓  ((↑ispair(l [])) ∨ (↑isaxiom(l []))))

Lemma: isaxiom-append-nil
[l:Base]. (↑isaxiom(l)) supposing ((↑isaxiom(l [])) and (l [])↓)

Lemma: evalall-append-implies-list-base
[a,b:Base].  a ∈ Base List supposing (evalall(a b))↓

Lemma: evalall-append-sqle
a,b:Top.  (evalall(a b) ≤ eval evalall(a) in eval evalall(b) in   evalall(u v))

Lemma: map_append_sq
[f,a,b:Top].  (map(f;a b) map(f;a) map(f;b))

Lemma: list_accum_append
[A:Top List]. ∀[B,y,f:Top].
  (accumulate (with value and list item a):
   over list:
   with starting value:
    y) accumulate (with value and list item a):
         over list:
         with starting value:
          accumulate (with value and list item a):
          over list:
          with starting value:

Lemma: rev-append-append
[as:Top List]. ∀[bs,cs:Top].  (rev(as bs) cs rev(bs) rev(as) cs)

Lemma: rev-append-rev-append
[as:Top List]. ∀[bs,cs:Top].  (rev(rev(as) bs) cs rev(bs) as cs)

Lemma: concat_conv_single_nil_lemma
concat([[]]) []

Lemma: concat-unroll
a:Top. (concat(a) if is pair then (fst(a)) concat(snd(a)) otherwise if Ax then [] otherwise ⊥)

Definition: cbv-concat
cbv-concat(ll) ==  reduce(λl,l'. eval in eval l' in   y;[];ll)

Lemma: cbv-concat-sq
[ll:Top List List]. (cbv-concat(ll) concat(ll))

Lemma: cbv-concat_wf
[T:Type]. ∀[ll:T List List].  (cbv-concat(ll) ∈ List)

Lemma: append_nil_sq
[l:Top List]. (l [] l)

Lemma: append_assoc_sq
[as,bs,cs:Top].  ((as bs) cs as bs cs)

Definition: list-accum
                   h];b;L) ==
  if is pair then let h,t 
                      in list-accum(t,a,h.f[t;
                                                 h];t) otherwise if Ax then otherwise ⊥

Lemma: list-accum_wf
[T,T':Type]. ∀[l:T List]. ∀[b:T']. ∀[f:(T List) ⟶ T' ⟶ T ⟶ T'].  (list-accum(t,a,h.f[t;a;h];b;l) ∈ T')

Lemma: list_acc_nil_red_lemma
b,f:Top.  (list-accum(t,a,h.f[t;a;h];b;[]) b)

Lemma: list_acc_cons_red_lemma
v,u,b,f:Top.  (list-accum(t,a,h.f[t;a;h];b;[u v]) list-accum(t,a,h.f[t;a;h];f[v;b;u];v))

Lemma: list-accum-append
[l1:Top List]. ∀[l2,b,f:Top].
  (list-accum(t,a,h.f[t;a;h];b;l1 l2) list-accum(t,a,h.f[t;a;h];list-accum(t,a,h.f[t l2;a;h];b;l1);l2))

Lemma: evalall-append-nil
[l:Base]. evalall(l []) supposing (evalall(l []))↓

Lemma: has-valueall-append-nil
[l:Base]. [] supposing has-valueall(l [])

Lemma: map_append
[A,B:Type]. ∀[f:A ⟶ B]. ∀[as,as':A List].  (map(f;as as') (map(f;as) map(f;as')) ∈ (B List))

Lemma: concat-single
[l:Top List]. (concat([l]) l)

Definition: length
||as|| ==  rec-case(as) of [] => a::b => r.r 1

Lemma: length_wf
[A:Type]. ∀[l:A List].  (||l|| ∈ ℤ)

Lemma: length_of_nil_lemma
||[]|| 0

Lemma: length_wf2
||[]|| ∈ ℤ

Lemma: length_of_cons_lemma
as,a:Top.  (||[a as]|| ||as|| 1)

Lemma: hd_wf
[A:Type]. ∀[l:A List].  hd(l) ∈ supposing ||l|| ≥ 

Lemma: non_neg_length
[A:Type]. ∀[l:A List].  (||l|| ≥ )

Lemma: length_wf_nat
[A:Type]. ∀[L:A List].  (||L|| ∈ ℕ)

Lemma: length_wf_nil
||[]|| ∈ ℕ

Lemma: length-wf-has-value
[l:Base]. ||l|| ∈ ℤ supposing (||l||)↓

Lemma: length-nat-if-has-value
l:Base. ((||l||)↓  (||l|| ∈ ℕ))

Lemma: list-if-has-value-length
l:Base. l ∈ Base List supposing (||l||)↓

Lemma: list-if-has-value-list_ind
  ∀l:Base. l ∈ Base List supposing (rec-case(l) of [] => a::b => r.f[a;r])↓ supposing ∀x:Base. strict(λu.f[x;u])

Lemma: list-if-has-value-length2
l:Base. l ∈ Base List supposing (||l||)↓

Lemma: comb_for_length_wf1
λA,l,z. ||l|| ∈ A:Type ⟶ l:(A List) ⟶ (↓True) ⟶ ℤ

Lemma: comb_for_length_wf2
λz.||[]|| ∈ (↓True) ⟶ ℤ

Lemma: length_cons
[A:Type]. ∀[a:A]. ∀[as:A List].  (||[a as]|| (||as|| 1) ∈ ℤ)

Lemma: length_nil
||[]|| 0 ∈ ℤ

Lemma: length-nil
||[]|| 0

Lemma: length-singleton
[x:Top]. (||[x]|| 1)

Lemma: pos_length
[A:Type]. ∀[l:A List].  ||l|| ≥ 1  supposing ¬(l [] ∈ (A List))

Lemma: length_one
[T:Type]. ∀L:T List. uiff(||L|| 1 ∈ ℤ;∃x:T. (L [x] ∈ (T List)))

Lemma: test-arith-length-additions
T:Type. ∀a:T. ∀b:T List. ∀i:ℤ.  (i < ||[a b]||  i < ||b|| 1)

Lemma: length_of_null_list
[A:Type]. ∀[as:A List].  ||as|| 0 ∈ ℤ supposing as [] ∈ (A List)

Lemma: length-is-colength
[t:Top]. (||t|| colength(t))

Lemma: non_nil_length
[T:Type]. ∀[L:T List].  0 < ||L|| supposing ¬(L [] ∈ (T List))

Lemma: map-length
[f,as:Top].  (||map(f;as)|| ||as||)

Lemma: map_length
[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List].  (||map(f;as)|| ||as|| ∈ ℤ)

Lemma: length-map
[f:Top]. ∀[T:Type]. ∀[L:T List].  (||map(f;L)|| ||L||)

Lemma: length-map-sq
[f:Top]. ∀[L:Top List].  (||map(f;L)|| ||L||)

Lemma: length_tl
[A:Type]. ∀[l:A List].  ||tl(l)|| (||l|| 1) ∈ ℤ supposing ||l|| ≥ 

Lemma: respects-equality-list
[A,B:Type].  respects-equality(A List;B List) supposing respects-equality(A;B)

Lemma: reject_cons_tl
[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ].
  ([a as]\[i] [a as\[i 1]] ∈ (T List)) supposing ((i ≤ ||as||) and 0 < i)

Lemma: listify_length
[T:Type]. ∀m,n:ℤ. ∀f:{m..n-} ⟶ T.  (n < m ∨ (||listify(f;m;n)|| (n m) ∈ ℤ))

Definition: list_n
List(n) ==  {x:A List| ||x|| n ∈ ℤ

Lemma: list_n_wf
[A:Type]. ∀[n:ℤ].  (A List(n) ∈ Type)

Definition: listp
List+ ==  {l:A List| 0 < ||l||} 

Lemma: listp_wf
[A:Type]. (A List+ ∈ Type)

Lemma: length-insert-int
[T:Type]. ∀[x:T]. ∀[l:T List].  (||insert-int(x;l)|| (||l|| 1) ∈ ℤsupposing T ⊆r ℤ

Lemma: length_cons_ge_one
[x:Top]. ∀[l:Top List].  (||[x l]|| ≥ )

Lemma: cons-listp
[T:Type]. ∀[l:T List]. ∀[x:T].  ([x l] ∈ List+)

Lemma: cons-not-nil
[S:Type]. ∀[a:S]. ∀[b:S List].  ([a b] [] ∈ (S List)))

Lemma: nil-not-cons
[S:Type]. ∀[a:S]. ∀[b:S List].  ([] [a b] ∈ (S List)))

Lemma: length-append
[as,bs:Top].  (||as bs|| ||as|| ||bs||)

Lemma: map_length_nat
[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List].  (||map(f;as)|| ||as|| ∈ ℕ)

Lemma: length-merge-int
[T:Type]. ∀[as,bs:T List].  (||merge-int(bs;as)|| (||bs|| ||as||) ∈ ℤsupposing T ⊆r ℤ

Lemma: length_append
[as,bs:Top List].  (||as bs|| (||as|| ||bs||) ∈ ℤ)

Lemma: length_of_not_nil
[A:Type]. ∀[as:A List].  uiff(¬(as [] ∈ (A List));||as|| ≥ )

Lemma: length_nth_tl
[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}].  (||nth_tl(n;as)|| (||as|| n) ∈ ℤ)

Lemma: length-rev-append
[as,bs:Top].  (||rev(as) bs|| ||as|| ||bs||)

Definition: select
L[n] ==  fix((λselect,n,L. let x,y in if (n) < (1)  then x  else eval in select y)) L

Lemma: select_wf
[A:Type]. ∀[l:A List]. ∀[n:ℤ].  (l[n] ∈ A) supposing (n < ||l|| and (0 ≤ n))

Lemma: test-select-nil
[][33] ~ ⊥

Lemma: select-cons-hd
[a,as:Top]. ∀[i:ℤ].  [a as][i] supposing i ≤ 0

Lemma: select-cons-tl
[a,as:Top]. ∀[i:ℤ].  [a as][i] as[i 1] supposing 0 < i

Lemma: select_cons_tl_sq2
[i:ℕ]. ∀[x,l:Top].  ([x l][i 1] l[i])

Lemma: select0
[L:Top]. (L[0] hd(L))

Lemma: select-nil
[i:Top]. ([][i] ~ ⊥)

Lemma: respects-equality-list-type
[A,B:Type].  ∀L:A List. ((∀i:ℕ||L||. (L[i] ∈ B))  (L ∈ List)) supposing respects-equality(A;B)

Lemma: hd-nil
hd([]) ~ ⊥

Lemma: select-as-hd
[L:Top List]. (L[0] hd(L))

Definition: l_member
(x ∈ l) ==  ∃i:ℕ(i < ||l|| c∧ (x l[i] ∈ T))

Lemma: l_member_wf
[T:Type]. ∀[x:T]. ∀[l:T List].  ((x ∈ l) ∈ ℙ)

Lemma: cons-has-member
[S:Type]. ∀a:S. ∀[b:S List]. ∃x:S. (x ∈ [a b])

Definition: sorted
sorted(L) ==  ∀i:ℕ||L||. ∀j:ℕi.  (L[j] ≤ L[i])

Lemma: sorted_wf
[T:Type]. ∀[L:T List]. (sorted(L) ∈ ℙsupposing T ⊆r ℤ

Definition: no_repeats
no_repeats(T;l) ==  ∀[i,j:ℕ].  (l[i] l[j] ∈ T)) supposing ((¬(i j ∈ ℕ)) and j < ||l|| and i < ||l||)

Lemma: no_repeats_wf
[T:Type]. ∀[l:T List].  (no_repeats(T;l) ∈ ℙ)

Definition: last
last(L) ==  L[||L|| 1]

Lemma: last_wf
[T:Type]. ∀[L:T List].  last(L) ∈ supposing ¬↑null(L)

Lemma: select_cons_hd
[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ].  [a as][i] a ∈ supposing i ≤ 0

Lemma: select_cons_tl
[T:Type]. ∀[a:T]. ∀[as:T List]. ∀[i:ℤ].  ([a as][i] as[i 1] ∈ T) supposing ((i ≤ ||as||) and 0 < i)

Lemma: select_cons_tl_sq
[T:Type]. ∀[x:T]. ∀[l:T List]. ∀[i:ℕ||l||].  ([x l][i 1] l[i])

Lemma: select_tl
[A:Type]. ∀[as:A List]. ∀[n:ℕ||as|| 1].  (tl(as)[n] as[n 1] ∈ A)

Lemma: select-cons
[x,L:Top]. ∀[i:ℤ].  ([x L][i] if i ≤then else L[i 1] fi )

Lemma: select-append
[L1,L2:Top List]. ∀[i:ℕ].  (L1 L2[i] if i <||L1|| then L1[i] else L2[i ||L1||] fi )

Lemma: select-is-bottom
[X:Top List]. ∀[i:ℕ].  X[i] ~ ⊥ supposing ||X|| ≤ i

Lemma: member_exists
[T:Type]. ∀L:T List. ∃x:T. (x ∈ L) supposing ¬(L [] ∈ (T List))

Lemma: nil_member
[T:Type]. ∀x:T. ((x ∈ []) ⇐⇒ False)

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

Lemma: free-from-atom-l_member
[T:Type]. ∀[L:T List]. ∀[a:Atom1]. ∀[x:T].  (a#x:T) supposing (a#L:T List and (x ∈ L))

Lemma: member_singleton
[T:Type]. ∀a,x:T.  ((x ∈ [a]) ⇐⇒ a ∈ T)

Lemma: member-merge-int
bs,as:ℤ List. ∀x:ℤ.  ((x ∈ merge-int(as;bs)) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))

Definition: first-success
first-success(f;L) ==
  rec-case(L) of
  [] => inr ⋅ 
  a::as =>
   r.case of inl(x) => inl <0, x> inr(_) => case of inl(p) => let i,x in inl <1, x> inr(z) => inr 

Lemma: first-success_wf
[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List].  (first-success(f;L) ∈ i:ℕ||L|| × A[L[i]]?)

Lemma: no_repeats_witness
[T:Type]. ∀[l:T List].  (no_repeats(T;l)  x.Ax ∈ no_repeats(T;l)))

Lemma: sq_stable__no_repeats
[T:Type]. ∀[l:T List].  SqStable(no_repeats(T;l))

Lemma: no_repeats_nil
[T:Top]. no_repeats(T;[])

Lemma: no_repeats_nil_uiff
[T:Top]. uiff(no_repeats(T;[]);True)

Lemma: last_nil
last([]) ~ ⊥

Lemma: last_member
[T:Type]. ∀L:T List. (last(L) ∈ L) supposing ¬↑null(L)

Lemma: last_cons2
[L:Top List]. ∀[x:Top].  (last([x L]) if null(L) then else last(L) fi )

Lemma: select_append_back
[T:Type]. ∀[as,bs:T List]. ∀[i:{||as||..||as|| ||bs||-}].  (as bs[i] bs[i ||as||] ∈ T)

Lemma: select_append_front
[T:Type]. ∀[as,bs:T List]. ∀[i:ℕ||as||].  (as bs[i] as[i] ∈ T)

Lemma: select-map
[f:Top]. ∀[L:Top List]. ∀[i:ℕ||L||].  (map(f;L)[i] L[i])

Lemma: select-rev-append
[T:Type]. ∀[L,bs:T List]. ∀[i:ℕ||L|| ||bs||].
  (rev(L) bs[i] if i <||L|| then L[||L|| i] else bs[i ||L||] fi  ∈ T)

Lemma: map_select
[A,B:Type]. ∀[f:A ⟶ B]. ∀[as:A List]. ∀[n:ℕ||as||].  (map(f;as)[n] (f as[n]) ∈ B)

Lemma: listify_select_id
[T:Type]. ∀[as:T List].  ((λi:ℕ||as||. as[i])[ℕ||as||] as ∈ (T List))

Lemma: select_listify_id
[T:Type]. ∀[n:ℕ]. ∀[f:ℕn ⟶ T]. ∀[i:ℕn].  ((f)[ℕn][i] (f i) ∈ T)

Lemma: member_tl
[T:Type]. ∀as:T List. ∀x:T.  (x ∈ tl(as))  (x ∈ as) supposing 0 < ||as||

Lemma: member-implies-null-eq-bfalse
[T:Type]. ∀[L:T List]. ∀[x:T].  null(L) ff supposing (x ∈ L)

Lemma: cons_member
[T:Type]. ∀l:T List. ∀a,x:T.  ((x ∈ [a l]) ⇐⇒ (x a ∈ T) ∨ (x ∈ l))

Lemma: list_extensionality
[T:Type]. ∀[a,b:T List].
  (a b ∈ (T List)) supposing ((∀i:ℕ(i < ||a||  (a[i] b[i] ∈ T))) and (||a|| ||b|| ∈ ℤ))

Definition: repeat-on-success
==r case first-success(f;as)
     of inl(v) =>
     eval as' evalall(g as) in
     eval b' in
     inr(_) =>
     <as, b>

Lemma: repeat-on-success_wf
  (∀[C:Type]. ∀[f:A ⟶ (C?)]. ∀[g:(ℕ × C) ⟶ (A List) ⟶ (A List)].
     ∀[h:(ℕ × C) ⟶ B ⟶ B]. ∀[as:A List]. ∀[b:B].  (repeat-on-success(f;g;h;as;b) ∈ List × B) 
     supposing ∃m:(A List) ⟶ ℕ
                ∀as:A List. ∀c:C. ∀j:ℕ.
                  ((first-success(f;as) (inl <j, c>) ∈ (ℕ × C?))  (g <j, c> as) < as)) supposing 
     (value-type(B) and 

Lemma: no_repeats_inject
[T:Type]. ∀[l:T List].  uiff(no_repeats(T;l);Inj(ℕ||l||;T;λi.l[i]))

Lemma: last_cons
[T:Type]. ∀[L:T List]. ∀[x:T].  last([x L]) last(L) ∈ supposing ¬↑null(L)

Lemma: list-subtype
[A:Type]. ∀[d:A List].  (d ∈ {a:A| (a ∈ d)}  List)

Definition: l_all
(∀x∈L.P[x]) ==  ∀i:ℕ||L||. P[L[i]]

Lemma: l_all_wf
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ].  ((∀x∈L.P[x]) ∈ ℙ)

Lemma: not-not-l_all-xmiddle
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ].  (¬¬(∀x∈L.P[x] ∨ P[x])))

Lemma: not-not-l_all-shift
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ].  ((∀x∈L.¬¬P[x])  (¬¬(∀x∈L.P[x])))

Definition: l_exists
(∃x∈L. P[x]) ==  ∃i:ℕ||L||. P[L[i]]

Lemma: l_exists_wf
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ].  ((∃x∈L. P[x]) ∈ ℙ)

Lemma: l_exists_wf_nil
[P:Void ⟶ Void]. ((∃x∈[]. P[x]) ∈ ℙ)

Lemma: filter_wf5
[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)}  ⟶ 𝔹].  (filter(P;l) ∈ List)

Lemma: filter_wf2
[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)}  ⟶ 𝔹].  (filter(P;l) ∈ {x:T| (x ∈ l)}  List)

Lemma: filter_wf_top
[T:Type]. ∀[l:T List]. ∀[P:{x:T| (x ∈ l)}  ⟶ 𝔹].  (filter(P;l) ∈ Top List)

Lemma: l_all_iff
[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ]. ((∀x∈L.P[x]) ⇐⇒ ∀x:T. ((x ∈ L)  P[x]))

Lemma: l_all_nil
[P:Top]. (∀x∈[].P[x])

Lemma: l_all_nil_iff
[P:Top]. uiff((∀x∈[].P[x]);True)

Lemma: l_all_single
[T:Type]. ∀t:T. ∀[P:{x:T| t ∈ T}  ⟶ ℙ]. ((∀x∈[t].P[x]) ⇐⇒ P[t])

Lemma: l_exists_functionality
  ∀L:T List. ∀[P,Q:{x:T| (x ∈ L)}  ⟶ ℙ].  ((∀x:{x:T| (x ∈ L)} (P[x] ⇐⇒ Q[x]))  {(∃x∈L. P[x]) ⇐⇒ (∃x∈L. Q[x])})

Lemma: l_exists_iff
[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ]. ((∃x∈L. P[x]) ⇐⇒ ∃x:T. ((x ∈ L) ∧ P[x]))

Lemma: l_exists_nil
[P:Top]. ((∃x∈[]. P[x]) ⇐⇒ False)

Lemma: l_exists_or
[T:Type]. ∀L:T List. ∀P,Q:{x:T| (x ∈ L)}  ⟶ ℙ.  ((∃x∈L. P[x]) ∨ (∃x∈L. Q[x]) ⇐⇒ (∃x∈L. P[x] ∨ Q[x]))

Lemma: l_all_not
[T:Type]. ∀L:T List. ∀P:T ⟶ ℙ.  ((∀x∈L.¬P[x]) ⇐⇒ ¬(∃x∈L. P[x]))

Lemma: sq_stable__l_all
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ].  ((∀[x:{x:T| (x ∈ L)} ]. SqStable(P[x]))  SqStable((∀x∈L.P[x])))

Lemma: l_all_functionality
[T:Type]. ∀L:T List. ∀P,Q:T ⟶ ℙ.  ((∀x:T. ((x ∈ L)  (P[x] ⇐⇒ Q[x])))  {(∀x∈L.P[x]) ⇐⇒ (∀x∈L.Q[x])})

Lemma: l_all_wf_nil
[P:Void ⟶ Void]. ((∀x∈[].P[x]) ∈ ℙ)

Lemma: l_all_cons
[T:Type]. ∀[P:T ⟶ ℙ].  ∀x:T. ∀L:T List.  ((∀y∈[x L].P[y]) ⇐⇒ P[x] ∧ (∀y∈L.P[y]))

Lemma: not-l_exists
[T:Type]. ∀L:T List. ∀[P:{x:T| (x ∈ L)}  ⟶ ℙ]. (∃x∈L. P[x]) ⇐⇒ (∀x∈L.¬P[x]))

Lemma: l_exists_cons
[T:Type]. ∀[P:T ⟶ ℙ].  ∀x:T. ∀L:T List.  ((∃y∈[x L]. P[y]) ⇐⇒ P[x] ∨ (∃y∈L. P[y]))

Lemma: l_exists_single
[T:Type]. ∀[P:T ⟶ ℙ].  ∀x:T. ((∃y∈[x]. P[y]) ⇐⇒ P[x])

Lemma: list-set-type
[T:Type]. ∀[L:T List].  (L ∈ {x:T| (x ∈ L)}  List)

Lemma: list-set-type2
[T:Type]. ∀[L:T List]. ∀[P:T ⟶ ℙ].  L ∈ {x:T| P[x]}  List supposing (∀x∈L.P[x])

Lemma: length-reverse
[L:Top]. (||rev(L)|| ||L||)

Lemma: select-reverse
[T:Type]. ∀[L:T List]. ∀[i:ℕ||rev(L)||].  (rev(L)[i] L[||L|| i] ∈ T)

Lemma: member-reverse
[T:Type]. ∀L:T List. ∀x:T.  ((x ∈ rev(L)) ⇐⇒ (x ∈ L))

Lemma: hd-reverse-is-last
[T:Type]. ∀[L:T List].  hd(rev(L)) last(L) ∈ supposing 0 < ||L||

Lemma: no_repeats_reverse
[T:Type]. ∀[L:T List].  uiff(no_repeats(T;rev(L));no_repeats(T;L))

Lemma: l_all_reverse
[T:Type]. ∀[P:T ⟶ ℙ].  ∀L:T List. ((∀x∈rev(L).P[x]) ⇐⇒ (∀x∈L.P[x]))

Lemma: l_exists_reduce
[T:Type]. ∀L:T List. ∀P:T ⟶ 𝔹.  ((∃x∈L. ↑P[x]) ⇐⇒ ↑reduce(λx,y. (P[x] ∨by);ff;L))

Lemma: isr-first-success
[T:Type]. ∀[A:T ⟶ Type]. ∀[f:x:T ⟶ (A[x]?)]. ∀[L:T List].  (↑isr(first-success(f;L)) ⇐⇒ (∀a∈L.↑isr(f a)))

Lemma: l_all_reduce
[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  uiff((∀x∈L.↑P[x]);↑reduce(λx,y. (P[x] ∧b y);tt;L))

Lemma: member_append
[T:Type]. ∀x:T. ∀l1,l2:T List.  ((x ∈ l1 l2) ⇐⇒ (x ∈ l1) ∨ (x ∈ l2))

Lemma: append_is_nil
[T:Type]. ∀[l1,l2:T List].  uiff((l1 l2) [] ∈ (T List);(l1 [] ∈ (T List)) ∧ (l2 [] ∈ (T List)))

Lemma: l_member_decomp
[T:Type]. ∀l:T List. ∀x:T.  ((x ∈ l) ⇐⇒ ∃l1,l2:T List. (l (l1 [x] l2) ∈ (T List)))

Lemma: l_exists_append
[T:Type]. ∀[P:T ⟶ ℙ].  ∀L1,L2:T List.  ((∃x∈L1 L2. P[x]) ⇐⇒ (∃x∈L1. P[x]) ∨ (∃x∈L2. P[x]))

Lemma: l_all_append
[T:Type]. ∀[P:T ⟶ ℙ].  ∀L1,L2:T List.  ((∀x∈L1 L2.P[x]) ⇐⇒ (∀x∈L1.P[x]) ∧ (∀x∈L2.P[x]))

Lemma: member_map
[T,T':Type].  ∀a:T List. ∀x:T'. ∀f:T ⟶ T'.  ((x ∈ map(f;a)) ⇐⇒ ∃y:T. ((y ∈ a) ∧ (x (f y) ∈ T')))

Lemma: member-map
[T,T':Type].  ∀f:T ⟶ T'. ∀a:T List. ∀x:T'.  ((x ∈ map(f;a)) ⇐⇒ ∃y:T. ((y ∈ a) ∧ (x (f y) ∈ T')))

Lemma: l_exists_map
[A,B:Type].  ∀f:A ⟶ B. ∀L:A List.  ∀[P:B ⟶ ℙ]. ((∃x∈map(f;L). P[x]) ⇐⇒ (∃x∈L. P[f x]))

Lemma: l_all_map
[A,B:Type].  ∀f:A ⟶ B. ∀L:A List.  ∀[P:B ⟶ ℙ]. ((∀x∈map(f;L).P[x]) ⇐⇒ (∀x∈L.P[f x]))

Definition: map2
==r if as Ax then [] otherwise if bs Ax then [] otherwise let a,more_as as 
                                                              in let b,more_bs bs 
                                                                 in eval in
                                                                    eval map2(f;more_as;more_bs) in
                                                                      [x L]

Lemma: map2_wf
[T:Type]. ∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].  (map2(f;as;bs) ∈ List) supposing value-type(T)

Lemma: cons_one_one
[T:Type]. ∀[a,a':T]. ∀[b,b':T List].  uiff([a b] [a' b'] ∈ (T List);{(a a' ∈ T) ∧ (b b' ∈ (T List))})

Lemma: co-cons-not-co-nil
[T:Type]. ∀[a:T]. ∀[b:colist(T)].  uiff([a b] () ∈ colist(T);False)

Lemma: co-cons_one_one
[T:Type]. ∀[a,a':T]. ∀[b,b':colist(T)].  uiff([a b] [a' b'] ∈ colist(T);{(a a' ∈ T) ∧ (b b' ∈ colist(T))})

Definition: sort-int
sort-int(as) ==  merge-int([];as)

Lemma: sort-int_wf
[T:Type]. ∀[as:T List]. (sort-int(as) ∈ List) supposing T ⊆r ℤ

Lemma: decidable__l_member
[A:Type]. ∀x:A. ((∀x,y:A.  Dec(x y ∈ A))  (∀L:A List. Dec((x ∈ L))))

Lemma: sq_stable__l_member
[A:Type]. ∀x:A. ((∀x,y:A.  Dec(x y ∈ A))  (∀L:A List. SqStable((x ∈ L))))

Definition: combine-list
combine-list(x,y.f[x; y];L) ==
  accumulate (with value and list item y):
   f[x; y]
  over list:
  with starting value:

Lemma: combine-list_wf
[A:Type]. ∀[f:A ⟶ A ⟶ A]. ∀[L:A List].  combine-list(x,y.f[x;y];L) ∈ supposing 0 < ||L||

Lemma: combine-list-cons
[A:Type]. ∀[f:A ⟶ A ⟶ A].
  ∀[L:A List]. ∀[a:A]. (combine-list(x,y.f[x;y];[a L]) f[a;combine-list(x,y.f[x;y];L)] ∈ A) supposing 0 < ||L|| 
  supposing Assoc(A;λx,y. f[x;y])

Lemma: combine-list-member
  ∀f:T ⟶ T ⟶ T. ∀L:T List.
    ((∀x,y:T.  ((f[x;y] x ∈ T) ∨ (f[x;y] y ∈ T)))  0 < ||L||  (combine-list(x,y.f[x;y];L) ∈ L))

Definition: imax-list
imax-list(L) ==  combine-list(x,y.imax(x;y);L)

Lemma: imax-list_wf
[L:ℤ List]. imax-list(L) ∈ ℤ supposing 0 < ||L||

Lemma: concat-cons
[l,ll:Top].  (concat([l ll]) concat(ll))

Lemma: concat_append
[a,b:Top].  (concat(a b) concat(a) concat(b))

Lemma: concat-map-nil
[L:Top List]. (concat(map(λx.[];L)) [])

Lemma: decidable__equal_int
x,y:ℤ.  Dec(x y ∈ ℤ)

Lemma: decidable__equal_function
[T:Type]. ((∀x,y:T.  Dec(x y ∈ T))  (∀i,j:ℤ. ∀f,g:{i..j-} ⟶ T.  Dec(f g ∈ ({i..j-} ⟶ T))))

Lemma: sorted-cons
[T:Type]. ∀[x:T]. ∀[L:T List].  uiff(sorted([x L]);sorted(L) ∧ (∀z∈L.x ≤ z)) supposing T ⊆r ℤ

Definition: intlex-aux
==r if l1 is pair then let a,as l1 
                         in let b,bs l2 
                            in if (a) < (b)  then inl Ax  else if a=b then intlex-aux(as;bs) else (inr Ax )
    otherwise inl Ax

Lemma: intlex-aux_wf
[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| ||l1|| ∈ ℤ].  (intlex-aux(l1;l2) ∈ 𝔹)

Lemma: insert-int-comm
T:Type. ∀a,b:T.  ((T ⊆r ℤ (∀L:T List. (insert-int(b;insert-int(a;L)) insert-int(a;insert-int(b;L)) ∈ (T List))))

Lemma: no_repeats_cons
[T:Type]. ∀[l:T List]. ∀[x:T].  uiff(no_repeats(T;[x l]);no_repeats(T;l) ∧ (x ∈ l)))

Definition: s-insert
s-insert(x;l) ==
  rec-case(l) of
  [] => [x]
  a::as =>
   v.if (x =z a) then [a as]
  if x <then [x; [a as]]
  else [a v]

Lemma: s-insert_wf
[T:Type]. ∀[x:T]. ∀[L:T List].  (s-insert(x;L) ∈ List) supposing T ⊆r ℤ

Lemma: member-s-insert
[T:Type]. ∀x:T. ∀L:T List. ∀z:T.  ((z ∈ s-insert(x;L)) ⇐⇒ (z x ∈ T) ∨ (z ∈ L)) supposing T ⊆r ℤ

Lemma: s-insert-sorted
[T:Type]. ∀[x:T]. ∀[L:T List].  sorted(s-insert(x;L)) supposing sorted(L) supposing T ⊆r ℤ

Lemma: intlex-aux-antisym
[l1:ℤ List]. ∀[l2:{as:ℤ List| ||as|| ||l1|| ∈ ℤ].
  (l1 l2 ∈ (ℤ List)) supposing (intlex-aux(l2;l1) tt and intlex-aux(l1;l2) tt)

Lemma: intlex-aux-transitive
[l1:ℤ List]. ∀[l2,l3:{as:ℤ List| ||as|| ||l1|| ∈ ℤ].
  (intlex-aux(l1;l3) tt) supposing (intlex-aux(l2;l3) tt and intlex-aux(l1;l2) tt)

Definition: intlex
l1 ≤_lex l2 ==  eval n1 ||l1|| in eval n2 ||l2|| in   n1 <n2 ∨b((n1 =z n2) ∧b intlex-aux(l1;l2))

Lemma: intlex_wf
[l1,l2:ℤ List].  (l1 ≤_lex l2 ∈ 𝔹)

Lemma: member-insert-int
[T:Type]. ∀l:T List. ∀x,z:T.  ((z ∈ insert-int(x;l)) ⇐⇒ (z x ∈ T) ∨ (z ∈ l)) supposing T ⊆r ℤ

Lemma: insert-int-sorted
[T:Type]. ∀[x:T]. ∀[l:T List].  sorted(insert-int(x;l)) supposing sorted(l) supposing T ⊆r ℤ

Lemma: merge-int-sorted
[T:Type]. ∀[as,bs:T List].  sorted(merge-int(bs;as)) supposing sorted(bs) supposing T ⊆r ℤ

Lemma: member-merge-int
bs,as:ℤ List. ∀x:ℤ.  ((x ∈ merge-int(as;bs)) ⇐⇒ (x ∈ as) ∨ (x ∈ bs))

Lemma: no_repeats_singleton
[T:Type]. ∀[x:T].  no_repeats(T;[x])

Lemma: no_repeats_singleton_uiff
[T:Type]. ∀[x:T].  uiff(no_repeats(T;[x]);True)

Lemma: intlex-length
[l1,l2:ℤ List].  ||l1|| ≤ ||l2|| supposing ↑l1 ≤_lex l2

Lemma: intlex-by-length
[l1,l2:ℤ List].  ↑l1 ≤_lex l2 supposing ||l1|| < ||l2||

Lemma: intlex-antisym
[l1,l2:ℤ List].  (l1 l2 ∈ (ℤ List)) supposing (l2 ≤_lex l1 tt and l1 ≤_lex l2 tt)

Lemma: intlex-transitive
[l1,l2,l3:ℤ List].  (l1 ≤_lex l3 tt) supposing (l2 ≤_lex l3 tt and l1 ≤_lex l2 tt)

Lemma: intlex-total
as,bs:ℤ List.  ((↑as ≤_lex bs) ∨ (↑bs ≤_lex as))

Lemma: intlex-cons
l1,l2:ℤ List. ∀x,y:ℤ.
  uiff(↑[x l1] ≤_lex [y l2];||l1|| < ||l2|| ∨ (x < y ∧ (||l1|| ||l2|| ∈ ℤ)) ∨ ((x y ∈ ℤ) ∧ (↑l1 ≤_lex l2)))

Definition: apply_alist
This version of apply alist assumes that the thing ⌜x⌝ being looked for
occurs in the association list.

Another version ⌜apply-alist(eq;L;x)⌝ will return ⌜inr ⋅ ⌝ when does
not occur.⋅

apply_alist(eq;L;x) ==  let a,more in let x',v in case eq x' of inl(_) => inr(_) => apply_alist(eq;more;x)

Lemma: apply_alist_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[V:Type]. ∀[L:(T × V) List].
  apply_alist(eq;L;x) ∈ {v:V| (<x, v> ∈ L)}  supposing (x ∈ map(λa.(fst(a));L))

Definition: apply-alist
apply-alist(eq;L;x) ==  rec-case(L) of [] => inr ⋅  p::ps => r.if eq (fst(p)) then inl (snd(p)) else fi 

Lemma: apply-alist_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[V:Type]. ∀[L:(T × V) List].  (apply-alist(eq;L;x) ∈ V?)

Lemma: apply_alist-eager-map
  ∀[eq:EqDecider(T)]. ∀[f:Top]. ∀[L:T List]. ∀[i:{i:T| (i ∈ L)} ].  (apply_alist(eq;eager-map(λi.<i, i>;L);i) i) 
  supposing value-type(T) ∧ (T ⊆Base)

Lemma: apply_alist-eager-map2
[A:Type]. ∀[L:A List]. ∀[T:Type].
  ∀[eq:EqDecider(T)]. ∀[g:A ⟶ T]. ∀[f:Top]. ∀[i:{i:T| (i ∈ eager-map(g;L))} ].
    (apply_alist(eq;eager-map(λa.<a, (g a)>;L);i) i) 
  supposing value-type(T) ∧ (T ⊆Base)

Lemma: apply_alist-eager-map-atom
[T:Type]. ∀[L:T List]. ∀[g:T ⟶ Atom]. ∀[f:Top]. ∀[i:{i:Atom| (i ∈ eager-map(g;L))} ].
  (apply_alist(AtomDeq;eager-map(λa.<a, (g a)>;L);i) i)

Lemma: apply-alist-function
[T,A:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[F:T ⟶ A]. ∀[L:T List].
  apply-alist(eq;map(λx.<x, F[x]>;L);x) (inl F[x]) ∈ (A?) supposing (x ∈ L)

Lemma: apply_alist_cons_lemma
x,v,u,eq:Top.  (apply-alist(eq;[u v];x) if eqof(eq) (fst(u)) then inl (snd(u)) else apply-alist(eq;v;x) fi )

Lemma: apply-updated-alist
[A,T:Type]. ∀[eq:EqDecider(T)]. ∀[x,y:T]. ∀[L:(T × A) List]. ∀[z:A]. ∀[f:A ⟶ A].
  case apply-alist(eq;L;y)
     of inl(v) =>
     inl if eq then f[v] else fi 
     inr(any) =>
     if eq then inl else inr ⋅  fi 
  ∈ (A?))

Lemma: apply-alist-cases
[T:Type]. ∀[eq:EqDecider(T)]. ∀[x:T]. ∀[L:(T × Top) List].
  (apply-alist(eq;L;x) ff supposing ¬(x ∈ map(λp.(fst(p));L))
  ∧ (∀[i:ℕ||L||]
       (apply-alist(eq;L;x) inl (snd(L[i]))) supposing (((fst(L[i])) x ∈ T) and (∀j:ℕi. ((fst(L[j])) x ∈ T))))))

Lemma: intlex-cons-same
[l1,l2:ℤ List]. ∀[x:ℤ].  uiff(↑[x l1] ≤_lex [x l2];↑l1 ≤_lex l2)

Definition: firstn
firstn(n;as) ==
  fix((λfirstn,n,as. case as of [] => [] a::as' => if 0 <then [a (firstn (n 1) as')] else [] fi  esac)) as

Lemma: firstn_wf
[A:Type]. ∀[as:A List]. ∀[n:ℤ].  (firstn(n;as) ∈ List)

Lemma: comb_for_firstn_wf
λA,as,n,z. firstn(n;as) ∈ A:Type ⟶ as:(A List) ⟶ n:ℤ ⟶ (↓True) ⟶ (A List)

Lemma: length_firstn
[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}].  (||firstn(n;as)|| n)

Lemma: length-firstn-le
[as:Top List]. ∀[n:ℕ].  (||firstn(n;as)|| ≤ n)

Lemma: first0
[L:Top List]. (firstn(0;L) [])

Lemma: firstn-firstn
[L:Top List]. ∀[n:ℕ]. ∀[m:ℕn].  (firstn(m;firstn(n;L)) firstn(m;L))

Definition: segment
as[m..n-==  firstn(n m;nth_tl(m;as))

Lemma: segment_wf
[T:Type]. ∀[as:T List]. ∀[m,n:ℤ].  (as[m..n-] ∈ List)

Lemma: whole_segment-sq
as:Top List. (as[0..||as||-as)

Lemma: whole_segment
T:Type. ∀as:T List.  ((as[0..||as||-]) as ∈ (T List))

Lemma: length_firstn_eq
[A:Type]. ∀[as:A List]. ∀[n:{0...||as||}].  (||firstn(n;as)|| n ∈ ℤ)

Lemma: comb_for_segment_wf
λT,as,m,n,z. (as[m..n-]) ∈ T:Type ⟶ as:(T List) ⟶ m:ℤ ⟶ n:ℤ ⟶ (↓True) ⟶ (T List)

Lemma: length_segment
[T:Type]. ∀[as:T List]. ∀[i:{0...||as||}]. ∀[j:{i...||as||}].  (||as[i..j-]|| (j i) ∈ ℤ)

Lemma: list_decomp
[T:Type]. ∀[L:T List].  [hd(L) tl(L)] supposing 0 < ||L||

Lemma: firstn_decomp
[T:Type]. ∀[j:ℕ]. ∀[l:T List].  (firstn(j 1;l) [l[j 1]] firstn(j;l)) supposing (j 1 < ||l|| and 0 < j)

Lemma: select-firstn
[L:Top List]. ∀[n:ℕ]. ∀[x:ℕn].  (firstn(n;L)[x] L[x])

Lemma: select_firstn
[T:Type]. ∀[as:T List]. ∀[n:{0...||as||}]. ∀[i:ℕn].  (firstn(n;as)[i] as[i] ∈ T)

Lemma: filter_nil_lemma
P:Top. (filter(P;[]) [])

Lemma: filter_cons_lemma
t,h,f:Top.  (filter(f;[h t]) if then [h filter(f;t)] else filter(f;t) fi )

Lemma: filter-cons
[P,x,L:Top].  (filter(P;[x L]) if then [x filter(P;L)] else filter(P;L) fi )

Definition: list_accum'
list_accum'(f;v;L)==r if null(L) then else let v' ⟵ in let a,as in list_accum'(f;v';as) fi 

Lemma: list_accum'_wf
  ∀[f:B ⟶ {L:A List| 0 < ||L||}  ⟶ B]. ∀[L:A List]. ∀[v:B].  (list_accum'(f;v;L) ∈ B) supposing valueall-type(B)

Definition: find_transitions
find_transitions(f;L) ==
  let h,hs 
  in eval hd(hs) in
     snd(snd(list_accum'(λd,l. let i,b,p,q 
                               in if isr(p) ∧b isr(q)
                                  then d
                                  else let a,as 
                                       in eval i' in
                                          if null(as)
                                          then eval b' in
                                               if b ∧b bb')
                                                 then eval q' if isl(q) then inr 0  else fi  in
                                                      <i', b', inr q'>
                                               if b' ∧b bb)
                                                 then eval p' if isl(p) then inr 0  else fi  in
                                                      <i', b', p', inr i >
                                               if isr(p) then <i', b', p, inr 0 >
                                               if isr(q) then <i', b', inr q>
                                               else <i', b', p, q>
                                          else eval b' hd(as) in
                                               if b ∧b bb') then <i', b', inr q>
                                               if b' ∧b bb) then <i', b', p, inr i >
                                               else <i', b', p, q>
                                  fi   ;<1, b, inl ⋅inl ⋅>;tl(L))))

Lemma: find_transitions_wf
[A:Type]. ∀[f:A ⟶ A ⟶ 𝔹]. ∀[L:A List].  find_transitions(f;L) ∈ Unit + ℤ × (Unit + ℤsupposing 1 < ||L||

Lemma: length-map2
  ∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].
    ||map2(f;as;bs)|| ||as|| ∈ ℤ supposing ||as|| ||bs|| ∈ ℤ 
  supposing value-type(T)

Lemma: select-map2
  ∀[A,B:Type]. ∀[f:A ⟶ B ⟶ T]. ∀[as:A List]. ∀[bs:B List].
    ∀[i:ℕ||as||]. (map2(f;as;bs)[i] (f as[i] bs[i]) ∈ T) supposing ||as|| ||bs|| ∈ ℤ 
  supposing value-type(T)

Lemma: sort-int-trivial
T:Type. ∀bs:T List.  ((T ⊆r ℤ sorted(bs)  (sort-int(bs) bs ∈ (T List)))

Lemma: merge-int-comm
  ∀[as,bs:T List].  merge-int(as;bs) merge-int(bs;as) ∈ (T List) supposing sorted(as) ∧ sorted(bs) supposing T ⊆r ℤ

Lemma: insert-int-1-1
  ∀[as,bs:T List].
    (∀[x:T]. as bs ∈ (T List) supposing insert-int(x;as) insert-int(x;bs) ∈ (T List)) supposing 
       (sorted(bs) and 
  supposing T ⊆r ℤ

Lemma: merge-int-1-1
  ∀[cs,as,bs:T List].
    (as bs ∈ (T List)) supposing ((merge-int(as;cs) merge-int(bs;cs) ∈ (T List)) and sorted(bs) and sorted(as)) 
  supposing T ⊆r ℤ

Lemma: merge-int-one-one
  ∀[as,bs,cs:T List].
    (as bs ∈ (T List)) supposing 
       ((merge-int(cs;as) merge-int(cs;bs) ∈ (T List)) and 
       sorted(bs) and 
       sorted(as) and 
  supposing T ⊆r ℤ

Lemma: intlex-aux-reflexive
[l1,l2:ℤ List].  intlex-aux(l1;l2) tt supposing l1 l2 ∈ (ℤ List)

Lemma: intlex-reflexive
[l1,l2:ℤ List].  l1 ≤_lex l2 tt supposing l1 l2 ∈ (ℤ List)

Lemma: insert-int-lex
as,bs:ℤ List. ∀x:ℤ.  ((↑as ≤_lex bs)  (↑insert-int(x;as) ≤_lex insert-int(x;bs)))

Lemma: merge-int-lex
cs,as,bs:ℤ List.  ((↑as ≤_lex bs)  (↑merge-int(as;cs) ≤_lex merge-int(bs;cs)))

Lemma: filter_trivial
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  filter(P;L) supposing (∀x∈L.↑P[x])

Lemma: filter_trivial2
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  filter(P;L) L ∈ (T List) supposing (∀x∈L.↑P[x])

Lemma: filter_tt
[L:Top List]. (filter(λx.tt;L) L)

Lemma: filter-bfalse
[L:Top List]. (filter(λx.ff;L) [])

Lemma: filter_type
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List].  (filter(P;l) ∈ {x:T| ↑(P x)}  List)

Lemma: filter_type2
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List].  (filter(λx.P[x];l) ∈ {x:T| ↑P[x]}  List)

Lemma: filter_wf3
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List].  (filter(λx.P[x];l) ∈ {x:T| ↑P[x]}  List)

Lemma: filter_wf4
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List].  (filter(λx.P[x];l) ∈ {x:T| (x ∈ l) ∧ (↑P[x])}  List)

Lemma: filter_wf4_2
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[l:T List].  (filter(P;l) ∈ {x:T| (x ∈ l) ∧ (↑P[x])}  List)

Lemma: member-filter
[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀x:{x:T| ↑P[x]} .  ((x ∈ filter(λx.P[x];L)) ⇐⇒ (x ∈ L))

Lemma: filter_is_nil
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  filter(P;L) [] supposing (∀x∈L.¬↑(P x))

Lemma: filter_is_nil2
[T:Type]. ∀[L:T List]. ∀[P:{x:T| (x ∈ L)}  ⟶ 𝔹].  filter(P;L) [] supposing (∀x∈L.¬↑P[x])

Lemma: null_filter
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  ↑null(filter(P;L)) supposing (∀x∈L.¬↑P[x])

Lemma: null-filter2
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  uiff(↑null(filter(P;L));(∀x∈L.¬↑(P x)))

Lemma: null-filter
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  uiff(↑null(filter(P;L));(∀x∈L.¬↑P[x]))

Lemma: non_null_filter
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  ¬↑null(filter(P;L)) supposing (∃x∈L. ↑P[x])

Lemma: member_filter
[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List. ∀x:T.  ((x ∈ filter(P;L)) ⇐⇒ (x ∈ L) ∧ (↑(P x)))

Lemma: sorted-filter
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  sorted(filter(P;L)) supposing sorted(L) supposing T ⊆r ℤ

Lemma: l_all_filter
[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  (∀x∈filter(P;L).↑(P x))

Lemma: l_all_filter_iff
[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_implies_l_all_filter
[T:Type]. ∀[Q:T ⟶ ℙ].  ∀P:T ⟶ 𝔹. ∀L:T List.  ((∀x∈L.Q[x])  (∀x∈filter(P;L).Q[x]))

Lemma: hd_member
[T:Type]. ∀L:T List. (hd(L) ∈ L) supposing ¬↑null(L)

Lemma: non_null_filter_iff
[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List.  uiff((∃x∈L. ↑P[x]);¬↑null(filter(P;L)))

Lemma: member_filter_2
[T:Type]. ∀L:T List. ∀P:{x:T| (x ∈ L)}  ⟶ 𝔹. ∀x:T.  ((x ∈ filter(P;L)) ⇐⇒ (x ∈ L) ∧ (↑(P x)))

Lemma: eval_list_sq
[t:Top List]. (eval_list(t) t)

Definition: insert
insert(a;L) ==  eval eval_list(L) in if a ∈b then else [a x] fi 

Lemma: insert_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].  (insert(a;L) ∈ List)

Lemma: deq_member_nil_lemma
x,eq:Top.  (x ∈b [] ff)

Lemma: deq_member_cons_lemma
v,u,x,eq:Top.  (x ∈b [u v] (eq x) ∨bx ∈b v)

Lemma: insert_nil_lemma
x,eq:Top.  (insert(x;[]) [x])

Lemma: assert-deq-member
[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀x:A.  (↑x ∈b ⇐⇒ (x ∈ L))

Lemma: deq-member-append
[A:Type]. ∀[eq:EqDecider(A)]. ∀[L1,L2:A List]. ∀[x:A].  (x ∈b L1 L2 x ∈b L1 ∨bx ∈b L2)

Lemma: insert-cases
[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].
  (insert(a;L) supposing (a ∈ L) ∧ insert(a;L) [a L] supposing ¬(a ∈ L))

Lemma: insert-cases2
[T:Type]. ∀eq:EqDecider(T). ∀a:T. ∀L:T List.  (((a ∈ L) ∧ (insert(a;L) L)) ∨ ((¬(a ∈ L)) ∧ (insert(a;L) [a L])))

Lemma: insert-not-nil
[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].  (insert(a;L) [] ∈ (T List)))

Lemma: last-insert
[T:Type]. ∀[eq:EqDecider(T)]. ∀[L:T List]. ∀[x:T].  (last(insert(x;L)) if null(L) then else last(L) fi  ∈ T)

Lemma: member-insert
[T:Type]. ∀eq:EqDecider(T). ∀a:T. ∀L:T List. ∀b:T.  ((b ∈ insert(a;L)) ⇐⇒ (b a ∈ T) ∨ (b ∈ L))

Lemma: insert_property
  ∀eq:EqDecider(T). ∀a:T. ∀L:T List.
    ((∀b:T. ((b ∈ insert(a;L)) ⇐⇒ (b a ∈ T) ∨ (b ∈ L))) ∧ no_repeats(T;insert(a;L)) supposing no_repeats(T;L))

Definition: l-union
as ⋃ bs ==  reduce(λa,L. insert(a;L);as;bs)

Lemma: l-union_wf
[T:Type]. ∀[eq:EqDecider(T)]. ∀[as,bs:T List].  (as ⋃ bs ∈ List)

Lemma: no_repeats-insert
[T:Type]. ∀[eq:EqDecider(T)]. ∀[a:T]. ∀[L:T List].  no_repeats(T;insert(a;L)) supposing no_repeats(T;L)

Lemma: trivial_map
[T:Type]. ∀[a:T List]. ∀[f:T ⟶ T].  map(f;a) a ∈ (T List) supposing ∀x:T. ((x ∈ a)  ((f x) x ∈ T))

Lemma: rev-append-property-top
[as,bs,cs:Top].  (rev(as) bs cs rev(as) bs cs)

Lemma: reverse-cons
[as,a:Top].  (rev([a as]) rev(as) [a])

Lemma: reverse_nil_lemma
rev([]) []

Lemma: map_map
[f,g,a:Top].  (map(g;map(f;a)) map(g f;a))

Lemma: map-map
[as,f,g:Top].  (map(g;map(f;as)) map(g f;as))

Lemma: map-id
[L:Top List]. (map(λx.x;L) L)

Definition: eager-accum
eager-accum(x,a.f[x; a];y;l) ==
  fix((λeager-accum,y,l. if Ax then otherwise let h,t in let z ⟵ f[y; h] in eager-accum t)) l

Lemma: eager-accum_wf
[T,T':Type]. ∀[l:T List]. ∀[y:T']. ∀[f:T' ⟶ T ⟶ T'].  eager-accum(x,a.f[x;a];y;l) ∈ T' supposing valueall-type(T')

Definition: merge-int-accum
merge-int-accum(as;bs) ==  eager-accum(l,b.insert-int(b;l);as;bs)

Lemma: merge-int-accum_wf
[as,bs:ℤ List].  (merge-int-accum(as;bs) ∈ ℤ List)

Lemma: merge-int-accum-sq
[bs,as:ℤ List].  (merge-int-accum(as;bs) merge-int(as;bs))

Lemma: pos-length
[A:Type]. ∀[l:A List].  uiff(¬(l [] ∈ (A List));0 < ||l||)

Definition: list-deq
list-deq(eq) ==
  λas,bs. (rec-case(as) of
           [] => λL.null(L)
           a::as' =>
            r.λL.rec-case(L) of
                 [] => ff
                 b::bs' =>
                  r2.(eq b) ∧b (r bs') 

Lemma: list-deq_wf1
[A:Type]. ∀[eq:A ⟶ A ⟶ 𝔹].  (list-deq(eq) ∈ (A List) ⟶ (A List) ⟶ 𝔹)

Lemma: list-deq_wf
[A:Type]. ∀[eq:EqDecider(A)].  (list-deq(eq) ∈ EqDecider(A List))

Definition: list_eq
list_eq(eq;as;bs) ==
  if null(as) then null(bs) else bnull(bs)) ∧b let a,aa as in let b,bb bs in (eq b) ∧b list_eq(eq;aa;bb) fi 

Lemma: list_eq_wf
[A:Type]. ∀[eq:A ⟶ A ⟶ 𝔹]. ∀[as,bs:A List].  (list_eq(eq;as;bs) ∈ 𝔹)

Lemma: assert-list_eq
[A:Type]. ∀[eq:EqDecider(A)]. ∀[as,bs:A List].  uiff(↑list_eq(eq;as;bs);as bs ∈ (A List))

Lemma: list_eq-sq-list-deq
[eq:Top]. ∀[as,bs:Top List].  (list_eq(eq;as;bs) list-deq(eq) as bs)

Lemma: firstn_all
[L:Top List]. ∀[n:ℤ].  firstn(n;L) supposing ||L|| ≤ n

Lemma: firstn-append
[L1,L2:Top List]. ∀[n:ℕ].  (firstn(n;L1 L2) if n ≤||L1|| then firstn(n;L1) else L1 firstn(n ||L1||;L2) fi )

Lemma: strong-continuous-list
[F:Type ⟶ Type]. Continuous+(T.F[T] List) supposing Continuous+(T.F[T])

Lemma: list-continuity
[X:ℕ ⟶ Type]. ((⋂n:ℕ(X[n] List)) ⊆((⋂n:ℕX[n]) List))

Lemma: sqntype_list
[A:Type]. ∀[n:ℕ].  sqntype(n;A List) supposing sqntype(n;A)

Home Index