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. Type
2. Type
3. value-type(E)
4. mono(E)
5. ⊥ ∈ S
6. S ⟶ partial(E)
7. S ⟶ S
⊢ 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