---

Step * 1 1 1 of Lemma C_Struct_vs_DVALp


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)))
BY
{ (ListInd 1 THEN Reduce 0) }

1
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)))

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

---

Latex:



1.  fields  :  (Atom  \mtimes{}  C\_TYPE())  List@i
2.  env  :  C\_TYPE\_env()@i
3.  lbls  :  Atom  List
4.  d2  :  \{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp()
\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

(ListInd  1  THEN  Reduce  0)

---

Home Index