---

Step * of Lemma C_DVALUEp_ind_wf

∀[A:Type]. ∀[R:A ─→ C_DVALUEp() ─→ ℙ]. ∀[v:C_DVALUEp()]. ∀[Null:x:Unit ─→ {x1:A| R[x1;DVp_Null(x)]} ].
∀[Int:int:ℤ ─→ {x:A| R[x;DVp_Int(int)]} ]. ∀[Pointer:ptr:(C_LVALUE()?) ─→ {x:A| R[x;DVp_Pointer(ptr)]} ].
∀[Array: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)]} ]. ∀[Struct: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)]} ].
  (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])  ∈ {x:A| R[x;v]} )
BY
{ ProveDatatypeIndWf TERMOF{C_DVALUEp-definition:o, 1:l, i:l}⋅ }

---

Latex:


\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  C\_DVALUEp()  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[v:C\_DVALUEp()].
\mforall{}[Null:x:Unit  {}\mrightarrow{}  \{x1:A|  R[x1;DVp\_Null(x)]\}  ].  \mforall{}[Int:int:\mBbbZ{}  {}\mrightarrow{}  \{x:A|  R[x;DVp\_Int(int)]\}  ].
\mforall{}[Pointer:ptr:(C\_LVALUE()?)  {}\mrightarrow{}  \{x:A|  R[x;DVp\_Pointer(ptr)]\}  ].
\mforall{}[Array:lower:\mBbbZ{}
                {}\mrightarrow{}  upper:\mBbbZ{}
                {}\mrightarrow{}  arr:(\{lower..upper\msupminus{}\}  {}\mrightarrow{}  C\_DVALUEp())
                {}\mrightarrow{}  (u:\{lower..upper\msupminus{}\}  {}\mrightarrow{}  \{x:A|  R[x;arr  u]\}  )
                {}\mrightarrow{}  \{x:A|  R[x;DVp\_Array(lower;upper;arr)]\}  ].  \mforall{}[Struct:lbls:(Atom  List)
                                                                                                                          {}\mrightarrow{}  struct:(\{a:Atom|  (a  \mmember{}  lbls)\} 
                                                                                                                                              {}\mrightarrow{}  C\_DVALUEp())
                                                                                                                          {}\mrightarrow{}  (u:\{a:Atom|  (a  \mmember{}  lbls)\}    {}\mrightarrow{}  \{x:A| 
                                                                                                                                                                                  R[x;struct 
                                                                                                                                                                                          u]\}  )
                                                                                                                          {}\mrightarrow{}  \{x:A| 
                                                                                                                                  R[x;DVp\_Struct(lbls;struct)]\}  ].
    (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{}  \{x:A|  R[x;v]\}  )


By

ProveDatatypeIndWf  TERMOF\{C\_DVALUEp-definition:o,  1:l,  i:l\}\mcdot{}

---

Home Index