---

Step * of Lemma int-decr-map-isEmpty-prop

∀[Value:Type]. ∀[m:int-decr-map-type(Value)].  (↑int-decr-map-isEmpty(m) ⇐⇒ ∀k:ℤ. (¬↑int-decr-map-inDom(k;m)))
BY
{ (Auto
   THEN Try (((RWO "int-decr-map-isEmpty-assert" (-2) THENA Auto)
              THEN (HypSubst' (-2) 0 THENA Auto)
              THEN RW (SymbolicComputeC []) 0
              THEN Auto))
   THEN SupposeNot
   THEN (Assert ⌈False⌉⋅ THEN Auto)
   THEN RepUR ``int-decr-map-isEmpty`` (-1)
   THEN AllPushDown
   THEN (FLemma `member_exists` [-1] THENA Auto)
   THEN ExRepD
   THEN DProdsAndUnions
   THEN (InstHyp [⌈x1⌉] (-5)⋅ THENA Auto)
   THEN (RWO "int-decr-map-inDom-prop" (-1) THENA Auto)
   THEN (FLemma `int-decr-map-find-prop2` [-1] THENA Auto)
   THEN (RWO "l_all_iff" (-1) THENA Auto)
   THEN InstHyp [⌈<x1, x2>⌉] (-1)⋅
   THEN Auto) }

---

Latex:


\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].
    (\muparrow{}int-decr-map-isEmpty(m)  \mLeftarrow{}{}\mRightarrow{}  \mforall{}k:\mBbbZ{}.  (\mneg{}\muparrow{}int-decr-map-inDom(k;m)))


By

(Auto
  THEN  Try  (((RWO  "int-decr-map-isEmpty-assert"  (-2)  THENA  Auto)
                        THEN  (HypSubst'  (-2)  0  THENA  Auto)
                        THEN  RW  (SymbolicComputeC  [])  0
                        THEN  Auto))
  THEN  SupposeNot
  THEN  (Assert  \mkleeneopen{}False\mkleeneclose{}\mcdot{}  THEN  Auto)
  THEN  RepUR  ``int-decr-map-isEmpty``  (-1)
  THEN  AllPushDown
  THEN  (FLemma  `member\_exists`  [-1]  THENA  Auto)
  THEN  ExRepD
  THEN  DProdsAndUnions
  THEN  (InstHyp  [\mkleeneopen{}x1\mkleeneclose{}]  (-5)\mcdot{}  THENA  Auto)
  THEN  (RWO  "int-decr-map-inDom-prop"  (-1)  THENA  Auto)
  THEN  (FLemma  `int-decr-map-find-prop2`  [-1]  THENA  Auto)
  THEN  (RWO  "l\_all\_iff"  (-1)  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}<x1,  x2>\mkleeneclose{}]  (-1)\mcdot{}
  THEN  Auto)

---

Home Index