Nuprl Lemma : C_type_of_field_wf
∀[ctyp:{t:C_TYPE()| ↑C_Struct?(t)} ]. ∀[a:{c:Atom| ↑C_field_of(c;ctyp)} ]. (C_type_of_field(a;ctyp) ∈ C_TYPE())
Proof
Definitions occuring in Statement :
C_type_of_field: C_type_of_field(a;ctyp),
C_field_of: C_field_of(a;ctyp),
C_Struct?: C_Struct?(v),
C_TYPE: C_TYPE(),
assert: ↑b,
uall: ∀[x:A]. B[x],
member: t ∈ T,
set: {x:A| B[x]} ,
atom: Atom
Lemmas :
outl_wf,
apply-alist_wf,
C_Struct-fields_wf,
set_wf,
assert_wf,
C_field_of_wf,
C_TYPE_wf,
C_Struct?_wf,
assert-deq-member,
atom-deq_wf,
map_wf,
apply-alist-cases,
subtype_rel_list,
top_wf,
subtype_rel_product,
subtype_top,
l_member-first,
length_wf,
non_neg_length,
length_wf_nat,
map_length,
lelt_wf,
equal-wf-T-base,
select_wf,
sq_stable__le,
atom_subtype_base,
int_seg_wf,
pi1_wf_top,
not_wf,
squash_wf,
true_wf,
equal_wf,
map_select,
iff_weakening_equal
\mforall{}[ctyp:\{t:C\_TYPE()| \muparrow{}C\_Struct?(t)\} ]. \mforall{}[a:\{c:Atom| \muparrow{}C\_field\_of(c;ctyp)\} ].
(C\_type\_of\_field(a;ctyp) \mmember{} C\_TYPE())
Date html generated:
2015_07_17-AM-07_43_39
Last ObjectModification:
2015_02_03-PM-09_38_37
Home
Index