---

Step * of Lemma split-at-first-gap-ext

∀[T:Type]
  ∀f:T ⟶ ℤ. ∀L:T List.
    (∃XY:T List × (T List) [let X,Y = XY 
                            in (L = (X @ Y) ∈ (T List))
                               ∧ (∀i:ℕ||X|| - 1. ((f X[i + 1]) = ((f X[i]) + 1) ∈ ℤ))
                               ∧ ((¬↑null(L))
                                 ⇒ ((¬↑null(X)) ∧ ¬((f hd(Y)) = ((f last(X)) + 1) ∈ ℤ) supposing ||Y|| ≥ 1 ))])
BY
{ Extract of Obid: split-at-first-gap
  not unfolding  list_ind
  finishing with Auto
  normalizes to:
  
  λf,L. rec-case(L) of
        [] => <Ax, Ax>
        a::L =>
         r.if L = Ax then <<a, Ax>, Ax> otherwise let u1,v1 = L 
                                   in if f u1=(f a) + 1 then let X1,X2 = r in <<a, X1>, X2> else <<a, Ax>, u1, v1> }

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:T  List.
        (\mexists{}XY:T  List  \mtimes{}  (T  List)  [let  X,Y  =  XY 
                                                        in  (L  =  (X  @  Y))
                                                              \mwedge{}  (\mforall{}i:\mBbbN{}||X||  -  1.  ((f  X[i  +  1])  =  ((f  X[i])  +  1)))
                                                              \mwedge{}  ((\mneg{}\muparrow{}null(L))
                                                                  {}\mRightarrow{}  ((\mneg{}\muparrow{}null(X))
                                                                        \mwedge{}  \mneg{}((f  hd(Y))  =  ((f  last(X))  +  1))  supposing  ||Y||  \mgeq{}  1  ))])


By

---

Latex:
Extract  of  Obid:  split-at-first-gap
not  unfolding    list\_ind
finishing  with  Auto
normalizes  to:

\mlambda{}f,L.  rec-case(L)  of
            []  =>  <Ax,  Ax>
            a::L  =>
              r.if  L  =  Ax  then  <<a,  Ax>,  Ax>  otherwise  let  u1,v1  =  L 
                                                                  in  if  f  u1=(f  a)  +  1
                                                                        then  let  X1,X2  =  r 
                                                                                  in  <<a,  X1>,  X2>
                                                                        else  <<a,  Ax>,  u1,  v1>

---

Home Index