---

Step * of Lemma C_TYPE-definition

∀[A:Type]. ∀[R:A ─→ C_TYPE() ─→ ℙ].
  ({x:A| R[x;C_Void()]} 
  ⇒ {x:A| R[x;C_Int()]} 
  ⇒ (∀fields:(Atom × C_TYPE()) List. ((∀u∈fields.let u1,u2 = u in {x:A| R[x;u2]} ) ⇒ {x:A| R[x;C_Struct(fields)]} ))
  ⇒ (∀length:ℕ. ∀elems:C_TYPE().  ({x:A| R[x;elems]}  ⇒ {x:A| R[x;C_Array(length;elems)]} ))
  ⇒ (∀to:C_TYPE(). ({x:A| R[x;to]}  ⇒ {x:A| R[x;C_Pointer(to)]} ))
  ⇒ {∀v:C_TYPE(). {x:A| R[x;v]} })
BY
{ ProveDatatypeDefinition `C_TYPE-induction` }

---

Latex:


\mforall{}[A:Type].  \mforall{}[R:A  {}\mrightarrow{}  C\_TYPE()  {}\mrightarrow{}  \mBbbP{}].
    (\{x:A|  R[x;C\_Void()]\} 
    {}\mRightarrow{}  \{x:A|  R[x;C\_Int()]\} 
    {}\mRightarrow{}  (\mforall{}fields:(Atom  \mtimes{}  C\_TYPE())  List
                ((\mforall{}u\mmember{}fields.let  u1,u2  =  u  in  \{x:A|  R[x;u2]\}  )  {}\mRightarrow{}  \{x:A|  R[x;C\_Struct(fields)]\}  ))
    {}\mRightarrow{}  (\mforall{}length:\mBbbN{}.  \mforall{}elems:C\_TYPE().    (\{x:A|  R[x;elems]\}    {}\mRightarrow{}  \{x:A|  R[x;C\_Array(length;elems)]\}  ))
    {}\mRightarrow{}  (\mforall{}to:C\_TYPE().  (\{x:A|  R[x;to]\}    {}\mRightarrow{}  \{x:A|  R[x;C\_Pointer(to)]\}  ))
    {}\mRightarrow{}  \{\mforall{}v:C\_TYPE().  \{x:A|  R[x;v]\}  \})


By

ProveDatatypeDefinition  `C\_TYPE-induction`

---

Home Index