---

Step * of Lemma split-gap_wf

∀[T:Type]
  ∀f:T ⟶ ℤ. ∀L:T List.
    (split-gap(f;L) ∈ ∃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
{ (Auto THEN Subst ⌜split-gap(f;L) ~ TERMOF{split-at-first-gap-ext:o, \\v:l, i:l} f L⌝ 0⋅ THEN Auto) }

1
.....equality..... 
1. T : Type
2. f : T ⟶ ℤ
3. L : T List
⊢ split-gap(f;L) ~ TERMOF{split-at-first-gap-ext:o, \\v:l, i:l} f L

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}f:T  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}L:T  List.
        (split-gap(f;L)  \mmember{}  \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:
(Auto  THEN  Subst  \mkleeneopen{}split-gap(f;L)  \msim{}  TERMOF\{split-at-first-gap-ext:o,  \mbackslash{}\mbackslash{}v:l,  i:l\}  f  L\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index