Step
*
of Lemma
bm_exists_downeq_wf
∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[m:binary-map(T;Key)]. ∀[k:Key]. ∀[p:T ─→ 𝔹].
(bm_exists_downeq(compare;m;k;p) ∈ 𝔹)
BY
{ (Auto
THEN (InstLemma `binary_map_ind-wf2` [⌈𝔹⌉;⌈T⌉;⌈Key⌉]⋅ THENA Auto)
THEN Unfold `bm_exists_downeq` 0
THEN BHyp -1
THEN Auto) }
Latex:
\mforall{}[T,Key:Type]. \mforall{}[compare:bm\_compare(Key)]. \mforall{}[m:binary-map(T;Key)]. \mforall{}[k:Key]. \mforall{}[p:T {}\mrightarrow{} \mBbbB{}].
(bm\_exists\_downeq(compare;m;k;p) \mmember{} \mBbbB{})
By
(Auto
THEN (InstLemma `binary\_map\_ind-wf2` [\mkleeneopen{}\mBbbB{}\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}Key\mkleeneclose{}]\mcdot{} THENA Auto)
THEN Unfold `bm\_exists\_downeq` 0
THEN BHyp -1
THEN Auto)
Home
Index