---

Step * 1 2 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])))
⊢ int_seg_decide(d;i;j) ∈ Dec(∃k:{i..j-}. F[k])
BY
{ TACTIC:TACTIC:(Unfold `int_seg_decide` 0 THEN (Decide ⌜i ≤ j⌝⋅ THENA Auto)) }

1
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])

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])))
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])

---

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


By

---

Latex:
TACTIC:TACTIC:(Unfold  `int\_seg\_decide`  0  THEN  (Decide  \mkleeneopen{}i  \mleq{}  j\mkleeneclose{}\mcdot{}  THENA  Auto))

---

Home Index