---

Step * 1 of Lemma split-at-first-rel


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 ))]
BY
{ (InstConcl [<[], []>]⋅ THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  [T]  :  Type
2.  [R]  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x,y:T.    Dec(R[x;y])
\mvdash{}  \mexists{}XY:T  List  \mtimes{}  (T  List)  [let  X,Y  =  XY 
                                                  in  ([]  =  (X  @  Y))
                                                        \mwedge{}  (\mforall{}i:\mBbbN{}||X||  -  1.  R[X[i];X[i  +  1]])
                                                        \mwedge{}  ((\mneg{}\muparrow{}null([]))
                                                            {}\mRightarrow{}  ((\mneg{}\muparrow{}null(X))  \mwedge{}  \mneg{}R[last(X);hd(Y)]  supposing  ||Y||  \mgeq{}  1  ))]


By

---

Latex:
(InstConcl  [<[],  []>]\mcdot{}  THEN  Reduce  0  THEN  Auto)

---

Home Index