---

Step * 2 of Lemma l-ordered-equality

.....antecedent..... 
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x:T. (¬R[x;x])
4. ∀x,y:T.  (R[x;y] ⇒ (¬R[y;x]))
5. as : T List
6. bs : T List
7. l-ordered(T;x,y.R[x;y];as)
8. l-ordered(T;x,y.R[x;y];bs)
9. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
⊢ (∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))) ∧ (∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs))
BY
{ (D 0 THEN Auto) }

1
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x:T. (¬R[x;x])
4. ∀x,y:T.  (R[x;y] ⇒ (¬R[y;x]))
5. as : T List
6. bs : T List
7. l-ordered(T;x,y.R[x;y];as)
8. l-ordered(T;x,y.R[x;y];bs)
9. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
10. x : T
11. y : T
12. x before y ∈ as
⊢ x before y ∈ bs

2
1. T : Type
2. R : T ⟶ T ⟶ ℙ
3. ∀x:T. (¬R[x;x])
4. ∀x,y:T.  (R[x;y] ⇒ (¬R[y;x]))
5. as : T List
6. bs : T List
7. l-ordered(T;x,y.R[x;y];as)
8. l-ordered(T;x,y.R[x;y];bs)
9. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
10. x : T
11. y : T
12. x before y ∈ bs
⊢ x before y ∈ as

---

Latex:

---

Latex:
.....antecedent..... 
1.  T  :  Type
2.  R  :  T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}x:T.  (\mneg{}R[x;x])
4.  \mforall{}x,y:T.    (R[x;y]  {}\mRightarrow{}  (\mneg{}R[y;x]))
5.  as  :  T  List
6.  bs  :  T  List
7.  l-ordered(T;x,y.R[x;y];as)
8.  l-ordered(T;x,y.R[x;y];bs)
9.  \mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs))
\mvdash{}  (\mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs)))  \mwedge{}  (\mforall{}x,y:T.    (x  before  y  \mmember{}  as  \mLeftarrow{}{}\mRightarrow{}  x  before  y  \mmember{}  bs))


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index