---

Step * 2 1 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 u ←─ evalall(u)
                     in let v ←─ evalall(z) @ evalall(b)
                        in F[<u, v>]
BY
{ ((RWO "evalall-sqequal" 0 THENA Auto) THEN Try ((Fold `has-valueall` 0 THEN Auto))) }

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 ←─ z @ b
  in F[<u, v>] ~ let u ←─ u
            in let v ←─ z @ 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  u  \mleftarrow{}{}  evalall(u)
                                          in  let  v  \mleftarrow{}{}  evalall(z)  @  evalall(b)
                                                in  F[<u,  v>]


By

((RWO  "evalall-sqequal"  0  THENA  Auto)  THEN  Try  ((Fold  `has-valueall`  0  THEN  Auto)))

---

Home Index