Nuprl Lemma : bm_double_R_wf
∀[T,Key:Type]. ∀[c:Key]. ∀[cv:T]. ∀[m,z:binary-map(T;Key)].
  (bm_double_R(c;cv;m;z) ∈ binary-map(T;Key)) supposing ((↑bm_T?(bm_T-right(m))) and (↑bm_T?(m)))
Proof
Definitions occuring in Statement : 
bm_double_R: bm_double_R(c;cv;m;z)
, 
binary-map: binary-map(T;Key)
, 
bm_T-right: bm_T-right(v)
, 
bm_T?: bm_T?(v)
, 
assert: ↑b
, 
uimplies: b supposing a
, 
uall: ∀[x:A]. B[x]
, 
member: t ∈ T
, 
universe: Type
Lemmas : 
binary_map-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, 
bm_cnt_prop_E_reduce_lemma, 
binary_map_case_E_reduce_lemma, 
eqff_to_assert, 
equal_wf, 
bool_cases_sqequal, 
bool_subtype_base, 
assert-bnot, 
neg_assert_of_eq_atom, 
binary_map_case_T_reduce_lemma, 
bm_cnt_prop_T, 
bm_T_wf, 
bm_N_wf, 
assert_wf, 
bm_cnt_prop_wf, 
bm_T?_wf, 
bm_T-right_wf, 
binary-map_wf
\mforall{}[T,Key:Type].  \mforall{}[c:Key].  \mforall{}[cv:T].  \mforall{}[m,z:binary-map(T;Key)].
    (bm\_double\_R(c;cv;m;z)  \mmember{}  binary-map(T;Key))  supposing  ((\muparrow{}bm\_T?(bm\_T-right(m)))  and  (\muparrow{}bm\_T?(m)))
Date html generated:
2015_07_17-AM-08_19_03
Last ObjectModification:
2015_01_27-PM-00_37_06
Home
Index