---

Step * of Lemma C_DVALUEp-definition

∀[A:Type]. ∀[R:A ─→ C_DVALUEp() ─→ ℙ].
  ((∀x:Unit. {x1:A| R[x1;DVp_Null(x)]} )
  ⇒ (∀int:ℤ. {x:A| R[x;DVp_Int(int)]} )
  ⇒ (∀ptr:C_LVALUE()?. {x:A| R[x;DVp_Pointer(ptr)]} )
  ⇒ (∀lower,upper:ℤ. ∀arr:{lower..upper-} ─→ C_DVALUEp().
        ((∀u:{lower..upper-}. {x:A| R[x;arr u]} ) ⇒ {x:A| R[x;DVp_Array(lower;upper;arr)]} ))
  ⇒ (∀lbls:Atom List. ∀struct:{a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp().
        ((∀u:{a:Atom| (a ∈ lbls)} . {x:A| R[x;struct u]} ) ⇒ {x:A| R[x;DVp_Struct(lbls;struct)]} ))
  ⇒ {∀v:C_DVALUEp(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `C_DVALUEp-induction` }

---

Latex:


\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  C\_DVALUEp()  {}\mrightarrow{}  \mBbbP{}].
    ((\mforall{}x:Unit.  \{x1:A|  R[x1;DVp\_Null(x)]\}  )
    {}\mRightarrow{}  (\mforall{}int:\mBbbZ{}.  \{x:A|  R[x;DVp\_Int(int)]\}  )
    {}\mRightarrow{}  (\mforall{}ptr:C\_LVALUE()?.  \{x:A|  R[x;DVp\_Pointer(ptr)]\}  )
    {}\mRightarrow{}  (\mforall{}lower,upper:\mBbbZ{}.  \mforall{}arr:\{lower..upper\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEp().
                ((\mforall{}u:\{lower..upper\msupminus{}\}.  \{x:A|  R[x;arr  u]\}  )  {}\mRightarrow{}  \{x:A|  R[x;DVp\_Array(lower;upper;arr)]\}  ))
    {}\mRightarrow{}  (\mforall{}lbls:Atom  List.  \mforall{}struct:\{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  C\_DVALUEp().
                ((\mforall{}u:\{a:Atom|  (a  \mmember{}  lbls)\}  .  \{x:A|  R[x;struct  u]\}  )  {}\mRightarrow{}  \{x:A|  R[x;DVp\_Struct(lbls;struct)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:C\_DVALUEp().  \{x:A|  R[x;v]\}  \})


By

ProveDatatypeDefinition  `C\_DVALUEp-induction`

---

Home Index