Nuprl Lemma : C_TYPE_eq_fun_wf
∀[a:C_TYPE()]. (C_TYPE_eq_fun(a) ∈ C_TYPE() ─→ 𝔹)
Proof
Definitions occuring in Statement : 
C_TYPE_eq_fun: C_TYPE_eq_fun(a)
, 
C_TYPE: C_TYPE()
, 
bool: 𝔹
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
function: x:A ─→ B[x]
Lemmas : 
C_TYPE_ind_wf_simple, 
C_TYPE_wf, 
bool_wf, 
C_Void?_wf, 
C_Int?_wf, 
eqtt_to_assert, 
eq_int_wf, 
length_wf, 
C_Struct-fields_wf, 
assert_of_eq_int, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
subtype_base_sq, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_int, 
bfalse_wf, 
l_all_wf2, 
l_member_wf, 
list_wf, 
C_Array?_wf, 
C_Array-length_wf, 
nat_wf, 
C_Array-elems_wf, 
C_Pointer?_wf, 
C_Pointer-to_wf, 
eq_atom_wf, 
select_wf, 
sq_stable__le, 
less_than_transitivity1, 
le_weakening, 
int_seg_wf, 
upto_wf, 
bl-all_wf, 
band_wf, 
lelt_wf, 
subtype_rel-equal
\mforall{}[a:C\_TYPE()].  (C\_TYPE\_eq\_fun(a)  \mmember{}  C\_TYPE()  {}\mrightarrow{}  \mBbbB{})
Date html generated:
2015_07_17-AM-07_42_45
Last ObjectModification:
2015_01_27-AM-09_47_12
Home
Index