---

Step * of Lemma exact-xover_wf

∀[n:ℤ]. ∀[f:{n...} ⟶ 𝔹].
  exact-xover(f;n) ∈ {x:ℤ| (n ≤ x) ∧ f x = ff ∧ f (x + 1) = tt}  
  supposing (∃m:{n...}. ((∀k:{n..m-}. f k = ff) ∧ (∀k:{m...}. f k = tt))) ∧ f n = ff
BY
{ (Assert ⌜∀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⌝⋅
THENM ((UnivCD THENA Auto) THEN ExRepD THEN InstHyp [⌜(m - n) + 1⌝;⌜n⌝;⌜f⌝] 1⋅ THEN Auto)
) }

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

---

Latex:

---

Latex:
\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...\}.  ((\mforall{}k:\{n..m\msupminus{}\}.  f  k  =  ff)  \mwedge{}  (\mforall{}k:\{m...\}.  f  k  =  tt)))  \mwedge{}  f  n  =  ff


By

---

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

---

Home Index