---

Step * of Lemma bm_listItems_d2l_wf

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

---

Latex:


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


By

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

---

Home Index