---

Step * of Lemma int-decr-map-remove_wf

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

1
1. Value : Type
2. k : ℤ
3. u : ℤ × Value
4. v : (ℤ × Value) List
5. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v) ⇒ (int-decr-map-remove(k;v) ∈ int-decr-map-type(Value))
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));[u / v])@i
⊢ int-decr-map-remove(k;[u / v]) ∈ int-decr-map-type(Value)

---

Latex:


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


By

(Auto  THEN  D  (-1)  THEN  ListInd  (-2)  THEN  Auto)

---

Home Index