---

Step * 1 1 of Lemma find-maximal-consecutive_wf


1. T : Type
2. g : T ─→ ℤ
3. u : T
4. v : T List
⊢ ∀n,t:ℤ.
    (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:
           v
         with starting value:
          <n, t>)) ∈ {n..(||v|| + 1) + n-})
BY
{ (ListInd (-1) THEN Reduce 0) }

1
1. T : Type
2. g : T ─→ ℤ
3. u : T
⊢ ∀n,t:ℤ.  (n ∈ {n..1 + n-})

2
1. T : Type
2. g : T ─→ ℤ
3. u : T
4. u1 : T
5. v : T List
6. ∀n,t:ℤ.
     (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:
            v
          with starting value:
           <n, t>)) ∈ {n..(||v|| + 1) + n-})
⊢ ∀n,t:ℤ.
    (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:
           v
         with starting value:
          eval z = g u1 in
          if t + 1=z  then <n + 1, z>  else <n, t>)) ∈ {n..((||v|| + 1) + 1) + n-})

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  u  :  T
4.  v  :  T  List
\mvdash{}  \mforall{}n,t:\mBbbZ{}.
        (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:
                      v
                  with  starting  value:
                    <n,  t>))  \mmember{}  \{n..(||v||  +  1)  +  n\msupminus{}\})


By

---

Latex:
(ListInd  (-1)  THEN  Reduce  0)

---

Home Index