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


1. [T] Type
2. [R] T ⟶ T ⟶ ℙ
3. ∀x,y:T.  Dec(R[x;y])
4. T
5. u1 T
6. List
7. ∃XY:T List × (T List) [let X,Y XY 
                          in ([u1 v] (X Y) ∈ (T List))
                             ∧ (∀i:ℕ||X|| 1. R[X[i];X[i 1]])
                             ∧ ((¬↑null([u1 v]))  ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ ))]
⊢ ∃XY:T List × (T List) [let X,Y XY 
                         in ([u; [u1 v]] (X Y) ∈ (T List))
                            ∧ (∀i:ℕ||X|| 1. R[X[i];X[i 1]])
                            ∧ ((¬↑null([u; [u1 v]]))  ((¬↑null(X)) ∧ ¬R[last(X);hd(Y)] supposing ||Y|| ≥ ))]
BY
(Decide ⌜R[u;u1]⌝⋅ THENA Auto) }

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

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


Latex:


Latex:

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


By


Latex:
(Decide  \mkleeneopen{}R[u;u1]\mkleeneclose{}\mcdot{}  THENA  Auto)




Home Index