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


Proof



Definitions occuring in Statement :  C_DVALUEp_ind: C_DVALUEp_ind,  DVp_Struct: DVp_Struct(lbls;struct),  DVp_Array: DVp_Array(lower;upper;arr),  DVp_Pointer: DVp_Pointer(ptr),  DVp_Int: DVp_Int(int),  DVp_Null: DVp_Null(x),  C_DVALUEp: C_DVALUEp(),  C_LVALUE: C_LVALUE(),  l_member: (x ∈ l),  list: T List,  int_seg: {i..j-},  uall: ∀[x:A]. B[x],  prop: ℙ,  so_apply: x[s1;s2;s3;s4],  so_apply: x[s1;s2;s3],  so_apply: x[s1;s2],  so_apply: x[s],  unit: Unit,  member: t ∈ T,  set: {x:A| B[x]} ,  apply: f a,  function: x:A ─→ B[x],  union: left + right,  int: ℤ,  atom: Atom,  universe: Type
Lemmas :  top_wf,  has-value_wf_base,  lifting-strict-atom_eq,  base_wf,  unit_wf2,  DVp_Null_wf,  DVp_Int_wf,  C_LVALUE_wf,  DVp_Pointer_wf,  int_seg_wf,  C_DVALUEp_wf,  DVp_Array_wf,  list_wf,  l_member_wf,  DVp_Struct_wf,  all_wf,  set_wf,  subtype_rel-equal
\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]\}  )


Date html generated: 2015_07_17-AM-07_45_04
Last ObjectModification: 2015_01_29-PM-04_39_25

Home Index