---

Step * 2 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)
9. k - fst(u) ≠ 0
10. 0 < k - fst(u)
⊢ [<k, v>; [u / v1]] ∈ int-decr-map-type(Value)
BY
{ ((MemTypeCD THEN Auto)
   THEN Repeat ((RW ListC 0 THEN Reduce 0 THEN Auto))
   THEN (RW ListC (-1) THENA Auto)
   THEN D (-1)
   THEN Try (Complete ((HypSubst (-1) 0 THEN Auto')))
   THEN Try (Complete ((InstHyp [⌜y⌝] (-7)⋅ 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)  \mneq{}  0
10.  0  <  k  -  fst(u)
\mvdash{}  [<k,  v>  [u  /  v1]]  \mmember{}  int-decr-map-type(Value)


By

---

Latex:
((MemTypeCD  THEN  Auto)
  THEN  Repeat  ((RW  ListC  0  THEN  Reduce  0  THEN  Auto))
  THEN  (RW  ListC  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  Try  (Complete  ((HypSubst  (-1)  0  THEN  Auto')))
  THEN  Try  (Complete  ((InstHyp  [\mkleeneopen{}y\mkleeneclose{}]  (-7)\mcdot{}  THEN  Auto'))))

---

Home Index