---

Step * 2 of Lemma llex_transitivity


1. [A] : Type
2. [<] : A ⟶ A ⟶ ℙ
3. Trans(A;a,b.<[a;b])
4. as : A List
5. bs : A List
6. cs : A List
7. ∃i:ℕ. (i < ||as|| ∧ i < ||bs|| ∧ (∀j:ℕi. (as[j] = bs[j] ∈ A)) ∧ <[as[i];bs[i]])
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
{ (OrRight THENA Auto) }

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

---

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.  \mexists{}i:\mBbbN{}.  (i  <  ||as||  \mwedge{}  i  <  ||bs||  \mwedge{}  (\mforall{}j:\mBbbN{}i.  (as[j]  =  bs[j]))  \mwedge{}  <[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:
(OrRight  THENA  Auto)

---

Home Index