### Nuprl 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]} })`

Proof

Definitions occuring in Statement :  C_Pointer: `C_Pointer(to)` C_Array: `C_Array(length;elems)` C_Struct: `C_Struct(fields)` C_Int: `C_Int()` C_Void: `C_Void()` C_TYPE: `C_TYPE()` l_all: `(∀x∈L.P[x])` list: `T List` nat: `ℕ` uall: `∀[x:A]. B[x]` prop: `ℙ` guard: `{T}` so_apply: `x[s1;s2]` all: `∀x:A. B[x]` implies: `P `` Q` set: `{x:A| B[x]} ` function: `x:A ─→ B[x]` spread: spread def product: `x:A × B[x]` atom: `Atom` universe: `Type`
Lemmas :  C_TYPE-induction set_wf all_wf C_TYPE_wf C_Pointer_wf nat_wf C_Array_wf list_wf l_all_wf2 l_member_wf C_Struct_wf C_Int_wf C_Void_wf
\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]\}  \})

Date html generated: 2015_07_17-AM-07_42_31
Last ObjectModification: 2015_01_27-AM-09_47_04

Home Index