Proof of Nuprl Lemma : find-xover-val

Step * 1 2 1 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')))}

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')))}

BY
{ (Auto THEN MemTypeCD THEN Try (OrRight) THEN Auto) }

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')))}

         ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))}

       ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))} )

15. v : T
16. n' : ℤ
17. (n + step) ≤ n'
18. v = (f n') ∈ T
19. test v = tt
20. x3 : ℤ
21. ((n' = (n + step) ∈ ℤ) ∧ (x3 = n ∈ ℤ))

∨ ((((n + step) ≤ x3) ∧ test (f x3) = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x3)))

⊢ n ≤ x3

2
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')))}

         ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))}

       ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))} )

15. v : T
16. n' : ℤ
17. (n + step) ≤ n'
18. v = (f n') ∈ T
19. test v = tt
20. x3 : ℤ
21. ((n' = (n + step) ∈ ℤ) ∧ (x3 = n ∈ ℤ))

∨ ((((n + step) ≤ x3) ∧ test (f x3) = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x3)))

22. n ≤ x3
⊢ test (f x3) = ff

3
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')))}

         ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))}

       ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x')))} )

15. v : T
16. n' : ℤ
17. (n + step) ≤ n'
18. v = (f n') ∈ T
19. test v = tt
20. x3 : ℤ
21. ((n' = (n + step) ∈ ℤ) ∧ (x3 = n ∈ ℤ))

∨ ((((n + step) ≤ x3) ∧ test (f x3) = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x3)))

22. n ≤ x3
23. test (f x3) = ff
⊢ (n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x3)

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')))\} 14. find-xover-val(test;f;n;n + step;2 * step) = find-xover-val(test;f;n;n + step;2 * step) 15. v : T 16. n' : \mBbbZ{} 17. ((n + step) \mleq{} n') \mwedge{} (v = (f n')) \mwedge{} test v = tt 18. x3 : \mBbbZ{} 19. ((n' = (n + step)) \mwedge{} (x3 = n)) \mvee{} ((((n + step) \mleq{} x3) \mwedge{} test (f x3) = ff) \mwedge{} ((n' = ((n + step) + (2 * step))) \mvee{} (((n + step) + (2 * step)) \mleq{} x3))) \mvdash{} <v, n', x3> \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: (Auto THEN MemTypeCD THEN Try (OrRight) THEN Auto) Home Index