---

Step * 1 of Lemma find-maximal-consecutive_wf


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-}
BY
{ ((Assert ⌜∀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:
                     tl(L)
                   with starting value:
                    <n, t>)) ∈ {n..||L|| + n-})⌝⋅
   THENM (BHyp -1  THEN Auto)
   )
   THEN D -2
   THEN Reduce (-1)
   THEN Try (Complete (Auto))
   THEN Thin (-1)
   THEN Reduce 0) }

1
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-})

---

Latex:

---

Latex:

1.  T  :  Type
2.  g  :  T  {}\mrightarrow{}  \mBbbZ{}
3.  L  :  T  List
4.  ||L||  \mgeq{}  1 
\mvdash{}  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:
              ə,  g  hd(L)>))  \mmember{}  \{1..||L||  +  1\msupminus{}\}


By

---

Latex:
((Assert  \mkleeneopen{}\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:
                                      tl(L)
                                  with  starting  value:
                                    <n,  t>))  \mmember{}  \{n..||L||  +  n\msupminus{}\})\mkleeneclose{}\mcdot{}
  THENM  (BHyp  -1    THEN  Auto)
  )
  THEN  D  -2
  THEN  Reduce  (-1)
  THEN  Try  (Complete  (Auto))
  THEN  Thin  (-1)
  THEN  Reduce  0)

---

Home Index