---

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


1. Value : Type
2. k : ℤ
3. u : ℤ × Value
4. v : (ℤ × Value) List
5. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v)@i
6. ∀y:ℤ × Value. ((y ∈ v) ⇒ ((fst(u)) > (fst(y))))@i
7. 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)) ∈ ℤ)))
8. (k - fst(u)) = 0 ∈ ℤ
⊢ inl (snd(u)) ∈ {v@0:Value| (¬False) ∧ (<k, v@0> ∈ [u / v])}  + (↓(∀p∈[u / v].¬(k = (fst(p)) ∈ ℤ)))
BY
{ (Auto THEN MemTypeCD THEN Auto THEN (RW ListC 0 THENA Auto) THEN OrLeft THEN Auto THEN Subst ⌜k ~ u1⌝ 0⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  Value  :  Type
2.  k  :  \mBbbZ{}
3.  u  :  \mBbbZ{}  \mtimes{}  Value
4.  v  :  (\mBbbZ{}  \mtimes{}  Value)  List
5.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));v)@i
6.  \mforall{}y:\mBbbZ{}  \mtimes{}  Value.  ((y  \mmember{}  v)  {}\mRightarrow{}  ((fst(u))  >  (fst(y))))@i
7.  case  find-combine(\mlambda{}p.(k  -  fst(p));v)  of  inl(x)  =>  inl  (snd(x))  |  inr(x)  =>  inr  \mcdot{} 
      \mmember{}  \{v@0:Value|  (\mneg{}\muparrow{}null(v))  \mwedge{}  (<k,  v@0>  \mmember{}  v)\}    +  (\mdownarrow{}(\mforall{}p\mmember{}v.\mneg{}(k  =  (fst(p)))))
8.  (k  -  fst(u))  =  0
\mvdash{}  inl  (snd(u))  \mmember{}  \{v@0:Value|  (\mneg{}False)  \mwedge{}  (<k,  v@0>  \mmember{}  [u  /  v])\}    +  (\mdownarrow{}(\mforall{}p\mmember{}[u  /  v].\mneg{}(k  =  (fst(p)))))


By

---

Latex:
(Auto
  THEN  MemTypeCD
  THEN  Auto
  THEN  (RW  ListC  0  THENA  Auto)
  THEN  OrLeft
  THEN  Auto
  THEN  Subst  \mkleeneopen{}k  \msim{}  u1\mkleeneclose{}  0\mcdot{}
  THEN  Auto')

---

Home Index