Step
*
2
1
1
1
of Lemma
equal-partial
1. T : Type
2. value-type(T)
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ base-partial(T)) ∧ (y ∈ base-partial(T)) ∧ per-partial(T;x;y)))
6. x ∈ base-partial(T)
7. x1 ∈ base-partial(T)
8. per-partial(T;x;x1)
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λx,y. ((x ∈ base-partial(T)) ∧ (y ∈ base-partial(T)) ∧ per-partial(T;x;y)))
12. y ∈ base-partial(T)
13. y1 ∈ base-partial(T)
14. per-partial(T;y;y1)
15. (y)↓ supposing (x)↓
16. (x)↓ supposing (y)↓
17. (x)↓
⇒ (x = y ∈ T)
18. Refl(base-partial(T);x,y.per-partial(T;x;y))
19. Sym(base-partial(T);x,y.per-partial(T;x;y))
20. Trans(base-partial(T);x,y.per-partial(T;x;y))
⊢ per-partial(T;x;y1)
BY
{ UseTrans ⌜y⌝⋅ }
1
1. T : Type
2. value-type(T)
3. x : Base
4. x1 : Base
5. x = x1 ∈ pertype(λx,y. ((x ∈ base-partial(T)) ∧ (y ∈ base-partial(T)) ∧ per-partial(T;x;y)))
6. x ∈ base-partial(T)
7. x1 ∈ base-partial(T)
8. per-partial(T;x;x1)
9. y : Base
10. y1 : Base
11. y = y1 ∈ pertype(λx,y. ((x ∈ base-partial(T)) ∧ (y ∈ base-partial(T)) ∧ per-partial(T;x;y)))
12. y ∈ base-partial(T)
13. y1 ∈ base-partial(T)
14. per-partial(T;y;y1)
15. (y)↓ supposing (x)↓
16. (x)↓ supposing (y)↓
17. (x)↓
⇒ (x = y ∈ T)
18. Refl(base-partial(T);x,y.per-partial(T;x;y))
19. Sym(base-partial(T);x,y.per-partial(T;x;y))
20. Trans(base-partial(T);x,y.per-partial(T;x;y))
⊢ per-partial(T;x;y)
Latex:
Latex:
1. T : Type
2. value-type(T)
3. x : Base
4. x1 : Base
5. x = x1
6. x \mmember{} base-partial(T)
7. x1 \mmember{} base-partial(T)
8. per-partial(T;x;x1)
9. y : Base
10. y1 : Base
11. y = y1
12. y \mmember{} base-partial(T)
13. y1 \mmember{} base-partial(T)
14. per-partial(T;y;y1)
15. (y)\mdownarrow{} supposing (x)\mdownarrow{}
16. (x)\mdownarrow{} supposing (y)\mdownarrow{}
17. (x)\mdownarrow{} {}\mRightarrow{} (x = y)
18. Refl(base-partial(T);x,y.per-partial(T;x;y))
19. Sym(base-partial(T);x,y.per-partial(T;x;y))
20. Trans(base-partial(T);x,y.per-partial(T;x;y))
\mvdash{} per-partial(T;x;y1)
By
Latex:
UseTrans \mkleeneopen{}y\mkleeneclose{}\mcdot{}
Home
Index