---

Step * 1 of Lemma interface-predecessors-tagged-true


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))
BY
{ (BLemma `filter-sq`
   THEN Reduce 0
   THEN Auto
   THEN (MoveToConcl (-1)
         THEN RepUR ``can-apply`` 0
         THEN Try (((GenConcl ⌈X(x) = p ∈ (Top × 𝔹)⌉⋅ THENA Auto)⋅
                    THEN D -2
                    THEN Reduce 0
                    THEN AutoSplit
                    THEN RepUR ``bfalse`` 0
                    THEN Auto))
         THEN Auto)⋅)⋅ }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top  \mtimes{}  \mBbbB{})
4.  e  :  E
\mvdash{}  filter(\mlambda{}e.(\#((\mlambda{}p.if  snd(p)  then  \{fst(p)\}  else  \{\}  fi  )  X(e))  =\msubz{}  1);\mleq{}(X)(e)) 
\msim{}  filter(\mlambda{}e.(snd(X(e)));\mleq{}(X)(e))


By

---

Latex:
(BLemma  `filter-sq`
  THEN  Reduce  0
  THEN  Auto
  THEN  (MoveToConcl  (-1)
              THEN  RepUR  ``can-apply``  0
              THEN  Try  (((GenConcl  \mkleeneopen{}X(x)  =  p\mkleeneclose{}\mcdot{}  THENA  Auto)\mcdot{}
                                    THEN  D  -2
                                    THEN  Reduce  0
                                    THEN  AutoSplit
                                    THEN  RepUR  ``bfalse``  0
                                    THEN  Auto))
              THEN  Auto)\mcdot{})\mcdot{}

---

Home Index