---

Step * of Lemma fixpoint-induction-bottom

∀[E,S:Type].
  (∀[G:S ⟶ partial(E)]. ∀[g:S ⟶ S].  (G fix(g) ∈ partial(E))) supposing ((⊥ ∈ S) and mono(E) and value-type(E))
BY
{ (UnivCD THENA (Try (Complete (Auto)) THEN Try (BLemma `bottom-member-prop`) THEN Auto)) }

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

---

Latex:

---

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


By

---

Latex:
(UnivCD  THENA  (Try  (Complete  (Auto))  THEN  Try  (BLemma  `bottom-member-prop`)  THEN  Auto))

---

Home Index