---

Step * 1 1 1 2 of Lemma C_Struct_vs_DVALp


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)))
BY
{ (RWO "l_all_cons" 0 THENA Auto) }

1
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)))
⇐⇒ (↑let a,wt = <fst(u), C_TYPE_vs_DVALp(env;snd(u))> 
      in a ∈b lbls) ∧b (wt (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)))

---

Latex:



1.  env  :  C\_TYPE\_env()@i
2.  lbls  :  Atom  List
3.  d2  :  \{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp()
4.  u  :  Atom  \mtimes{}  C\_TYPE()@i
5.  v  :  (Atom  \mtimes{}  C\_TYPE())  List@i
6.  \mforall{}i:\mBbbN{}||v||
          (\muparrow{}eval  a  =  fst(v[i])  in
              a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (let  v2,v3  =  v[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))>v).\muparrow{}let  a,wt  =  p 
                                                                                                                  in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (wt  (d2  a)))@i
\mvdash{}  \mforall{}i:\mBbbN{}||v||  +  1
        (\muparrow{}eval  a  =  fst([u  /  v][i])  in
            a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (let  v2,v3  =  [u  /  v][i]  in  C\_TYPE\_vs\_DVALp(env;v3)  (d2  a)))
\mLeftarrow{}{}\mRightarrow{}  (\mforall{}p\mmember{}[<fst(u),  C\_TYPE\_vs\_DVALp(env;snd(u))>  /  map(\mlambda{}p.<fst(p),  C\_TYPE\_vs\_DVALp(env;snd(p))>v)].
              \muparrow{}let  a,wt  =  p 
                in  a  \mmember{}\msubb{}  lbls)  \mwedge{}\msubb{}  (wt  (d2  a)))


By

(RWO  "l\_all\_cons"  0  THENA  Auto)

---

Home Index