---

Step * 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. ∀e:E. (¬(e ∈ {}@i))
⊢ {}@i ~ []
BY
{ ((MoveToConcl (-1) THEN GenConclAtAddr [2;1]) THEN (D 0 THENA Auto) THEN D -3) }

1
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
⊢ [] ~ []

2
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] ~ []

---

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.  \mforall{}e:E.  (\mneg{}(e  \mmember{}  \{\}@i))
\mvdash{}  \{\}@i  \msim{}  []


By

((MoveToConcl  (-1)  THEN  GenConclAtAddr  [2;1])  THEN  (D  0  THENA  Auto)  THEN  D  -3)

---

Home Index