---

Step * 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)
⊢ ¬is-exception(imax(a;b))
BY
{ ((D 0 THENA Auto)
   THEN SquashConcl
   THEN Unfold `imax` 7
   THEN RepeatFor 2 ((ExceptionCases 7 THEN Auto THEN (CallByValueReduce 7 THENA 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)↓
⊢ ↓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)
\mvdash{}  \mneg{}is-exception(imax(a;b))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  SquashConcl
  THEN  Unfold  `imax`  7
  THEN  RepeatFor  2  ((ExceptionCases  7  THEN  Auto  THEN  (CallByValueReduce  7  THENA  Auto))))

---

Home Index