Step
*
2
1
1
1
1
1
of Lemma
weakly-safe-extension
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. ¬(∀p,q:ℕ.
(homogeneous(R;n + 1;s.p@n) ⇒ homogeneous(R;n + 1;s.q@n) ⇒ p < q ⇒ (¬¬homogeneous(R;n + 2;s.p@n.q@n + 1))))
5. p : ℕ
6. q : ℕ
7. homogeneous(R;n + 1;s.p@n)
8. homogeneous(R;n + 1;s.q@n)
9. p < q
10. ¬homogeneous(R;n + 2;s.p@n.q@n + 1)
11. x : ℕ
12. m : ℕ
13. x < m ∧ q < m
14. ¬¬(∃q@0:ℕ. (m < q@0 ∧ homogeneous(R;n + 1;s.q@0@n)))
⊢ ¬¬(∃q@0:ℕ. (x < q@0 ∧ (homogeneous(R;n + 2;s.p@n.q@0@n + 1) ∨ homogeneous(R;n + 2;s.q@n.q@0@n + 1))))
BY
{ TACTIC:((SupposeMore (-1) THENA Auto) THEN ExRepD) }
1
1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. ¬(∀p,q:ℕ.
(homogeneous(R;n + 1;s.p@n) ⇒ homogeneous(R;n + 1;s.q@n) ⇒ p < q ⇒ (¬¬homogeneous(R;n + 2;s.p@n.q@n + 1))))
5. p : ℕ
6. q : ℕ
7. homogeneous(R;n + 1;s.p@n)
8. homogeneous(R;n + 1;s.q@n)
9. p < q
10. ¬homogeneous(R;n + 2;s.p@n.q@n + 1)
11. x : ℕ
12. m : ℕ
13. x < m
14. q < m
15. q@0 : ℕ
16. m < q@0
17. homogeneous(R;n + 1;s.q@0@n)
⊢ ¬¬(∃q@0:ℕ. (x < q@0 ∧ (homogeneous(R;n + 2;s.p@n.q@0@n + 1) ∨ homogeneous(R;n + 2;s.q@n.q@0@n + 1))))
Latex:
Latex:
1. R : \mBbbN{} {}\mrightarrow{} \mBbbN{} {}\mrightarrow{} \mBbbP{}
2. n : \mBbbN{}
3. s : \mBbbN{}n {}\mrightarrow{} \mBbbN{}
4. \mneg{}(\mforall{}p,q:\mBbbN{}.
(homogeneous(R;n + 1;s.p@n)
{}\mRightarrow{} homogeneous(R;n + 1;s.q@n)
{}\mRightarrow{} p < q
{}\mRightarrow{} (\mneg{}\mneg{}homogeneous(R;n + 2;s.p@n.q@n + 1))))
5. p : \mBbbN{}
6. q : \mBbbN{}
7. homogeneous(R;n + 1;s.p@n)
8. homogeneous(R;n + 1;s.q@n)
9. p < q
10. \mneg{}homogeneous(R;n + 2;s.p@n.q@n + 1)
11. x : \mBbbN{}
12. m : \mBbbN{}
13. x < m \mwedge{} q < m
14. \mneg{}\mneg{}(\mexists{}q@0:\mBbbN{}. (m < q@0 \mwedge{} homogeneous(R;n + 1;s.q@0@n)))
\mvdash{} \mneg{}\mneg{}(\mexists{}q@0:\mBbbN{}
(x < q@0 \mwedge{} (homogeneous(R;n + 2;s.p@n.q@0@n + 1) \mvee{} homogeneous(R;n + 2;s.q@n.q@0@n + 1))))
By
Latex:
TACTIC:((SupposeMore (-1) THENA Auto) THEN ExRepD)
Home
Index