---

Step * of Lemma find-maximal-consecutive_wf

∀[T:Type]. ∀[g:T ⟶ ℤ]. ∀[L:T List+].  (find-maximal-consecutive(g;L) ∈ {1..||L|| + 1-})
BY
{ (Intros THEN Unhide THEN D -1 THEN Unfold `find-maximal-consecutive` 0) }

1
1. T : Type
2. g : T ⟶ ℤ
3. L : T List
4. ||L|| ≥ 1 
⊢ fst(accumulate (with value ix and list item y):
       eval z = g y in
       let i,x = ix 
       in if x + 1=z  then <i + 1, z>  else ix
      over list:
        tl(L)
      with starting value:
       <1, g hd(L)>)) ∈ {1..||L|| + 1-}

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[g:T  {}\mrightarrow{}  \mBbbZ{}].  \mforall{}[L:T  List\msupplus{}].    (find-maximal-consecutive(g;L)  \mmember{}  \{1..||L||  +  1\msupminus{}\})


By

---

Latex:
(Intros  THEN  Unhide  THEN  D  -1  THEN  Unfold  `find-maximal-consecutive`  0)

---

Home Index