---

Step * 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)))
⊢ ¬¬(∃p:ℕ. weakly-safe-seq(R;n + 1;s.p@n))
BY
{ TACTIC:((Assert ¬¬(∃q:ℕ. homogeneous(R;n + 1;s.q@n)) BY
                 ((With ⌜0⌝ (D 4)⋅ THENA Auto) THEN RepeatFor 2 (ParallelLast) THEN Auto))
          THEN (SupposeMore (-1) THENA Auto)
          THEN D -1) }

1
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. q : ℕ
7. homogeneous(R;n + 1;s.q@n)
⊢ ¬¬(∃p:ℕ. weakly-safe-seq(R;n + 1;s.p@n))

---

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)))
\mvdash{}  \mneg{}\mneg{}(\mexists{}p:\mBbbN{}.  weakly-safe-seq(R;n  +  1;s.p@n))


By

---

Latex:
TACTIC:((Assert  \mneg{}\mneg{}(\mexists{}q:\mBbbN{}.  homogeneous(R;n  +  1;s.q@n))  BY
                              ((With  \mkleeneopen{}0\mkleeneclose{}  (D  4)\mcdot{}  THENA  Auto)  THEN  RepeatFor  2  (ParallelLast)  THEN  Auto))
                THEN  (SupposeMore  (-1)  THENA  Auto)
                THEN  D  -1)

---

Home Index