---

Step * 2 1 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 ∈ ℤ
⊢ [u / v1] ∈ int-decr-map-type(Value)
BY
{ ((MemTypeCD THEN Auto) THEN (RW ListC 0 THEN Auto) THEN Reduce 0 THEN InstHyp [⌜y⌝] (-6)⋅ THEN Auto') }

---

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))  =  0
\mvdash{}  [u  /  v1]  \mmember{}  int-decr-map-type(Value)


By

---

Latex:
((MemTypeCD  THEN  Auto)
  THEN  (RW  ListC  0  THEN  Auto)
  THEN  Reduce  0
  THEN  InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-6)\mcdot{}
  THEN  Auto')

---

Home Index