Step * 1 of Lemma llex_transitivity


1. [A] Type
2. [<A ⟶ A ⟶ ℙ
3. Trans(A;a,b.<[a;b])
4. as List
5. bs List
6. cs List
7. ||as|| < ||bs|| ∧ (∀i:ℕ||as||. (as[i] bs[i] ∈ A))
8. ||bs|| < ||cs|| ∧ (∀i:ℕ||bs||. (bs[i] cs[i] ∈ A))
⊢ (||as|| < ||cs|| ∧ (∀i:ℕ||as||. (as[i] cs[i] ∈ A)))
∨ (∃i:ℕ(i < ||as|| ∧ i < ||cs|| ∧ (∀j:ℕi. (as[j] cs[j] ∈ A)) ∧ <[as[i];cs[i]]))
BY
(OrLeft THEN Auto) }


Latex:


Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  Trans(A;a,b.<[a;b])
4.  as  :  A  List
5.  bs  :  A  List
6.  cs  :  A  List
7.  ||as||  <  ||bs||  \mwedge{}  (\mforall{}i:\mBbbN{}||as||.  (as[i]  =  bs[i]))
8.  ||bs||  <  ||cs||  \mwedge{}  (\mforall{}i:\mBbbN{}||bs||.  (bs[i]  =  cs[i]))
\mvdash{}  (||as||  <  ||cs||  \mwedge{}  (\mforall{}i:\mBbbN{}||as||.  (as[i]  =  cs[i])))
\mvee{}  (\mexists{}i:\mBbbN{}.  (i  <  ||as||  \mwedge{}  i  <  ||cs||  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (as[j]  =  cs[j]))  \mwedge{}  <[as[i];cs[i]]))


By


Latex:
(OrLeft  THEN  Auto)




Home Index