---

Step * 1 1 2 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. u : E
6. v : E List
7. {}@i = [u / v] ∈ (E List)@i
8. ∀e:E. (¬(e ∈ [u / v]))@i
⊢ [u / v] ~ []
BY
{ ((InstHyp [⌈u⌉] (-1)⋅ THENM D -1) THEN 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.  u  :  E
6.  v  :  E  List
7.  \{\}@i  =  [u  /  v]@i
8.  \mforall{}e:E.  (\mneg{}(e  \mmember{}  [u  /  v]))@i
\mvdash{}  [u  /  v]  \msim{}  []


By

((InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}  THENM  D  -1)  THEN  Auto)

---

Home Index