---

Step * of Lemma int-decr-map-find-not-in

∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
  int-decr-map-find(k;m) = (inr ⋅ ) ∈ (Value?) supposing (∀p∈m.¬(k = (fst(p)) ∈ ℤ))
BY
{ (Auto
   THEN D (-2)
   THEN ListInd (-3)
   THEN Auto
   THEN All(RW ListC)
   THEN Auto
   THEN Unfold `int-decr-map-find` 0
   THEN (RWO "find-combine-cons" 0 THENA Auto)
   THEN Reduce 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (SimpleSplit)
   THEN Try (Fold `int-decr-map-find` 0)
   THEN Auto') }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  D  (-2)
  THEN  ListInd  (-3)
  THEN  Auto
  THEN  All(RW  ListC)
  THEN  Auto
  THEN  Unfold  `int-decr-map-find`  0
  THEN  (RWO  "find-combine-cons"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (SimpleSplit)
  THEN  Try  (Fold  `int-decr-map-find`  0)
  THEN  Auto')

---

Home Index