---

Step * of Lemma int-decr-map-inDom-prop2

∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].  (∀p∈m.¬(k = (fst(p)) ∈ ℤ)) supposing ¬↑int-decr-map-inDom(k;m)
BY
{ (Auto THEN (RWO "int-decr-map-inDom-prop" (-1) THENA Auto) THEN FLemma `int-decr-map-find-prop2` [-1] THEN Auto) }

---

Latex:


\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[m:int-decr-map-type(Value)].
    (\mforall{}p\mmember{}m.\mneg{}(k  =  (fst(p))))  supposing  \mneg{}\muparrow{}int-decr-map-inDom(k;m)


By

(Auto
  THEN  (RWO  "int-decr-map-inDom-prop"  (-1)  THENA  Auto)
  THEN  FLemma  `int-decr-map-find-prop2`  [-1]
  THEN  Auto)

---

Home Index