---

Step * 2 of Lemma int-decr-map-add-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-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?)
BY
{ (Unfold `int-decr-map-add` 0
   THEN (RWO "insert-combine-cons" 0 THENA Auto)
   THEN Fold `int-decr-map-add` 0
   THEN RepUR ``int-minus-comparison`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (SimpleSplit)
   THEN Try (SimpleSplitGen (Using [`Value',⌈Value⌉] (BLemma `int-decr-map-inDom_wf`)⋅ THEN Auto) 0⋅)
   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 (All(\i.Using [`Value',⌈Value⌉] (FLemma `int-decr-map-inDom-prop2` [i])⋅)⋅ THENA Auto)
                 THEN (All(RWO "l_all_iff") THENA Auto)
                 THEN Try (Complete ((InstHyp [⌈u⌉] (-1)⋅ THEN Auto')))))
   THEN All(\i.(RW ListC i THEN Auto))⋅
   THEN Repeat (OnSomeHyp(\i.SimpleSplitGen (Auto
                                             THEN Using [`Value',⌈Value⌉] (BLemma `int-decr-map-inDom_wf`)⋅
                                             THEN Auto) i)⋅)
   THEN Auto
   THEN Try (OnSomeHyp(\i.Complete ((FLemma `int-decr-map-inDom-cons` [i] THEN Auto')))⋅)
   THEN OnSomeHyp(\i.(Unfold `int-decr-map-inDom` i
                      THEN Unfold `int-decr-map-find` i
                      THEN (RWO "find-combine-cons" i THENA Auto)
                      THEN Reduce i
                      THEN (CallByValueReduce i THENA Auto)
                      THEN Repeat (SimpleSplitGen Auto i)
                      THEN Try (Fold `int-decr-map-find` i)
                      THEN Try (Fold `int-decr-map-inDom` i)
                      THEN Auto'))⋅) }

---

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-add(k2;v;v1))
      =  if  (k1  =\msubz{}  k2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}int-decr-map-inDom(k2;v1))  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-add(k2;v;[u  /  v1]))
=  if  (k1  =\msubz{}  k2)  \mwedge{}\msubb{}  (\mneg{}\msubb{}int-decr-map-inDom(k2;[u  /  v1]))
    then  inl  v
    else  int-decr-map-find(k1;[u  /  v1])
    fi 


By

(Unfold  `int-decr-map-add`  0
  THEN  (RWO  "insert-combine-cons"  0  THENA  Auto)
  THEN  Fold  `int-decr-map-add`  0
  THEN  RepUR  ``int-minus-comparison``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (SimpleSplit)
  THEN  Try  (SimpleSplitGen  (Using  [`Value',\mkleeneopen{}Value\mkleeneclose{}]  (BLemma  `int-decr-map-inDom\_wf`)\mcdot{}  THEN  Auto)  0\mcdot{})
  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  (All(\mbackslash{}i.Using  [`Value',\mkleeneopen{}Value\mkleeneclose{}]  (FLemma  `int-decr-map-inDom-prop2`  [i])\mcdot{})\mcdot{}
                                          THENA  Auto
                                          )
                              THEN  (All(RWO  "l\_all\_iff")  THENA  Auto)
                              THEN  Try  (Complete  ((InstHyp  [\mkleeneopen{}u\mkleeneclose{}]  (-1)\mcdot{}  THEN  Auto')))))
  THEN  All(\mbackslash{}i.(RW  ListC  i  THEN  Auto))\mcdot{}
  THEN  Repeat  (OnSomeHyp(\mbackslash{}i.SimpleSplitGen  (Auto
                                                                                      THEN  Using  [`Value',\mkleeneopen{}Value\mkleeneclose{}
                                                                                      ]  (BLemma  `int-decr-map-inDom\_wf`)\mcdot{}
                                                                                      THEN  Auto)  i)\mcdot{})
  THEN  Auto
  THEN  Try  (OnSomeHyp(\mbackslash{}i.Complete  ((FLemma  `int-decr-map-inDom-cons`  [i]  THEN  Auto')))\mcdot{})
  THEN  OnSomeHyp(\mbackslash{}i.(Unfold  `int-decr-map-inDom`  i
                                        THEN  Unfold  `int-decr-map-find`  i
                                        THEN  (RWO  "find-combine-cons"  i  THENA  Auto)
                                        THEN  Reduce  i
                                        THEN  (CallByValueReduce  i  THENA  Auto)
                                        THEN  Repeat  (SimpleSplitGen  Auto  i)
                                        THEN  Try  (Fold  `int-decr-map-find`  i)
                                        THEN  Try  (Fold  `int-decr-map-inDom`  i)
                                        THEN  Auto'))\mcdot{})

---

Home Index