---

Step * 2 of Lemma loc-ordered-equality


1. es : EO@i'
2. ∀as,bs:E List.
     (l-ordered(E;x,y.(x <loc y);as)
     ⇒ l-ordered(E;x,y.(x <loc y);bs)
     ⇒ (as = bs ∈ (E List) ⇐⇒ ∀x:E. ((x ∈ as) ⇐⇒ (x ∈ bs))))
⊢ ∀as,bs:E List.  (loc-ordered(es;as) ⇒ loc-ordered(es;bs) ⇒ (as = bs ∈ (E List) ⇐⇒ ∀e:E. ((e ∈ as) ⇐⇒ (e ∈ bs))))
BY
{ (Unfold `loc-ordered` 0 THEN Trivial) }

---

Latex:



1.  es  :  EO@i'
2.  \mforall{}as,bs:E  List.
          (l-ordered(E;x,y.(x  <loc  y);as)
          {}\mRightarrow{}  l-ordered(E;x,y.(x  <loc  y);bs)
          {}\mRightarrow{}  (as  =  bs  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:E.  ((x  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  bs))))
\mvdash{}  \mforall{}as,bs:E  List.
        (loc-ordered(es;as)  {}\mRightarrow{}  loc-ordered(es;bs)  {}\mRightarrow{}  (as  =  bs  \mLeftarrow{}{}\mRightarrow{}  \mforall{}e:E.  ((e  \mmember{}  as)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  bs))))


By

(Unfold  `loc-ordered`  0  THEN  Trivial)

---

Home Index