---

Step * 1 1 2 of Lemma posint_well_fnd


1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
⊢ WellFnd{i}(ℕ+;x,y.(x | y) ∧ (¬(y | x)))
BY
{ ((RWH (HypC 1) 0) THENA Auto) }

1
1. ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b}
⊢ WellFnd{i}(ℕ+;x,y.x < y)

---

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)  \mwedge{}  (\mneg{}(y  |  x)))


By

---

Latex:
((RWH  (HypC  1)  0)  THENA  Auto)

---

Home Index