---

Step * 3 1 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. ||as|| < ||bs||
8. ∀i:ℕ||as||. (as[i] = bs[i] ∈ A)
9. i : ℕ
10. i < ||bs||
11. i < ||cs||
12. ∀j:ℕi. (bs[j] = cs[j] ∈ A)
13. <[bs[i];cs[i]]
14. i < ||as||
⊢ (||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) THEN D 0 With ⌜i⌝  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||
8.  \mforall{}i:\mBbbN{}||as||.  (as[i]  =  bs[i])
9.  i  :  \mBbbN{}
10.  i  <  ||bs||
11.  i  <  ||cs||
12.  \mforall{}j:\mBbbN{}i.  (bs[j]  =  cs[j])
13.  <[bs[i];cs[i]]
14.  i  <  ||as||
\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)  THEN  D  0  With  \mkleeneopen{}i\mkleeneclose{}    THEN  Auto)

---

Home Index