---

Step * 2 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. 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)
⊢ ¬¬(w∃∞q.homogeneous(R;n + 2;s.p@n.q@n + 1) ∨ w∃∞q@0.homogeneous(R;n + 2;s.q@n.q@0@n + 1))
BY
{ TACTIC:(InstLemma `weakly-infinite-cases` [⌜λ2k.homogeneous(R;n + 2;s.p@n.k@n + 1)
                                              ∨ homogeneous(R;n + 2;s.q@n.k@n + 1)⌝;⌜λ2k.homogeneous(R;n + 2;s.p@n.k@n
                                                                                     + 1)⌝]⋅
          THENA Auto
          ) }

1
.....antecedent..... 
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)
⊢ w∃∞x.homogeneous(R;n + 2;s.p@n.x@n + 1) ∨ homogeneous(R;n + 2;s.q@n.x@n + 1)

2
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)
12. ¬¬(w∃∞n@0.homogeneous(R;n + 2;s.p@n.n@0@n + 1)
∨ w∃∞n@0.(homogeneous(R;n + 2;s.p@n.n@0@n + 1) ∨ homogeneous(R;n + 2;s.q@n.n@0@n + 1))
  ∧ (¬homogeneous(R;n + 2;s.p@n.n@0@n + 1)))
⊢ ¬¬(w∃∞q.homogeneous(R;n + 2;s.p@n.q@n + 1) ∨ w∃∞q@0.homogeneous(R;n + 2;s.q@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.  \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))))
6.  p  :  \mBbbN{}
7.  q  :  \mBbbN{}
8.  homogeneous(R;n  +  1;s.p@n)
9.  homogeneous(R;n  +  1;s.q@n)
10.  p  <  q
11.  \mneg{}homogeneous(R;n  +  2;s.p@n.q@n  +  1)
\mvdash{}  \mneg{}\mneg{}(w\mexists{}\minfty{}q.homogeneous(R;n  +  2;s.p@n.q@n  +  1)  \mvee{}  w\mexists{}\minfty{}q@0.homogeneous(R;n  +  2;s.q@n.q@0@n  +  1))


By

---

Latex:
TACTIC:(InstLemma  `weakly-infinite-cases`  [\mkleeneopen{}\mlambda{}\msubtwo{}k.homogeneous(R;n  +  2;s.p@n.k@n  +  1)
                                                                                        \mvee{}  homogeneous(R;n  +  2;s.q@n.k@n  +  1)\mkleeneclose{};
                \mkleeneopen{}\mlambda{}\msubtwo{}k.homogeneous(R;n  +  2;s.p@n.k@n  +  1)\mkleeneclose{}]\mcdot{}
                THENA  Auto
                )

---

Home Index