---

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

∀[Value:Type]
  ∀k:ℤ. ∀m:int-decr-map-type(Value).
    (¬↑null(m)) ∧ (<k, outl(int-decr-map-find(k;m))> ∈ m) supposing ↑int-decr-map-inDom(k;m)
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "int-decr-map-inDom-prop" (-1) THENA Auto)
   THEN InstLemma `int-decr-map-find-prop` [⌈Value⌉;⌈k⌉;⌈m⌉]⋅
   THEN Auto) }

---

Latex:


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


By

((UnivCD  THENA  Auto)
  THEN  (RWO  "int-decr-map-inDom-prop"  (-1)  THENA  Auto)
  THEN  InstLemma  `int-decr-map-find-prop`  [\mkleeneopen{}Value\mkleeneclose{};\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index