---

Step * of Lemma bm_remove_wf

∀[T,Key:Type]. ∀[compare:bm_compare(Key)]. ∀[x:Key]. ∀[m:binary-map(T;Key)].
  bm_remove(compare;m;x) ∈ binary-map(T;Key) × T supposing ↑bm_inDomain(compare;m;x)
BY
{ (Auto
   THEN D -2
   THEN RepeatFor 2 (MoveToConcl (-1))
   THEN (OnVar `m' SimpleDatatypeInduction⋅
         THEN RWW "bm_cnt_prop_E bm_cnt_prop_T" 0 THENA Auto⋅
         THEN RepUR ``bm_inDomain bm_remove`` 0
         THEN Try (Folds ``bm_inDomain bm_remove`` 0)
         THEN Try ((CallByValueReduce 0 THENA Auto))
         THEN Try (BLemma `bm_T-wf2`)
         THEN Auto
         THEN BackThruSomeHyp
         THEN Repeat ((AllHyps h.SplitOnHypITE h   THEN Auto))
         THEN Try ((InstLemma `bm_compare_greater_greater_false` [⌈Key⌉;⌈compare⌉;⌈x⌉;⌈key⌉]⋅ THEN Complete (Auto)))
         THEN Try ((InstLemma `bm_compare_less_less_false` [⌈Key⌉;⌈compare⌉;⌈x⌉;⌈key⌉]⋅ THEN Complete (Auto)))
         THEN Try (Complete (((Assert ⌈(compare x key) = 0 ∈ ℤ⌉⋅ THENA Auto)
                              THEN FLemma `bm_compare_sym_eq` [-1]
                              THEN Auto)))
         THEN Try (Complete ((Auto THEN GenConclAtAddrType ⌈binary-map(T;Key) × T⌉ [2;1]⋅ THEN Auto))))⋅) }

---

Latex:


\mforall{}[T,Key:Type].  \mforall{}[compare:bm\_compare(Key)].  \mforall{}[x:Key].  \mforall{}[m:binary-map(T;Key)].
    bm\_remove(compare;m;x)  \mmember{}  binary-map(T;Key)  \mtimes{}  T  supposing  \muparrow{}bm\_inDomain(compare;m;x)


By

(Auto
  THEN  D  -2
  THEN  RepeatFor  2  (MoveToConcl  (-1))
  THEN  (OnVar  `m'  SimpleDatatypeInduction\mcdot{}
              THEN  RWW  "bm\_cnt\_prop\_E  bm\_cnt\_prop\_T"  0  THENA  Auto\mcdot{}
              THEN  RepUR  ``bm\_inDomain  bm\_remove``  0
              THEN  Try  (Folds  ``bm\_inDomain  bm\_remove``  0)
              THEN  Try  ((CallByValueReduce  0  THENA  Auto))
              THEN  Try  (BLemma  `bm\_T-wf2`)
              THEN  Auto
              THEN  BackThruSomeHyp
              THEN  Repeat  ((AllHyps  h.SplitOnHypITE  h      THEN  Auto))
              THEN  Try  ((InstLemma  `bm\_compare\_greater\_greater\_false`  [\mkleeneopen{}Key\mkleeneclose{};\mkleeneopen{}compare\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}key\mkleeneclose{}]\mcdot{}
                                    THEN  Complete  (Auto)
                                    ))
              THEN  Try  ((InstLemma  `bm\_compare\_less\_less\_false`  [\mkleeneopen{}Key\mkleeneclose{};\mkleeneopen{}compare\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}key\mkleeneclose{}]\mcdot{}
                                    THEN  Complete  (Auto)
                                    ))
              THEN  Try  (Complete  (((Assert  \mkleeneopen{}(compare  x  key)  =  0\mkleeneclose{}\mcdot{}  THENA  Auto)
                                                        THEN  FLemma  `bm\_compare\_sym\_eq`  [-1]
                                                        THEN  Auto)))
              THEN  Try  (Complete  ((Auto
                                                        THEN  GenConclAtAddrType  \mkleeneopen{}binary-map(T;Key)  \mtimes{}  T\mkleeneclose{}  [2;1]\mcdot{}
                                                        THEN  Auto))))\mcdot{})

---

Home Index