---

Step * 1 of Lemma find-xover_wf

.....assertion..... 
∀d:ℕ
  ∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
    find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                    ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
                                    ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
    supposing ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
BY
{ (CompleteInductionOnNat
   THEN (UnivCD THENA Auto)
   THEN RecUnfold `find-xover` 0
   THEN AutoSplit
   THEN RepeatFor 2 ((CallByValueReduce 0 THENA Auto))) }

1
1. d : ℕ
2. ∀d:ℕd
     ∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
       find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                       ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
                                       ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
       supposing ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
3. x : ℤ
4. n : {x...}
5. step : ℕ+
6. f : {x...} ⟶ 𝔹
7. ¬↑(f n)
8. ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
⊢ find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                  ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
                                  ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))} 

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}d:\mBbbN{}
    \mforall{}[x:\mBbbZ{}].  \mforall{}[n:\{x...\}].  \mforall{}[step:\mBbbN{}\msupplus{}].  \mforall{}[f:\{x...\}  {}\mrightarrow{}  \mBbbB{}].
        find-xover(f;x;n;step)  \mmember{}  n':\{n':\mBbbZ{}|  (n  \mleq{}  n')  \mwedge{}  f  n'  =  tt\}    \mtimes{}  \{x':\mBbbZ{}| 
                                                                        ((n'  =  n)  \mwedge{}  (x'  =  x))
                                                                        \mvee{}  (((n  \mleq{}  x')  \mwedge{}  f  x'  =  ff)
                                                                            \mwedge{}  ((n'  =  (n  +  step))  \mvee{}  ((n  +  step)  \mleq{}  x')))\}   
        supposing  \mexists{}m:\{n..n  +  d\msupminus{}\}.  \mforall{}k:\{m...\}.  f  k  =  tt


By

---

Latex:
(CompleteInductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  RecUnfold  `find-xover`  0
  THEN  AutoSplit
  THEN  RepeatFor  2  ((CallByValueReduce  0  THENA  Auto)))

---

Home Index