---

Step * of Lemma split-at-first-gap

∀[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
{ (Auto THEN InstLemma `split-at-first-rel` [⌜T⌝; ⌜λ2x y.(f y) = ((f x) + 1) ∈ ℤ⌝;⌜L⌝]⋅ THEN Auto) }

---

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:
(Auto  THEN  InstLemma  `split-at-first-rel`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}x  y.(f  y)  =  ((f  x)  +  1)\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}  THEN  Auto)

---

Home Index