---

Step * 1 1 of Lemma C_Struct_vs_DVALp


1. store : C_STOREp()@i
2. fields : (Atom × C_TYPE()) List@i
3. (∀u∈fields.let u1,u2 = u 
              in ∀env:C_TYPE_env(). ∀dval:C_DVALUEp().
                   (C_STOREp-welltyped(env;store)
                   ⇒ (↑C_Struct?(u2))
                   ⇒ C_TYPE_vs_DVALp(env;u2) dval 
                      = if DVp_Struct?(dval)
                        then (∀p∈map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;C_Struct-fields(u2)).
                                let a,wt = p 
                                in a ∈b DVp_Struct-lbls(dval)) ∧b (wt (DVp_Struct-struct(dval) a)))_b
                        else ff
                        fi ))@i
4. env : C_TYPE_env()@i
5. lbls : Atom List
6. d2 : {a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()
7. C_STOREp-welltyped(env;store)@i
8. True@i
9. True
⊢ ∀i:ℕ||fields||. (↑eval a = fst(fields[i]) in a ∈b lbls) ∧b (let v2,v3 = fields[i] in C_TYPE_vs_DVALp(env;v3) (d2 a)))
⇐⇒ (∀p∈map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;fields).↑let a,wt = p 
                                                              in a ∈b lbls) ∧b (wt (d2 a)))
BY
{ All Thin }

1
1. fields : (Atom × C_TYPE()) List@i
2. env : C_TYPE_env()@i
3. lbls : Atom List
4. d2 : {a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()
⊢ ∀i:ℕ||fields||. (↑eval a = fst(fields[i]) in a ∈b lbls) ∧b (let v2,v3 = fields[i] in C_TYPE_vs_DVALp(env;v3) (d2 a)))
⇐⇒ (∀p∈map(λp.<fst(p), C_TYPE_vs_DVALp(env;snd(p))>;fields).↑let a,wt = p 
                                                              in a ∈b lbls) ∧b (wt (d2 a)))

---

Latex:



1.  store  :  C\_STOREp()@i
2.  fields  :  (Atom  \mtimes{}  C\_TYPE())  List@i
3.  (\mforall{}u\mmember{}fields.let  u1,u2  =  u 
                            in  \mforall{}env:C\_TYPE\_env().  \mforall{}dval:C\_DVALUEp().
                                      (C\_STOREp-welltyped(env;store)
                                      {}\mRightarrow{}  (\muparrow{}C\_Struct?(u2))
                                      {}\mRightarrow{}  C\_TYPE\_vs\_DVALp(env;u2)  dval 
                                            =  if  DVp\_Struct?(dval)
                                                then  (\mforall{}p\mmember{}map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>C\_Struct-fields(u2)).
                                                                let  a,wt  =  p 
                                                                in  a  \mmember{}\msubb{}  DVp\_Struct-lbls(dval))
                                                                      \mwedge{}\msubb{}  (wt  (DVp\_Struct-struct(dval)  a)))\_b
                                                else  ff
                                                fi  ))@i
4.  env  :  C\_TYPE\_env()@i
5.  lbls  :  Atom  List
6.  d2  :  \{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp()
7.  C\_STOREp-welltyped(env;store)@i
8.  True@i
9.  True
\mvdash{}  \mforall{}i:\mBbbN{}||fields||
        (\muparrow{}eval  a  =  fst(fields[i])  in
            a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (let  v2,v3  =  fields[i]  in  C\_TYPE\_vs\_DVALp(env;v3)  (d2  a)))
\mLeftarrow{}{}\mRightarrow{}  (\mforall{}p\mmember{}map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>fields).\muparrow{}let  a,wt  =  p 
                                                                                                                            in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (wt  (d2  a)))


By

All  Thin

---

Home Index