---

Step * 1 2 of Lemma find-xover-val_wf


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-}
12. ∀k:{m...}. test (f k) = tt
13. find-xover-val(test;f;n;n + step;2 * step) ∈ v:T
    × n':{n':ℤ| ((n + step) ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
    × {x':ℤ| 
       ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
       ∨ ((((n + step) ≤ x') ∧ test (f x') = ff)
         ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))} 
⊢ 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')))} 
BY
{ (DoSubsume THEN Auto THEN (D 0 THENA Auto) THEN RepeatFor 2 (D -1) THEN D -2 THEN D -1) }

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-}
12. ∀k:{m...}. test (f k) = tt
13. find-xover-val(test;f;n;n + step;2 * step) ∈ v:T
    × n':{n':ℤ| ((n + step) ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
    × {x':ℤ| 
       ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
       ∨ ((((n + step) ≤ x') ∧ test (f x') = ff)
         ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))} 
14. find-xover-val(test;f;n;n + step;2 * step)
= find-xover-val(test;f;n;n + step;2 * step)
∈ (v:T
  × n':{n':ℤ| ((n + step) ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt} 
  × {x':ℤ| 
     ((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
     ∨ ((((n + step) ≤ x') ∧ test (f x') = ff)
       ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))} )
15. v : T
16. n' : ℤ
17. ((n + step) ≤ n') ∧ (v = (f n') ∈ T) ∧ test v = tt
18. x3 : ℤ
19. ((n' = (n + step) ∈ ℤ) ∧ (x3 = n ∈ ℤ))
∨ ((((n + step) ≤ x3) ∧ test (f x3) = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x3)))
⊢ <v, n', x3> ∈ 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:

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


By

---

Latex:
(DoSubsume  THEN  Auto  THEN  (D  0  THENA  Auto)  THEN  RepeatFor  2  (D  -1)  THEN  D  -2  THEN  D  -1)

---

Home Index