---

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

∀[Value:Type]
  ∀k:ℤ. ∀m:int-decr-map-type(Value).
    ((↑isl(int-decr-map-find(k;m))) ⇒ ((¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m)))
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN GenConclAtAddr [1;1;1]
   THEN DProdsAndUnions
   THEN Reduce 0
   THEN D 0
   THEN Try (Complete (Auto))
   THEN DVarSets
   THEN Auto
   THEN (Assert ⌈SqStable((<k, x> ∈ m))⌉⋅ THENA (BLemma `int-decr-map-type-member-sq-stable` THEN Auto))
   THEN Unfold `sq_stable` (-1)
   THEN D (-1)
   THEN Auto
   THEN Unhide
   THEN Auto) }

---

Latex:


\mforall{}[Value:Type]
    \mforall{}k:\mBbbZ{}.  \mforall{}m:int-decr-map-type(Value).
        ((\muparrow{}isl(int-decr-map-find(k;m)))  {}\mRightarrow{}  ((\mneg{}\muparrow{}null(m))  \mwedge{}  (<k,  outl(int-decr-map-find(k;m))>  \mmember{}  m)))


By

(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  GenConclAtAddr  [1;1;1]
  THEN  DProdsAndUnions
  THEN  Reduce  0
  THEN  D  0
  THEN  Try  (Complete  (Auto))
  THEN  DVarSets
  THEN  Auto
  THEN  (Assert  \mkleeneopen{}SqStable((<k,  x>  \mmember{}  m))\mkleeneclose{}\mcdot{}
              THENA  (BLemma  `int-decr-map-type-member-sq-stable`  THEN  Auto)
              )
  THEN  Unfold  `sq\_stable`  (-1)
  THEN  D  (-1)
  THEN  Auto
  THEN  Unhide
  THEN  Auto)

---

Home Index