---

Step * 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. homogeneous(R;n + 1;s.p@n)
7. q : ℕ
8. m : ℕ
9. p ≤ m
10. q ≤ m
11. r : ℕ
12. m < r
13. homogeneous(R;n + 1;s.r@n)
⊢ ¬¬(∃q@0:ℕ. (q < q@0 ∧ homogeneous(R;(n + 1) + 1;s.p@n.q@0@n + 1)))
BY
{ TACTIC:((Assert ¬¬homogeneous(R;n + 2;s.p@n.r@n + 1) BY Auto) THEN (SupposeMore (-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. homogeneous(R;n + 1;s.p@n)
7. q : ℕ
8. m : ℕ
9. p ≤ m
10. q ≤ m
11. r : ℕ
12. m < r
13. homogeneous(R;n + 1;s.r@n)
14. homogeneous(R;n + 2;s.p@n.r@n + 1)
⊢ ¬¬(∃q@0:ℕ. (q < q@0 ∧ homogeneous(R;(n + 1) + 1;s.p@n.q@0@n + 1)))

---

Latex:

---

Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  \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.  homogeneous(R;n  +  1;s.p@n)
7.  q  :  \mBbbN{}
8.  m  :  \mBbbN{}
9.  p  \mleq{}  m
10.  q  \mleq{}  m
11.  r  :  \mBbbN{}
12.  m  <  r
13.  homogeneous(R;n  +  1;s.r@n)
\mvdash{}  \mneg{}\mneg{}(\mexists{}q@0:\mBbbN{}.  (q  <  q@0  \mwedge{}  homogeneous(R;(n  +  1)  +  1;s.p@n.q@0@n  +  1)))


By

---

Latex:
TACTIC:((Assert  \mneg{}\mneg{}homogeneous(R;n  +  2;s.p@n.r@n  +  1)  BY  Auto)  THEN  (SupposeMore  (-1)  THENA  Auto))

---

Home Index