---

Step * of Lemma apply-partial

∀[A:Type]. ∀[B:A ⟶ Type]. ∀[f:partial(a:A ⟶ B[a])]. ∀[a:A].  f a ∈ partial(B[a]) supposing value-type(B[a])
BY
{ (RepeatFor 4 ((D 0 THENA Auto))
   THEN Assert ⌜(λp.let f,a = p in f a ∈ partial(B[a]) supposing value-type(B[a])) <f, a>⌝⋅
   THEN Reduce (-1)
   THEN Try (Trivial)
   THEN (GenConclTerm ⌜<f, a>⌝⋅ THENA Auto)
   THEN ThinVar `f'
   THEN ThinVar `a'
   THEN PointwiseFunctionality (-1)
   THEN ((UseWitness ⌜Ax⌝⋅ THEN Reduce 0 THEN AutoPairEta [1;1] 0⋅ THEN Auto)
   ORELSE (Reduce 0 THEN (AutoPairEta [2;1] 0⋅ THEN Auto)⋅ THEN ((AutoPairEta [3;1] 0⋅ THEN Auto) THEN EqCD))⋅
   )
   THEN (Assert snd(a) ∈ A BY
               (GenConcl ⌜a = p ∈ (partial(a:A ⟶ B[a]) × A)⌝⋅ THEN Auto))
   THEN Auto
   THEN (Assert (¬is-exception(fst(a))) ∧ ((fst(a))↓ ⇒ (fst(a) ∈ a:A ⟶ B[a])) BY
               ((Assert fst(a) ∈ partial(a:A ⟶ B[a]) BY
                       (GenConcl ⌜a = 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))
   THEN (Assert (fst(a)) (snd(a)) ∈ partial(B[snd(a)]) BY
               (BLemma `base-member-partial`
                THEN Auto
                THEN Try ((HasValueD (-1) THEN (D -3 THENA Trivial) THEN Auto))
                THEN (D 0 THENA Auto)
                THEN SquashConcl
                THEN ExceptionCases (-1)
                THEN Auto
                THEN FLemma `exception-not-value` [-3]
                THEN Auto))
   THEN (Trivial ORELSE (EqCD THEN Auto))
   THEN (BLemma `base-equal-partial` THENA Auto)
   THEN Try (Trivial)) }

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)])
⊢ ((((fst(a)) (snd(a)))↓ ⇐⇒ ((fst(b)) (snd(b)))↓)
  ∧ ((fst(a)) (snd(a))) = ((fst(b)) (snd(b))) ∈ B[snd(a)] supposing ((fst(a)) (snd(a)))↓)
∧ (¬is-exception((fst(a)) (snd(a))))
∧ (¬is-exception((fst(b)) (snd(b))))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}[B:A  {}\mrightarrow{}  Type].  \mforall{}[f:partial(a:A  {}\mrightarrow{}  B[a])].  \mforall{}[a:A].
    f  a  \mmember{}  partial(B[a])  supposing  value-type(B[a])


By

---

Latex:
(RepeatFor  4  ((D  0  THENA  Auto))
  THEN  Assert  \mkleeneopen{}(\mlambda{}p.let  f,a  =  p  in  f  a  \mmember{}  partial(B[a])  supposing  value-type(B[a]))  <f,  a>\mkleeneclose{}\mcdot{}
  THEN  Reduce  (-1)
  THEN  Try  (Trivial)
  THEN  (GenConclTerm  \mkleeneopen{}<f,  a>\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `f'
  THEN  ThinVar  `a'
  THEN  PointwiseFunctionality  (-1)
  THEN  ((UseWitness  \mkleeneopen{}Ax\mkleeneclose{}\mcdot{}  THEN  Reduce  0  THEN  AutoPairEta  [1;1]  0\mcdot{}  THEN  Auto)
  ORELSE  (Reduce  0
                  THEN  (AutoPairEta  [2;1]  0\mcdot{}  THEN  Auto)\mcdot{}
                  THEN  ((AutoPairEta  [3;1]  0\mcdot{}  THEN  Auto)  THEN  EqCD))\mcdot{}
  )
  THEN  (Assert  snd(a)  \mmember{}  A  BY
                          (GenConcl  \mkleeneopen{}a  =  p\mkleeneclose{}\mcdot{}  THEN  Auto))
  THEN  Auto
  THEN  (Assert  (\mneg{}is-exception(fst(a)))  \mwedge{}  ((fst(a))\mdownarrow{}  {}\mRightarrow{}  (fst(a)  \mmember{}  a:A  {}\mrightarrow{}  B[a]))  BY
                          ((Assert  fst(a)  \mmember{}  partial(a:A  {}\mrightarrow{}  B[a])  BY
                                          (GenConcl  \mkleeneopen{}a  =  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))
  THEN  (Assert  (fst(a))  (snd(a))  \mmember{}  partial(B[snd(a)])  BY
                          (BLemma  `base-member-partial`
                            THEN  Auto
                            THEN  Try  ((HasValueD  (-1)  THEN  (D  -3  THENA  Trivial)  THEN  Auto))
                            THEN  (D  0  THENA  Auto)
                            THEN  SquashConcl
                            THEN  ExceptionCases  (-1)
                            THEN  Auto
                            THEN  FLemma  `exception-not-value`  [-3]
                            THEN  Auto))
  THEN  (Trivial  ORELSE  (EqCD  THEN  Auto))
  THEN  (BLemma  `base-equal-partial`  THENA  Auto)
  THEN  Try  (Trivial))

---

Home Index