---

Step * of Lemma int_upper_uwell_founded

∀n:ℤ. uWellFnd({n...};x,y.x < y)
BY
{ (Auto
   THEN InstLemma `uniform-comp-nat-induction` []
   THEN Unfold `uwellfounded` 0
   THEN Auto
   THEN (InstHyp [⌜λ2i.P[n + i]⌝] 2⋅ THENA Auto')) }

1
1. n : ℤ
2. ∀[P:ℕ ⟶ ℙ]. ((∀[n:ℕ]. ((∀[m:ℕn]. P[m]) ⇒ P[n])) ⇒ (∀[n:ℕ]. P[n]))
3. [P] : {n...} ⟶ ℙ
4. ∀[j:{n...}]. ((∀[k:{k:{n...}| k < j} ]. P[k]) ⇒ P[j])
5. [n1] : {n...}
6. [n@0] : ℕ
7. ∀[m:ℕn@0]. P[n + m]
⊢ P[n + n@0]

2
1. n : ℤ
2. ∀[P:ℕ ⟶ ℙ]. ((∀[n:ℕ]. ((∀[m:ℕn]. P[m]) ⇒ P[n])) ⇒ (∀[n:ℕ]. P[n]))
3. [P] : {n...} ⟶ ℙ
4. ∀[j:{n...}]. ((∀[k:{k:{n...}| k < j} ]. P[k]) ⇒ P[j])
5. [n1] : {n...}
6. ∀[n@0:ℕ]. P[n + n@0]
⊢ P[n1]

---

Latex:

---

Latex:
\mforall{}n:\mBbbZ{}.  uWellFnd(\{n...\};x,y.x  <  y)


By

---

Latex:
(Auto
  THEN  InstLemma  `uniform-comp-nat-induction`  []
  THEN  Unfold  `uwellfounded`  0
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}i.P[n  +  i]\mkleeneclose{}]  2\mcdot{}  THENA  Auto'))

---

Home Index