Nuprl Definition : bm_exists_downeq
bm_exists_downeq(compare;m;k;p) ==
binary_map_ind(m;ff;key,value,cnt,left,right,recL,recR.if 0 ≤z compare key k
then p[value] ∨bbm_exists(left;p) ∨brecR
else recL
fi )
Definitions occuring in Statement :
bm_exists: bm_exists(m;p),
binary_map_ind: binary_map_ind(v;E;key,value,cnt,left,right,rec1,rec2.T[key;value;cnt;left;right;rec1;rec2]),
le_int: i ≤z j,
bor: p ∨bq,
ifthenelse: if b then t else f fi ,
bfalse: ff,
so_apply: x[s],
apply: f a,
natural_number: $n
FDL editor aliases :
bm_exists_downeq
Latex:
bm\_exists\_downeq(compare;m;k;p) ==
binary\_map\_ind(m;ff;key,value,cnt,left,right,recL,recR.if 0 \mleq{}z compare key k
then p[value] \mvee{}\msubb{}bm\_exists(left;p) \mvee{}\msubb{}recR
else recL
fi )
Date html generated:
2016_05_17-PM-01_42_01
Last ObjectModification:
2012_09_13-PM-00_34_41
Theory : binary-map
Home
Index