---

Step * 1 2 1 of Lemma int_seg_decide_wf


1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ{u}
4. d : ∀k:{i..j-}. Dec(F[k])
5. ∀n:ℕ. ∀x:ℤ.
     (((i ≤ x) ∧ (j ≤ (x + n)))
     ⇒ (fix((λG,x. if (x) < (j)  then case d x of inl(z) => inl <x, z> | inr(z) => G (x + 1)  else (inr (λx.⋅) ))) x
         ∈ Dec(∃k:{x..j-}. F[k])))
6. i ≤ j
⊢ fix((λG,x. if (x) < (j)  then case d x of inl(z) => inl <x, z> | inr(z) => G (x + 1)  else (inr (λx.⋅) ))) i ∈ Dec(∃k:\000C{i..j-}
                                                                                                              F[k])
BY
{ (InstHyp [⌜j - i⌝;⌜i⌝] (-2)⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  j  :  \mBbbZ{}
3.  F  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}\{u\}
4.  d  :  \mforall{}k:\{i..j\msupminus{}\}.  Dec(F[k])
5.  \mforall{}n:\mBbbN{}.  \mforall{}x:\mBbbZ{}.
          (((i  \mleq{}  x)  \mwedge{}  (j  \mleq{}  (x  +  n)))
          {}\mRightarrow{}  (fix((\mlambda{}G,x.  if  (x)  <  (j)
                                              then  case  d  x  of  inl(z)  =>  inl  <x,  z>  |  inr(z)  =>  G  (x  +  1)
                                              else  (inr  (\mlambda{}x.\mcdot{})  ))) 
                  x  \mmember{}  Dec(\mexists{}k:\{x..j\msupminus{}\}.  F[k])))
6.  i  \mleq{}  j
\mvdash{}  fix((\mlambda{}G,x.  if  (x)  <  (j)
                                then  case  d  x  of  inl(z)  =>  inl  <x,  z>  |  inr(z)  =>  G  (x  +  1)
                                else  (inr  (\mlambda{}x.\mcdot{})  ))) 
    i  \mmember{}  Dec(\mexists{}k:\{i..j\msupminus{}\}.  F[k])


By

---

Latex:
(InstHyp  [\mkleeneopen{}j  -  i\mkleeneclose{};\mkleeneopen{}i\mkleeneclose{}]  (-2)\mcdot{}  THEN  Auto')

---

Home Index