---

Step * 3 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)
⊢ ¬is-exception(f a b)
BY
{ ((InstLemma `partial-not-exception` [⌜A⌝;⌜a⌝]⋅ THENA Auto)
   THEN (InstLemma `partial-not-exception` [⌜B⌝;⌜b⌝]⋅ THENA Auto)
   THEN D 0
   THEN Auto
   THEN InstHyp [⌜a⌝;⌜b⌝] (-7)⋅
   THEN 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{}  \mneg{}is-exception(f  a  b)


By

---

Latex:
((InstLemma  `partial-not-exception`  [\mkleeneopen{}A\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `partial-not-exception`  [\mkleeneopen{}B\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  0
  THEN  Auto
  THEN  InstHyp  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]  (-7)\mcdot{}
  THEN  Auto)

---

Home Index