---

Step * 2 of Lemma cons_filter2

.....falsecase..... 
1. T : Type
2. x : T
3. L : T List
4. P : ℕ||L|| + 1 ⟶ 𝔹
5. ¬↑(P 0)
⊢ reduce2(λx,i,l. if P i then [x / l] else l fi ;[];1;L) = filter2(λi.(P (i + 1));L) ∈ (T List)
BY
{ (Unfold `filter2` 0 THEN Symmetry) }

1
1. T : Type
2. x : T
3. L : T List
4. P : ℕ||L|| + 1 ⟶ 𝔹
5. ¬↑(P 0)
⊢ reduce2(λx,i,l. if (λi.(P (i + 1))) i then [x / l] else l fi ;[];0;L)
= reduce2(λx,i,l. if P i then [x / l] else l fi ;[];1;L)
∈ (T List)

---

Latex:

---

Latex:
.....falsecase..... 
1.  T  :  Type
2.  x  :  T
3.  L  :  T  List
4.  P  :  \mBbbN{}||L||  +  1  {}\mrightarrow{}  \mBbbB{}
5.  \mneg{}\muparrow{}(P  0)
\mvdash{}  reduce2(\mlambda{}x,i,l.  if  P  i  then  [x  /  l]  else  l  fi  ;[];1;L)  =  filter2(\mlambda{}i.(P  (i  +  1));L)


By

---

Latex:
(Unfold  `filter2`  0  THEN  Symmetry)

---

Home Index