---

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


1. Value : Type
2. k : ℤ
3. v : Value
4. True@i
⊢ int-decr-map-add(k;v;[]) ∈ int-decr-map-type(Value)
BY
{ (RepUR ``int-decr-map-add insert-combine int-decr-map-type`` 0
   THEN MemTypeCD
   THEN Auto
   THEN Repeat ((RW ListC 0 THEN Auto))) }

---

Latex:



1.  Value  :  Type
2.  k  :  \mBbbZ{}
3.  v  :  Value
4.  True@i
\mvdash{}  int-decr-map-add(k;v;[])  \mmember{}  int-decr-map-type(Value)


By

(RepUR  ``int-decr-map-add  insert-combine  int-decr-map-type``  0
  THEN  MemTypeCD
  THEN  Auto
  THEN  Repeat  ((RW  ListC  0  THEN  Auto)))

---

Home Index