---

Step * 1 of Lemma l-ordered-equality


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. as = bs ∈ (T List)
10. (∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))) ∧ (∀x,y:T.  (x before y ∈ as ⇐⇒ x before y ∈ bs))
⊢ ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
BY
{ (D -1 THEN Auto) }

---

Latex:

---

Latex:

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.  as  =  bs
10.  (\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))
\mvdash{}  \mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs))


By

---

Latex:
(D  -1  THEN  Auto)

---

Home Index