---

Step * of Lemma es-interface-restrict-conditional

∀[Info,A:Type]. ∀[I:EClass(A)]. ∀[P:es:EO+(Info) ─→ E ─→ ℙ]. ∀[p:∀es:EO+(Info). ∀e:E.  Dec(P[es;e])].
  [(I|p)?(I|¬p)] = I ∈ EClass(A) supposing Singlevalued(I)
BY
{ (Auto
   THEN Unfold `eclass` 0
   THEN RepeatFor 2 ((Ext THEN Auto THEN Try ((Fold `eclass` 0 THEN Auto))))
   THEN RepUR ``cond-class eclass-compose2 es-interface-restrict es-interface-co-restrict`` 0
   THEN GenConclAtAddr[2;1;1;1;1]
   THEN D -2
   THEN Reduce 0
   THEN Auto) }

1
1. Info : Type
2. A : Type
3. I : EClass(A)
4. P : es:EO+(Info) ─→ E ─→ ℙ
5. p : ∀es:EO+(Info). ∀e:E.  Dec(P[es;e])
6. Singlevalued(I)
7. x : EO+(Info)
8. x1 : E
9. x2 : P[x;x1]@i
10. (p x x1) = (inl x2) ∈ Dec(P[x;x1])@i
⊢ if (#(I x x1) =z 1) then I x x1 else {} fi  = (I x x1) ∈ bag(A)

---

Latex:

---

Latex:
\mforall{}[Info,A:Type].  \mforall{}[I:EClass(A)].  \mforall{}[P:es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}].
\mforall{}[p:\mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P[es;e])].
    [(I|p)?(I|\mneg{}p)]  =  I  supposing  Singlevalued(I)


By

---

Latex:
(Auto
  THEN  Unfold  `eclass`  0
  THEN  RepeatFor  2  ((Ext  THEN  Auto  THEN  Try  ((Fold  `eclass`  0  THEN  Auto))))
  THEN  RepUR  ``cond-class  eclass-compose2  es-interface-restrict  es-interface-co-restrict``  0
  THEN  GenConclAtAddr[2;1;1;1;1]
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto)

---

Home Index