Step
*
1
1
of Lemma
reg-less_wf
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. (x n1) + 4 < y n1
5. ∀b:{4...}. ∃n:ℕ+. ∀m:{n...}. (x m) + b < y m
6. n : ℕ+
7. ∀m:{n...}. (x m) + 4 < y m
⊢ find-ge(λn.(x n) + 4 <z y n;1) ∈ {n:ℕ+| (x n) + 4 < y n}
BY
{ (DoSubsume THEN Auto) }
1
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. (x n1) + 4 < y n1
5. ∀b:{4...}. ∃n:ℕ+. ∀m:{n...}. (x m) + b < y m
6. n : ℕ+
7. ∀m:{n...}. (x m) + 4 < y m
⊢ ∃m:{1...}. ∀k:{m...}. (λn.(x n) + 4 <z y n) k = tt
2
1. x : ℝ
2. y : ℝ
3. n1 : ℕ+
4. (x n1) + 4 < y n1
5. ∀b:{4...}. ∃n:ℕ+. ∀m:{n...}. (x m) + b < y m
6. n : ℕ+
7. ∀m:{n...}. (x m) + 4 < y m
8. find-ge(λn.(x n) + 4 <z y n;1) = find-ge(λn.(x n) + 4 <z y n;1) ∈ {n':ℤ| (1 ≤ n') ∧ (λn.(x n) + 4 <z y n) n' = tt}
⊢ {n':ℤ| (1 ≤ n') ∧ (λn.(x n) + 4 <z y n) n' = tt} ⊆r {n:ℕ+| (x n) + 4 < y n}
Latex:
Latex:
1. x : \mBbbR{}
2. y : \mBbbR{}
3. n1 : \mBbbN{}\msupplus{}
4. (x n1) + 4 < y n1
5. \mforall{}b:\{4...\}. \mexists{}n:\mBbbN{}\msupplus{}. \mforall{}m:\{n...\}. (x m) + b < y m
6. n : \mBbbN{}\msupplus{}
7. \mforall{}m:\{n...\}. (x m) + 4 < y m
\mvdash{} find-ge(\mlambda{}n.(x n) + 4 <z y n;1) \mmember{} \{n:\mBbbN{}\msupplus{}| (x n) + 4 < y n\}
By
Latex:
(DoSubsume THEN Auto)
Home
Index