---

Step * of Lemma fixpoint-induction-bottom-base

∀E,S:Type. ∀G,g:Base.
  ((G ∈ S ⟶ partial(E)) ⇒ (g ∈ S ⟶ S) ⇒ value-type(E) ⇒ mono(E) ⇒ (⊥ ∈ S) ⇒ (G fix(g) ∈ partial(E)))
BY
{ TACTIC:(UnivCD
          THENA (Try (Complete (((Unfold `member` 0 THEN BLemma `equal-wf-base`) THEN Auto)))
                 THEN Try (BLemma `bottom-member-prop`)
                 THEN Auto)
          ) }

1
1. E : Type
2. S : Type
3. G : Base
4. g : Base
5. G ∈ S ⟶ partial(E)
6. g ∈ S ⟶ S
7. value-type(E)
8. mono(E)
9. ⊥ ∈ S
⊢ G fix(g) ∈ partial(E)

---

Latex:

---

Latex:
\mforall{}E,S:Type.  \mforall{}G,g:Base.
    ((G  \mmember{}  S  {}\mrightarrow{}  partial(E))
    {}\mRightarrow{}  (g  \mmember{}  S  {}\mrightarrow{}  S)
    {}\mRightarrow{}  value-type(E)
    {}\mRightarrow{}  mono(E)
    {}\mRightarrow{}  (\mbot{}  \mmember{}  S)
    {}\mRightarrow{}  (G  fix(g)  \mmember{}  partial(E)))


By

---

Latex:
TACTIC:(UnivCD
                THENA  (Try  (Complete  (((Unfold  `member`  0  THEN  BLemma  `equal-wf-base`)  THEN  Auto)))
                              THEN  Try  (BLemma  `bottom-member-prop`)
                              THEN  Auto)
                )

---

Home Index