---

Step * of Lemma last_index_property

∀[T:Type]. ∀[P:T ⟶ 𝔹]. ∀[L:T List].
  ((↑P[L[last_index(L;x.P[x]) - 1]]) ∧ (¬(∃x∈nth_tl(last_index(L;x.P[x]);L). ↑P[x])) supposing 0 < last_index(L;x.P[x])
  ∧ ¬(∃x∈L. ↑P[x]) supposing last_index(L;x.P[x]) = 0 ∈ ℤ)
BY
{ TACTIC:InductionOnList }

1
1. T : Type
2. P : T ⟶ 𝔹
⊢ (↑P[[][last_index([];x.P[x]) - 1]]) ∧ (¬(∃x∈nth_tl(last_index([];x.P[x]);[]). ↑P[x])) 
  supposing 0 < last_index([];x.P[x])
∧ ¬(∃x∈[]. ↑P[x]) supposing last_index([];x.P[x]) = 0 ∈ ℤ

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. (↑P[v[last_index(v;x.P[x]) - 1]]) ∧ (¬(∃x∈nth_tl(last_index(v;x.P[x]);v). ↑P[x])) supposing 0 < last_index(v;x.P[x])
∧ ¬(∃x∈v. ↑P[x]) supposing last_index(v;x.P[x]) = 0 ∈ ℤ
⊢ (↑P[[u / v][last_index([u / v];x.P[x]) - 1]]) ∧ (¬(∃x∈nth_tl(last_index([u / v];x.P[x]);[u / v]). ↑P[x])) 
  supposing 0 < last_index([u / v];x.P[x])
∧ ¬(∃x∈[u / v]. ↑P[x]) supposing last_index([u / v];x.P[x]) = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[L:T  List].
    ((\muparrow{}P[L[last\_index(L;x.P[x])  -  1]])  \mwedge{}  (\mneg{}(\mexists{}x\mmember{}nth\_tl(last\_index(L;x.P[x]);L).  \muparrow{}P[x])) 
      supposing  0  <  last\_index(L;x.P[x])
    \mwedge{}  \mneg{}(\mexists{}x\mmember{}L.  \muparrow{}P[x])  supposing  last\_index(L;x.P[x])  =  0)


By

---

Latex:
TACTIC:InductionOnList

---

Home Index