---

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

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. 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)))

---

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


By

---

Latex:
TACTIC:(RenameVar  `p'  (-2)
                THEN  (D  0  THENA  Auto)
                THEN  D  -1
                THEN  (With  \mkleeneopen{}p\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)
                THEN  D  0
                THEN  Auto
                THEN  skip\{RenameVar  `q'  (-2)\})

---

Home Index