---

Step * of Lemma apply-2-partial

∀[A,B,C:Type].
  (∀[f:Base]
     (∀[a:partial(A)]. ∀[b:partial(B)].  (f a b ∈ partial(C))) supposing 
        ((∀a:partial(A). ∀b:partial(B).  ((f a b)↓ ⇒ ((a)↓ ∧ (b)↓))) and 
        (∀a:partial(A). ∀b:partial(B).  (((¬is-exception(a)) ∧ (¬is-exception(b))) ⇒ (¬is-exception(f a b)))) and 
        (f ∈ A ⟶ B ⟶ C))) supposing 
     (value-type(C) and 
     (value-type(B) ∧ (B ⊆r Base)) and 
     (value-type(A) ∧ (A ⊆r Base)))
BY
{ (RepeatFor 7 (Intro)
   THEN (Assert partial(Base) ⊆r Base BY
               Auto)
   THEN (Assert partial(A) ⊆r Base BY
               Auto)
   THEN (Assert partial(B) ⊆r Base BY
               Auto)
   THEN Intros
   THEN (BLemma `base-member-partial` THENA Auto)) }

1
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)

2
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)
⊢ f a b ∈ C supposing (f a b)↓

3
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)

---

Latex:

---

Latex:
\mforall{}[A,B,C:Type].
    (\mforall{}[f:Base]
          (\mforall{}[a:partial(A)].  \mforall{}[b:partial(B)].    (f  a  b  \mmember{}  partial(C)))  supposing 
                ((\mforall{}a:partial(A).  \mforall{}b:partial(B).    ((f  a  b)\mdownarrow{}  {}\mRightarrow{}  ((a)\mdownarrow{}  \mwedge{}  (b)\mdownarrow{})))  and 
                (\mforall{}a:partial(A).  \mforall{}b:partial(B).
                      (((\mneg{}is-exception(a))  \mwedge{}  (\mneg{}is-exception(b)))  {}\mRightarrow{}  (\mneg{}is-exception(f  a  b))))  and 
                (f  \mmember{}  A  {}\mrightarrow{}  B  {}\mrightarrow{}  C)))  supposing 
          (value-type(C)  and 
          (value-type(B)  \mwedge{}  (B  \msubseteq{}r  Base))  and 
          (value-type(A)  \mwedge{}  (A  \msubseteq{}r  Base)))


By

---

Latex:
(RepeatFor  7  (Intro)
  THEN  (Assert  partial(Base)  \msubseteq{}r  Base  BY
                          Auto)
  THEN  (Assert  partial(A)  \msubseteq{}r  Base  BY
                          Auto)
  THEN  (Assert  partial(B)  \msubseteq{}r  Base  BY
                          Auto)
  THEN  Intros
  THEN  (BLemma  `base-member-partial`  THENA  Auto))

---

Home Index