---

Step * 1 1 2 1 of Lemma posint_well_fnd


1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
⊢ WellFnd{i}(ℕ+;x,y.x < y)
BY
{ RepeatFor 2 ((D 0 THEN Auto)) }

1
1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
2. [P] : ℕ+ ⟶ ℙ
3. ∀j:ℕ+. ((∀k:ℕ+. (k < j ⇒ P[k])) ⇒ P[j])
4. n : ℕ+
⊢ P[n]

---

Latex:

---

Latex:

1.  \mforall{}a,b:\mBbbN{}\msupplus{}.    \{((a  |  b)  \mwedge{}  (\mneg{}(b  |  a)))  {}\mRightarrow{}  a  <  b\}
\mvdash{}  WellFnd\{i\}(\mBbbN{}\msupplus{};x,y.x  <  y)


By

---

Latex:
RepeatFor  2  ((D  0  THEN  Auto))

---

Home Index