---

Step * of Lemma es-interface-val-conditional

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X,Y:EClass(A)]. ∀[e:E].
  [X?Y](e) = if e ∈b X then X(e) else Y(e) fi  ∈ A supposing ↑e ∈b [X?Y]
BY
{ (RepeatFor 6 ((D 0 THENA Auto))
   THEN (All (RepUR ``cond-class in-eclass eclass-val eclass-compose2``))
   THEN Folds ``in-eclass`` 0
   THEN AutoSplit
   THEN (RW assert_pushdownC 0 THEN Auto THEN BLemma `single-valued-bag-if-le1` THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X,Y:EClass(A)].  \mforall{}[e:E].
    [X?Y](e)  =  if  e  \mmember{}\msubb{}  X  then  X(e)  else  Y(e)  fi    supposing  \muparrow{}e  \mmember{}\msubb{}  [X?Y]


By

---

Latex:
(RepeatFor  6  ((D  0  THENA  Auto))
  THEN  (All  (RepUR  ``cond-class  in-eclass  eclass-val  eclass-compose2``))
  THEN  Folds  ``in-eclass``  0
  THEN  AutoSplit
  THEN  (RW  assert\_pushdownC  0  THEN  Auto  THEN  BLemma  `single-valued-bag-if-le1`  THEN  Auto)\mcdot{})

---

Home Index