---

Step * 1 1 2 of Lemma find-xover_wf


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-}
9. ∀k:{m...}. f k = tt
10. find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                             ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                             ∨ ((((n + step) ≤ x') ∧ f x' = ff)
                                               ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
                                                 ∨ (((n + step) + (2 * step)) ≤ x')))} 
⊢ 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')))} 
BY
{ (DoSubsume THEN 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-}
9. ∀k:{m...}. f k = tt
10. find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                             ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                             ∨ ((((n + step) ≤ x') ∧ f x' = ff)
                                               ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
                                                 ∨ (((n + step) + (2 * step)) ≤ x')))} 
11. find-xover(f;n;n + step;2 * step)
= find-xover(f;n;n + step;2 * step)
∈ (n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                           ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                           ∨ ((((n + step) ≤ x') ∧ f x' = ff)
                                             ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
                                               ∨ (((n + step) + (2 * step)) ≤ x')))} )
⊢ (n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                             ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                             ∨ ((((n + step) ≤ x') ∧ f x' = ff)
                                               ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
                                                 ∨ (((n + step) + (2 * step)) ≤ x')))} ) ⊆r (n':{n':ℤ| 
                                                                                                (n ≤ n') ∧ f n' = tt}  ×\000C {x':ℤ| 
                              ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
                              ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))} )

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d
          \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
3.  x  :  \mBbbZ{}
4.  n  :  \{x...\}
5.  step  :  \mBbbN{}\msupplus{}
6.  f  :  \{x...\}  {}\mrightarrow{}  \mBbbB{}
7.  \mneg{}\muparrow{}(f  n)
8.  m  :  \{n..n  +  d\msupminus{}\}
9.  \mforall{}k:\{m...\}.  f  k  =  tt
10.  find-xover(f;n;n  +  step;2  *  step)  \mmember{}  n':\{n':\mBbbZ{}|  ((n  +  step)  \mleq{}  n')  \mwedge{}  f  n'  =  tt\}    \mtimes{}  \{x':\mBbbZ{}| 
                                                                                          ((n'  =  (n  +  step))  \mwedge{}  (x'  =  n))
                                                                                          \mvee{}  ((((n  +  step)  \mleq{}  x')  \mwedge{}  f  x'  =  ff)
                                                                                              \mwedge{}  ((n'  =  ((n  +  step)  +  (2  *  step)))
                                                                                                  \mvee{}  (((n  +  step)  +  (2  *  step))  \mleq{}  x')))\} 
\mvdash{}  find-xover(f;n;n  +  step;2  *  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')))\} 


By

---

Latex:
(DoSubsume  THEN  Auto)

---

Home Index