---

Step * 1 of Lemma last_index_wf

.....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
BY
{ xxx((Assert ⌜∀n:ℕ. ∀m:ℕn + 1.
                 (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:
                   <n, m>) ∈ k:{n..n + ||L|| + 1-} × ℕk + 1)⌝⋅
       THENA (ListInd 2 THEN Reduce 0 THEN Auto)
       )
THENM (InstHyp [⌜0⌝;⌜0⌝] (-1)⋅ THEN Auto)
)xxx }

---

Latex:

---

Latex:
.....wf..... 
1.  T  :  Type
2.  L  :  T  List
3.  P  :  T  {}\mrightarrow{}  \mBbbB{}
\mvdash{}  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>)  \mmember{}  n:\mBbbN{}||L||  +  1  \mtimes{}  \mBbbN{}n  +  1


By

---

Latex:
xxx((Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}m:\mBbbN{}n  +  1.
                              (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:
                                  <n,  m>)  \mmember{}  k:\{n..n  +  ||L||  +  1\msupminus{}\}  \mtimes{}  \mBbbN{}k  +  1)\mkleeneclose{}\mcdot{}
          THENA  (ListInd  2  THEN  Reduce  0  THEN  Auto)
          )
THENM  (InstHyp  [\mkleeneopen{}0\mkleeneclose{};\mkleeneopen{}0\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto)
)xxx

---

Home Index