---

Step * 1 of Lemma int-decr-map-remove_wf


1. Value : Type
2. k : ℤ
3. u : ℤ × Value
4. v : (ℤ × Value) List
5. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v) ⇒ (int-decr-map-remove(k;v) ∈ int-decr-map-type(Value))
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));[u / v])@i
⊢ int-decr-map-remove(k;[u / v]) ∈ int-decr-map-type(Value)
BY
{ (Unfold `int-decr-map-remove` 0
   THEN (RWO "remove-combine-cons" 0 THENA Auto)
   THEN Reduce 0
   THEN Fold `int-decr-map-remove` 0
   THEN Repeat (SimpleSplit)
   THEN All(RW ListC)
   THEN Auto
   THEN Try (Complete ((MemTypeCD THEN Auto THEN RW ListC 0 THEN Auto)))
   THEN (MemTypeHD (-1) THENA Auto)
   THEN MemTypeCD
   THEN Auto
   THEN RW ListC 0
   THEN Auto
   THEN Unfold `int-decr-map-remove` (-1)
   THEN FLemma `remove-combine-implies-member` [-1]
   THEN Auto) }

---

Latex:



1.  Value  :  Type
2.  k  :  \mBbbZ{}
3.  u  :  \mBbbZ{}  \mtimes{}  Value
4.  v  :  (\mBbbZ{}  \mtimes{}  Value)  List
5.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));v)
{}\mRightarrow{}  (int-decr-map-remove(k;v)  \mmember{}  int-decr-map-type(Value))
6.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));[u  /  v])@i
\mvdash{}  int-decr-map-remove(k;[u  /  v])  \mmember{}  int-decr-map-type(Value)


By

(Unfold  `int-decr-map-remove`  0
  THEN  (RWO  "remove-combine-cons"  0  THENA  Auto)
  THEN  Reduce  0
  THEN  Fold  `int-decr-map-remove`  0
  THEN  Repeat  (SimpleSplit)
  THEN  All(RW  ListC)
  THEN  Auto
  THEN  Try  (Complete  ((MemTypeCD  THEN  Auto  THEN  RW  ListC  0  THEN  Auto)))
  THEN  (MemTypeHD  (-1)  THENA  Auto)
  THEN  MemTypeCD
  THEN  Auto
  THEN  RW  ListC  0
  THEN  Auto
  THEN  Unfold  `int-decr-map-remove`  (-1)
  THEN  FLemma  `remove-combine-implies-member`  [-1]
  THEN  Auto)

---

Home Index