---

Step * 1 1 1 1 of Lemma length-remove-first


1. T : Type
2. P : T ⟶ 𝔹
3. L : T List
4. (∃x∈L. ↑(P x))
5. (∃x∈L. ↑(P x))
⊢ ||remove-first(P;L)|| = (||L|| - 1) ∈ ℤ
BY
{ TACTIC:(Thin (-1) THEN Unfold `remove-first` 0 THEN ListInd (-2) THEN Reduce 0 THEN Auto) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. (∃x∈[]. ↑(P x))
⊢ 0 = (-1) ∈ ℤ

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. (∃x∈v. ↑(P x)) ⇒ (||rec-case(v) of [] => [] | a::as => r.if P a then as else [a / r] fi || = (||v|| - 1) ∈ ℤ)
6. (∃x∈[u / v]. ↑(P x))
⊢ ||if P u then v else [u / rec-case(v) of [] => [] | h::t => r.if P h then t else [h / r] fi ] fi ||
= ((||v|| + 1) - 1)
∈ ℤ

---

Latex:

---

Latex:

1.  T  :  Type
2.  P  :  T  {}\mrightarrow{}  \mBbbB{}
3.  L  :  T  List
4.  (\mexists{}x\mmember{}L.  \muparrow{}(P  x))
5.  (\mexists{}x\mmember{}L.  \muparrow{}(P  x))
\mvdash{}  ||remove-first(P;L)||  =  (||L||  -  1)


By

---

Latex:
TACTIC:(Thin  (-1)  THEN  Unfold  `remove-first`  0  THEN  ListInd  (-2)  THEN  Reduce  0  THEN  Auto)

---

Home Index