---

Step * 1 1 of Lemma imax-wf-partial-nat


1. partial(Base) ⊆r Base
2. partial(ℕ) ⊆r Base
3. a : partial(ℕ)
4. b : partial(ℕ)
5. ¬is-exception(a)
6. ¬is-exception(b)
7. is-exception(if a ≤z b then b else a fi )
8. (a)↓
9. (b)↓
⊢ ↓False
BY
{ ((Assert a ∈ ℕ BY (BLemma `termination` THEN Auto)) THEN (Assert b ∈ ℕ BY (BLemma `termination` THEN Auto))) }

1
1. partial(Base) ⊆r Base
2. partial(ℕ) ⊆r Base
3. a : partial(ℕ)
4. b : partial(ℕ)
5. ¬is-exception(a)
6. ¬is-exception(b)
7. is-exception(if a ≤z b then b else a fi )
8. (a)↓
9. (b)↓
10. a ∈ ℕ
11. b ∈ ℕ
⊢ ↓False

---

Latex:

---

Latex:

1.  partial(Base)  \msubseteq{}r  Base
2.  partial(\mBbbN{})  \msubseteq{}r  Base
3.  a  :  partial(\mBbbN{})
4.  b  :  partial(\mBbbN{})
5.  \mneg{}is-exception(a)
6.  \mneg{}is-exception(b)
7.  is-exception(if  a  \mleq{}z  b  then  b  else  a  fi  )
8.  (a)\mdownarrow{}
9.  (b)\mdownarrow{}
\mvdash{}  \mdownarrow{}False


By

---

Latex:
((Assert  a  \mmember{}  \mBbbN{}  BY
                (BLemma  `termination`  THEN  Auto))
  THEN  (Assert  b  \mmember{}  \mBbbN{}  BY
                          (BLemma  `termination`  THEN  Auto))
  )

---

Home Index