---

Step * of Lemma bm_listItemsi_d2l_wf

∀[T,Key:Type]. ∀[m:binary-map(T;Key)].  (bm_listItemsi_d2l(m) ∈ ((Key × T) List) ─→ ((Key × T) List))
BY
{ ((Auto THEN D -1)
   THEN BinMapInd `m'
   THEN RepUR ``bm_listItemsi_d2l`` 0
   THEN Try (Fold `bm_listItemsi_d2l` 0)
   THEN Auto
   THEN DVarSets
   THEN OnSomeHyp(\i.RWO "bm_cnt_prop_T" i THEN Auto)⋅
   THEN Assert ⌈bm_listItemsi_d2l(left) ∈ ((Key × T) List) ─→ ((Key × T) List)⌉⋅
   THEN Auto
   THEN Assert ⌈bm_listItemsi_d2l(y4) ∈ ((Key × T) List) ─→ ((Key × T) List)⌉⋅
   THEN Auto) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[m:binary-map(T;Key)].
    (bm\_listItemsi\_d2l(m)  \mmember{}  ((Key  \mtimes{}  T)  List)  {}\mrightarrow{}  ((Key  \mtimes{}  T)  List))


By

((Auto  THEN  D  -1)
  THEN  BinMapInd  `m'
  THEN  RepUR  ``bm\_listItemsi\_d2l``  0
  THEN  Try  (Fold  `bm\_listItemsi\_d2l`  0)
  THEN  Auto
  THEN  DVarSets
  THEN  OnSomeHyp(\mbackslash{}i.RWO  "bm\_cnt\_prop\_T"  i  THEN  Auto)\mcdot{}
  THEN  Assert  \mkleeneopen{}bm\_listItemsi\_d2l(left)  \mmember{}  ((Key  \mtimes{}  T)  List)  {}\mrightarrow{}  ((Key  \mtimes{}  T)  List)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Assert  \mkleeneopen{}bm\_listItemsi\_d2l(y4)  \mmember{}  ((Key  \mtimes{}  T)  List)  {}\mrightarrow{}  ((Key  \mtimes{}  T)  List)\mkleeneclose{}\mcdot{}
  THEN  Auto)

---

Home Index