---

Step * of Lemma bm_collate_left_wf

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

---

Latex:


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


By

(Auto
  THEN  D  -1
  THEN  BinMapInd  `m'
  THEN  RepUR  ``bm\_collate\_left``  0
  THEN  Try  (Fold  `bm\_collate\_left`  0)
  THEN  Auto
  THEN  DVarSets
  THEN  RWO  "bm\_cnt\_prop\_T"  (-2)
  THEN  Auto
  THEN  Assert  \mkleeneopen{}bm\_collate\_left(left)  \mmember{}  (binary-map(T;Key)  List)  {}\mrightarrow{}  (binary-map(T;Key)  List)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  BLemma  `bm\_T-wf2`
  THEN  Auto)

---

Home Index