Lemma: comb_for_nth_tl_wf
`λA,as,i,z. nth_tl(i;as) ∈ A:Type ⟶ as:(A List) ⟶ i:ℤ ⟶ (↓True) ⟶ (A List)`

Lemma: comb_for_ifthenelse_wf
`λb,A,p,q,z. if b then p else q fi  ∈ b:𝔹 ⟶ A:Type ⟶ p:A ⟶ q:A ⟶ (↓True) ⟶ A`

Lemma: map_equal2
`∀[T,T':Type]. ∀[a:T List]. ∀[f,g:T ⟶ T'].`
`  map(f;a) = map(g;a) ∈ (T' List) supposing ∀x:T. ((x ∈ a) `` ((f x) = (g x) ∈ T'))`

Lemma: comb_for_l_member_wf
`λT,x,l,z. (x ∈ l) ∈ T:Type ⟶ x:T ⟶ l:(T List) ⟶ (↓True) ⟶ ℙ`

Definition: agree_on_common
`agree_on_common(T;as;bs) ==`
`  fix((λagree_on_common,as,bs. case as of `
`                                 [] => True `
`                                 a::as' =>`
`                                  case bs of `
`                                    [] => True `
`                                    b::bs' =>`
`                                     ((¬(a ∈ bs)) ∧ (agree_on_common as' bs))`
`                                    ∨ ((¬(b ∈ as)) ∧ (agree_on_common as bs'))`
`                                    ∨ ((a = b ∈ T) ∧ (agree_on_common as' bs')) `
`                                 esac `
`                              esac)) `
`  as `
`  bs`

Lemma: agree_on_common_wf
`∀[T:Type]. ∀[as,bs:T List].  (agree_on_common(T;as;bs) ∈ ℙ)`

Lemma: agree_on_common_cons
`∀[T:Type]. ∀as,bs:T List. ∀x:T.  (agree_on_common(T;[x / as];[x / bs]) `⇐⇒` agree_on_common(T;as;bs))`

Lemma: agree_on_common_weakening
`∀[T:Type]. ∀as,bs:T List.  agree_on_common(T;as;bs) supposing as = bs ∈ (T List)`

Lemma: agree_on_common_symmetry
`∀[T:Type]. ∀as,bs:T List.  (agree_on_common(T;as;bs) `` agree_on_common(T;bs;as))`

Lemma: agree_on_common_nil
`∀[T:Type]. ∀as:T List. (agree_on_common(T;as;[]) `⇐⇒` True)`

Lemma: agree_on_common_cons2
`∀[T:Type]`
`  ∀as,bs:T List. ∀x:T.`
`    (agree_on_common(T;[x / as];bs) `⇐⇒` agree_on_common(T;as;bs) supposing ¬(x ∈ bs)`
`    ∧ agree_on_common(T;as;[x / bs]) `⇐⇒` agree_on_common(T;as;bs) supposing ¬(x ∈ as))`

Definition: reverse_select
`reverse_select(l;n) ==  l[||l|| - n + 1]`

Lemma: reverse_select_wf
`∀[T:Type]. ∀[l:T List]. ∀[n:ℕ].  reverse_select(l;n) ∈ T supposing n < ||l||`

Definition: strong_before
`x << y ∈ l ==  ((x ∈ l) ∧ (y ∈ l)) ∧ (∀i,j:ℕ.  (i < ||l|| `` j < ||l|| `` (l[i] = x ∈ T) `` (l[j] = y ∈ T) `` i < j))`

Lemma: strong_before_wf
`∀[T:Type]. ∀[L:T List]. ∀[x,y:T].  (x << y ∈ L ∈ ℙ)`

Definition: same_order
`same_order(x1;y1;x2;y2;L;T) ==  x1 << y1 ∈ L `` (x2 ∈ L) `` (y2 ∈ L) `` x2 << y2 ∈ L`

Lemma: same_order_wf
`∀[T:Type]. ∀[L:T List]. ∀[x1,x2,y1,y2:T].  (same_order(x1;y1;x2;y2;L;T) ∈ ℙ)`

Definition: l_succ
`y = succ(x) in l`` P[y] ==  ∀i:ℕ. (i + 1 < ||l|| `` (l[i] = x ∈ T) `` P[l[i + 1]])`

Lemma: l_succ_wf
`∀[T:Type]. ∀[l:T List]. ∀[x:T]. ∀[P:T ⟶ ℙ].  (y = succ(x) in l`` P[y] ∈ ℙ)`

Lemma: comb_for_l_succ_wf
`λT,l,x,P,z. y = succ(x) in l`` P[y] ∈ T:Type ⟶ l:(T List) ⟶ x:T ⟶ P:(T ⟶ ℙ) ⟶ (↓True) ⟶ ℙ`

Lemma: cons_succ
`∀[T:Type]`
`  ∀l:T List`
`    ∀[P:T ⟶ ℙ]`
`      ∀a,x:T.`
`        (y = succ(x) in [a / l]`
`        `` P[y]`
`        `` ((P[hd(l)]) supposing (0 < ||l|| and (x = a ∈ T)) ∧ y = succ(x) in l`` P[y] supposing ¬(x = a ∈ T)))`

Lemma: map_equal3
`∀[T,T':Type]. ∀[a:T List+]. ∀[f,g:T ⟶ T'].`
`  map(f;a) = map(g;a) ∈ T' List+ supposing ∀x:T. ((x ∈ a) `` ((f x) = (g x) ∈ T'))`

Lemma: hd_map
`∀[T,T':Type]. ∀[a:T List+]. ∀[f:T ⟶ T'].  (hd(map(f;a)) = (f hd(a)) ∈ T')`

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

Lemma: cons_wf_listp
`∀[A:Type]. ∀[l:A List]. ∀[x:A].  ([x / l] ∈ A List+)`

Lemma: comb_for_cons_wf_listp
`λA,l,x,z. [x / l] ∈ A:Type ⟶ l:(A List) ⟶ x:A ⟶ (↓True) ⟶ A List+`

Lemma: agree_on_common_filter
`∀[T:Type]. ∀P:T ⟶ 𝔹. ∀as,bs:T List.  (agree_on_common(T;as;bs) `` agree_on_common(T;filter(P;as);filter(P;bs)))`

Lemma: agree_on_common_iseg
`∀[T:Type]`
`  ∀as2,bs2,as1,bs1:T List.  (as1 ≤ as2 `` bs1 ≤ bs2 `` agree_on_common(T;as2;bs2) `` agree_on_common(T;as1;bs1))`

Lemma: append-impossible2
`∀[T:Type]. ∀[as,bs,cs:T List].  ∀[b:T]. uiff(cs = (as @ [b / bs]) ∈ (T List);False) supposing cs ≤ as`

Lemma: list_accum_split
`∀[T:Type]. ∀[i:ℕ]. ∀[l:T List]. ∀[f:Top ⟶ T ⟶ Top]. ∀[y:Top].`
`  accumulate (with value x and list item a):`
`   f[x;a]`
`  over list:`
`    l`
`  with starting value:`
`   y) ~ accumulate (with value x and list item a):`
`         f[x;a]`
`        over list:`
`          nth_tl(i;l)`
`        with starting value:`
`         accumulate (with value x and list item a):`
`          f[x;a]`
`         over list:`
`           firstn(i;l)`
`         with starting value:`
`          y)) `
`  supposing i < ||l||`

Definition: find
`(first x ∈ as s.t. P[x] else d) ==  case filter(λx.P[x];as) of [] => d | a::b => a esac`

Lemma: find_wf
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[as:T List]. ∀[d:T].  ((first a ∈ as s.t. P[a] else d) ∈ T)`

Lemma: find_property
`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀as:T List. ∀d:T.  (((first a ∈ as s.t. P[a] else d) ∈ as) ∨ ((first a ∈ as s.t. P[a] else d) = d ∈ T))`

Definition: list_all
`list_all(x.P[x];l) ==  reduce(λa,b. (P[a] ∧ b);True;l)`

Lemma: list_all_wf
`∀[T:Type]. ∀[l:T List]. ∀[P:T ⟶ ℙ].  (list_all(x.P[x];l) ∈ ℙ)`

Lemma: list_all_iff
`∀[T:Type]. ∀l:T List. ∀[P:T ⟶ ℙ]. (list_all(x.P[x];l) `⇐⇒` ∀x:T. ((x ∈ l) `` P[x]))`

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

Definition: append_rel
`append_rel(T;L1;L2;L) ==  (L1 @ L2) = L ∈ (T List)`

Lemma: append_rel_wf
`∀[T:Type]. ∀[L1,L2,L:T List].  (append_rel(T;L1;L2;L) ∈ ℙ)`

Definition: safety
`safety(A;tr.P[tr]) ==  ∀tr1,tr2:A List.  (tr1 ≤ tr2 `` P[tr2] `` P[tr1])`

Lemma: safety_wf
`∀[A:Type]. ∀[P:(A List) ⟶ ℙ].  (safety(A;x.P[x]) ∈ ℙ)`

Lemma: no_repeats_safety
`∀[A:Type]. safety(A;L.no_repeats(A;L))`

Lemma: filter_safety
`∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ∀f:T ⟶ 𝔹. (safety(T;L.P L) `` safety(T;L.P filter(f;L)))`

Lemma: all_safety
`∀[T,I:Type]. ∀[P:I ⟶ (T List) ⟶ ℙ].  ((∀x:I. safety(T;L.P[x;L])) `` safety(T;L.∀x:I. P[x;L]))`

Lemma: safety_and
`∀[A:Type]. ∀[P,Q:(A List) ⟶ ℙ].  (safety(A;x.P[x]) `` safety(A;x.Q[x]) `` safety(A;x.P[x] ∧ Q[x]))`

Lemma: safety_nil
`∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ((∃l:T List. P[l]) `` safety(T;x.P[x]) `` P[[]])`

Lemma: cond_safety_and
`∀[A:Type]. ∀[P,Q:(A List) ⟶ ℙ].`
`  (safety(A;x.P[x]) `` (∀tr1,tr2:A List.  (tr1 ≤ tr2 `` P[tr2] `` Q[tr2] `` Q[tr1])) `` safety(A;x.P[x] ∧ Q[x]))`

Lemma: agree_on_common_append
`∀[T:Type]`
`  ∀as,bs,cs,ds:T List.`
`    (agree_on_common(T;as;cs) `` agree_on_common(T;bs;ds) `` agree_on_common(T;as @ bs;cs @ ds)) supposing `
`       ((∀x∈as.¬(x ∈ ds)) and `
`       (∀x∈cs.¬(x ∈ bs)))`

Lemma: split_rel_last
`∀[A:Type]`
`  ∀r:A ⟶ A ⟶ 𝔹. ∀L:A List.`
`    (∃L1,L2:A List`
`      (((L = (L1 @ L2) ∈ (A List)) ∧ (¬↑null(L2)) ∧ (∀b∈L2.↑r[b;last(L)]))`
`      ∧ ¬↑r[last(L1);last(L)] supposing ¬↑null(L1))) supposing `
`       ((¬↑null(L)) and `
`       (∀a:A. (↑r[a;a])))`

Lemma: append_split
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:T ⟶ ℙ]`
`      ((∀x:ℕ||L||. Dec(P L[x]))`
`      `` (∀i,j:ℕ||L||.  ((P L[i]) `` P L[j] supposing i < j))`
`      `` (∃L1,L2:T List`
`           (((L = (L1 @ L2) ∈ (T List)) ∧ (∀i:ℕ||L1||. (¬(P L1[i]))) ∧ (∀i:ℕ||L2||. (P L2[i])))`
`           ∧ (∀x∈L.(P x) `` (x ∈ L2)))))`

Definition: l_all2
`(∀x<y∈L.P[x; y]) ==  ∀x,y:T.  (x before y ∈ L `` P[x; y])`

Lemma: l_all2_wf
`∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ T ⟶ ℙ].  ((∀x<y∈L.P[x;y]) ∈ ℙ)`

Lemma: l_all2_cons
`∀[T:Type]. ∀L:T List. ∀[P:T ⟶ T ⟶ ℙ]. ∀u:T. ((∀x<y∈[u / L].P[x;y]) `⇐⇒` (∀y∈L.P[u;y]) ∧ (∀x<y∈L.P[x;y]))`

Definition: l_all_since
`(∀x≥a∈L.P[x]) ==  P[a] ∧ (∀b:T. (a before b ∈ L `` P[b]))`

Lemma: l_all_since_wf
`∀[T:Type]. ∀[P:T ⟶ ℙ]. ∀[L:T List]. ∀[a:T].  ((∀x≥a∈L.P[x]) ∈ ℙ)`

Definition: split_tail
`split_tail(L | ∀x.f[x]) ==`
`  fix((λsplit_tail,L. case L of `
`                        [] => <[], []> `
`                        a::as =>`
`                         let hs,ftail = split_tail as `
`                         in case hs of `
`                              [] => if f[a] then <[], [a / ftail]> else <[a], ftail> fi  `
`                              x::y =>`
`                               <[a / hs], ftail> `
`                            esac `
`                     esac)) `
`  L`

Lemma: split_tail_wf
`∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].  (split_tail(L | ∀x.f[x]) ∈ A List × (A List))`

Lemma: split_tail_trivial
`∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].`
`  split_tail(L | ∀x.f[x]) = <[], L> ∈ (A List × (A List)) supposing ∀b:A. ((b ∈ L) `` (↑f[b]))`

Lemma: split_tail_max
`∀[A:Type]`
`  ∀f:A ⟶ 𝔹. ∀L:A List. ∀a:A.`
`    ((a ∈ L) `` ((a ∈ snd(split_tail(L | ∀x.f[x])))) supposing ((∀b:A. (a before b ∈ L `` (↑f[b]))) and (↑f[a])))`

Lemma: split_tail_correct
`∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].  (∀b∈snd(split_tail(L | ∀x.f[x])).↑f[b])`

Lemma: split_tail_rel
`∀[A:Type]. ∀[f:A ⟶ 𝔹]. ∀[L:A List].  (((fst(split_tail(L | ∀x.f[x]))) @ (snd(split_tail(L | ∀x.f[x])))) = L ∈ (A List))`

Lemma: split_tail_lemma
`∀[A:Type]`
`  ∀f:A ⟶ 𝔹. ∀L:A List.`
`    (∀a∈L.∃L1,L2:A List. (((L = (L1 @ L2) ∈ (A List)) ∧ (a ∈ L2) ∧ (∀b∈L2.↑f[b])) ∧ ¬↑f[last(L1)] supposing ¬↑null(L1)) `
`          supposing (∀b≥a∈L.↑f[b]))`

Definition: reduce2
`reduce2(f;k;i;as) ==  fix((λreduce2,i,as. case as of [] => k | a::as' => f a i (reduce2 (i + 1) as') esac)) i as`

Lemma: reduce2_wf
`∀[A,T:Type]. ∀[L:T List]. ∀[k:A]. ∀[i:ℕ]. ∀[f:T ⟶ {i..i + ||L||-} ⟶ A ⟶ A].  (reduce2(f;k;i;L) ∈ A)`

Lemma: reduce2_nil_lemma
`∀i,k,f:Top.  (reduce2(f;k;i;[]) ~ k)`

Lemma: reduce2_cons_lemma
`∀t,h,i,k,f:Top.  (reduce2(f;k;i;[h / t]) ~ f h i reduce2(f;k;i + 1;t))`

Lemma: reduce2_shift
`∀[A,T:Type]. ∀[L:T List]. ∀[k:A]. ∀[i:ℕ]. ∀[f:T ⟶ {i..i + ||L||-} ⟶ A ⟶ A].`
`  (reduce2(f;k;i;L) = reduce2(λx,i,l. (f x (i - 1) l);k;i + 1;L) ∈ A)`

Lemma: comb_for_reduce2_wf
`λA,T,L,k,i,f,z. reduce2(f;k;i;L) ∈ A:Type ⟶ T:Type ⟶ L:(T List) ⟶ k:A ⟶ i:ℕ ⟶ f:(T ⟶ {i..i + ||L||-} ⟶ A ⟶ A) ⟶\000C (↓True) ⟶ A`

Definition: filter2
`filter2(P;L) ==  reduce2(λx,i,l. if P i then [x / l] else l fi ;[];0;L)`

Lemma: filter2_wf
`∀[T:Type]. ∀[L:T List]. ∀[P:ℕ||L|| ⟶ 𝔹].  (filter2(P;L) ∈ T List)`

Lemma: cons_filter2
`∀[T:Type]. ∀[x:T]. ∀[L:T List]. ∀[P:ℕ||L|| + 1 ⟶ 𝔹].`
`  (filter2(P;[x / L]) = if P 0 then [x / filter2(λi.(P (i + 1));L)] else filter2(λi.(P (i + 1));L) fi  ∈ (T List))`

Lemma: filter2_nil_lemma
`∀P:Top. (filter2(P;[]) ~ [])`

Lemma: filter_filter2
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].  (filter(P;L) = filter2(λi.(P L[i]);L) ∈ (T List))`

Lemma: member_filter2
`∀[T:Type]. ∀L:T List. ∀P:ℕ||L|| ⟶ 𝔹. ∀x:T.  ((x ∈ filter2(P;L)) `⇐⇒` ∃i:ℕ||L||. ((x = L[i] ∈ T) ∧ (↑(P i))))`

Lemma: filter2_functionality
`∀[A:Type]. ∀[L:A List]. ∀[f1,f2:ℕ||L|| ⟶ 𝔹].`
`  filter2(f2;L) = filter2(f1;L) ∈ (A List) supposing f1 = f2 ∈ (ℕ||L|| ⟶ 𝔹)`

Lemma: filter_of_filter2
`∀[T:Type]. ∀[L:T List]. ∀[P:ℕ||L|| ⟶ 𝔹]. ∀[Q:T ⟶ 𝔹].`
`  (filter(Q;filter2(P;L)) = filter2(λi.((P i) ∧b (Q L[i]));L) ∈ (T List))`

Definition: sublist_occurence
`sublist_occurence(T;L1;L2;f) ==  increasing(f;||L1||) ∧ (∀j:ℕ||L1||. (L1[j] = L2[f j] ∈ T))`

Lemma: sublist_occurence_wf
`∀[T:Type]. ∀[L1,L2:T List]. ∀[f:ℕ||L1|| ⟶ ℕ||L2||].  (sublist_occurence(T;L1;L2;f) ∈ ℙ)`

Lemma: range_sublist
`∀[T:Type]`
`  ∀L:T List. ∀n:ℕ. ∀f:ℕn ⟶ ℕ||L||.`
`    ∃L1:T List. ((||L1|| = n ∈ ℤ) c∧ sublist_occurence(T;L1;L;f)) supposing increasing(f;n)`

Definition: disjoint_sublists
`disjoint_sublists(T;L1;L2;L) ==`
`  ∃f1:ℕ||L1|| ⟶ ℕ||L||`
`   ∃f2:ℕ||L2|| ⟶ ℕ||L||`
`    ((increasing(f1;||L1||) ∧ (∀j:ℕ||L1||. (L1[j] = L[f1 j] ∈ T)))`
`    ∧ (increasing(f2;||L2||) ∧ (∀j:ℕ||L2||. (L2[j] = L[f2 j] ∈ T)))`
`    ∧ (∀j1:ℕ||L1||. ∀j2:ℕ||L2||.  (¬((f1 j1) = (f2 j2) ∈ ℤ))))`

Lemma: disjoint_sublists_wf
`∀[T:Type]. ∀[L1,L2,L:T List].  (disjoint_sublists(T;L1;L2;L) ∈ ℙ)`

Lemma: disjoint_sublists_sublist
`∀[T:Type]. ∀L1,L2,L:T List.  (disjoint_sublists(T;L1;L2;L) `` {L1 ⊆ L ∧ L2 ⊆ L})`

Lemma: disjoint_sublists_witness
`∀[T:Type]`
`  ∀L1,L2,L:T List.`
`    (disjoint_sublists(T;L1;L2;L)`
`    `` (∃f:ℕ||L1|| + ||L2|| ⟶ ℕ||L||`
`         (Inj(ℕ||L1|| + ||L2||;ℕ||L||;f)`
`         ∧ (∀i:ℕ||L1|| + ||L2||`
`              (L1[i] = L[f i] ∈ T supposing i < ||L1|| ∧ L2[i - ||L1||] = L[f i] ∈ T supposing ||L1|| ≤ i)))))`

Lemma: length_disjoint_sublists
`∀[T:Type]. ∀[L1,L2,L:T List].  (||L1|| + ||L2||) ≤ ||L|| supposing disjoint_sublists(T;L1;L2;L)`

Definition: interleaving
`interleaving(T;L1;L2;L) ==  (||L|| = (||L1|| + ||L2||) ∈ ℕ) ∧ disjoint_sublists(T;L1;L2;L)`

Lemma: interleaving_wf
`∀[T:Type]. ∀[L1,L2,L:T List].  (interleaving(T;L1;L2;L) ∈ ℙ)`

Lemma: l_before_interleaving
`∀[T:Type]. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `` {∀x,y:T.  (x before y ∈ L1 `` x before y ∈ L)})`

Lemma: nil_interleaving
`∀[T:Type]. ∀L1,L:T List.  (interleaving(T;[];L1;L) `⇐⇒` L = L1 ∈ (T List))`

Lemma: nil_interleaving2
`∀[T:Type]. ∀L1,L:T List.  (interleaving(T;L1;[];L) `⇐⇒` L = L1 ∈ (T List))`

Lemma: member_interleaving
`∀[T:Type]. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `` {∀x:T. ((x ∈ L) `⇐⇒` (x ∈ L1) ∨ (x ∈ L2))})`

Lemma: cons_interleaving
`∀[T:Type]. ∀x:T. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `` interleaving(T;[x / L1];L2;[x / L]))`

Lemma: comb_for_interleaving_wf
`λT,L1,L2,L,z. interleaving(T;L1;L2;L) ∈ T:Type ⟶ L1:(T List) ⟶ L2:(T List) ⟶ L:(T List) ⟶ (↓True) ⟶ ℙ`

Lemma: length_interleaving
`∀[T:Type]. ∀[L,L1,L2:T List].  ||L|| = (||L1|| + ||L2||) ∈ ℕ supposing interleaving(T;L1;L2;L)`

Lemma: interleaving_of_nil
`∀[T:Type]. ∀L1,L2:T List.  (interleaving(T;L1;L2;[]) `⇐⇒` (L1 = [] ∈ (T List)) ∧ (L2 = [] ∈ (T List)))`

Lemma: interleaving_symmetry
`∀[T:Type]. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `⇐⇒` interleaving(T;L2;L1;L))`

Lemma: cons_interleaving2
`∀[T:Type]. ∀x:T. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `` interleaving(T;L1;[x / L2];[x / L]))`

Lemma: interleaving_of_cons
`∀[T:Type]`
`  ∀x:T. ∀L,L1,L2:T List.`
`    (interleaving(T;L1;L2;[x / L])`
`    `⇐⇒` (0 < ||L1|| c∧ ((L1[0] = x ∈ T) ∧ interleaving(T;tl(L1);L2;L)))`
`        ∨ (0 < ||L2|| c∧ ((L2[0] = x ∈ T) ∧ interleaving(T;L1;tl(L2);L))))`

Lemma: interleaving_filter2
`∀[T:Type]`
`  ∀L,L1,L2:T List.`
`    (interleaving(T;L1;L2;L)`
`    `⇐⇒` ∃P:ℕ||L|| ⟶ 𝔹. ((L1 = filter2(P;L) ∈ (T List)) ∧ (L2 = filter2(λi.(¬b(P i));L) ∈ (T List))))`

Lemma: filter_interleaving
`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `` interleaving(T;filter(P;L1);filter(P;L2);filter(P;L)))`

Lemma: interleaving_as_filter
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L,L1,L2:T List].`
`  ({(L2 = filter(P;L) ∈ (T List)) ∧ (L1 = filter(λx.(¬b(P x));L) ∈ (T List))}) supposing `
`     ((∀x∈L1.¬↑(P x)) and `
`     (∀x∈L2.↑(P x)) and `
`     interleaving(T;L1;L2;L))`

Lemma: interleaving_as_filter_2
`∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L,L1,L2:T List].`
`  ({(L2 = filter(P;L) ∈ (T List)) ∧ (L1 = filter(λx.(¬b(P x));L) ∈ (T List))}) supposing `
`     ((filter(P;L1) = [] ∈ (T List)) and `
`     (L2 = filter(P;L2) ∈ (T List)) and `
`     interleaving(T;L1;L2;L))`

Lemma: sublist_interleaved
`∀[T:Type]. ∀L,L1:T List.  (L1 ⊆ L `` (∃L2:T List. interleaving(T;L1;L2;L)))`

Lemma: interleaved_split
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:T ⟶ ℙ]`
`      ((∀x:T. Dec(P[x]))`
`      `` (∃L1,L2:T List`
`           (interleaving(T;L1;L2;L)`
`           ∧ (∀x:T. ((x ∈ L1) `⇐⇒` (x ∈ L) ∧ P[x]))`
`           ∧ (∀x:T. ((x ∈ L2) `⇐⇒` (x ∈ L) ∧ (¬P[x]))))))`

Lemma: interleaving_sublist
`∀[T:Type]. ∀L,L1,L2:T List.  (interleaving(T;L1;L2;L) `` L1 ⊆ L)`

Lemma: append_interleaving
`∀[T:Type]. ∀L1,L2:T List.  interleaving(T;L1;L2;L1 @ L2)`

Definition: interleaving_occurence
`interleaving_occurence(T;L1;L2;L;f1;f2) ==`
`  (||L|| = (||L1|| + ||L2||) ∈ ℕ)`
`  ∧ (increasing(f1;||L1||) ∧ (∀j:ℕ||L1||. (L1[j] = L[f1 j] ∈ T)))`
`  ∧ (increasing(f2;||L2||) ∧ (∀j:ℕ||L2||. (L2[j] = L[f2 j] ∈ T)))`
`  ∧ (∀j1:ℕ||L1||. ∀j2:ℕ||L2||.  (¬((f1 j1) = (f2 j2) ∈ ℤ)))`

Lemma: interleaving_occurence_wf
`∀[T:Type]. ∀[L1,L2,L:T List]. ∀[f1:ℕ||L1|| ⟶ ℕ||L||]. ∀[f2:ℕ||L2|| ⟶ ℕ||L||].`
`  (interleaving_occurence(T;L1;L2;L;f1;f2) ∈ ℙ)`

Lemma: interleaving_implies_occurence
`∀[T:Type]`
`  ∀L1,L2,L:T List.`
`    (interleaving(T;L1;L2;L) `` (∃f1:ℕ||L1|| ⟶ ℕ||L||. ∃f2:ℕ||L2|| ⟶ ℕ||L||. interleaving_occurence(T;L1;L2;L;f1;f2)))`

Lemma: interleaving_occurence_onto
`∀[A:Type]`
`  ∀L,L1,L2:A List. ∀f1:ℕ||L1|| ⟶ ℕ||L||. ∀f2:ℕ||L2|| ⟶ ℕ||L||.`
`    ∀j:ℕ||L||. ((∃k:ℕ||L1||. (j = (f1 k) ∈ ℤ)) ∨ (∃k:ℕ||L2||. (j = (f2 k) ∈ ℤ))) `
`    supposing interleaving_occurence(A;L1;L2;L;f1;f2)`

Lemma: interleaving_split
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:ℕ||L|| ⟶ ℙ]`
`      ((∀x:ℕ||L||. Dec(P x))`
`      `` (∃L1,L2:T List`
`           ∃f1:ℕ||L1|| ⟶ ℕ||L||`
`            ∃f2:ℕ||L2|| ⟶ ℕ||L||`
`             (interleaving_occurence(T;L1;L2;L;f1;f2)`
`             ∧ ((∀i:ℕ||L1||. (P (f1 i))) ∧ (∀i:ℕ||L2||. (¬(P (f2 i)))))`
`             ∧ (∀i:ℕ||L||`
`                  (((P i) `` (∃j:ℕ||L1||. ((f1 j) = i ∈ ℤ))) ∧ ∃j:ℕ||L2||. ((f2 j) = i ∈ ℤ) supposing ¬(P i))))))`

Lemma: interleaving_singleton
`∀[T:Type]`
`  ∀L:T List. ∀i:ℕ||L||.`
`    ∃L2:T List`
`     ∃f1:ℕ1 ⟶ ℕ||L||. ∃f2:ℕ||L2|| ⟶ ℕ||L||. (interleaving_occurence(T;[L[i]];L2;L;f1;f2) ∧ ((f1 0) = i ∈ ℤ))`

Lemma: last_with_property
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P:ℕ||L|| ⟶ ℙ]`
`      ((∀x:ℕ||L||. Dec(P x)) `` (∃i:ℕ||L||. (P i)) `` (∃i:ℕ||L||. ((P i) ∧ (∀j:ℕ||L||. ¬(P j) supposing i < j))))`

Lemma: occurence_implies_interleaving
`∀[T:Type]`
`  ∀L1,L2,L:T List. ∀f1:ℕ||L1|| ⟶ ℕ||L||. ∀f2:ℕ||L2|| ⟶ ℕ||L||.`
`    interleaving(T;L1;L2;L) supposing interleaving_occurence(T;L1;L2;L;f1;f2)`

Lemma: filter_is_interleaving
`∀[T:Type]. ∀P:T ⟶ 𝔹. ∀L:T List.  interleaving(T;filter(λx.(¬b(P x));L);filter(P;L);L)`

Lemma: filter_interleaving_occurence
`∀[T:Type]`
`  ∀P:T ⟶ 𝔹. ∀L:T List.`
`    ∃f1:ℕ||filter(λx.(¬b(P x));L)|| ⟶ ℕ||L||`
`     ∃f2:ℕ||filter(P;L)|| ⟶ ℕ||L||`
`      (interleaving_occurence(T;filter(λx.(¬b(P x));L);filter(P;L);L;f1;f2)`
`      ∧ ((∀i:ℕ||L||. ∃k:ℕ||filter(P;L)||. ((i = (f2 k) ∈ ℤ) ∧ (L[i] = filter(P;L)[k] ∈ T)) supposing ↑(P L[i]))`
`        ∧ (∀i:ℕ||L||`
`             ∃k:ℕ||filter(λx.(¬b(P x));L)||. ((i = (f1 k) ∈ ℤ) ∧ (L[i] = filter(λx.(¬b(P x));L)[k] ∈ T)) `
`             supposing ¬↑(P L[i])))`
`      ∧ (∀i:ℕ||filter(λx.(¬b(P x));L)||. (¬↑(P L[f1 i])))`
`      ∧ (∀i:ℕ||filter(P;L)||. (↑(P L[f2 i]))))`

Definition: causal_order
`causal_order(L;R;P;Q) ==  ∀i:ℕ||L||. ((Q i) `` (∃j:ℕ||L||. (((j ≤ i) ∧ (P j)) ∧ (R j i))))`

Lemma: causal_order_wf
`∀[T:Type]. ∀[L:T List]. ∀[P,Q:ℕ||L|| ⟶ ℙ]. ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ].  (causal_order(L;R;P;Q) ∈ ℙ)`

Lemma: causal_order_filter_iseg
`∀[T,T':Type].`
`  ∀L:T List. ∀P,Q:ℕ||L|| ⟶ 𝔹. ∀f,g:T ⟶ T'.`
`    ((∀L':T List. (L' ≤ L `` map(f;filter2(P;L')) ≤ map(g;filter2(Q;L'))))`
`    `` causal_order(L;λi,j. ((g L[i]) = (f L[j]) ∈ T');λi.(↑Q[i]);λi.(↑P[i])))`

Lemma: causal_order_transitivity
`∀[T:Type]`
`  ∀L:T List`
`    ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ]. ∀[P1,P2,P3:ℕ||L|| ⟶ ℙ].`
`      (Trans(ℕ||L||)(R _1 _2) `` causal_order(L;R;P1;P2) `` causal_order(L;R;P2;P3) `` causal_order(L;R;P1;P3))`

Lemma: causal_order_reflexive
`∀[T:Type]. ∀L:T List. ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ]. ∀[P:ℕ||L|| ⟶ ℙ].  (Refl(ℕ||L||)(R _1 _2) `` causal_order(L;R;P;P))`

Lemma: causal_order_or
`∀[T:Type]`
`  ∀L:T List`
`    ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ]. ∀[P1,P2,P3:ℕ||L|| ⟶ ℙ].`
`      (Trans(ℕ||L||)(R _1 _2)`
`      `` causal_order(L;R;P1;P2)`
`      `` causal_order(L;R;P1;P3)`
`      `` causal_order(L;R;P1;λi.((P2 i) ∨ (P3 i))))`

Lemma: causal_order_sigma
`∀[T,A:Type].`
`  ∀L:T List`
`    ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ]. ∀[P,Q:A ⟶ ℕ||L|| ⟶ ℙ].`
`      (Trans(ℕ||L||)(R _1 _2)`
`      `` (∀x:A. causal_order(L;R;λi.P[x;i];λi.Q[x;i]))`
`      `` causal_order(L;R;λi.∃x:A. P[x;i];λi.∃x:A. Q[x;i]))`

Lemma: causal_order_monotonic
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P,Q1,Q2:ℕ||L|| ⟶ ℙ]. ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ].`
`      ((∀i:ℕ||L||. ((Q2 i) `` (Q1 i))) `` causal_order(L;R;P;Q1) `` causal_order(L;R;P;Q2))`

Lemma: causal_order_monotonic2
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P1,P2,Q:ℕ||L|| ⟶ ℙ]. ∀[R:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ].`
`      ((∀i:ℕ||L||. ((P1 i) `` (P2 i))) `` causal_order(L;R;P1;Q) `` causal_order(L;R;P2;Q))`

Lemma: causal_order_monotonic3
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P1,P2,Q1,Q2:ℕ||L|| ⟶ ℙ]. ∀[R1,R2:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ].`
`      ((∀i:ℕ||L||. ((P1 i) `` (P2 i)))`
`      `` (∀i:ℕ||L||. ((Q2 i) `` (Q1 i)))`
`      `` (∀i,j:ℕ||L||.  ((R1 i j) `` (R2 i j)))`
`      `` causal_order(L;R1;P1;Q1)`
`      `` causal_order(L;R2;P2;Q2))`

Lemma: causal_order_monotonic4
`∀[T:Type]`
`  ∀L:T List`
`    ∀[P1,P2,Q:ℕ||L|| ⟶ ℙ]. ∀[R1,R2:ℕ||L|| ⟶ ℕ||L|| ⟶ ℙ].`
`      ((∀i:ℕ||L||. ((P1 i) `` (P2 i)))`
`      `` (∀x,y:ℕ||L||.  ((R1 x y) `` (R2 x y)))`
`      `` causal_order(L;R1;P1;Q)`
`      `` causal_order(L;R2;P2;Q))`

Definition: interleaved_family_occurence
`interleaved_family_occurence(T;I;L;L2;f) ==`
`  ((∀i:I. (increasing(f i;||L i||) ∧ (∀j:ℕ||L i||. (L i[j] = L2[f i j] ∈ T))))`
`  ∧ (∀i1,i2:I.  ((¬(i1 = i2 ∈ I)) `` (∀j1:ℕ||L i1||. ∀j2:ℕ||L i2||.  (¬((f i1 j1) = (f i2 j2) ∈ ℤ))))))`
`  ∧ (∀x:ℕ||L2||. ∃i:I. ∃j:ℕ||L i||. (x = (f i j) ∈ ℤ))`

Lemma: interleaved_family_occurence_wf
`∀[T,I:Type]. ∀[L:I ⟶ (T List)]. ∀[L2:T List]. ∀[f:i:I ⟶ ℕ||L i|| ⟶ ℕ||L2||].`
`  (interleaved_family_occurence(T;I;L;L2;f) ∈ ℙ)`

Definition: interleaved_family
`interleaved_family(T;I;L;L2) ==  ∃f:i:I ⟶ ℕ||L i|| ⟶ ℕ||L2||. interleaved_family_occurence(T;I;L;L2;f)`

Lemma: interleaved_family_wf
`∀[T,I:Type]. ∀[L:I ⟶ (T List)]. ∀[L2:T List].  (interleaved_family(T;I;L;L2) ∈ ℙ)`

Definition: swap
`swap(L;i;j) ==  (L o (i, j))`

Lemma: swap_wf
`∀[T:Type]. ∀[L:T List]. ∀[i,j:ℕ||L||].  (swap(L;i;j) ∈ T List)`

Lemma: swap_select
`∀[T:Type]. ∀[L:T List]. ∀[i,j,x:ℕ||L||].  (swap(L;i;j)[x] = L[(i, j) x] ∈ T)`

Lemma: swap_length
`∀[T:Type]. ∀[L:T List]. ∀[i,j:ℕ||L||].  (||swap(L;i;j)|| = ||L|| ∈ ℤ)`

Lemma: swap_swap
`∀[T:Type]. ∀[L1:T List]. ∀[i,j:ℕ||L1||].  (swap(swap(L1;i;j);i;j) = L1 ∈ (T List))`

Lemma: swapped_select
`∀[T:Type]. ∀[L1,L2:T List]. ∀[i,j:ℕ||L1||].`
`  {(((L2[i] = L1[j] ∈ T) ∧ (L2[j] = L1[i] ∈ T)) ∧ (||L2|| = ||L1|| ∈ ℤ) ∧ (L1 = swap(L2;i;j) ∈ (T List)))`
`  ∧ (∀[x:ℕ||L2||]. (L2[x] = L1[x] ∈ T) supposing ((¬(x = j ∈ ℤ)) and (¬(x = i ∈ ℤ))))} `
`  supposing L2 = swap(L1;i;j) ∈ (T List)`

Lemma: swap_cons
`∀[T:Type]. ∀[L:T List]. ∀[x:T]. ∀[i,j:ℕ+||L|| + 1].  (swap([x / L];i;j) = [x / swap(L;i - 1;j - 1)] ∈ (T List))`

`∀[A:Type]`
`  ∀i:ℕ. ∀L:A List.`
`    ∃X,Y:A List`
`     ((L = (X @ [L[i]; L[i + 1]] @ Y) ∈ (A List)) ∧ (swap(L;i;i + 1) = (X @ [L[i + 1]; L[i]] @ Y) ∈ (A List))) `
`    supposing i + 1 < ||L||`

Lemma: l_before_swap
`∀[T:Type]`
`  ∀L:T List. ∀i:ℕ||L|| - 1. ∀a,b:T.`
`    (a before b ∈ swap(L;i;i + 1) `` (a before b ∈ L ∨ ((a = L[i + 1] ∈ T) ∧ (b = L[i] ∈ T))))`

Lemma: map_permute_list
`∀[A,B:Type]. ∀[f:B ⟶ A]. ∀[x:B List]. ∀[g:ℕ||x|| ⟶ ℕ||x||].  (map(f;(x o g)) = (map(f;x) o g) ∈ (A List))`

Lemma: map_swap
`∀[A,B:Type]. ∀[f:B ⟶ A]. ∀[x:B List]. ∀[i,j:ℕ||x||].  (map(f;swap(x;i;j)) = swap(map(f;x);i;j) ∈ (A List))`

Lemma: comb_for_swap_wf
`λT,L,i,j,z. swap(L;i;j) ∈ T:Type ⟶ L:(T List) ⟶ i:ℕ||L|| ⟶ j:ℕ||L|| ⟶ (↓True) ⟶ (T List)`

Definition: guarded_permutation
`guarded_permutation(T;P) ==  (λL1,L2. ∃i:ℕ||L1|| - 1. ((P L1 i) ∧ (L2 = swap(L1;i;i + 1) ∈ (T List))))^*`

Lemma: guarded_permutation_wf
`∀[T:Type]. ∀[P:L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℙ].  (guarded_permutation(T;P) ∈ (T List) ⟶ (T List) ⟶ ℙ)`

Lemma: guarded_permutation_transitivity
`∀[T:Type]. ∀[P:L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℙ].  Trans(T List)(_1 guarded_permutation(T;P) _2)`

Definition: count_index_pairs
`count(i<j<||L|| : P L i j) ==  sum(if i <z j ∧b (P L i j) then 1 else 0 fi  | i < ||L||; j < ||L||)`

Lemma: count_index_pairs_wf
`∀[T:Type]. ∀[P:L:(T List) ⟶ ℕ||L|| - 1 ⟶ ℕ||L|| ⟶ 𝔹]. ∀[L:T List].  (count(i<j<||L|| : P L i j) ∈ ℕ)`

Definition: count_pairs
`count(x < y in L | P[x; y]) ==  sum(if i <z j ∧b P[L[i]; L[j]] then 1 else 0 fi  | i < ||L||; j < ||L||)`

Lemma: count_pairs_wf
`∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ T ⟶ 𝔹].  (count(x < y in L | P[x;y]) ∈ ℕ)`

Definition: first_index
`index-of-first x in L.P[x] ==  search(||L||;λi.P[L[i]])`

Lemma: first_index_wf
`∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  (index-of-first x in L.P[x] ∈ ℕ)`

Lemma: first_index_cons
`∀[T:Type]. ∀[L:T List]. ∀[a:T]. ∀[P:T ⟶ 𝔹].`
`  (index-of-first x in [a / L].P[x] ~ if P[a] then 1`
`  if 0 <z index-of-first x in L.P[x] then index-of-first x in L.P[x] + 1`
`  else 0`
`  fi )`

Definition: agree_on
`agree_on(T;x.P[x]) ==  λL1,L2. ((||L1|| = ||L2|| ∈ ℤ) c∧ (∀i:ℕ||L1||. ((P[L1[i]] ∨ P[L2[i]]) `` (L1[i] = L2[i] ∈ T))))`

Lemma: agree_on_wf
`∀[T:Type]. ∀[P:T ⟶ ℙ].  (agree_on(T;a.P[a]) ∈ (T List) ⟶ (T List) ⟶ ℙ)`

Lemma: first_index_equal
`∀[T:Type]. ∀[L1,L2:T List]. ∀[P,Q:T ⟶ 𝔹].`
`  index-of-first a in L1.P[a] ∧b Q[a] = index-of-first a in L2.P[a] ∧b Q[a] ∈ ℤ supposing L1 agree_on(T;a.↑P[a]) L2`

Lemma: iseg_map
`∀[A,B:Type].  ∀f:A ⟶ B. ∀L1,L2:A List.  (L1 ≤ L2 `` map(f;L1) ≤ map(f;L2))`

Lemma: safety_induced
`∀[A,B:Type].  ∀f:A ⟶ B. ∀[P:(B List) ⟶ ℙ]. (safety(B;L.P[L]) `` safety(A;L.P[map(f;L)]))`

Lemma: agree_on_equiv
`∀[T:Type]. ∀[P:T ⟶ ℙ].  EquivRel(T List)(_1 agree_on(T;a.P[a]) _2)`

Definition: strong_safety
`strong_safety(T;tr.P[tr]) ==  ∀tr1,tr2:T List.  (tr1 ⊆ tr2 `` P[tr2] `` P[tr1])`

Lemma: strong_safety_wf
`∀[A:Type]. ∀[P:(A List) ⟶ ℙ].  (strong_safety(A;x.P[x]) ∈ ℙ)`

Lemma: filter_strong_safety
`∀[T:Type]. ∀[P:(T List) ⟶ ℙ].  ∀f:T ⟶ 𝔹. (strong_safety(T;L.P L) `` strong_safety(T;L.P filter(f;L)))`

Lemma: strong_safety_safety
`∀[A:Type]. ∀[P:(A List) ⟶ ℙ].  (strong_safety(A;x.P[x]) `` safety(A;x.P[x]))`

Definition: sublist*
`sublist*(T;as;bs) ==  ∀cs:T List. (cs ⊆ as `` l_subset(T;cs;bs) `` cs ⊆ bs)`

Lemma: sublist*_wf
`∀[T:Type]. ∀[as,bs:T List].  (sublist*(T;as;bs) ∈ ℙ)`

Lemma: sublist*_filter
`∀[T:Type]. ∀P:T ⟶ 𝔹. ∀as,bs:T List.  (sublist*(T;as;bs) `` sublist*(T;filter(P;as);filter(P;bs)))`

Lemma: list-decomp-no_repeats
`∀[T:Type]. ∀[l1,l2,l3,l4:T List]. ∀[x:T].`
`  ((l1 = l3 ∈ (T List)) ∧ (l2 = l4 ∈ (T List))) supposing `
`     ((((l1 @ [x]) @ l2) = ((l3 @ [x]) @ l4) ∈ (T List)) and `
`     no_repeats(T;(l1 @ [x]) @ l2))`

Home Index