---

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


1. u : Top
2. v : Top List
3. ∀[b,F:Top].  (let x ⟵ v @ b in F[x] ~ let u ⟵ v in let v ⟵ b in let x ⟵ u @ v in F[x])
⊢ ∀[b,F:Top].  (let x ⟵ [u / v] @ b in F[x] ~ let u ⟵ [u / v] in let v ⟵ b in let x ⟵ u @ v in F[x])
BY
{ ((UnivCD THENA Auto)
   THEN Unfold `callbyvalueall` 0
   THEN Reduce 0
   THEN (RWO "evalall-cons" 0 THENA Auto)
   THEN LiftRed
   THEN Fold `callbyvalueall` 0
   THEN (RWO "3" 0 THENA Auto)
   THEN (GenConcl ⌜v = z ∈ Top⌝⋅ THENA Auto)
   THEN All Thin
   THEN SqEqualBase
   THEN RepeatFor 3 (UseCbvaSq)) }

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 x ⟵ [evalall(u) / (evalall(z) @ evalall(b))]
                     in F[x]

---

Latex:

---

Latex:

1.  u  :  Top
2.  v  :  Top  List
3.  \mforall{}[b,F:Top].    (let  x  \mleftarrow{}{}  v  @  b  in  F[x]  \msim{}  let  u  \mleftarrow{}{}  v  in  let  v  \mleftarrow{}{}  b  in  let  x  \mleftarrow{}{}  u  @  v  in  F[x])
\mvdash{}  \mforall{}[b,F:Top].
        (let  x  \mleftarrow{}{}  [u  /  v]  @  b
          in  F[x]  \msim{}  let  u  \mleftarrow{}{}  [u  /  v]
                              in  let  v  \mleftarrow{}{}  b
                                    in  let  x  \mleftarrow{}{}  u  @  v
                                          in  F[x])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `callbyvalueall`  0
  THEN  Reduce  0
  THEN  (RWO  "evalall-cons"  0  THENA  Auto)
  THEN  LiftRed
  THEN  Fold  `callbyvalueall`  0
  THEN  (RWO  "3"  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}v  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  SqEqualBase
  THEN  RepeatFor  3  (UseCbvaSq))

---

Home Index