---

Step * of 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))))
BY
{ InductionOnList }

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

2
1. [T] : Type
2. u : T
3. v : T List
4. ∀L1,L2:T List.
     (interleaving(T;L1;L2;v)
     ⇐⇒ ∃P:ℕ||v|| ⟶ 𝔹. ((L1 = filter2(P;v) ∈ (T List)) ∧ (L2 = filter2(λi.(¬b(P i));v) ∈ (T List))))
⊢ ∀L1,L2:T List.
    (interleaving(T;L1;L2;[u / v])
    ⇐⇒ ∃P:ℕ||[u / v]|| ⟶ 𝔹. ((L1 = filter2(P;[u / v]) ∈ (T List)) ∧ (L2 = filter2(λi.(¬b(P i));[u / v]) ∈ (T List))))

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}L,L1,L2:T  List.
        (interleaving(T;L1;L2;L)
        \mLeftarrow{}{}\mRightarrow{}  \mexists{}P:\mBbbN{}||L||  {}\mrightarrow{}  \mBbbB{}.  ((L1  =  filter2(P;L))  \mwedge{}  (L2  =  filter2(\mlambda{}i.(\mneg{}\msubb{}(P  i));L))))


By

---

Latex:
InductionOnList

---

Home Index