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
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
implies: P ⇒ Q,
guard: {T},
so_lambda: λ2x.t[x],
member: t ∈ T,
so_apply: x[s1;s2],
subtype_rel: A ⊆r B,
so_apply: x[s],
prop: ℙ,
all: ∀x:A. B[x]
Lemmas referenced :
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
Rules used in proof :
cut,
lemma_by_obid,
sqequalSubstitution,
sqequalTransitivity,
computationStep,
sqequalReflexivity,
isect_memberFormation,
lambdaFormation,
hypothesis,
sqequalHypSubstitution,
isectElimination,
thin,
sqequalRule,
lambdaEquality,
hypothesisEquality,
applyEquality,
because_Cache,
independent_functionElimination,
atomEquality,
functionEquality,
setEquality,
setElimination,
rename,
dependent_set_memberEquality,
intEquality,
unionEquality,
cumulativity,
universeEquality
Latex:
\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:
2016_05_16-AM-08_50_55
Last ObjectModification:
2015_12_28-PM-06_55_20
Theory : C-semantics
Home
Index