Step
*
1
of Lemma
apply-2-partial
1. A : Type
2. B : Type
3. C : Type
4. value-type(A) ∧ (A ⊆r Base)
5. value-type(B) ∧ (B ⊆r Base)
6. value-type(C)
7. f : Base
8. partial(Base) ⊆r Base
9. partial(A) ⊆r Base
10. partial(B) ⊆r Base
11. f ∈ A ⟶ B ⟶ C
12. ∀a:partial(A). ∀b:partial(B). (((¬is-exception(a)) ∧ (¬is-exception(b)))
⇒ (¬is-exception(f a b)))
13. ∀a:partial(A). ∀b:partial(B). ((f a b)↓
⇒ ((a)↓ ∧ (b)↓))
14. a : partial(A)
15. b : partial(B)
⊢ value-type(C)
BY
{ Auto }
Latex:
Latex:
1. A : Type
2. B : Type
3. C : Type
4. value-type(A) \mwedge{} (A \msubseteq{}r Base)
5. value-type(B) \mwedge{} (B \msubseteq{}r Base)
6. value-type(C)
7. f : Base
8. partial(Base) \msubseteq{}r Base
9. partial(A) \msubseteq{}r Base
10. partial(B) \msubseteq{}r Base
11. f \mmember{} A {}\mrightarrow{} B {}\mrightarrow{} C
12. \mforall{}a:partial(A). \mforall{}b:partial(B).
(((\mneg{}is-exception(a)) \mwedge{} (\mneg{}is-exception(b))) {}\mRightarrow{} (\mneg{}is-exception(f a b)))
13. \mforall{}a:partial(A). \mforall{}b:partial(B). ((f a b)\mdownarrow{} {}\mRightarrow{} ((a)\mdownarrow{} \mwedge{} (b)\mdownarrow{}))
14. a : partial(A)
15. b : partial(B)
\mvdash{} value-type(C)
By
Latex:
Auto
Home
Index