---

Step * 2 2 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. ∀x:T. ((x ∈ as) ⇐⇒ (x ∈ bs))
10. x : T
11. y : T
12. x before y ∈ bs
⊢ x before y ∈ as
BY
{ ((RepUR ``l-ordered`` 8 THEN (InstHyp [⌜x⌝; ⌜y⌝] 8)⋅)
   THEN Try (Complete (Auto))
   THEN ((InstLemma `l_tricotomy` [⌜T⌝; ⌜x⌝; ⌜y⌝; ⌜as⌝])⋅ THENA Auto)
   THEN Try ((BackThruSomeHyp THEN (FLemma `l_before_member2` [-2]) THEN Complete (Auto)))
   THEN Try ((BackThruSomeHyp THEN (FLemma `l_before_member` [-2]) THEN Complete (Auto)))
   THEN (SplitOrHyps THEN Auto)
   THEN (InstHyp [⌜y⌝; ⌜x⌝] 4)⋅
   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.  \mforall{}x:T.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs))
10.  x  :  T
11.  y  :  T
12.  x  before  y  \mmember{}  bs
\mvdash{}  x  before  y  \mmember{}  as


By

---

Latex:
((RepUR  ``l-ordered``  8  THEN  (InstHyp  [\mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{}]  8)\mcdot{})
  THEN  Try  (Complete  (Auto))
  THEN  ((InstLemma  `l\_tricotomy`  [\mkleeneopen{}T\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{};  \mkleeneopen{}y\mkleeneclose{};  \mkleeneopen{}as\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  Try  ((BackThruSomeHyp  THEN  (FLemma  `l\_before\_member2`  [-2])  THEN  Complete  (Auto)))
  THEN  Try  ((BackThruSomeHyp  THEN  (FLemma  `l\_before\_member`  [-2])  THEN  Complete  (Auto)))
  THEN  (SplitOrHyps  THEN  Auto)
  THEN  (InstHyp  [\mkleeneopen{}y\mkleeneclose{};  \mkleeneopen{}x\mkleeneclose{}]  4)\mcdot{}
  THEN  Auto)

---

Home Index