---

Step * 1 1 1 of Lemma es-empty-fset-at


1. es : EO
2. i : Id
3. ∀s:fset(E). ((∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ s@i))) ∧ no_repeats(E;s@i) ∧ sorted-by(λe,e'. e ≤loc e' ;s@i)\000C)
4. (∀e:E. (e ∈ {} ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ {}@i))) ∧ no_repeats(E;{}@i) ∧ sorted-by(λe,e'. e ≤loc e' ;{}@i)
5. {}@i = [] ∈ (E List)@i
6. ∀e:E. (¬(e ∈ []))@i
⊢ [] ~ []
BY
{ Auto }

---

Latex:



1.  es  :  EO
2.  i  :  Id
3.  \mforall{}s:fset(E)
          ((\mforall{}e:E.  (e  \mmember{}  s  \mwedge{}  (loc(e)  =  i)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  s@i)))
          \mwedge{}  no\_repeats(E;s@i)
          \mwedge{}  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;s@i))
4.  (\mforall{}e:E.  (e  \mmember{}  \{\}  \mwedge{}  (loc(e)  =  i)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  \{\}@i)))
\mwedge{}  no\_repeats(E;\{\}@i)
\mwedge{}  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;\{\}@i)
5.  \{\}@i  =  []@i
6.  \mforall{}e:E.  (\mneg{}(e  \mmember{}  []))@i
\mvdash{}  []  \msim{}  []


By

Auto

---

Home Index