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))
Lemma: swap_adjacent_decomp
∀[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