---

Step * 1 of Lemma int_seg_decide_wf


1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ{u}
4. d : ∀k:{i..j-}. Dec(F[k])
⊢ int_seg_decide(d;i;j) ∈ Dec(∃k:{i..j-}. F[k])
BY
{ Assert ⌜∀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.⋅) )\000C)) x
                ∈ Dec(∃k:{x..j-}. F[k])))⌝⋅ }

1
.....assertion..... 
1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ{u}
4. d : ∀k:{i..j-}. Dec(F[k])
⊢ ∀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])))

2
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])))
⊢ int_seg_decide(d;i;j) ∈ Dec(∃k:{i..j-}. F[k])

---

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])
\mvdash{}  int\_seg\_decide(d;i;j)  \mmember{}  Dec(\mexists{}k:\{i..j\msupminus{}\}.  F[k])


By

---

Latex:
Assert  \mkleeneopen{}\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])))\mkleeneclose{}\mcdot{}

---

Home Index