---

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


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?)
BY
{ (RepUR ``int-decr-map-add insert-combine int-decr-map-find find-combine`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (SimpleSplit)
   THEN Auto') }

---

Latex:



1.  Value  :  Type
2.  k1  :  \mBbbZ{}
3.  k2  :  \mBbbZ{}
4.  v  :  Value
5.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));[])@i
\mvdash{}  int-decr-map-find(k1;int-decr-map-add(k2;v;[]))
=  if  (k1  =\msubz{}  k2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}int-decr-map-inDom(k2;[]))  then  inl  v  else  int-decr-map-find(k1;[])  fi 


By

(RepUR  ``int-decr-map-add  insert-combine  int-decr-map-find  find-combine``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (SimpleSplit)
  THEN  Auto')

---

Home Index