---

Step * 1 2 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. 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])
BY
{ (GenConclAtAddr [2;1] THEN Thin (-1) THEN 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. y : ∀k:{i..i + (M - 1)-}. G[k]
13. x : F[i + (M - 1)]
⊢ inl <i + (M - 1), 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]
13. y1 : G[i + (M - 1)]
⊢ inr (λk.if (k) < (i + (M - 1))  then y k  else y1)  ∈ (∃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.  y  :  \mforall{}k:\{i..i  +  (M  -  1)\msupminus{}\}.  G[k]
\mvdash{}  case  d  (i  +  (M  -  1))
      of  inl(z)  =>
      inl  <i  +  (M  -  1),  z>
      |  inr(u)  =>
      inr  (\mlambda{}k.if  (k)  <  (i  +  (M  -  1))    then  y  k    else  u)    \mmember{}  (\mexists{}k:\{i..i  +  M\msupminus{}\}.  F[k])
    \mvee{}  (\mforall{}k:\{i..i  +  M\msupminus{}\}.  G[k])


By

---

Latex:
(GenConclAtAddr  [2;1]  THEN  Thin  (-1)  THEN  D  -1  THEN  Reduce  0)

---

Home Index