---

Step * 1 of Lemma es-prior-class-when-programmable


1. Info : Type
2. A : Type
3. B : Type
4. X : EClass(A)
5. Y : EClass(B)
6. d : A
7. Singlevalued(X)
8. es : EO+(Info)@i'
9. e : E@i
⊢ ↑e ∈b (X'?d) when Y
⇐⇒ ↑e ∈b eclass-compose2(λys,xs. if (#(ys) =z 1)
                                 then if (#(xs) =z 1) then {<only(ys), only(xs)>} else {<only(ys), d>} fi 
                                 else {}
                                 fi ;Y;Prior(X))
BY
{ ((RWO "is-prior-class-when" 0 THENA Auto)
   THEN RepUR ``in-eclass eclass-compose2`` 0
   THEN Folds ``in-eclass eclass-val`` 0
   THEN RepeatFor 2 (AutoSplit)
   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.  d  :  A
7.  Singlevalued(X)
8.  es  :  EO+(Info)@i'
9.  e  :  E@i
\mvdash{}  \muparrow{}e  \mmember{}\msubb{}  (X'?d)  when  Y
\mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  eclass-compose2(\mlambda{}ys,xs.  if  (\#(ys)  =\msubz{}  1)
                                                                  then  if  (\#(xs)  =\msubz{}  1)
                                                                            then  \{<only(ys),  only(xs)>\}
                                                                            else  \{<only(ys),  d>\}
                                                                            fi 
                                                                  else  \{\}
                                                                  fi  ;Y;Prior(X))


By

---

Latex:
((RWO  "is-prior-class-when"  0  THENA  Auto)
  THEN  RepUR  ``in-eclass  eclass-compose2``  0
  THEN  Folds  ``in-eclass  eclass-val``  0
  THEN  RepeatFor  2  (AutoSplit)
  THEN  RWO  "primed-class-prior-val"  (-1)
  THEN  Auto)\mcdot{}

---

Home Index