---

Step * of Lemma int-seg-case_wf

∀[i,j:ℤ]. ∀[F,G:{i..j-} ⟶ ℙ]. ∀[d:∀k:{i..j-}. (F[k] ∨ G[k])].
  (int-seg-case(i;j;d) ∈ (∃k:{i..j-}. F[k]) ∨ (∀k:{i..j-}. G[k]))
BY
{ (Intros
   THEN Unhide
   THEN Unfold `int-seg-case` 0
   THEN (((Decide ⌜j < i⌝⋅ THENA Auto) THEN OReduce 0)
         THENL [Auto
               ; ((Assert ⌜∀M:ℕ
                             (((i + M) ≤ j)
                             ⇒ (primrec(M;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-}. F[k]) ∨ (∀k:{i..i + M-}. G[k])))⌝⋅
                  THENM ((InstHyp [⌜j - i⌝] (-1)⋅ THENA Auto) THEN NthHypSq (-1) THEN EqCD THEN Auto)
                  )
                  THEN (InductionOnNat
                        THENL [(Reduce 0 THEN Auto)
                              ; ((ParallelLast THENA Auto)
                                 THEN (RWO "primrec-unroll" 0 THENA Auto)
                                 THEN ((SplitOnConclITE THENA Auto)
                                       THENL [Auto; ((GenConclAtAddr [2;2] THENA Auto) THEN Thin (-1))]
                                 ))]
                       )
                  )]
   )) }

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

---

Latex:

---

Latex:
\mforall{}[i,j:\mBbbZ{}].  \mforall{}[F,G:\{i..j\msupminus{}\}  {}\mrightarrow{}  \mBbbP{}].  \mforall{}[d:\mforall{}k:\{i..j\msupminus{}\}.  (F[k]  \mvee{}  G[k])].
    (int-seg-case(i;j;d)  \mmember{}  (\mexists{}k:\{i..j\msupminus{}\}.  F[k])  \mvee{}  (\mforall{}k:\{i..j\msupminus{}\}.  G[k]))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `int-seg-case`  0
  THEN  (((Decide  \mkleeneopen{}j  <  i\mkleeneclose{}\mcdot{}  THENA  Auto)  THEN  OReduce  0)
              THENL  [Auto
                          ;  ((Assert  \mkleeneopen{}\mforall{}M:\mBbbN{}
                                                      (((i  +  M)  \mleq{}  j)
                                                      {}\mRightarrow{}  (primrec(M;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\msupminus{}\}
                                                                                                                                                                    F[k])
                                                              \mvee{}  (\mforall{}k:\{i..i  +  M\msupminus{}\}.  G[k])))\mkleeneclose{}\mcdot{}
                                THENM  ((InstHyp  [\mkleeneopen{}j  -  i\mkleeneclose{}]  (-1)\mcdot{}  THENA  Auto)  THEN  NthHypSq  (-1)  THEN  EqCD  THEN  Auto)
                                )
                                THEN  (InductionOnNat
                                            THENL  [(Reduce  0  THEN  Auto)
                                                        ;  ((ParallelLast  THENA  Auto)
                                                              THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                                                              THEN  ((SplitOnConclITE  THENA  Auto)
                                                                          THENL  [Auto
                                                                                      ;  ((GenConclAtAddr  [2;2]  THENA  Auto)  THEN  Thin  (-1))]
                                                              ))]
                                          )
                                )]
  ))

---

Home Index