---

Step * 1 1 1 1 2 2 1 of Lemma exact-xover_wf


1. d : ℕ
2. ∀d:ℕd
     ∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].
       exact-xover(f;n) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt}  
       supposing (∃m:{n..n + d-}. ((∀k:{n..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))) ∧ f n = ff
3. n : ℤ
4. f : {n...} ⟶ 𝔹
5. m : {n..n + d-}
6. ∀k:{n..m-}. f k = ff
7. ∀k:{m...}. f k = tt
8. f n = ff
9. n' : ℤ
10. n ≤ n'
11. f n' = tt
12. v1 : ℤ
13. n' ≠ v1 + 1
14. ((n' = n ∈ ℤ) ∧ (v1 = n ∈ ℤ)) ∨ (((n ≤ v1) ∧ f v1 = ff) ∧ ((n' = (n + 1) ∈ ℤ) ∨ ((n + 1) ≤ v1)))
15. find-xover(f;n;n;1)
= <n', v1>
∈ (n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                  ((n' = n ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                  ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + 1) ∈ ℤ) ∨ ((n + 1) ≤ x')))} )
16. ¬(d = 0 ∈ ℤ)
17. n ≤ v1
18. d - 1 ∈ ℕd
⊢ exact-xover(f;v1) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt} 
BY
{ (InstHyp [⌜d - 1⌝;⌜v1⌝;⌜f⌝] 2⋅ THEN Auto) }

1
1. d : ℕ
2. ∀d:ℕd
     ∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].
       exact-xover(f;n) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt}  
       supposing (∃m:{n..n + d-}. ((∀k:{n..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))) ∧ f n = ff
3. n : ℤ
4. f : {n...} ⟶ 𝔹
5. m : {n..n + d-}
6. ∀k:{n..m-}. f k = ff
7. ∀k:{m...}. f k = tt
8. f n = ff
9. n' : ℤ
10. n ≤ n'
11. f n' = tt
12. v1 : ℤ
13. n' ≠ v1 + 1
14. ((n' = n ∈ ℤ) ∧ (v1 = n ∈ ℤ)) ∨ (((n ≤ v1) ∧ f v1 = ff) ∧ ((n' = (n + 1) ∈ ℤ) ∨ ((n + 1) ≤ v1)))
15. find-xover(f;n;n;1)
= <n', v1>
∈ (n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                  ((n' = n ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                  ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + 1) ∈ ℤ) ∨ ((n + 1) ≤ x')))} )
16. ¬(d = 0 ∈ ℤ)
17. n ≤ v1
18. d - 1 ∈ ℕd
⊢ ∃m:{v1..v1 + (d - 1)-}. ((∀k:{v1..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))

2
1. d : ℕ
2. ∀d:ℕd
     ∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].
       exact-xover(f;n) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt}  
       supposing (∃m:{n..n + d-}. ((∀k:{n..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))) ∧ f n = ff
3. n : ℤ
4. f : {n...} ⟶ 𝔹
5. m : {n..n + d-}
6. ∀k:{n..m-}. f k = ff
7. ∀k:{m...}. f k = tt
8. f n = ff
9. n' : ℤ
10. n ≤ n'
11. f n' = tt
12. v1 : ℤ
13. n' ≠ v1 + 1
14. ((n' = n ∈ ℤ) ∧ (v1 = n ∈ ℤ)) ∨ (((n ≤ v1) ∧ f v1 = ff) ∧ ((n' = (n + 1) ∈ ℤ) ∨ ((n + 1) ≤ v1)))
15. find-xover(f;n;n;1)
= <n', v1>
∈ (n':{n':ℤ| (n ≤ n') ∧ f n' = tt}  × {x':ℤ| 
                                  ((n' = n ∈ ℤ) ∧ (x' = n ∈ ℤ))
                                  ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + 1) ∈ ℤ) ∨ ((n + 1) ≤ x')))} )
16. ¬(d = 0 ∈ ℤ)
17. n ≤ v1
18. d - 1 ∈ ℕd
19. ∃m:{v1..v1 + (d - 1)-}. ((∀k:{v1..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))
⊢ f v1 = ff

---

Latex:

---

Latex:

1.  d  :  \mBbbN{}
2.  \mforall{}d:\mBbbN{}d
          \mforall{}[n:\mBbbZ{}].  \mforall{}[f:\{n...\}  {}\mrightarrow{}  \mBbbB{}].
              exact-xover(f;n)  \mmember{}  \{x:\mBbbZ{}|  (n  \mleq{}  x)  \mwedge{}  f  x  =  ff  \mwedge{}  f  (x  +  1)  =  tt\}   
              supposing  (\mexists{}m:\{n..n  +  d\msupminus{}\}.  ((\mforall{}k:\{n..m\msupminus{}\}.  f  k  =  ff)  \mwedge{}  (\mforall{}k:\{m...\}.  f  k  =  tt)))  \mwedge{}  f  n  =  ff
3.  n  :  \mBbbZ{}
4.  f  :  \{n...\}  {}\mrightarrow{}  \mBbbB{}
5.  m  :  \{n..n  +  d\msupminus{}\}
6.  \mforall{}k:\{n..m\msupminus{}\}.  f  k  =  ff
7.  \mforall{}k:\{m...\}.  f  k  =  tt
8.  f  n  =  ff
9.  n'  :  \mBbbZ{}
10.  n  \mleq{}  n'
11.  f  n'  =  tt
12.  v1  :  \mBbbZ{}
13.  n'  \mneq{}  v1  +  1
14.  ((n'  =  n)  \mwedge{}  (v1  =  n))  \mvee{}  (((n  \mleq{}  v1)  \mwedge{}  f  v1  =  ff)  \mwedge{}  ((n'  =  (n  +  1))  \mvee{}  ((n  +  1)  \mleq{}  v1)))
15.  find-xover(f;n;n;1)  =  <n',  v1>
16.  \mneg{}(d  =  0)
17.  n  \mleq{}  v1
18.  d  -  1  \mmember{}  \mBbbN{}d
\mvdash{}  exact-xover(f;v1)  \mmember{}  \{x:\mBbbZ{}|  (n  \mleq{}  x)  \mwedge{}  f  x  =  ff  \mwedge{}  f  (x  +  1)  =  tt\} 


By

---

Latex:
(InstHyp  [\mkleeneopen{}d  -  1\mkleeneclose{};\mkleeneopen{}v1\mkleeneclose{};\mkleeneopen{}f\mkleeneclose{}]  2\mcdot{}  THEN  Auto)

---

Home Index