Step
*
1
1
2
1
1
of Lemma
find-xover_wf
1. d : ℕ
2. ∀d:ℕd
∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}
supposing ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
3. x : ℤ
4. n : {x...}
5. step : ℕ+
6. f : {x...} ⟶ 𝔹
7. ¬↑(f n)
8. m : {n..n + d-}
9. ∀k:{m...}. f k = tt
10. find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))}
11. find-xover(f;n;n + step;2 * step)
= find-xover(f;n;n + step;2 * step)
∈ (n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))} )
12. n' : ℤ
13. (n + step) ≤ n'
14. f n' = tt
15. x2 : ℤ
16. ((n' = (n + step) ∈ ℤ) ∧ (x2 = n ∈ ℤ))
∨ ((((n + step) ≤ x2) ∧ f x2 = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x2)))
⊢ x2 ∈ {x':ℤ| ((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ)) ∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}
BY
{ (MemTypeCD THEN Try (OrRight) THEN Auto) }
1
1. d : ℕ
2. ∀d:ℕd
∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}
supposing ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
3. x : ℤ
4. n : {x...}
5. step : ℕ+
6. f : {x...} ⟶ 𝔹
7. ¬↑(f n)
8. m : {n..n + d-}
9. ∀k:{m...}. f k = tt
10. find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))}
11. find-xover(f;n;n + step;2 * step)
= find-xover(f;n;n + step;2 * step)
∈ (n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))} )
12. n' : ℤ
13. (n + step) ≤ n'
14. f n' = tt
15. x2 : ℤ
16. ((n' = (n + step) ∈ ℤ) ∧ (x2 = n ∈ ℤ))
∨ ((((n + step) ≤ x2) ∧ f x2 = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x2)))
⊢ n ≤ x2
2
1. d : ℕ
2. ∀d:ℕd
∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}
supposing ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
3. x : ℤ
4. n : {x...}
5. step : ℕ+
6. f : {x...} ⟶ 𝔹
7. ¬↑(f n)
8. m : {n..n + d-}
9. ∀k:{m...}. f k = tt
10. find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))}
11. find-xover(f;n;n + step;2 * step)
= find-xover(f;n;n + step;2 * step)
∈ (n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))} )
12. n' : ℤ
13. (n + step) ≤ n'
14. f n' = tt
15. x2 : ℤ
16. ((n' = (n + step) ∈ ℤ) ∧ (x2 = n ∈ ℤ))
∨ ((((n + step) ≤ x2) ∧ f x2 = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x2)))
17. n ≤ x2
⊢ f x2 = ff
3
1. d : ℕ
2. ∀d:ℕd
∀[x:ℤ]. ∀[n:{x...}]. ∀[step:ℕ+]. ∀[f:{x...} ⟶ 𝔹].
find-xover(f;x;n;step) ∈ n':{n':ℤ| (n ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = n ∈ ℤ) ∧ (x' = x ∈ ℤ))
∨ (((n ≤ x') ∧ f x' = ff) ∧ ((n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x')))}
supposing ∃m:{n..n + d-}. ∀k:{m...}. f k = tt
3. x : ℤ
4. n : {x...}
5. step : ℕ+
6. f : {x...} ⟶ 𝔹
7. ¬↑(f n)
8. m : {n..n + d-}
9. ∀k:{m...}. f k = tt
10. find-xover(f;n;n + step;2 * step) ∈ n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))}
11. find-xover(f;n;n + step;2 * step)
= find-xover(f;n;n + step;2 * step)
∈ (n':{n':ℤ| ((n + step) ≤ n') ∧ f n' = tt} × {x':ℤ|
((n' = (n + step) ∈ ℤ) ∧ (x' = n ∈ ℤ))
∨ ((((n + step) ≤ x') ∧ f x' = ff)
∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ)
∨ (((n + step) + (2 * step)) ≤ x')))} )
12. n' : ℤ
13. (n + step) ≤ n'
14. f n' = tt
15. x2 : ℤ
16. ((n' = (n + step) ∈ ℤ) ∧ (x2 = n ∈ ℤ))
∨ ((((n + step) ≤ x2) ∧ f x2 = ff) ∧ ((n' = ((n + step) + (2 * step)) ∈ ℤ) ∨ (((n + step) + (2 * step)) ≤ x2)))
17. n ≤ x2
18. f x2 = ff
⊢ (n' = (n + step) ∈ ℤ) ∨ ((n + step) ≤ x2)
Latex:
Latex:
1. d : \mBbbN{}
2. \mforall{}d:\mBbbN{}d
\mforall{}[x:\mBbbZ{}]. \mforall{}[n:\{x...\}]. \mforall{}[step:\mBbbN{}\msupplus{}]. \mforall{}[f:\{x...\} {}\mrightarrow{} \mBbbB{}].
find-xover(f;x;n;step) \mmember{} n':\{n':\mBbbZ{}| (n \mleq{} n') \mwedge{} f n' = tt\} \mtimes{} \{x':\mBbbZ{}|
((n' = n) \mwedge{} (x' = x))
\mvee{} (((n \mleq{} x') \mwedge{} f x' = ff)
\mwedge{} ((n' = (n + step)) \mvee{} ((n + step) \mleq{} x')))\}
supposing \mexists{}m:\{n..n + d\msupminus{}\}. \mforall{}k:\{m...\}. f k = tt
3. x : \mBbbZ{}
4. n : \{x...\}
5. step : \mBbbN{}\msupplus{}
6. f : \{x...\} {}\mrightarrow{} \mBbbB{}
7. \mneg{}\muparrow{}(f n)
8. m : \{n..n + d\msupminus{}\}
9. \mforall{}k:\{m...\}. f k = tt
10. find-xover(f;n;n + step;2 * step) \mmember{} n':\{n':\mBbbZ{}| ((n + step) \mleq{} n') \mwedge{} f n' = tt\} \mtimes{} \{x':\mBbbZ{}|
((n' = (n + step)) \mwedge{} (x' = n))
\mvee{} ((((n + step) \mleq{} x') \mwedge{} f x' = ff)
\mwedge{} ((n' = ((n + step) + (2 * step)))
\mvee{} (((n + step) + (2 * step)) \mleq{} x')))\}
11. find-xover(f;n;n + step;2 * step) = find-xover(f;n;n + step;2 * step)
12. n' : \mBbbZ{}
13. (n + step) \mleq{} n'
14. f n' = tt
15. x2 : \mBbbZ{}
16. ((n' = (n + step)) \mwedge{} (x2 = n))
\mvee{} ((((n + step) \mleq{} x2) \mwedge{} f x2 = ff)
\mwedge{} ((n' = ((n + step) + (2 * step))) \mvee{} (((n + step) + (2 * step)) \mleq{} x2)))
\mvdash{} x2 \mmember{} \{x':\mBbbZ{}|
((n' = n) \mwedge{} (x' = x)) \mvee{} (((n \mleq{} x') \mwedge{} f x' = ff) \mwedge{} ((n' = (n + step)) \mvee{} ((n + step) \mleq{} x')))\}
By
Latex:
(MemTypeCD THEN Try (OrRight) THEN Auto)
Home
Index