---

Step * 1 1 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)])
⊢ (((fst(a)) (snd(a)))↓ ⇐⇒ ((fst(b)) (snd(b)))↓)
∧ ((fst(a)) (snd(a))) = ((fst(b)) (snd(b))) ∈ B[snd(a)] supposing ((fst(a)) (snd(a)))↓
BY
{ ((RepeatFor 2 ((D 0 THENA Auto)) THEN Try ((D 0 THENA Auto)))
   THEN ((Assert (fst(a)) = (fst(b)) ∈ (a:A ⟶ B[a]) BY
                Complete (((BLemma `termination-equality-base` THEN Auto)
                           THEN Try ((HasValueD (-1) THEN Complete (Auto)))
                           THEN Try ((D 0 THEN With ⌜snd(a)⌝ (D 0)⋅ THEN Auto)))))
        ORELSE (Assert (fst(b)) = (fst(a)) ∈ (a:A ⟶ B[a]) BY
                      Complete (((BLemma `termination-equality-base` THEN Auto)
                                 THEN Try ((HasValueD (-1) THEN Complete (Auto)))
                                 THEN Try ((D 0 THEN With ⌜snd(a)⌝ (D 0)⋅ 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. ((fst(a)) (snd(a)))↓
12. (fst(a)) = (fst(b)) ∈ (a:A ⟶ B[a])
⊢ ((fst(b)) (snd(b)))↓

2
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. ((fst(b)) (snd(b)))↓
12. (fst(b)) = (fst(a)) ∈ (a:A ⟶ B[a])
⊢ ((fst(a)) (snd(a)))↓

3
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. ((fst(a)) (snd(a)))↓
12. (fst(a)) = (fst(b)) ∈ (a:A ⟶ B[a])
⊢ ((fst(a)) (snd(a))) = ((fst(b)) (snd(b))) ∈ B[snd(a)]

---

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{}  (((fst(a))  (snd(a)))\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  ((fst(b))  (snd(b)))\mdownarrow{})
\mwedge{}  ((fst(a))  (snd(a)))  =  ((fst(b))  (snd(b)))  supposing  ((fst(a))  (snd(a)))\mdownarrow{}


By

---

Latex:
((RepeatFor  2  ((D  0  THENA  Auto))  THEN  Try  ((D  0  THENA  Auto)))
  THEN  ((Assert  (fst(a))  =  (fst(b))  BY
                            Complete  (((BLemma  `termination-equality-base`  THEN  Auto)
                                                  THEN  Try  ((HasValueD  (-1)  THEN  Complete  (Auto)))
                                                  THEN  Try  ((D  0  THEN  With  \mkleeneopen{}snd(a)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))))
            ORELSE  (Assert  (fst(b))  =  (fst(a))  BY
                                        Complete  (((BLemma  `termination-equality-base`  THEN  Auto)
                                                              THEN  Try  ((HasValueD  (-1)  THEN  Complete  (Auto)))
                                                              THEN  Try  ((D  0  THEN  With  \mkleeneopen{}snd(a)\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))))
            )
  )

---

Home Index