---

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

∀[Value:Type]. ∀[m:int-decr-map-type(Value)]. ∀[k1,k2:ℤ]. ∀[v:Value].
  (int-decr-map-find(k1;int-decr-map-add(k2;v;m))
  = if (k1 =z k2) ∧b (¬bint-decr-map-inDom(k2;m)) then inl v else int-decr-map-find(k1;m) fi 
  ∈ (Value?))
BY
{ (Auto THEN D (-4) THEN ListInd (-5) THEN (D 0 THENA Auto)) }

1
1. Value : Type
2. k1 : ℤ
3. k2 : ℤ
4. v : Value
5. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));[])@i
⊢ int-decr-map-find(k1;int-decr-map-add(k2;v;[]))
= if (k1 =z k2) ∧b (¬bint-decr-map-inDom(k2;[])) then inl v else int-decr-map-find(k1;[]) fi 
∈ (Value?)

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

---

Latex:


\mforall{}[Value:Type].  \mforall{}[m:int-decr-map-type(Value)].  \mforall{}[k1,k2:\mBbbZ{}].  \mforall{}[v:Value].
    (int-decr-map-find(k1;int-decr-map-add(k2;v;m))
    =  if  (k1  =\msubz{}  k2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}int-decr-map-inDom(k2;m))  then  inl  v  else  int-decr-map-find(k1;m)  fi  )


By

(Auto  THEN  D  (-4)  THEN  ListInd  (-5)  THEN  (D  0  THENA  Auto))

---

Home Index