---

Step * 2 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
{ ((Assert ¬¬(∃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)))) BY
          (ParallelLast THEN Intros THEN ParallelOp 5 THEN Auto))
   THEN (SupposeMore (-1) THENA Auto)
   THEN ExRepD) }

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. p : ℕ
7. q : ℕ
8. homogeneous(R;n + 1;s.p@n)
9. homogeneous(R;n + 1;s.q@n)
10. p < q
11. ¬homogeneous(R;n + 2;s.p@n.q@n + 1)
⊢ ¬¬(∃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.  \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))))
\mvdash{}  \mneg{}\mneg{}(\mexists{}p:\mBbbN{}.  weakly-safe-seq(R;n  +  1;s.p@n))


By

---

Latex:
((Assert  \mneg{}\mneg{}(\mexists{}p,q:\mBbbN{}
                          (homogeneous(R;n  +  1;s.p@n)
                          \mwedge{}  homogeneous(R;n  +  1;s.q@n)
                          \mwedge{}  p  <  q
                          \mwedge{}  (\mneg{}homogeneous(R;n  +  2;s.p@n.q@n  +  1))))  BY
                (ParallelLast  THEN  Intros  THEN  ParallelOp  5  THEN  Auto))
  THEN  (SupposeMore  (-1)  THENA  Auto)
  THEN  ExRepD)

---

Home Index