---

Step * of Lemma C_TYPE-induction

∀[P:C_TYPE() ─→ ℙ]
  (P[C_Void()]
  ⇒ P[C_Int()]
  ⇒ (∀fields:(Atom × C_TYPE()) List. ((∀u∈fields.let u1,u2 = u in P[u2]) ⇒ P[C_Struct(fields)]))
  ⇒ (∀length:ℕ. ∀elems:C_TYPE().  (P[elems] ⇒ P[C_Array(length;elems)]))
  ⇒ (∀to:C_TYPE(). (P[to] ⇒ P[C_Pointer(to)]))
  ⇒ {∀v:C_TYPE(). P[v]})
BY
{ ProveDatatypeInd }

---

Latex:


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


By

ProveDatatypeInd

---

Home Index