---

Step * 1 2 of Lemma C_TYPE-valueall-type


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

1
.....assertion..... 
1. v1 : (Atom × C_TYPE()) List
2. ∀i:ℕ||v1||. (evalall(snd(v1[i])))↓
⊢ (evalall(v1))↓

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

---

Latex:

---

Latex:

1.  v1  :  (Atom  \mtimes{}  C\_TYPE())  List
2.  \mforall{}i:\mBbbN{}||v1||.  (evalall(snd(v1[i])))\mdownarrow{}
\mvdash{}  (eval  b'  =  evalall(v1)  in
      <evalall("Struct"),  b'>)\mdownarrow{}


By

---

Latex:
Assert  \mkleeneopen{}(evalall(v1))\mdownarrow{}\mkleeneclose{}\mcdot{}

---

Home Index