Nuprl Definition : bm_exists
bm_exists(m;p) == binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.p[value] ∨brecL ∨brecR)
Definitions occuring in Statement :
binary_map_ind: binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]),
bor: p ∨bq,
bfalse: ff,
so_apply: x[s]
FDL editor aliases :
bm_exists
bm\_exists(m;p) == binary\_map\_ind(m;ff;key,value,cnt,left,right,recL,recR.p[value] \mvee{}\msubb{}recL \mvee{}\msubb{}recR)
Date html generated:
2015_07_17-AM-08_19_54
Last ObjectModification:
2012_09_13-AM-01_06_34
Home
Index