---

Step * of Lemma find-xover-val_wf

∀[T:Type]
  ∀[test:T ⟶ 𝔹]. ∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ T].
    find-xover-val(test;f;x;n;step) ∈ v:T
    × n':{n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
    × {x':ℤ| 
       ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ)) ∨ (((n ≤ x') ∧ test (f x') = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
    supposing ∃m:{n...}. ∀k:{m...}. test (f k) = tt 
  supposing value-type(T)
BY
{ (RepeatFor 3 (Intro)
   THEN (Assert ⌜∀d:ℕ
                   ∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ T].
                     find-xover-val(test;f;x;n;step) ∈ v:T
                     × n':{n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
                     × {x':ℤ| 
                        ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
                        ∨ (((n ≤ x') ∧ test (f x') = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
                     supposing ∃m:{n..n + d-}. ∀k:{m...}. test (f k) = tt⌝⋅
   THENM ((UnivCD THENA Auto) THEN ExRepD THEN InstHyp [⌜(m - n) + 1⌝;⌜x⌝;⌜n⌝;⌜step⌝;⌜f⌝] 4⋅ THEN Auto)
   )
   THEN CompleteInductionOnNat
   THEN (UnivCD THENA Auto)
   THEN Unfold `find-xover-val` 0
   THEN RepeatFor 3 ((CallByValueReduce 0 THENA Auto))
   THEN AutoSplit) }

1
1. T : Type
2. value-type(T)
3. test : T ⟶ 𝔹
4. d : ℕ
5. ∀d:ℕd
     ∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ T].
       find-xover-val(test;f;x;n;step) ∈ v:T
       × n':{n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
       × {x':ℤ| 
          ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
          ∨ (((n ≤ x') ∧ test (f x') = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}  
       supposing ∃m:{n..n + d-}. ∀k:{m...}. test (f k) = tt
6. x : ℤ
7. n : {x...}
8. step : ℕ+
9. f : {x...} ⟶ T
10. ¬↑(test (f n))
11. ∃m:{n..n + d-}. ∀k:{m...}. test (f k) = tt
⊢ find-xover-val(test;f;n;n + step;2 * step) ∈ v:T
  × n':{n':ℤ| (n ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
  × {x':ℤ| 
     ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ)) ∨ (((n ≤ x') ∧ test (f x') = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))} 

---

Latex:

---

Latex:
\mforall{}[T:Type]
    \mforall{}[test:T  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[x:\mBbbZ{}].  \mforall{}[n:\{x...\}].  \mforall{}[step:\mBbbN{}\msupplus{}].  \mforall{}[f:\{x...\}  {}\mrightarrow{}  T].
        find-xover-val(test;f;x;n;step)  \mmember{}  v:T
        \mtimes{}  n':\{n':\mBbbZ{}|  (n  \mleq{}  n')  \mwedge{}  (v  =  (f  n'))  \mwedge{}  test  v  =  tt\} 
        \mtimes{}  \{x':\mBbbZ{}| 
              ((n'  =  n)  \mwedge{}  (x'  =  x))
              \mvee{}  (((n  \mleq{}  x')  \mwedge{}  test  (f  x')  =  ff)  \mwedge{}  ((n'  =  (n  +  step))  \mvee{}  ((n  +  step)  \mleq{}  x')))\}   
        supposing  \mexists{}m:\{n...\}.  \mforall{}k:\{m...\}.  test  (f  k)  =  tt 
    supposing  value-type(T)


By

---

Latex:
(RepeatFor  3  (Intro)
  THEN  (Assert  \mkleeneopen{}\mforall{}d:\mBbbN{}
                                  \mforall{}[x:\mBbbZ{}].  \mforall{}[n:\{x...\}].  \mforall{}[step:\mBbbN{}\msupplus{}].  \mforall{}[f:\{x...\}  {}\mrightarrow{}  T].
                                      find-xover-val(test;f;x;n;step)  \mmember{}  v:T
                                      \mtimes{}  n':\{n':\mBbbZ{}|  (n  \mleq{}  n')  \mwedge{}  (v  =  (f  n'))  \mwedge{}  test  v  =  tt\} 
                                      \mtimes{}  \{x':\mBbbZ{}| 
                                            ((n'  =  n)  \mwedge{}  (x'  =  x))
                                            \mvee{}  (((n  \mleq{}  x')  \mwedge{}  test  (f  x')  =  ff)  \mwedge{}  ((n'  =  (n  +  step))  \mvee{}  ((n  +  step)  \mleq{}  x')))\}   
                                      supposing  \mexists{}m:\{n..n  +  d\msupminus{}\}.  \mforall{}k:\{m...\}.  test  (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{}]  4\mcdot{}
                THEN  Auto)
  )
  THEN  CompleteInductionOnNat
  THEN  (UnivCD  THENA  Auto)
  THEN  Unfold  `find-xover-val`  0
  THEN  RepeatFor  3  ((CallByValueReduce  0  THENA  Auto))
  THEN  AutoSplit)

---

Home Index