---

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


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)))
BY
{ (GenConclAtAddr [2;1;2;1] THEN D -2 THEN Reduce 0 THEN Auto) }

---

Latex:



1.  es  :  EO@i'
2.  i  :  Id@i
3.  s  :  fset(E)@i
\mvdash{}  (\mforall{}e:E.  (e  \mmember{}  s  \mwedge{}  (loc(e)  =  i)  \mLeftarrow{}{}\mRightarrow{}  (e  \mmember{}  fst((TERMOF\{es-fset-at-loc:o,  1:l,  i:l\}  es  i  s)))))
\mwedge{}  no\_repeats(E;fst((TERMOF\{es-fset-at-loc:o,  1:l,  i:l\}  es  i  s)))
\mwedge{}  sorted-by(\mlambda{}e,e'.  e  \mleq{}loc  e'  ;fst((TERMOF\{es-fset-at-loc:o,  1:l,  i:l\}  es  i  s)))


By

(GenConclAtAddr  [2;1;2;1]  THEN  D  -2  THEN  Reduce  0  THEN  Auto)

---

Home Index