---

Step * 2 3 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)
9. k - fst(u) ≠ 0
10. ¬0 < k - fst(u)
⊢ [u / int-decr-map-add(k;v;v1)] ∈ int-decr-map-type(Value)
BY
{ ((MemTypeHD (-3) THEN Auto) THEN (MemTypeCD THEN Auto) THEN RW ListC 0 THEN Auto) }

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-add(k;v;v1) ∈ ((ℤ × Value) List)
9. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));int-decr-map-add(k;v;v1))
10. k - fst(u) ≠ 0
11. ¬0 < k - fst(u)
12. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));int-decr-map-add(k;v;v1))
13. y : ℤ × Value@i
14. (y ∈ int-decr-map-add(k;v;v1))@i
⊢ fst(y) < fst(u)

---

Latex:

---

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)
9.  k  -  fst(u)  \mneq{}  0
10.  \mneg{}0  <  k  -  fst(u)
\mvdash{}  [u  /  int-decr-map-add(k;v;v1)]  \mmember{}  int-decr-map-type(Value)


By

---

Latex:
((MemTypeHD  (-3)  THEN  Auto)  THEN  (MemTypeCD  THEN  Auto)  THEN  RW  ListC  0  THEN  Auto)

---

Home Index