---

Step * of Lemma split-at-first-rel

∀[T:Type]. ∀[R:T ⟶ T ⟶ ℙ].
  ((∀x,y:T.  Dec(R[x;y]))
  ⇒ (∀L:T List
        (∃XY:T List × (T List) [let X,Y = XY 
                                in (L = (X @ Y) ∈ (T List))
                                   ∧ (∀i:ℕ||X|| - 1. R[X[i];X[i + 1]])
                                   ∧ ((¬↑null(L)) ⇒ ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ 1 ))])))
BY
{ TACTIC:InductionOnList }

1
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
⊢ ∃XY:T List × (T List) [let X,Y = XY 
                         in ([] = (X @ Y) ∈ (T List))
                            ∧ (∀i:ℕ||X|| - 1. R[X[i];X[i + 1]])
                            ∧ ((¬↑null([])) ⇒ ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ 1 ))]

2
1. [T] : Type
2. [R] : T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. u : T
5. v : T List
6. ∃XY:T List × (T List) [let X,Y = XY 
                          in (v = (X @ Y) ∈ (T List))
                             ∧ (∀i:ℕ||X|| - 1. R[X[i];X[i + 1]])
                             ∧ ((¬↑null(v)) ⇒ ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ 1 ))]
⊢ ∃XY:T List × (T List) [let X,Y = XY 
                         in ([u / v] = (X @ Y) ∈ (T List))
                            ∧ (∀i:ℕ||X|| - 1. R[X[i];X[i + 1]])
                            ∧ ((¬↑null([u / v])) ⇒ ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ 1 ))]

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[R:T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x,y:T.    Dec(R[x;y]))
    {}\mRightarrow{}  (\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.  R[X[i];X[i  +  1]])
                                                                      \mwedge{}  ((\mneg{}\muparrow{}null(L))
                                                                          {}\mRightarrow{}  ((\mneg{}\muparrow{}null(X))  \mwedge{}  \mneg{}R[last(X);hd(Y)]  supposing  ||Y||  \mgeq{}  1  ))])))


By

---

Latex:
TACTIC:InductionOnList

---

Home Index