---

Step * 1 1 of Lemma int_seg_decide_wf

.....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])))
BY
{ ((InductionOnNat THEN Auto)
   THEN (RW (SweepUpC UnrollRecursionC) 0 THENA Auto)
   THEN Reduce 0
   THEN RenameTo `a' `x'
   THEN WeakAutoSplit
   THEN (((GenConclAtAddr [2;1] THENA Auto') THEN UnfoldTop `decidable` (-2) THEN D -2 THEN Reduce 0) ORELSE Auto)
   THEN ((SubsumeC ⌜Dec(∃k:{a + 1..j-}. F[k])⌝⋅
          THEN Try ((BLemma `decidable-exists-int_seg-subtype` THEN Auto))
          THEN BackThruSomeHyp
          THEN Auto)
   ORELSE Auto
   )) }

---

Latex:

---

Latex:
.....assertion..... 
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{}  \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])))


By

---

Latex:
((InductionOnNat  THEN  Auto)
  THEN  (RW  (SweepUpC  UnrollRecursionC)  0  THENA  Auto)
  THEN  Reduce  0
  THEN  RenameTo  `a'  `x'
  THEN  WeakAutoSplit
  THEN  (((GenConclAtAddr  [2;1]  THENA  Auto')  THEN  UnfoldTop  `decidable`  (-2)  THEN  D  -2  THEN  Reduce  0)
  ORELSE  Auto
  )
  THEN  ((SubsumeC  \mkleeneopen{}Dec(\mexists{}k:\{a  +  1..j\msupminus{}\}.  F[k])\mkleeneclose{}\mcdot{}
                THEN  Try  ((BLemma  `decidable-exists-int\_seg-subtype`  THEN  Auto))
                THEN  BackThruSomeHyp
                THEN  Auto)
  ORELSE  Auto
  ))

---

Home Index