---

Step * 2 of Lemma int-decr-map-add_wf


1. Value : Type
2. k : ℤ
3. v : Value
4. u : ℤ × Value
5. v1 : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v1)@i
7. ∀y:ℤ × Value. ((y ∈ v1) ⇒ ((fst(u)) > (fst(y))))@i
8. int-decr-map-add(k;v;v1) ∈ int-decr-map-type(Value)
⊢ int-decr-map-add(k;v;[u / v1]) ∈ int-decr-map-type(Value)
BY
{ (Unfold `int-decr-map-add` 0
   THEN (RW ListC 0 THENA Auto)
   THEN Fold `int-decr-map-add` 0
   THEN RepUR ``int-minus-comparison`` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN Repeat (SimpleSplit)) }

1
1. Value : Type
2. k : ℤ
3. v : Value
4. u : ℤ × Value
5. v1 : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v1)@i
7. ∀y:ℤ × Value. ((y ∈ v1) ⇒ ((fst(u)) > (fst(y))))@i
8. int-decr-map-add(k;v;v1) ∈ int-decr-map-type(Value)
9. (k - fst(u)) = 0 ∈ ℤ
⊢ [u / v1] ∈ int-decr-map-type(Value)

2
1. Value : Type
2. k : ℤ
3. v : Value
4. u : ℤ × Value
5. v1 : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v1)@i
7. ∀y:ℤ × Value. ((y ∈ v1) ⇒ ((fst(u)) > (fst(y))))@i
8. int-decr-map-add(k;v;v1) ∈ int-decr-map-type(Value)
9. k - fst(u) ≠ 0
10. 0 < k - fst(u)
⊢ [<k, v>; [u / v1]] ∈ int-decr-map-type(Value)

3
1. Value : Type
2. k : ℤ
3. v : Value
4. u : ℤ × Value
5. v1 : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v1)@i
7. ∀y:ℤ × Value. ((y ∈ v1) ⇒ ((fst(u)) > (fst(y))))@i
8. int-decr-map-add(k;v;v1) ∈ int-decr-map-type(Value)
9. k - fst(u) ≠ 0
10. ¬0 < k - fst(u)
⊢ [u / int-decr-map-add(k;v;v1)] ∈ int-decr-map-type(Value)

---

Latex:



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


By

(Unfold  `int-decr-map-add`  0
  THEN  (RW  ListC  0  THENA  Auto)
  THEN  Fold  `int-decr-map-add`  0
  THEN  RepUR  ``int-minus-comparison``  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  Repeat  (SimpleSplit))

---

Home Index