---

Step * 2 1 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)
16. (f a b)↓
17. (a)↓ ∧ (b)↓
⊢ f a b ∈ C
BY
{ ((GenConcl ⌜a = n ∈ A⌝⋅ THENA (BLemma `termination` THEN Auto))
   THEN (GenConcl ⌜b = m ∈ B⌝⋅ THENA (BLemma `termination` THEN 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)
16. (f a b)↓
17. (a)↓ ∧ (b)↓
18. n : A
19. a = n ∈ A
20. m : B
21. b = m ∈ B
⊢ f n m ∈ C

---

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)
16.  (f  a  b)\mdownarrow{}
17.  (a)\mdownarrow{}  \mwedge{}  (b)\mdownarrow{}
\mvdash{}  f  a  b  \mmember{}  C


By

---

Latex:
((GenConcl  \mkleeneopen{}a  =  n\mkleeneclose{}\mcdot{}  THENA  (BLemma  `termination`  THEN  Auto))
  THEN  (GenConcl  \mkleeneopen{}b  =  m\mkleeneclose{}\mcdot{}  THENA  (BLemma  `termination`  THEN  Auto))
  )

---

Home Index