---

Step * 2 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
10. ↑e ∈b (X'?d) when Y@i
11. ↑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))@i
⊢ (X'?d) when Y(e)
= 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))(e)
∈ (B × A)
BY
{ (Thin (-1)
   THEN ((RWO "is-prior-class-when" (-1) THENA Auto)
         THEN (RepUR ``eclass-val eclass-compose2 es-prior-class-when`` 0
               THEN Folds ``in-eclass eclass-val`` 0
               THEN RepeatFor 3 (AutoSplit)⋅
               THEN EqCD
               THEN Auto
               THEN Try (OnSomeHyp (\h. (RWO "primed-class-prior-val" h⋅ THEN Complete (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
10.  \muparrow{}e  \mmember{}\msubb{}  (X'?d)  when  Y@i
11.  \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))@i
\mvdash{}  (X'?d)  when  Y(e)
=  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))(e)


By

---

Latex:
(Thin  (-1)
  THEN  ((RWO  "is-prior-class-when"  (-1)  THENA  Auto)
              THEN  (RepUR  ``eclass-val  eclass-compose2  es-prior-class-when``  0
                          THEN  Folds  ``in-eclass  eclass-val``  0
                          THEN  RepeatFor  3  (AutoSplit)\mcdot{}
                          THEN  EqCD
                          THEN  Auto
                          THEN  Try  (OnSomeHyp  (\mbackslash{}h.  (RWO  "primed-class-prior-val"  h\mcdot{}  THEN  Complete  (Auto))  )\mcdot{}))\mcdot{}
              )\mcdot{}
  )\mcdot{}

---

Home Index