---

Step * of Lemma int-decr-map-add_wf

∀[Value:Type]. ∀[k:ℤ]. ∀[v:Value]. ∀[m:int-decr-map-type(Value)].  (int-decr-map-add(k;v;m) ∈ int-decr-map-type(Value))
BY
{ (Auto THEN D (-1) THEN ListInd (-2) THEN (RW ListC 0 THENA Auto) THEN Auto) }

1
1. Value : Type
2. k : ℤ
3. v : Value
4. True@i
⊢ int-decr-map-add(k;v;[]) ∈ 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)
⊢ int-decr-map-add(k;v;[u / v1]) ∈ int-decr-map-type(Value)

---

Latex:


\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[v:Value].  \mforall{}[m:int-decr-map-type(Value)].
    (int-decr-map-add(k;v;m)  \mmember{}  int-decr-map-type(Value))


By

(Auto  THEN  D  (-1)  THEN  ListInd  (-2)  THEN  (RW  ListC  0  THENA  Auto)  THEN  Auto)

---

Home Index