Step
*
1
of Lemma
base-member-partial
1. [A] : Type
2. [%] : value-type(A)
3. [a] : Base
4. [%1] : a ∈ A supposing (a)↓
⊢ a ∈ partial(A) supposing ¬is-exception(a)
BY
{ TACTIC:D 0 }
1
1. A : Type
2. value-type(A)
3. a : Base
4. a ∈ A supposing (a)↓
5. ¬is-exception(a)
⊢ a ∈ partial(A)
2
.....wf.....
1. A : Type
2. value-type(A)
3. a : Base
4. a ∈ A supposing (a)↓
⊢ istype(¬is-exception(a))
Latex:
Latex:
1. [A] : Type
2. [\%] : value-type(A)
3. [a] : Base
4. [\%1] : a \mmember{} A supposing (a)\mdownarrow{}
\mvdash{} a \mmember{} partial(A) supposing \mneg{}is-exception(a)
By
Latex:
TACTIC:D 0
Home
Index