---

Step * 2 1 of Lemma sqequal-append-cbva-weak2


1. F : Base
2. b : Base
3. z : Base
4. u : Base
5. has-valueall(u)@i
6. has-valueall(z)@i
7. has-valueall(b)@i
⊢ let v ←─ evalall(z) @ evalall(b)
  in F[<evalall(u), v>] ~ let x ←─ [evalall(u) / (evalall(z) @ evalall(b))]
                     in F[x]
BY
{ (Unfold `callbyvalueall` 0
   THEN Reduce 0
   THEN (RWO "evalall-cons" 0 THENA Auto)
   THEN LiftRed
   THEN Fold `callbyvalueall` 0) }

1
1. F : Base
2. b : Base
3. z : Base
4. u : Base
5. has-valueall(u)@i
6. has-valueall(z)@i
7. has-valueall(b)@i
⊢ let v ←─ evalall(z) @ evalall(b)
  in F[<evalall(u), v>] ~ let u ←─ evalall(u)
                     in let v ←─ evalall(z) @ evalall(b)
                        in F[<u, v>]

---

Latex:



1.  F  :  Base
2.  b  :  Base
3.  z  :  Base
4.  u  :  Base
5.  has-valueall(u)@i
6.  has-valueall(z)@i
7.  has-valueall(b)@i
\mvdash{}  let  v  \mleftarrow{}{}  evalall(z)  @  evalall(b)
    in  F[<evalall(u),  v>]  \msim{}  let  x  \mleftarrow{}{}  [evalall(u)  /  (evalall(z)  @  evalall(b))]
                                          in  F[x]


By

(Unfold  `callbyvalueall`  0
  THEN  Reduce  0
  THEN  (RWO  "evalall-cons"  0  THENA  Auto)
  THEN  LiftRed
  THEN  Fold  `callbyvalueall`  0)

---

Home Index