---

Step * of Lemma last_index_wf

∀[T:Type]. ∀[L:T List]. ∀[P:T ⟶ 𝔹].  (last_index(L;x.P[x]) ∈ ℕ||L|| + 1)
BY
{ xxx(Intros
      THEN Unfold `last_index` 0
      THEN Unhide
      THEN GenConclAtAddrType ⌜n:ℕ||L|| + 1 × ℕn + 1⌝ [2;1]⋅
      THEN Try (CompleteAuto))xxx }

1
.....wf..... 
1. T : Type
2. L : T List
3. P : T ⟶ 𝔹
⊢ accumulate (with value p and list item x):
   let n,lst = p 
   in <n + 1, if P[x] then n + 1 else lst fi >
  over list:
    L
  with starting value:
   <0, 0>) ∈ n:ℕ||L|| + 1 × ℕn + 1

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[P:T  {}\mrightarrow{}  \mBbbB{}].    (last\_index(L;x.P[x])  \mmember{}  \mBbbN{}||L||  +  1)


By

---

Latex:
xxx(Intros
        THEN  Unfold  `last\_index`  0
        THEN  Unhide
        THEN  GenConclAtAddrType  \mkleeneopen{}n:\mBbbN{}||L||  +  1  \mtimes{}  \mBbbN{}n  +  1\mkleeneclose{}  [2;1]\mcdot{}
        THEN  Try  (CompleteAuto))xxx

---

Home Index