---

Step * 1 1 1 1 of Lemma C_Struct_vs_DVALp


1. env : C_TYPE_env()@i
2. lbls : Atom List
3. d2 : {a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()
⊢ ∀i:ℕ0. (↑eval a = fst(⊥) in a ∈b lbls) ∧b (let v2,v3 = ⊥ in C_TYPE_vs_DVALp(env;v3) (d2 a)))
⇐⇒ (∀p∈[].↑let a,wt = p 
            in a ∈b lbls) ∧b (wt (d2 a)))
BY
{ Auto }

---

Latex:



1.  env  :  C\_TYPE\_env()@i
2.  lbls  :  Atom  List
3.  d2  :  \{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp()
\mvdash{}  \mforall{}i:\mBbbN{}0.  (\muparrow{}eval  a  =  fst(\mbot{})  in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (let  v2,v3  =  \mbot{}  in  C\_TYPE\_vs\_DVALp(env;v3)  (d2  a)))
\mLeftarrow{}{}\mRightarrow{}  (\mforall{}p\mmember{}[].\muparrow{}let  a,wt  =  p 
                        in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (wt  (d2  a)))


By

Auto

---

Home Index