---

Step * 1 of Lemma no-weakly-safe-extensions


1. R : ℕ ⟶ ℕ ⟶ ℙ
2. n : ℕ
3. s : ℕn ⟶ ℕ
4. ∀p:ℕ. (¬weakly-safe-seq(R;n + 1;s.p@n))
5. weakly-safe-seq(R;n;s)
6. ∃p:ℕ. weakly-safe-seq(R;n + 1;s.p@n)
⊢ False
BY
{ (ExRepD THEN InstHyp [⌜p⌝] 4⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  R  :  \mBbbN{}  {}\mrightarrow{}  \mBbbN{}  {}\mrightarrow{}  \mBbbP{}
2.  n  :  \mBbbN{}
3.  s  :  \mBbbN{}n  {}\mrightarrow{}  \mBbbN{}
4.  \mforall{}p:\mBbbN{}.  (\mneg{}weakly-safe-seq(R;n  +  1;s.p@n))
5.  weakly-safe-seq(R;n;s)
6.  \mexists{}p:\mBbbN{}.  weakly-safe-seq(R;n  +  1;s.p@n)
\mvdash{}  False


By

---

Latex:
(ExRepD  THEN  InstHyp  [\mkleeneopen{}p\mkleeneclose{}]  4\mcdot{}  THEN  Auto)

---

Home Index