---

Step * 1 of Lemma C_TYPE-valueall-type


1. v : C_TYPE()@i
⊢ (evalall(v))↓
BY
{ (SimpleDatatypeInduction 1
   THEN RepUR ``C_Void C_Int C_Struct C_Array C_Pointer`` 0
   THEN Try ((RecUnfold `evalall` 0 THEN Reduce 0))) }

1
1. sz : ℕ
2. ∀sz:ℕsz. ∀v:C_TYPE().  (evalall(v))↓ supposing C_TYPE_size(v) ≤ sz
3. 0 ≤ sz
⊢ 0 ≤ 0

2
1. v1 : (Atom × C_TYPE()) List
2. ∀i:ℕ||v1||. (evalall(snd(v1[i])))↓
⊢ (eval b' = evalall(v1) in
   <evalall("Struct"), b'>)↓

3
1. length : ℕ
2. v2 : C_TYPE()
3. (evalall(v2))↓
⊢ (eval b' = evalall(<length, v2>) in
   <evalall("Array"), b'>)↓

4
1. v1 : C_TYPE()
2. (evalall(v1))↓
⊢ (eval b' = evalall(v1) in
   <evalall("Pointer"), b'>)↓

---

Latex:



1.  v  :  C\_TYPE()@i
\mvdash{}  (evalall(v))\mdownarrow{}


By

(SimpleDatatypeInduction  1
  THEN  RepUR  ``C\_Void  C\_Int  C\_Struct  C\_Array  C\_Pointer``  0
  THEN  Try  ((RecUnfold  `evalall`  0  THEN  Reduce  0)))

---

Home Index