---

Step * 2 1 1 1 1 1 1 1 of Lemma weakly-safe-extension

.....assertion..... 
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. r : ℕ
16. m < r
17. homogeneous(R;n + 1;s.r@n)
⊢ ¬¬(homogeneous(R;n + 2;s.p@n.r@n + 1) ∨ homogeneous(R;n + 2;s.q@n.r@n + 1))
BY
{ TACTIC:(DistinguishCases ⌜homogeneous(R;n + 2;s.p@n.r@n + 1)⌝⋅ THENA Auto) }

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. r : ℕ
16. m < r
17. homogeneous(R;n + 1;s.r@n)
18. homogeneous(R;n + 2;s.p@n.r@n + 1)
⊢ ¬¬(homogeneous(R;n + 2;s.p@n.r@n + 1) ∨ homogeneous(R;n + 2;s.q@n.r@n + 1))

2
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. r : ℕ
16. m < r
17. homogeneous(R;n + 1;s.r@n)
18. ¬homogeneous(R;n + 2;s.p@n.r@n + 1)
⊢ ¬¬(homogeneous(R;n + 2;s.p@n.r@n + 1) ∨ homogeneous(R;n + 2;s.q@n.r@n + 1))

---

Latex:

---

Latex:
.....assertion..... 
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
14.  q  <  m
15.  r  :  \mBbbN{}
16.  m  <  r
17.  homogeneous(R;n  +  1;s.r@n)
\mvdash{}  \mneg{}\mneg{}(homogeneous(R;n  +  2;s.p@n.r@n  +  1)  \mvee{}  homogeneous(R;n  +  2;s.q@n.r@n  +  1))


By

---

Latex:
TACTIC:(DistinguishCases  \mkleeneopen{}homogeneous(R;n  +  2;s.p@n.r@n  +  1)\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index