---

Step * of Lemma C_DVALUEp_ind_wf_simple

∀[A:Type]. ∀[v:C_DVALUEp()]. ∀[Null:x:Unit ─→ A]. ∀[Int:int:ℤ ─→ A]. ∀[Pointer:ptr:(C_LVALUE()?) ─→ A].
∀[Array:lower:ℤ ─→ upper:ℤ ─→ arr:({lower..upper-} ─→ C_DVALUEp()) ─→ (u:{lower..upper-} ─→ A) ─→ A].
∀[Struct:lbls:(Atom List) ─→ struct:({a:Atom| (a ∈ lbls)}  ─→ C_DVALUEp()) ─→ (u:{a:Atom| (a ∈ lbls)}  ─→ A) ─→ A].
  (C_DVALUEp_ind(v;
                 DVp_Null(x)⇒ Null[x];
                 DVp_Int(int)⇒ Int[int];
                 DVp_Pointer(ptr)⇒ Pointer[ptr];
                 DVp_Array(lower,upper,arr)⇒ rec1.Array[lower;upper;arr;rec1];
                 DVp_Struct(lbls,struct)⇒ rec2.Struct[lbls;struct;rec2])  ∈ A)
BY
{ ProveDatatypeIndWfSimple 0 `C_DVALUEp_ind_wf` }

---

Latex:


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


By

ProveDatatypeIndWfSimple  0  `C\_DVALUEp\_ind\_wf`

---

Home Index