---

Step * of Lemma bm_collate_next_wf

∀[T,Key:Type]. ∀[l:binary-map(T;Key) List].  (bm_collate_next(l) ∈ binary-map(T;Key) × (binary-map(T;Key) List))
BY
{ (Auto
   THEN Unfold `bm_collate_next` 0
   THEN D (-1)
   THEN Reduce 0
   THEN Try (Complete ((Auto THEN BLemma `bm_E-wf2` THEN Auto)))
   THEN BLemma `binary_map_case-wf2`
   THEN Try (Complete (Auto))
   THEN Try (Complete ((Auto THEN BLemma `bm_E-wf2` THEN Auto)))) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[l:binary-map(T;Key)  List].
    (bm\_collate\_next(l)  \mmember{}  binary-map(T;Key)  \mtimes{}  (binary-map(T;Key)  List))


By

(Auto
  THEN  Unfold  `bm\_collate\_next`  0
  THEN  D  (-1)
  THEN  Reduce  0
  THEN  Try  (Complete  ((Auto  THEN  BLemma  `bm\_E-wf2`  THEN  Auto)))
  THEN  BLemma  `binary\_map\_case-wf2`
  THEN  Try  (Complete  (Auto))
  THEN  Try  (Complete  ((Auto  THEN  BLemma  `bm\_E-wf2`  THEN  Auto))))

---

Home Index