---

Step * 3 of Lemma es-interface-pair-prior-programmable


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. Singlevalued(X)
7. es : EO+(Info)@i'
8. e : E@i
⊢ ↑e ∈b X;Y
⇐⇒ ↑e
    ∈b eclass-compose2(λys,xs. if (#(ys) =z 1)
                              then if (#(xs) =z 1) then {<only(xs), only(ys)>} else {} fi 
                              else {}
                              fi ;Y;Prior(X))
BY
{ ((RWO "is-pair-prior" 0 THENA Auto)
   THEN RepUR ``in-eclass eclass-compose2`` 0
   THEN Folds ``in-eclass eclass-val`` 0
   THEN RepeatFor 2 (OldAutoSplit)
   THEN RWO "primed-class-prior-val" (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  A  :  Type
3.  B  :  Type
4.  X  :  EClass(A)
5.  Y  :  EClass(B)
6.  Singlevalued(X)
7.  es  :  EO+(Info)@i'
8.  e  :  E@i
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  X;Y
\mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  eclass-compose2(\mlambda{}ys,xs.  if  (\#(ys)  =\msubz{}  1)
                                                                  then  if  (\#(xs)  =\msubz{}  1)  then  \{<only(xs),  only(ys)>\}  else  \{\}  fi 
                                                                  else  \{\}
                                                                  fi  ;Y;Prior(X))


By

---

Latex:
((RWO  "is-pair-prior"  0  THENA  Auto)
  THEN  RepUR  ``in-eclass  eclass-compose2``  0
  THEN  Folds  ``in-eclass  eclass-val``  0
  THEN  RepeatFor  2  (OldAutoSplit)
  THEN  RWO  "primed-class-prior-val"  (-1)
  THEN  Auto)

---

Home Index