---

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


1. Value : Type
2. k : ℤ
3. u : ℤ × Value
4. k - fst(u) ≠ 0
5. v : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v)@i
7. ∀y:ℤ × Value. ((y ∈ v) ⇒ ((fst(u)) > (fst(y))))@i
8. 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)) ∈ ℤ)))
⊢ case if 0 <z k - fst(u) 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)) ∈ ℤ)))
BY
{ AutoSplit }

1
1. Value : Type
2. k : ℤ
3. u : ℤ × Value
4. k - fst(u) ≠ 0
5. v : (ℤ × Value) List
6. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v)@i
7. ∀y:ℤ × Value. ((y ∈ v) ⇒ ((fst(u)) > (fst(y))))@i
8. 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)) ∈ ℤ)))
9. 0 < k - fst(u)
⊢ inr ⋅  ∈ {v@0:Value| (¬False) ∧ (<k, v@0> ∈ [u / v])}  + (↓(∀p∈[u / v].¬(k = (fst(p)) ∈ ℤ)))

2
1. Value : Type
2. k : ℤ
3. u : ℤ × Value
4. ¬0 < k - fst(u)
5. k - fst(u) ≠ 0
6. v : (ℤ × Value) List
7. l-ordered(ℤ × Value;x,y.(fst(x)) > (fst(y));v)@i
8. ∀y:ℤ × Value. ((y ∈ v) ⇒ ((fst(u)) > (fst(y))))@i
9. 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)) ∈ ℤ)))
⊢ case find-combine(λp.(k - fst(p));v) 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:

---

Latex:

1.  Value  :  Type
2.  k  :  \mBbbZ{}
3.  u  :  \mBbbZ{}  \mtimes{}  Value
4.  k  -  fst(u)  \mneq{}  0
5.  v  :  (\mBbbZ{}  \mtimes{}  Value)  List
6.  l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));v)@i
7.  \mforall{}y:\mBbbZ{}  \mtimes{}  Value.  ((y  \mmember{}  v)  {}\mRightarrow{}  ((fst(u))  >  (fst(y))))@i
8.  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)))))
\mvdash{}  case  if  0  <z  k  -  fst(u)  then  inr  \mcdot{}    else  find-combine(\mlambda{}p.(k  -  fst(p));v)  fi 
      of  inl(x)  =>
      inl  (snd(x))
      |  inr(x)  =>
      inr  \mcdot{}    \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:
AutoSplit

---

Home Index