---

Step * 1 of Lemma fixpoint-induction-bottom-base


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)
BY
{ (BLemma `base-member-partial` THEN Try (Complete (EAuto 2)))⋅ }

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) ∈ E supposing (G fix(g))↓

---

Latex:

---

Latex:

1.  E  :  Type
2.  S  :  Type
3.  G  :  Base
4.  g  :  Base
5.  G  \mmember{}  S  {}\mrightarrow{}  partial(E)
6.  g  \mmember{}  S  {}\mrightarrow{}  S
7.  value-type(E)
8.  mono(E)
9.  \mbot{}  \mmember{}  S
\mvdash{}  G  fix(g)  \mmember{}  partial(E)


By

---

Latex:
(BLemma  `base-member-partial`  THEN  Try  (Complete  (EAuto  2)))\mcdot{}

---

Home Index