---

Step * 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)
⇒ (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)) ∈ ℤ))))
BY
{ ((UnivCD THENA Auto) THEN D (-1) THEN (D (-3) THENA Auto) THEN (CallByValueReduce 0 THENA Auto) THEN AutoSplit) }

1
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)) ∈ ℤ)))

2
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)) ∈ ℤ)))

---

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)
{}\mRightarrow{}  (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{}  (l-ordered(\mBbbZ{}  \mtimes{}  Value;x,y.(fst(x))  >  (fst(y));v)
\mwedge{}  (\mforall{}y:\mBbbZ{}  \mtimes{}  Value.  ((y  \mmember{}  v)  {}\mRightarrow{}  ((fst(u))  >  (fst(y))))))
{}\mRightarrow{}  (case  eval  tst  =  k  -  fst(u)  in
                  if  (tst  =\msubz{}  0)  then  inl  u
                  if  0  <z  tst  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

((UnivCD  THENA  Auto)
  THEN  D  (-1)
  THEN  (D  (-3)  THENA  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index