Nuprl 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)


Proof



Definitions occuring in Statement :  C_DVALUEp_ind: C_DVALUEp_ind,  C_DVALUEp: C_DVALUEp(),  C_LVALUE: C_LVALUE(),  l_member: (x ∈ l),  list: T List,  int_seg: {i..j-},  uall: ∀[x:A]. B[x],  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2;s3],  so_apply: x[s],  unit: Unit,  member: t ∈ T,  set: {x:A| B[x]} ,  function: x:A ─→ B[x],  union: left + right,  int: ℤ,  atom: Atom,  universe: Type
Lemmas :  C_DVALUEp_ind_wf,  true_wf,  C_DVALUEp_wf,  subtype_rel_dep_function,  int_seg_wf,  l_member_wf,  set_wf,  list_wf,  C_LVALUE_wf,  unit_wf2
\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)


Date html generated: 2015_07_17-AM-07_45_05
Last ObjectModification: 2015_01_27-AM-09_45_15

Home Index