---

Step * 4 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. 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]]))
BY
{ (Decide ⌜i < i1⌝⋅ 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. 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]]
17. i < i1
⊢ (||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]]))

2
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]]
17. ¬i < i1
⊢ (||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.  i1  :  \mBbbN{}
8.  i1  <  ||as||
9.  i1  <  ||bs||
10.  \mforall{}j:\mBbbN{}i1.  (as[j]  =  bs[j])
11.  <[as[i1];bs[i1]]
12.  i  :  \mBbbN{}
13.  i  <  ||bs||
14.  i  <  ||cs||
15.  \mforall{}j:\mBbbN{}i.  (bs[j]  =  cs[j])
16.  <[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:
(Decide  \mkleeneopen{}i  <  i1\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index