---

Step * 1 1 of Lemma es-is-interface-filter


1. Info : Type@i'
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)@i'
5. P : A ─→ 𝔹@i
6. e : E@i
⊢ ↑(#(if (#(X es e) =z 1) then [a∈X es e|P[a]] else {} fi ) =z 1) ⇐⇒ (↑(#(X es e) =z 1)) ∧ (↑P[only(X es e)])
BY
{ (AutoSplit THEN ElimBagSizeOne' THEN Reduce 0) }

1
1. Info : Type@i'
2. es : EO+(Info)@i'
3. A : Type@i'
4. X : es:EO+(Info) ─→ e:E ─→ bag(A)@i'
5. P : A ─→ 𝔹@i
6. e : E@i
7. #(X es e) = 1 ∈ ℤ
8. X es e ~ {only(X es e)}
9. x : A@i
⊢ ↑(#([a∈{x}|P[a]]) =z 1) ⇐⇒ True ∧ (↑P[x])

---

Latex:

---

Latex:

1.  Info  :  Type@i'
2.  es  :  EO+(Info)@i'
3.  A  :  Type@i'
4.  X  :  es:EO+(Info)  {}\mrightarrow{}  e:E  {}\mrightarrow{}  bag(A)@i'
5.  P  :  A  {}\mrightarrow{}  \mBbbB{}@i
6.  e  :  E@i
\mvdash{}  \muparrow{}(\#(if  (\#(X  es  e)  =\msubz{}  1)  then  [a\mmember{}X  es  e|P[a]]  else  \{\}  fi  )  =\msubz{}  1)
\mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(\#(X  es  e)  =\msubz{}  1))  \mwedge{}  (\muparrow{}P[only(X  es  e)])


By

---

Latex:
(AutoSplit  THEN  ElimBagSizeOne'  THEN  Reduce  0)

---

Home Index