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