---

Step * 2 of Lemma last_index_property


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 ∈ ℤ
BY
{ TACTIC:((InstLemma `last_index_cons` [⌜T⌝;⌜P⌝;⌜v⌝;⌜u⌝]⋅ THENA Auto)
          THEN HypSubst' (-1) 0
          THEN (BoolCase ⌜0 <z last_index(v;x.P[x])⌝⋅ THENA Auto)
          THEN ThinTrivial) }

1
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 ∈ ℤ
6. last_index([u / v];x.P[x]) = if 0 <z last_index(v;x.P[x]) then 1 + last_index(v;x.P[x]) if P[u] then 1 else 0 fi  ∈ ℤ
7. 0 < last_index(v;x.P[x])
⊢ (↑P[[u / v][(1 + last_index(v;x.P[x])) - 1]]) ∧ (¬(∃x∈nth_tl(1 + last_index(v;x.P[x]);[u / v]). ↑P[x])) 
  supposing 0 < 1 + last_index(v;x.P[x])
∧ ¬(∃x∈[u / v]. ↑P[x]) supposing (1 + last_index(v;x.P[x])) = 0 ∈ ℤ

2
1. T : Type
2. P : T ⟶ 𝔹
3. u : T
4. v : T List
5. ¬0 < last_index(v;x.P[x])
6. (↑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 ∈ ℤ
7. last_index([u / v];x.P[x]) = if P[u] then 1 else 0 fi  ∈ ℤ
⊢ (↑P[[u / v][if P[u] then 1 else 0 fi  - 1]]) ∧ (¬(∃x∈nth_tl(if P[u] then 1 else 0 fi ;[u / v]). ↑P[x])) 
  supposing 0 < if P[u] then 1 else 0 fi 
∧ ¬(∃x∈[u / v]. ↑P[x]) supposing if P[u] then 1 else 0 fi  = 0 ∈ ℤ

---

Latex:

---

Latex:

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


By

---

Latex:
TACTIC:((InstLemma  `last\_index\_cons`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}P\mkleeneclose{};\mkleeneopen{}v\mkleeneclose{};\mkleeneopen{}u\mkleeneclose{}]\mcdot{}  THENA  Auto)
                THEN  HypSubst'  (-1)  0
                THEN  (BoolCase  \mkleeneopen{}0  <z  last\_index(v;x.P[x])\mkleeneclose{}\mcdot{}  THENA  Auto)
                THEN  ThinTrivial)

---

Home Index