---

Step * 1 1 of Lemma posint_well_fnd


WellFnd{i}(ℕ+;x,y.(x | y) ∧ (¬(y | x)))
BY
{ Assert ∀a,b:ℕ+.  {((a | b) ∧ (¬(b | a))) ⇒ a < b} 
THENA ((Unfold `guard` 0 THEN UnivCD) THENA Auto) }

1
1. a : ℕ+
2. b : ℕ+
3. (a | b) ∧ (¬(b | a))
⊢ a < b

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

---

Latex:

---

Latex:

WellFnd\{i\}(\mBbbN{}\msupplus{};x,y.(x  |  y)  \mwedge{}  (\mneg{}(y  |  x)))


By

---

Latex:
Assert  \mforall{}a,b:\mBbbN{}\msupplus{}.    \{((a  |  b)  \mwedge{}  (\mneg{}(b  |  a)))  {}\mRightarrow{}  a  <  b\} 
THENA  ((Unfold  `guard`  0  THEN  UnivCD)  THENA  Auto)

---

Home Index