---

Step * 2 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)))
⇒ ((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
{ Auto⋅ }

1
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)

---

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)
{}\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)))
{}\mRightarrow{}  ((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\000C 
                                                        else  \{\}
                                                        fi  ;Y;Prior(X))(e))


By

---

Latex:
Auto\mcdot{}

---

Home Index