---

Step * 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)
⊢ {}@i ~ []
BY
{ (Assert ∀e:E. (¬(e ∈ {}@i)) BY
         (Reduce (-1) THEN D -1 THEN ParallelOp -2 THEN (D 0 THEN Auto) THEN ThinTrivial THEN Auto)) }

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. ∀e:E. (¬(e ∈ {}@i))
⊢ {}@i ~ []

---

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)
\mvdash{}  \{\}@i  \msim{}  []


By

(Assert  \mforall{}e:E.  (\mneg{}(e  \mmember{}  \{\}@i))  BY
              (Reduce  (-1)  THEN  D  -1  THEN  ParallelOp  -2  THEN  (D  0  THEN  Auto)  THEN  ThinTrivial  THEN  Auto))

---

Home Index