---

Step * 1 4 of Lemma C_TYPE-valueall-type


1. v1 : C_TYPE()
2. (evalall(v1))↓
⊢ (eval b' = evalall(v1) in
   <evalall("Pointer"), b'>)↓
BY
{ ((CallByValueReduce 0⋅ THENA Auto) THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:

1.  v1  :  C\_TYPE()
2.  (evalall(v1))\mdownarrow{}
\mvdash{}  (eval  b'  =  evalall(v1)  in
      <evalall("Pointer"),  b'>)\mdownarrow{}


By

---

Latex:
((CallByValueReduce  0\mcdot{}  THENA  Auto)  THEN  Reduce  0  THEN  Auto)

---

Home Index