Nuprl Lemma : C_DVALUEp-definition
∀[A:Type]. ∀[R:A ─→ C_DVALUEp() ─→ ℙ].
((∀x:Unit. {x1:A| R[x1;DVp_Null(x)]} )
⇒ (∀int:ℤ. {x:A| R[x;DVp_Int(int)]} )
⇒ (∀ptr:C_LVALUE()?. {x:A| R[x;DVp_Pointer(ptr)]} )
⇒ (∀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)]} ))
⇒ (∀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)]} ))
⇒ {∀v:C_DVALUEp(). {x:A| R[x;v]} })
Proof
Definitions occuring in Statement :
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: ℙ,
guard: {T},
so_apply: x[s1;s2],
all: ∀x:A. B[x],
implies: P ⇒ Q,
unit: Unit,
set: {x:A| B[x]} ,
apply: f a,
function: x:A ─→ B[x],
union: left + right,
int: ℤ,
atom: Atom,
universe: Type
Lemmas :
C_DVALUEp-induction,
set_wf,
C_DVALUEp_wf,
all_wf,
list_wf,
l_member_wf,
DVp_Struct_wf,
int_seg_wf,
DVp_Array_wf,
C_LVALUE_wf,
unit_wf2,
DVp_Pointer_wf,
DVp_Int_wf,
DVp_Null_wf
\mforall{}[A:Type]. \mforall{}[R:A {}\mrightarrow{} C\_DVALUEp() {}\mrightarrow{} \mBbbP{}].
((\mforall{}x:Unit. \{x1:A| R[x1;DVp\_Null(x)]\} )
{}\mRightarrow{} (\mforall{}int:\mBbbZ{}. \{x:A| R[x;DVp\_Int(int)]\} )
{}\mRightarrow{} (\mforall{}ptr:C\_LVALUE()?. \{x:A| R[x;DVp\_Pointer(ptr)]\} )
{}\mRightarrow{} (\mforall{}lower,upper:\mBbbZ{}. \mforall{}arr:\{lower..upper\msupminus{}\} {}\mrightarrow{} C\_DVALUEp().
((\mforall{}u:\{lower..upper\msupminus{}\}. \{x:A| R[x;arr u]\} ) {}\mRightarrow{} \{x:A| R[x;DVp\_Array(lower;upper;arr)]\} ))
{}\mRightarrow{} (\mforall{}lbls:Atom List. \mforall{}struct:\{a:Atom| (a \mmember{} lbls)\} {}\mrightarrow{} C\_DVALUEp().
((\mforall{}u:\{a:Atom| (a \mmember{} lbls)\} . \{x:A| R[x;struct u]\} ) {}\mRightarrow{} \{x:A| R[x;DVp\_Struct(lbls;struct)]\} ))
{}\mRightarrow{} \{\mforall{}v:C\_DVALUEp(). \{x:A| R[x;v]\} \})
Date html generated:
2015_07_17-AM-07_44_59
Last ObjectModification:
2015_01_27-AM-09_45_28
Home
Index