---

Step * 1 of Lemma int-seg-case_wf


1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ
4. G : {i..j-} ⟶ ℙ
5. d : ∀k:{i..j-}. (F[k] ∨ G[k])
6. ¬j < i
7. M : ℤ
8. 0 < M
9. (i + M) ≤ j
10. primrec(M - 1;inr (λk.Ax) ;λn,x. case x
                                     of inl(p) =>
                                     inl p
                                     | inr(f) =>
                                     case d (i + n)
                                      of inl(z) =>
                                      inl <i + n, z>
                                      | inr(u) =>
                                      inr (λk.if (k) < (i + n)  then f k  else u) ) ∈ (∃k:{i..i + (M - 1)-}. F[k])
    ∨ (∀k:{i..i + (M - 1)-}. G[k])
11. 1 ≤ M
12. v : (∃k:{i..i + (M - 1)-}. F[k]) ∨ (∀k:{i..i + (M - 1)-}. G[k])
⊢ (λn,x. case x
         of inl(p) =>
         inl p
         | inr(f) =>
         case d (i + n) of inl(z) => inl <i + n, z> | inr(u) => inr (λk.if (k) < (i + n)  then f k  else u) ) 
  (M - 1) 
  v ∈ (∃k:{i..i + M-}. F[k]) ∨ (∀k:{i..i + M-}. G[k])
BY
{ (D -1 THEN Reduce 0) }

1
1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ
4. G : {i..j-} ⟶ ℙ
5. d : ∀k:{i..j-}. (F[k] ∨ G[k])
6. ¬j < i
7. M : ℤ
8. 0 < M
9. (i + M) ≤ j
10. primrec(M - 1;inr (λk.Ax) ;λn,x. case x
                                     of inl(p) =>
                                     inl p
                                     | inr(f) =>
                                     case d (i + n)
                                      of inl(z) =>
                                      inl <i + n, z>
                                      | inr(u) =>
                                      inr (λk.if (k) < (i + n)  then f k  else u) ) ∈ (∃k:{i..i + (M - 1)-}. F[k])
    ∨ (∀k:{i..i + (M - 1)-}. G[k])
11. 1 ≤ M
12. x : ∃k:{i..i + (M - 1)-}. F[k]
⊢ inl x ∈ (∃k:{i..i + M-}. F[k]) ∨ (∀k:{i..i + M-}. G[k])

2
1. i : ℤ
2. j : ℤ
3. F : {i..j-} ⟶ ℙ
4. G : {i..j-} ⟶ ℙ
5. d : ∀k:{i..j-}. (F[k] ∨ G[k])
6. ¬j < i
7. M : ℤ
8. 0 < M
9. (i + M) ≤ j
10. primrec(M - 1;inr (λk.Ax) ;λn,x. case x
                                     of inl(p) =>
                                     inl p
                                     | inr(f) =>
                                     case d (i + n)
                                      of inl(z) =>
                                      inl <i + n, z>
                                      | inr(u) =>
                                      inr (λk.if (k) < (i + n)  then f k  else u) ) ∈ (∃k:{i..i + (M - 1)-}. F[k])
    ∨ (∀k:{i..i + (M - 1)-}. G[k])
11. 1 ≤ M
12. y : ∀k:{i..i + (M - 1)-}. G[k]
⊢ case d (i + (M - 1)) of inl(z) => inl <i + (M - 1), z> | inr(u) => inr (λk.if (k) < (i + (M - 1))  then y k  else u) 
  ∈ (∃k:{i..i + M-}. F[k]) ∨ (∀k:{i..i + M-}. G[k])

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  j  :  \mBbbZ{}
3.  F  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}
4.  G  :  \{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}
5.  d  :  \mforall{}k:\{i..j\msupminus{}\}.  (F[k]  \mvee{}  G[k])
6.  \mneg{}j  <  i
7.  M  :  \mBbbZ{}
8.  0  <  M
9.  (i  +  M)  \mleq{}  j
10.  primrec(M  -  1;inr  (\mlambda{}k.Ax)  ;\mlambda{}n,x.  case  x
                                                                          of  inl(p)  =>
                                                                          inl  p
                                                                          |  inr(f)  =>
                                                                          case  d  (i  +  n)
                                                                            of  inl(z)  =>
                                                                            inl  <i  +  n,  z>
                                                                            |  inr(u)  =>
                                                                            inr  (\mlambda{}k.if  (k)  <  (i  +  n)    then  f  k    else  u)  )  \mmember{}  (\mexists{}k:\{i..i
                                                                                                                                                                            +  (M  -  1)\msupminus{}\}
                                                                                                                                                                        F[k])
        \mvee{}  (\mforall{}k:\{i..i  +  (M  -  1)\msupminus{}\}.  G[k])
11.  1  \mleq{}  M
12.  v  :  (\mexists{}k:\{i..i  +  (M  -  1)\msupminus{}\}.  F[k])  \mvee{}  (\mforall{}k:\{i..i  +  (M  -  1)\msupminus{}\}.  G[k])
\mvdash{}  (\mlambda{}n,x.  case  x
                  of  inl(p)  =>
                  inl  p
                  |  inr(f)  =>
                  case  d  (i  +  n)
                    of  inl(z)  =>
                    inl  <i  +  n,  z>
                    |  inr(u)  =>
                    inr  (\mlambda{}k.if  (k)  <  (i  +  n)    then  f  k    else  u)  ) 
    (M  -  1) 
    v  \mmember{}  (\mexists{}k:\{i..i  +  M\msupminus{}\}.  F[k])  \mvee{}  (\mforall{}k:\{i..i  +  M\msupminus{}\}.  G[k])


By

---

Latex:
(D  -1  THEN  Reduce  0)

---

Home Index