---

Step * of Lemma es-empty-fset-at

∀[es:EO]. ∀[i:Id].  ({}@i ~ [])
BY
{ (InstLemma `es-fset-at-property` [] THEN RepeatFor 2 (ParallelLast') THEN (InstHyp [⌈{}⌉] (-1)⋅ THENA 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)
⊢ {}@i ~ []

---

Latex:


\mforall{}[es:EO].  \mforall{}[i:Id].    (\{\}@i  \msim{}  [])


By

(InstLemma  `es-fset-at-property`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  (InstHyp  [\mkleeneopen{}\{\}\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto))

---

Home Index