---

Step * 2 of Lemma int-decr-map-update-prop


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-update(k2;v;v1))
   = if (k1 =z k2) 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-update(k2;v;[u / v1]))
= if (k1 =z k2) then inl v else int-decr-map-find(k1;[u / v1]) fi 
∈ (Value?)
BY
{ (Unfold `int-decr-map-update` 0
   THEN (RWO "insert-combine-cons" 0 THENA Auto)
   THEN Fold `int-decr-map-update` 0
   THEN RepUR ``int-minus-comparison`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (SimpleSplit)
   THEN Repeat ((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 Auto'
                 THEN Try (Fold `int-decr-map-find` 0)))
   THEN (RW ListC (-6) THEN Auto)
   THEN SplitOnHypITE (-1)
   THEN Auto) }

---

Latex:

---

Latex:

1.  Value  :  Type
2.  k1  :  \mBbbZ{}
3.  k2  :  \mBbbZ{}
4.  v  :  Value
5.  u  :  \mBbbZ{}  \mtimes{}  Value
6.  v1  :  (\mBbbZ{}  \mtimes{}  Value)  List
7.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));v1)
{}\mRightarrow{}  (int-decr-map-find(k1;int-decr-map-update(k2;v;v1))
      =  if  (k1  =\msubz{}  k2)  then  inl  v  else  int-decr-map-find(k1;v1)  fi  )
8.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));[u  /  v1])@i
\mvdash{}  int-decr-map-find(k1;int-decr-map-update(k2;v;[u  /  v1]))
=  if  (k1  =\msubz{}  k2)  then  inl  v  else  int-decr-map-find(k1;[u  /  v1])  fi 


By

---

Latex:
(Unfold  `int-decr-map-update`  0
  THEN  (RWO  "insert-combine-cons"  0  THENA  Auto)
  THEN  Fold  `int-decr-map-update`  0
  THEN  RepUR  ``int-minus-comparison``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (SimpleSplit)
  THEN  Repeat  ((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  Auto'
                              THEN  Try  (Fold  `int-decr-map-find`  0)))
  THEN  (RW  ListC  (-6)  THEN  Auto)
  THEN  SplitOnHypITE  (-1)
  THEN  Auto)

---

Home Index