---

Step * of Lemma interface-or-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[X:EClass(A)]. ∀[Y:EClass(B)]. ∀[e:E].
  (X | Y)(e)
  = if e ∈b X then if e ∈b Y then oobboth(<X(e), Y(e)>) else oobleft(X(e)) fi  else oobright(Y(e)) fi 
  ∈ one_or_both(A;B) 
  supposing ↑e ∈b (X | Y)
BY
{ (Auto
   THEN MoveToConcl (-1)
   THEN All (RepUR ``eclass es-interface-or eclass-compose2
           eclass-val in-eclass oob-apply`` )⋅
   THEN (RepeatFor 2 ((GenConclAtAddr [1;1;1;1;1;1;1] THEN AutoSplit)) THEN EAuto 1⋅)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A,B:Type].  \mforall{}[X:EClass(A)].  \mforall{}[Y:EClass(B)].  \mforall{}[e:E].
    (X  |  Y)(e)
    =  if  e  \mmember{}\msubb{}  X  then  if  e  \mmember{}\msubb{}  Y  then  oobboth(<X(e),  Y(e)>)  else  oobleft(X(e))  fi    else  oobright(Y(e))  f\000Ci   
    supposing  \muparrow{}e  \mmember{}\msubb{}  (X  |  Y)


By

---

Latex:
(Auto
  THEN  MoveToConcl  (-1)
  THEN  All  (RepUR  ``eclass  es-interface-or  eclass-compose2
                  eclass-val  in-eclass  oob-apply``  )\mcdot{}
  THEN  (RepeatFor  2  ((GenConclAtAddr  [1;1;1;1;1;1;1]  THEN  AutoSplit))  THEN  EAuto  1\mcdot{})\mcdot{})

---

Home Index