---

Step * of Lemma normalization-callbyvalueall-spread2

∀[F,G,H,a:Top].
  (let x ⟵ a
   in F[x] let u,v = x in H[x;u;v] let y ⟵ v in G[x;u;v;y] ~ let x ⟵ a
                                                              in F[x] let u,v = x in H[x;u;v] G[x;u;v;v])
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualBase
   THEN UseCbvaSq
   THEN (RWO "evalall-sqequal" 0 THENA Auto)
   THEN Try ((Fold `has-valueall` 0 THEN Auto))) }

1
1. G : Base
2. H : Base
3. F : Base
4. a : Base
5. has-valueall(a)@i
⊢ F[a] let u,v = a in H[a;u;v] let y ⟵ v in G[a;u;v;y] ~ F[a] let u,v = a in H[a;u;v] G[a;u;v;v]

---

Latex:

---

Latex:
\mforall{}[F,G,H,a:Top].
    (let  x  \mleftarrow{}{}  a
      in  F[x]  let  u,v  =  x  in  H[x;u;v]  let  y  \mleftarrow{}{}  v  in  G[x;u;v;y]  \msim{}  let  x  \mleftarrow{}{}  a
                                                                                                                            in  F[x] 
                                                                                                                                  let  u,v  =  x 
                                                                                                                                  in  H[x;u;v]  G[x;u;v;v])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualBase
  THEN  UseCbvaSq
  THEN  (RWO  "evalall-sqequal"  0  THENA  Auto)
  THEN  Try  ((Fold  `has-valueall`  0  THEN  Auto)))

---

Home Index