---

Step * 4 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. ∃i:ℕ. (i < ||bs|| ∧ i < ||cs|| ∧ (∀j:ℕi. (bs[j] = cs[j] ∈ A)) ∧ <[bs[i];cs[i]])
⊢ (||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
{ ExRepD }

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. i1 : ℕ
8. i1 < ||as||
9. i1 < ||bs||
10. ∀j:ℕi1. (as[j] = bs[j] ∈ A)
11. <[as[i1];bs[i1]]
12. i : ℕ
13. i < ||bs||
14. i < ||cs||
15. ∀j:ℕi. (bs[j] = cs[j] ∈ A)
16. <[bs[i];cs[i]]
⊢ (||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]]))

---

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

---

Home Index