---

Step * of Lemma normalization-callbyvalueall-spread1

∀[F,G,H,a:Top].
  (let x ⟵ a
   in F[x] let u,v = x in H[x;u;v] let y ⟵ u 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;u])
BY
{ ((UnivCD THENA Auto)
   THEN SqEqualBase
   THEN UseCbvaSq
   THEN EqCD
   THEN Try (Trivial)
   THEN RWO  "evalall-sqequal" 0
   THEN Try (Fold `has-valueall` 0)
   THEN Try (Complete (Auto))
   THEN SqequalSqle
   THEN AssumeHasValue
   THEN (HasValueD (-1)⋅ ORELSE (ExceptionCases (-1) THEN Try (Complete (SameException))))
   THEN (InstLemma `pair-eta` [⌜a⌝]⋅ THENA Auto)
   THEN (HypSubst' -1 0 THEN Reduce 0)
   THEN CallByValueReduce 0
   THEN Auto
   THEN (Assert has-valueall(<fst(a), snd(a)>) BY
               (RevHypSubst (-1) 0 THEN Hypothesis))
   THEN FLemma `has-valueall-pair` [-1]
   THEN Auto) }

---

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{}{}  u  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;u])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  SqEqualBase
  THEN  UseCbvaSq
  THEN  EqCD
  THEN  Try  (Trivial)
  THEN  RWO    "evalall-sqequal"  0
  THEN  Try  (Fold  `has-valueall`  0)
  THEN  Try  (Complete  (Auto))
  THEN  SqequalSqle
  THEN  AssumeHasValue
  THEN  (HasValueD  (-1)\mcdot{}  ORELSE  (ExceptionCases  (-1)  THEN  Try  (Complete  (SameException))))
  THEN  (InstLemma  `pair-eta`  [\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (HypSubst'  -1  0  THEN  Reduce  0)
  THEN  CallByValueReduce  0
  THEN  Auto
  THEN  (Assert  has-valueall(<fst(a),  snd(a)>)  BY
                          (RevHypSubst  (-1)  0  THEN  Hypothesis))
  THEN  FLemma  `has-valueall-pair`  [-1]
  THEN  Auto)

---

Home Index