---

Step * of Lemma callbyvalueall-reduce-repeat-right-branch

∀[a,d,F,G:Top].
  (let x ⟵ a
   in case d[x] of inl(u) => F[x;u] | inr(v) => let y ⟵ x in G[y;v] ~ let x ⟵ a
                                                                       in case d[x]
                                                                        of inl(u) =>
                                                                        F[x;u]
                                                                        | inr(v) =>
                                                                        G[x;v])
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualBase
   THEN UseCbvaSq
   THEN RWO "evalall-sqequal" 0
   THEN Auto
   THEN CallByValueReduce 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,d,F,G:Top].
    (let  x  \mleftarrow{}{}  a
      in  case  d[x]  of  inl(u)  =>  F[x;u]  |  inr(v)  =>  let  y  \mleftarrow{}{}  x  in  G[y;v]  \msim{}  let  x  \mleftarrow{}{}  a
                                                                                                                                              in  case  d[x]
                                                                                                                                                of  inl(u)  =>
                                                                                                                                                F[x;u]
                                                                                                                                                |  inr(v)  =>
                                                                                                                                                G[x;v])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualBase
  THEN  UseCbvaSq
  THEN  RWO  "evalall-sqequal"  0
  THEN  Auto
  THEN  CallByValueReduce  0
  THEN  Auto)

---

Home Index