---

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

∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
  (∀p∈m.¬(k = (fst(p)) ∈ ℤ)) supposing ¬↑isl(int-decr-map-find(k;m))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN GenConclAtAddr [1;1;1;1]
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN D 0
   THEN Try (Complete (Auto))
   THEN D (-3)
   THEN Unhide
   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{}isl(int-decr-map-find(k;m))


By

(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  GenConclAtAddr  [1;1;1;1]
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  D  0
  THEN  Try  (Complete  (Auto))
  THEN  D  (-3)
  THEN  Unhide
  THEN  Auto)

---

Home Index