Nuprl Lemma : bm_unionWith_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m1,m2:binary-map(T;Key)]. ∀[f:T ─→ T ─→ T].
(bm_unionWith(compare;f;m1;m2) ∈ binary-map(T;Key))
Proof
Definitions occuring in Statement :
bm_unionWith: bm_unionWith(compare;f;m1;m2),
bm_compare: bm_compare(K),
binary-map: binary-map(T;Key),
uall: ∀[x:A]. B[x],
member: t ∈ T,
function: x:A ─→ B[x],
universe: Type
Lemmas :
lt_int_wf,
bm_numItems_wf,
bool_wf,
uiff_transitivity,
equal-wf-T-base,
assert_wf,
less_than_wf,
eqtt_to_assert,
assert_of_lt_int,
bm_foldli_wf,
bm_unionWith_ins_wf,
le_int_wf,
le_wf,
bnot_wf,
eqff_to_assert,
assert_functionality_wrt_uiff,
bnot_of_lt_int,
assert_of_le_int,
binary-map_wf,
bm_compare_wf
\mforall{}[T,Key:Type]. \mforall{}[compare:bm\_compare(Key)]. \mforall{}[m1,m2:binary-map(T;Key)]. \mforall{}[f:T {}\mrightarrow{} T {}\mrightarrow{} T].
(bm\_unionWith(compare;f;m1;m2) \mmember{} binary-map(T;Key))
Date html generated:
2015_07_17-AM-08_21_00
Last ObjectModification:
2015_01_27-PM-00_36_58
Home
Index