---

Step * 1 of Lemma last_index_property


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 ∈ ℤ
BY
{ TACTIC:(RepUR ``last_index`` 0 THEN Auto) }

1
1. T : Type
2. P : T ⟶ 𝔹
3. (↑P[⊥]) ∧ (¬(∃x∈[]. ↑P[x])) supposing 0 < 0
4. 0 = 0 ∈ ℤ
⊢ ¬(∃x∈[]. ↑P[x])

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:(RepUR  ``last\_index``  0  THEN  Auto)

---

Home Index