---

Step * of Lemma int-decr-map-find_wf

∀[Value:Type]. ∀[k:ℤ]. ∀[m:int-decr-map-type(Value)].
  (int-decr-map-find(k;m) ∈ {v:Value| (¬↑null(m)) ∧ (<k, v> ∈ m)}  + (↓(∀p∈m.¬(k = (fst(p)) ∈ ℤ))))
BY
{ ((UnivCD THENA Auto)
   THEN RepUR ``int-decr-map-find`` 0
   THEN Unfold `int-decr-map-type` (-1)
   THEN DVarSets
   THEN ListInd (-2)
   THEN Repeat ((RW List2C 0 THEN Reduce 0 THEN Try (Complete (Auto))))
   THEN Try (Complete ((Unfold `it` 0 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)
⇒ (case find-combine(λp.(k - fst(p));v) of inl(x) => inl (snd(x)) | inr(x) => inr ⋅ 
    ∈ {v@0:Value| (¬↑null(v)) ∧ (<k, v@0> ∈ v)}  + (↓(∀p∈v.¬(k = (fst(p)) ∈ ℤ))))
⊢ (l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v) ∧ (∀y:ℤ × Value. ((y ∈ v) ⇒ ((fst(u)) > (fst(y))))))
⇒ (case eval tst = k - fst(u) in
         if (tst =z 0) then inl u
         if 0 <z tst then inr ⋅ 
         else find-combine(λp.(k - fst(p));v)
         fi 
     of inl(x) =>
     inl (snd(x))
     | inr(x) =>
     inr ⋅  ∈ {v@0:Value| (¬False) ∧ (<k, v@0> ∈ [u / v])}  + (↓(∀p∈[u / v].¬(k = (fst(p)) ∈ ℤ))))

---

Latex:


\mforall{}[Value:Type].  \mforall{}[k:\mBbbZ{}].  \mforall{}[m:int-decr-map-type(Value)].
    (int-decr-map-find(k;m)  \mmember{}  \{v:Value|  (\mneg{}\muparrow{}null(m))  \mwedge{}  (<k,  v>  \mmember{}  m)\}    +  (\mdownarrow{}(\mforall{}p\mmember{}m.\mneg{}(k  =  (fst(p))))))


By

((UnivCD  THENA  Auto)
  THEN  RepUR  ``int-decr-map-find``  0
  THEN  Unfold  `int-decr-map-type`  (-1)
  THEN  DVarSets
  THEN  ListInd  (-2)
  THEN  Repeat  ((RW  List2C  0  THEN  Reduce  0  THEN  Try  (Complete  (Auto))))
  THEN  Try  (Complete  ((Unfold  `it`  0  THEN  Auto))))

---

Home Index