---

Step * of Lemma find-xover_wf

∀[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...}. ∀k:{m...}. f k = tt
BY
{ (Assert ⌜∀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⌝⋅
THENM ((UnivCD THENA Auto) THEN ExRepD THEN InstHyp [⌜(m - n) + 1⌝;⌜x⌝;⌜n⌝;⌜step⌝;⌜f⌝] 1⋅ THEN Auto)
) }

1
.....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

---

Latex:

---

Latex:
\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...\}.  \mforall{}k:\{m...\}.  f  k  =  tt


By

---

Latex:
(Assert  \mkleeneopen{}\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\mkleeneclose{}\mcdot{}
THENM  ((UnivCD  THENA  Auto)  THEN  ExRepD  THEN  InstHyp  [\mkleeneopen{}(m  -  n)  +  1\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}step\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  1\mcdot{}  THEN  Auto)
)

---

Home Index