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. T
3. 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