---

Step * of Lemma es-fset-at-property

∀es:EO. ∀i:Id. ∀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))
BY
{ (RepeatFor 3 ((D 0 THENA Auto)) THEN Unfold `es-fset-at` 0) }

1
1. es : EO@i'
2. i : Id@i
3. s : fset(E)@i
⊢ (∀e:E. (e ∈ s ∧ (loc(e) = i ∈ Id) ⇐⇒ (e ∈ fst((TERMOF{es-fset-at-loc:o, 1:l, i:l} es i s)))))
∧ no_repeats(E;fst((TERMOF{es-fset-at-loc:o, 1:l, i:l} es i s)))
∧ sorted-by(λe,e'. e ≤loc e' ;fst((TERMOF{es-fset-at-loc:o, 1:l, i:l} es i s)))

---

Latex:


\mforall{}es:EO.  \mforall{}i:Id.  \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@\000Ci))


By

(RepeatFor  3  ((D  0  THENA  Auto))  THEN  Unfold  `es-fset-at`  0)

---

Home Index