---

Step * 1 1 2 of Lemma find-maximal-consecutive_wf


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-})
BY
{ ((UnivCD THENA Auto) THEN (CallByValueReduceOn ⌈g u1⌉ 0⋅ THENA Auto) THEN AutoSplit) }

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  u  :  T
4.  u1  :  T
5.  v  :  T  List
6.  \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{}\})
\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:
                    eval  z  =  g  u1  in
                    if  t  +  1=z    then  <n  +  1,  z>    else  <n,  t>))  \mmember{}  \{n..((||v||  +  1)  +  1)  +  n\msupminus{}\})


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  (CallByValueReduceOn  \mkleeneopen{}g  u1\mkleeneclose{}  0\mcdot{}  THENA  Auto)  THEN  AutoSplit)

---

Home Index