---

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


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?)
BY
{ (Unfold `int-decr-map-remove` 0
   THEN (RWO "remove-combine-cons" 0 THENA Auto)
   THEN Fold `int-decr-map-remove` 0
   THEN Reduce 0
   THEN Repeat (SimpleSplit)
   THEN All(RW ListC)
   THEN Auto
   THEN SimpleSplitGen Auto (-1)
   THEN Auto
   THEN Try ((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 Try (Fold `int-decr-map-find` 0)
              THEN Auto'))
   THEN Try (Complete ((MemTypeCD THEN Auto THEN RW ListC 0 THEN Auto)))
   THEN BLemma `int-decr-map-find-not-in`
   THEN Auto
   THEN RWO "l_all_iff" 0
   THEN Auto
   THEN OnSomeHyp(\i.Complete(InstHyp [⌈p⌉] i THEN Auto'))⋅) }

---

Latex:



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


By

(Unfold  `int-decr-map-remove`  0
  THEN  (RWO  "remove-combine-cons"  0  THENA  Auto)
  THEN  Fold  `int-decr-map-remove`  0
  THEN  Reduce  0
  THEN  Repeat  (SimpleSplit)
  THEN  All(RW  ListC)
  THEN  Auto
  THEN  SimpleSplitGen  Auto  (-1)
  THEN  Auto
  THEN  Try  ((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  Try  (Fold  `int-decr-map-find`  0)
                        THEN  Auto'))
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto  THEN  RW  ListC  0  THEN  Auto)))
  THEN  BLemma  `int-decr-map-find-not-in`
  THEN  Auto
  THEN  RWO  "l\_all\_iff"  0
  THEN  Auto
  THEN  OnSomeHyp(\mbackslash{}i.Complete(InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  i  THEN  Auto'))\mcdot{})

---

Home Index