---

Step * of Lemma loc-ordered-equality

∀es:EO. ∀as,bs:E List.
  (loc-ordered(es;as) ⇒ loc-ordered(es;bs) ⇒ (as = bs ∈ (E List) ⇐⇒ ∀e:E. ((e ∈ as) ⇐⇒ (e ∈ bs))))
BY
{ (((D 0 THENA Auto) THEN (InstLemma `l-ordered-equality` [⌜E⌝; ⌜λ2x y.(x <loc y)⌝])⋅) THENA Auto) }

1
1. es : EO@i'
2. x : E@i
3. y : E@i
4. (x <loc y)@i
⊢ ¬(y <loc x)

2
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))))

---

Latex:

---

Latex:
\mforall{}es:EO.  \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

---

Latex:
(((D  0  THENA  Auto)  THEN  (InstLemma  `l-ordered-equality`  [\mkleeneopen{}E\mkleeneclose{};  \mkleeneopen{}\mlambda{}\msubtwo{}x  y.(x  <loc  y)\mkleeneclose{}])\mcdot{})  THENA  Auto)

---

Home Index