---

Step * of Lemma llex_transitivity

No Annotations
∀[A:Type]. ∀[<:A ⟶ A ⟶ ℙ].
  (Trans(A;a,b.<[a;b])
  ⇒ (∀as,bs,cs:A List.  ((as llex(A;a,b.<[a;b]) bs) ⇒ (bs llex(A;a,b.<[a;b]) cs) ⇒ (as llex(A;a,b.<[a;b]) cs))))
BY
{ (Auto THEN All (RepUR ``llex``) THEN SplitOrHyps) }

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. ||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]]))

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. ∃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]]))

3
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|| ∧ (∀i:ℕ||as||. (as[i] = bs[i] ∈ A))
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]]))

4
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]]))

---

Latex:

---

Latex:
No  Annotations
\mforall{}[A:Type].  \mforall{}[<:A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}].
    (Trans(A;a,b.<[a;b])
    {}\mRightarrow{}  (\mforall{}as,bs,cs:A  List.
                ((as  llex(A;a,b.<[a;b])  bs)  {}\mRightarrow{}  (bs  llex(A;a,b.<[a;b])  cs)  {}\mRightarrow{}  (as  llex(A;a,b.<[a;b])  cs))))


By

---

Latex:
(Auto  THEN  All  (RepUR  ``llex``)  THEN  SplitOrHyps)

---

Home Index