---

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

∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ].
  (int-decr-map-find(k1;int-decr-map-remove(k2;m))
  = if (k1 =z k2) then inr ⋅  else int-decr-map-find(k1;m) fi 
  ∈ (Value?))
BY
{ (Auto
   THEN D (-3)
   THEN ListInd (-4)
   THEN Auto
   THEN Try (Complete ((SimpleSplit THEN RW (SymbolicComputeC []) 0 THEN Auto)))) }

1
1. Value : Type
2. k1 : ℤ
3. k2 : ℤ
4. u : ℤ × Value
5. v : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v)
⇒ (int-decr-map-find(k1;int-decr-map-remove(k2;v))
   = if (k1 =z k2) then inr ⋅  else int-decr-map-find(k1;v) fi 
   ∈ (Value?))
7. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));[u / v])@i
⊢ int-decr-map-find(k1;int-decr-map-remove(k2;[u / v]))
= if (k1 =z k2) then inr ⋅  else int-decr-map-find(k1;[u / v]) fi 
∈ (Value?)

---

Latex:

---

Latex:
\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].  \mforall{}[k1,k2:\mBbbZ{}].
    (int-decr-map-find(k1;int-decr-map-remove(k2;m))
    =  if  (k1  =\msubz{}  k2)  then  inr  \mcdot{}    else  int-decr-map-find(k1;m)  fi  )


By

---

Latex:
(Auto
  THEN  D  (-3)
  THEN  ListInd  (-4)
  THEN  Auto
  THEN  Try  (Complete  ((SimpleSplit  THEN  RW  (SymbolicComputeC  [])  0  THEN  Auto))))

---

Home Index