Step
*
1
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)↓
10. a ∈ ℕ
11. b ∈ ℕ
⊢ ↓False
BY
{ (FLemma `exception-not-value` [-5] THEN Auto) }
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{}
10.  a  \mmember{}  \mBbbN{}
11.  b  \mmember{}  \mBbbN{}
\mvdash{}  \mdownarrow{}False
By
Latex:
(FLemma  `exception-not-value`  [-5]  THEN  Auto)
Home
Index