Step
*
3
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|| ∧ (∀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]]))
BY
{ (ExRepD THEN (Decide ⌜i < ||as||⌝⋅ 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. ||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]]))
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. ||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]]))
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|| \mwedge{} (\mforall{}i:\mBbbN{}||as||. (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 THEN (Decide \mkleeneopen{}i < ||as||\mkleeneclose{}\mcdot{} THENA Auto))
Home
Index