---

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


1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. weakly-safe-seq(R;n;s)
5. ∀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)))
6. p : ℕ
7. homogeneous(R;n + 1;s.p@n)
8. q : ℕ
⊢ ¬¬(∃q@0:ℕ. (q < q@0 ∧ homogeneous(R;(n + 1) + 1;s.p@n.q@0@n + 1)))
BY
{ ((Assert ∃m:ℕ. ((p ≤ m) ∧ (q ≤ m)) BY
          (Decide ⌜p ≤ q⌝⋅ THEN Auto))
   THEN D -1
   THEN TACTIC:((With ⌜m⌝ (D 4)⋅ THENA Auto) THEN (SupposeMore (-1) THENA Auto) THEN ExRepD THEN RenameVar `r' (-3))) }

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)
⊢ ¬¬(∃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.  weakly-safe-seq(R;n;s)
5.  \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)))
6.  p  :  \mBbbN{}
7.  homogeneous(R;n  +  1;s.p@n)
8.  q  :  \mBbbN{}
\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:
((Assert  \mexists{}m:\mBbbN{}.  ((p  \mleq{}  m)  \mwedge{}  (q  \mleq{}  m))  BY
                (Decide  \mkleeneopen{}p  \mleq{}  q\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  D  -1
  THEN  TACTIC:((With  \mkleeneopen{}m\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)
                            THEN  (SupposeMore  (-1)  THENA  Auto)
                            THEN  ExRepD
                            THEN  RenameVar  `r'  (-3)))

---

Home Index