---

Step * 4 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)))
⇒ (X;Y(e)
   = 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))(e)
   ∈ (A × B))
BY
{ (Auto
   THEN Thin (-1)
   THEN ((RWO "is-pair-prior" (-1) THENA Auto)
         THEN (RepUR ``eclass-val eclass-compose2 es-interface-pair-prior`` 0
               THEN Folds ``in-eclass eclass-val`` 0
               THEN RepeatFor 2 (OldAutoSplit))⋅
         )⋅) }

1
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
9. (↑e ∈b (X)') ∧ (↑e ∈b Y)
10. ↑e ∈b (X)'
11. ↑e ∈b Y
⊢ <(X)'(e), Y(e)> = only(if e ∈b Prior(X) then {<Prior(X)(e), Y(e)>} else {} fi ) ∈ (A × B)

---

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)
{}\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)))
{}\mRightarrow{}  (X;Y(e)
      =  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))(e))


By

---

Latex:
(Auto
  THEN  Thin  (-1)
  THEN  ((RWO  "is-pair-prior"  (-1)  THENA  Auto)
              THEN  (RepUR  ``eclass-val  eclass-compose2  es-interface-pair-prior``  0
                          THEN  Folds  ``in-eclass  eclass-val``  0
                          THEN  RepeatFor  2  (OldAutoSplit))\mcdot{}
              )\mcdot{})

---

Home Index