---

Step * 1 1 2 of Lemma partial-base


1. x : base-partial(Base)
2. x1 : base-partial(Base)
3. (x1)↓ supposing (x)↓
4. (x)↓ supposing (x1)↓
5. x = x1 ∈ Base supposing (x)↓
6. is-exception(x1)
⊢ x1 ≤ x
BY
{ ((Assert ¬is-exception(x1) BY Auto) THEN Auto) }

---

Latex:

---

Latex:

1.  x  :  base-partial(Base)
2.  x1  :  base-partial(Base)
3.  (x1)\mdownarrow{}  supposing  (x)\mdownarrow{}
4.  (x)\mdownarrow{}  supposing  (x1)\mdownarrow{}
5.  x  =  x1  supposing  (x)\mdownarrow{}
6.  is-exception(x1)
\mvdash{}  x1  \mleq{}  x


By

---

Latex:
((Assert  \mneg{}is-exception(x1)  BY  Auto)  THEN  Auto)

---

Home Index