---

Step * 1 1 of Lemma partial-base

.....equality..... 
1. x : base-partial(Base)
2. x1 : base-partial(Base)
3. uiff((x)↓;(x1)↓)
4. x = x1 ∈ Base supposing (x)↓
⊢ x ~ x1
BY
{ ((SqequalSqle THEN Auto) THEN Try ((OnMaybeHyp 4 (\h. HypSubst' h 0⋅) THEN Complete (Auto)))) }

1
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(x)
⊢ x ≤ x1

2
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

---

Latex:

---

Latex:
.....equality..... 
1.  x  :  base-partial(Base)
2.  x1  :  base-partial(Base)
3.  uiff((x)\mdownarrow{};(x1)\mdownarrow{})
4.  x  =  x1  supposing  (x)\mdownarrow{}
\mvdash{}  x  \msim{}  x1


By

---

Latex:
((SqequalSqle  THEN  Auto)  THEN  Try  ((OnMaybeHyp  4  (\mbackslash{}h.  HypSubst'  h  0\mcdot{})  THEN  Complete  (Auto))))

---

Home Index