---

Step * 1 2 2 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]
13. y1 : G[i + (M - 1)]
14. k : {i..i + M-}
15. ¬k < i + (M - 1)
⊢ y1 ∈ G[k]
BY
{ (Subst' k ~ i + (M - 1) 0 THEN Auto) }

---

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]
13.  y1  :  G[i  +  (M  -  1)]
14.  k  :  \{i..i  +  M\msupminus{}\}
15.  \mneg{}k  <  i  +  (M  -  1)
\mvdash{}  y1  \mmember{}  G[k]


By

---

Latex:
(Subst'  k  \msim{}  i  +  (M  -  1)  0  THEN  Auto)

---

Home Index