---

Step * of Lemma C_DVALUEp-induction

∀[P:C_DVALUEp() ⟶ ℙ]
  ((∀x:Unit. P[DVp_Null(x)])
  ⇒ (∀int:ℤ. P[DVp_Int(int)])
  ⇒ (∀ptr:C_LVALUE()?. P[DVp_Pointer(ptr)])
  ⇒ (∀lower,upper:ℤ. ∀arr:{lower..upper-} ⟶ C_DVALUEp().
        ((∀u:{lower..upper-}. P[arr u]) ⇒ P[DVp_Array(lower;upper;arr)]))
  ⇒ (∀lbls:Atom List. ∀struct:{a:Atom| (a ∈ lbls)}  ⟶ C_DVALUEp().
        ((∀u:{a:Atom| (a ∈ lbls)} . P[struct u]) ⇒ P[DVp_Struct(lbls;struct)]))
  ⇒ {∀v:C_DVALUEp(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:

---

Latex:
\mforall{}[P:C\_DVALUEp()  {}\mrightarrow{}  \mBbbP{}]
    ((\mforall{}x:Unit.  P[DVp\_Null(x)])
    {}\mRightarrow{}  (\mforall{}int:\mBbbZ{}.  P[DVp\_Int(int)])
    {}\mRightarrow{}  (\mforall{}ptr:C\_LVALUE()?.  P[DVp\_Pointer(ptr)])
    {}\mRightarrow{}  (\mforall{}lower,upper:\mBbbZ{}.  \mforall{}arr:\{lower..upper\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEp().
                ((\mforall{}u:\{lower..upper\msupminus{}\}.  P[arr  u])  {}\mRightarrow{}  P[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)\}  .  P[struct  u])  {}\mRightarrow{}  P[DVp\_Struct(lbls;struct)]))
    {}\mRightarrow{}  \{\mforall{}v:C\_DVALUEp().  P[v]\})


By

---

Latex:
ProveDatatypeInd

---

Home Index