---

Step * 1 of Lemma exact-xover_wf

.....assertion..... 
∀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
BY
{ (CompleteInductionOnNat THEN (UnivCD THENA Auto) THEN RecUnfold `exact-xover` 0) }

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-}. ((∀k:{n..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))) ∧ f n = ff
⊢ let b,a = find-xover(f;n;n;1) 
  in if b=a + 1  then a  else exact-xover(f;a) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt} 

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}d:\mBbbN{}
    \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


By

---

Latex:
(CompleteInductionOnNat  THEN  (UnivCD  THENA  Auto)  THEN  RecUnfold  `exact-xover`  0)

---

Home Index