---

Step * of Lemma interface-predecessors-tagged-true

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[X:EClass(Top × 𝔹)]. ∀[e:E].  (≤(Tagged_tt(X))(e) ~ filter(λe.(snd(X(e)));≤(X)(e)))
BY
{ (((UnivCD THENA Auto) THEN Unfold `es-tagged-true-class` 0)
   THEN (InstLemma `interface-predecessors-filter-image` [⌈Info⌉;⌈Top × 𝔹⌉;⌈Top⌉]⋅ THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN Thin (-1)) }

1
1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top × 𝔹)
4. e : E
⊢ filter(λe.(#((λp.if snd(p) then {fst(p)} else {} fi ) X(e)) =z 1);≤(X)(e)) ~ filter(λe.(snd(X(e)));≤(X)(e))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[X:EClass(Top  \mtimes{}  \mBbbB{})].  \mforall{}[e:E].
    (\mleq{}(Tagged\_tt(X))(e)  \msim{}  filter(\mlambda{}e.(snd(X(e)));\mleq{}(X)(e)))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  Unfold  `es-tagged-true-class`  0)
  THEN  (InstLemma  `interface-predecessors-filter-image`  [\mkleeneopen{}Info\mkleeneclose{};\mkleeneopen{}Top  \mtimes{}  \mBbbB{}\mkleeneclose{};\mkleeneopen{}Top\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  Thin  (-1))

---

Home Index