---

Step * 1 1 of Lemma imax-wf-partial


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(\mBbbZ{})  \msubseteq{}r  Base
3.  a  :  partial(\mBbbZ{})
4.  b  :  partial(\mBbbZ{})
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{}  \mBbbZ{}  BY
                (BLemma  `termination`  THEN  Auto))
  THEN  (Assert  b  \mmember{}  \mBbbZ{}  BY
                          (BLemma  `termination`  THEN  Auto))
  )

---

Home Index