Nuprl Lemma : DVp_Struct-struct_wf
∀[v:C_DVALUEp()]. DVp_Struct-struct(v) ∈ {a:Atom| (a ∈ DVp_Struct-lbls(v))}  ─→ C_DVALUEp() supposing ↑DVp_Struct?(v)
Proof
Definitions occuring in Statement : 
DVp_Struct-struct: DVp_Struct-struct(v)
, 
DVp_Struct-lbls: DVp_Struct-lbls(v)
, 
DVp_Struct?: DVp_Struct?(v)
, 
C_DVALUEp: C_DVALUEp()
, 
l_member: (x ∈ l)
, 
assert: ↑b
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
set: {x:A| B[x]} 
, 
function: x:A ─→ B[x]
, 
atom: Atom
Lemmas : 
C_DVALUEp-ext, 
eq_atom_wf, 
bool_wf, 
eqtt_to_assert, 
assert_of_eq_atom, 
subtype_base_sq, 
atom_subtype_base, 
unit_wf2, 
unit_subtype_base, 
it_wf, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
list_wf, 
list_subtype_base, 
assert_wf, 
DVp_Struct?_wf, 
C_DVALUEp_wf
\mforall{}[v:C\_DVALUEp()].  DVp\_Struct-struct(v)  \mmember{}  \{a:Atom|  (a  \mmember{}  DVp\_Struct-lbls(v))\}    {}\mrightarrow{}  C\_DVALUEp()  supposin\000Cg  \muparrow{}DVp\_Struct?(v)
Date html generated:
2015_07_17-AM-07_44_54
Last ObjectModification:
2015_01_27-AM-09_45_54
Home
Index