---

Step * 1 2 2 of Lemma apply-partial


1. A : Type
2. B : A ⟶ Type
3. a : Base
4. b : Base
5. c : a = b ∈ (partial(a:A ⟶ B[a]) × A)
6. value-type(B[snd(a)])
7. snd(a) ∈ A
8. ¬is-exception(fst(a))
9. (fst(a))↓ ⇒ (fst(a) ∈ a:A ⟶ B[a])
10. (fst(a)) (snd(a)) ∈ partial(B[snd(a)])
⊢ ¬is-exception((fst(b)) (snd(b)))
BY
{ (Assert (¬is-exception(fst(b))) ∧ ((fst(b))↓ ⇒ (fst(b) ∈ a:A ⟶ B[a])) BY
         ((Assert fst(b) ∈ partial(a:A ⟶ B[a]) BY
                 (GenConcl ⌜b = p ∈ (partial(a:A ⟶ B[a]) × A)⌝⋅ THEN Auto))
          THEN D 0
          THEN Try ((BLemma `partial-not-exception`  THEN Auto))
          THEN (D 0 THENA Auto)
          THEN BLemma `termination`
          THEN Auto)) }

1
1. A : Type
2. B : A ⟶ Type
3. a : Base
4. b : Base
5. c : a = b ∈ (partial(a:A ⟶ B[a]) × A)
6. value-type(B[snd(a)])
7. snd(a) ∈ A
8. ¬is-exception(fst(a))
9. (fst(a))↓ ⇒ (fst(a) ∈ a:A ⟶ B[a])
10. (fst(a)) (snd(a)) ∈ partial(B[snd(a)])
11. (¬is-exception(fst(b))) ∧ ((fst(b))↓ ⇒ (fst(b) ∈ a:A ⟶ B[a]))
⊢ ¬is-exception((fst(b)) (snd(b)))

---

Latex:

---

Latex:

1.  A  :  Type
2.  B  :  A  {}\mrightarrow{}  Type
3.  a  :  Base
4.  b  :  Base
5.  c  :  a  =  b
6.  value-type(B[snd(a)])
7.  snd(a)  \mmember{}  A
8.  \mneg{}is-exception(fst(a))
9.  (fst(a))\mdownarrow{}  {}\mRightarrow{}  (fst(a)  \mmember{}  a:A  {}\mrightarrow{}  B[a])
10.  (fst(a))  (snd(a))  \mmember{}  partial(B[snd(a)])
\mvdash{}  \mneg{}is-exception((fst(b))  (snd(b)))


By

---

Latex:
(Assert  (\mneg{}is-exception(fst(b)))  \mwedge{}  ((fst(b))\mdownarrow{}  {}\mRightarrow{}  (fst(b)  \mmember{}  a:A  {}\mrightarrow{}  B[a]))  BY
              ((Assert  fst(b)  \mmember{}  partial(a:A  {}\mrightarrow{}  B[a])  BY
                              (GenConcl  \mkleeneopen{}b  =  p\mkleeneclose{}\mcdot{}  THEN  Auto))
                THEN  D  0
                THEN  Try  ((BLemma  `partial-not-exception`    THEN  Auto))
                THEN  (D  0  THENA  Auto)
                THEN  BLemma  `termination`
                THEN  Auto))

---

Home Index