---

Step * of Lemma fixpoint-induction2

∀A:Type. ∀T:A ⟶ Type.
  ((A ⊆r Base)
  ⇒ (∀a:A. value-type(T[a]))
  ⇒ (∀a:A. mono(T[a]))
  ⇒ (∀f:(a:A ⟶ partial(T[a])) ⟶ a:A ⟶ partial(T[a]) ⋂ Base. (fix(f) ∈ a:A ⟶ partial(T[a]))))
BY
{ (Auto
   THEN (Assert (⊥ ∈ Void ⟶ Void) ∧ (fix(f) ∈ Void ⟶ Void) BY
               Auto)
   THEN BetterExt⋅
   THEN Try (Complete (Auto))
   THEN (D 0 THENA Auto)
   THEN ((Assert ⊥ ∈ a:A ⟶ partial(T[a]) BY
                (BetterExt ⋅ THEN Try (Complete (Auto)) THEN (D 0 THENA Auto) THEN Strictness⋅ THEN Auto))
         THEN BLemma `base-member-partial`
         THEN Try (Complete (Auto)))⋅) }

1
1. A : Type
2. T : A ⟶ Type
3. A ⊆r Base
4. ∀a:A. value-type(T[a])
5. ∀a:A. mono(T[a])
6. f : (a:A ⟶ partial(T[a])) ⟶ a:A ⟶ partial(T[a]) ⋂ Base
7. (⊥ ∈ Void ⟶ Void) ∧ (fix(f) ∈ Void ⟶ Void)
8. a : A
9. ⊥ ∈ a:A ⟶ partial(T[a])
⊢ fix(f) a ∈ T[a] supposing (fix(f) a)↓

2
1. A : Type
2. T : A ⟶ Type
3. A ⊆r Base
4. ∀a:A. value-type(T[a])
5. ∀a:A. mono(T[a])
6. f : (a:A ⟶ partial(T[a])) ⟶ a:A ⟶ partial(T[a]) ⋂ Base
7. (⊥ ∈ Void ⟶ Void) ∧ (fix(f) ∈ Void ⟶ Void)
8. a : A
9. ⊥ ∈ a:A ⟶ partial(T[a])
⊢ ¬is-exception(fix(f) a)

---

Latex:

---

Latex:
\mforall{}A:Type.  \mforall{}T:A  {}\mrightarrow{}  Type.
    ((A  \msubseteq{}r  Base)
    {}\mRightarrow{}  (\mforall{}a:A.  value-type(T[a]))
    {}\mRightarrow{}  (\mforall{}a:A.  mono(T[a]))
    {}\mRightarrow{}  (\mforall{}f:(a:A  {}\mrightarrow{}  partial(T[a]))  {}\mrightarrow{}  a:A  {}\mrightarrow{}  partial(T[a])  \mcap{}  Base.  (fix(f)  \mmember{}  a:A  {}\mrightarrow{}  partial(T[a]))))


By

---

Latex:
(Auto
  THEN  (Assert  (\mbot{}  \mmember{}  Void  {}\mrightarrow{}  Void)  \mwedge{}  (fix(f)  \mmember{}  Void  {}\mrightarrow{}  Void)  BY
                          Auto)
  THEN  BetterExt\mcdot{}
  THEN  Try  (Complete  (Auto))
  THEN  (D  0  THENA  Auto)
  THEN  ((Assert  \mbot{}  \mmember{}  a:A  {}\mrightarrow{}  partial(T[a])  BY
                            (BetterExt  \mcdot{}
                              THEN  Try  (Complete  (Auto))
                              THEN  (D  0  THENA  Auto)
                              THEN  Strictness\mcdot{}
                              THEN  Auto))
              THEN  BLemma  `base-member-partial`
              THEN  Try  (Complete  (Auto)))\mcdot{})

---

Home Index