---

Step * 1 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) ∈ E supposing (G fix(g))↓
BY
{ (D 0 THENA (UniverseIsType THEN BLemma `has-value_wf_base` 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
10. (G fix(g))↓
⊢ G fix(g) ∈ E

---

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{}  E  supposing  (G  fix(g))\mdownarrow{}


By

---

Latex:
(D  0  THENA  (UniverseIsType  THEN  BLemma  `has-value\_wf\_base`  THEN  Auto))

---

Home Index