---

Step * 1 3 of Lemma C_TYPE-valueall-type


1. length : ℕ
2. v2 : C_TYPE()
3. (evalall(v2))↓
⊢ (eval b' = evalall(<length, v2>) in
   <evalall("Array"), b'>)↓
BY
{ ((Assert valueall-type(ℕ) BY
          Auto)
   THEN RecUnfold `evalall` 0
   THEN Reduce 0
   THEN (CallByValueReduceOn ⌜evalall(length)⌝ 0⋅ THENA Auto)
   THEN (CallByValueReduceOn ⌜evalall(v2)⌝ 0⋅ THENA Auto)
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  length  :  \mBbbN{}
2.  v2  :  C\_TYPE()
3.  (evalall(v2))\mdownarrow{}
\mvdash{}  (eval  b'  =  evalall(<length,  v2>)  in
      <evalall("Array"),  b'>)\mdownarrow{}


By

---

Latex:
((Assert  valueall-type(\mBbbN{})  BY
                Auto)
  THEN  RecUnfold  `evalall`  0
  THEN  Reduce  0
  THEN  (CallByValueReduceOn  \mkleeneopen{}evalall(length)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  (CallByValueReduceOn  \mkleeneopen{}evalall(v2)\mkleeneclose{}  0\mcdot{}  THENA  Auto)
  THEN  Reduce  0
  THEN  Auto)

---

Home Index