---

Step * 1 of Lemma base-equal-partial


1. A : Type
2. value-type(A)
3. a : Base
4. b : Base
5. (((a)↓ ⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b))
⊢ a = b ∈ partial(A)
BY
{ (EqTypeCD
   THEN Try (Complete (Auto))
   THEN (Try (At ⌜Type⌝ MemTypeCD⋅)
         THEN Try ((MemCD THEN Try ((Unfold `member` 0 THEN BLemma `equal-wf-base` THEN Complete (Auto))) THEN Auto))
         THEN Try (Complete (Auto)))⋅) }

1
.....set predicate..... 
1. A : Type
2. value-type(A)
3. a : Base
4. b : Base
5. (((a)↓ ⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b))
⊢ b ∈ A supposing (b)↓ ∧ (¬is-exception(b))

2
.....antecedent..... 
1. A : Type
2. value-type(A)
3. a : Base
4. b : Base
5. (((a)↓ ⇐⇒ (b)↓) ∧ a = b ∈ A supposing (a)↓) ∧ (¬is-exception(a)) ∧ (¬is-exception(b))
⊢ per-partial(A;a;b)

---

Latex:

---

Latex:

1.  A  :  Type
2.  value-type(A)
3.  a  :  Base
4.  b  :  Base
5.  (((a)\mdownarrow{}  \mLeftarrow{}{}\mRightarrow{}  (b)\mdownarrow{})  \mwedge{}  a  =  b  supposing  (a)\mdownarrow{})  \mwedge{}  (\mneg{}is-exception(a))  \mwedge{}  (\mneg{}is-exception(b))
\mvdash{}  a  =  b


By

---

Latex:
(EqTypeCD
  THEN  Try  (Complete  (Auto))
  THEN  (Try  (At  \mkleeneopen{}Type\mkleeneclose{}  MemTypeCD\mcdot{})
              THEN  Try  ((MemCD
                                    THEN  Try  ((Unfold  `member`  0  THEN  BLemma  `equal-wf-base`  THEN  Complete  (Auto)))
                                    THEN  Auto))
              THEN  Try  (Complete  (Auto)))\mcdot{})

---

Home Index