Step * 2 2 2 of Lemma llex-linear


1. [A] Type
2. [<A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (<[a;b] ∨ (a b ∈ A) ∨ <[b;a])
4. A
5. List
6. ∀L2:A List. ((v llex(A;a,b.<[a;b]) L2) ∨ (v L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) v))
7. u1 A
8. v1 List
9. ([u v] llex(A;a,b.<[a;b]) v1) ∨ ([u v] v1 ∈ (A List)) ∨ (v1 llex(A;a,b.<[a;b]) [u v])
10. (u u1 ∈ A) ∨ <[u1;u]
⊢ ([u v] llex(A;a,b.<[a;b]) [u1 v1]) ∨ ([u v] [u1 v1] ∈ (A List)) ∨ ([u1 v1] llex(A;a,b.<[a;b]) [u v])
BY
(-1) }

1
1. [A] Type
2. [<A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (<[a;b] ∨ (a b ∈ A) ∨ <[b;a])
4. A
5. List
6. ∀L2:A List. ((v llex(A;a,b.<[a;b]) L2) ∨ (v L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) v))
7. u1 A
8. v1 List
9. ([u v] llex(A;a,b.<[a;b]) v1) ∨ ([u v] v1 ∈ (A List)) ∨ (v1 llex(A;a,b.<[a;b]) [u v])
10. u1 ∈ A
⊢ ([u v] llex(A;a,b.<[a;b]) [u1 v1]) ∨ ([u v] [u1 v1] ∈ (A List)) ∨ ([u1 v1] llex(A;a,b.<[a;b]) [u v])

2
1. [A] Type
2. [<A ⟶ A ⟶ ℙ
3. ∀a,b:A.  (<[a;b] ∨ (a b ∈ A) ∨ <[b;a])
4. A
5. List
6. ∀L2:A List. ((v llex(A;a,b.<[a;b]) L2) ∨ (v L2 ∈ (A List)) ∨ (L2 llex(A;a,b.<[a;b]) v))
7. u1 A
8. v1 List
9. ([u v] llex(A;a,b.<[a;b]) v1) ∨ ([u v] v1 ∈ (A List)) ∨ (v1 llex(A;a,b.<[a;b]) [u v])
10. <[u1;u]
⊢ ([u v] llex(A;a,b.<[a;b]) [u1 v1]) ∨ ([u v] [u1 v1] ∈ (A List)) ∨ ([u1 v1] llex(A;a,b.<[a;b]) [u v])


Latex:


Latex:

1.  [A]  :  Type
2.  [<]  :  A  {}\mrightarrow{}  A  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}a,b:A.    (<[a;b]  \mvee{}  (a  =  b)  \mvee{}  <[b;a])
4.  u  :  A
5.  v  :  A  List
6.  \mforall{}L2:A  List.  ((v  llex(A;a,b.<[a;b])  L2)  \mvee{}  (v  =  L2)  \mvee{}  (L2  llex(A;a,b.<[a;b])  v))
7.  u1  :  A
8.  v1  :  A  List
9.  ([u  /  v]  llex(A;a,b.<[a;b])  v1)  \mvee{}  ([u  /  v]  =  v1)  \mvee{}  (v1  llex(A;a,b.<[a;b])  [u  /  v])
10.  (u  =  u1)  \mvee{}  <[u1;u]
\mvdash{}  ([u  /  v]  llex(A;a,b.<[a;b])  [u1  /  v1])
\mvee{}  ([u  /  v]  =  [u1  /  v1])
\mvee{}  ([u1  /  v1]  llex(A;a,b.<[a;b])  [u  /  v])


By


Latex:
D  (-1)




Home Index