Step * 2 2 of Lemma l-ordered-equality


1. Type
2. T ⟶ T ⟶ ℙ
3. ∀x:T. R[x;x])
4. ∀x,y:T.  (R[x;y]  R[y;x]))
5. as List
6. bs 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. T
11. T
12. before y ∈ bs
⊢ before y ∈ as
BY
((RepUR ``l-ordered`` 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