---

Step * 1 of Lemma ni-max_wf


1. f : ℕ ⟶ 𝔹
2. ∀n:ℕ. ((↑(f (n + 1))) ⇒ (↑(f n)))
3. g : ℕ ⟶ 𝔹
4. ∀n:ℕ. ((↑(g (n + 1))) ⇒ (↑(g n)))
5. n : ℕ@i
6. ↑((f (n + 1)) ∨b(g (n + 1)))@i
⊢ (↑(f n)) ∨ (↑(g n))
BY
{ ((RW assert_pushdownC (-1) THENM D -1) THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
2.  \mforall{}n:\mBbbN{}.  ((\muparrow{}(f  (n  +  1)))  {}\mRightarrow{}  (\muparrow{}(f  n)))
3.  g  :  \mBbbN{}  {}\mrightarrow{}  \mBbbB{}
4.  \mforall{}n:\mBbbN{}.  ((\muparrow{}(g  (n  +  1)))  {}\mRightarrow{}  (\muparrow{}(g  n)))
5.  n  :  \mBbbN{}@i
6.  \muparrow{}((f  (n  +  1))  \mvee{}\msubb{}(g  (n  +  1)))@i
\mvdash{}  (\muparrow{}(f  n))  \mvee{}  (\muparrow{}(g  n))


By

---

Latex:
((RW  assert\_pushdownC  (-1)  THENM  D  -1)  THEN  Auto)

---

Home Index