---

Step * of Lemma fix_wf_corec-partial1

∀[A:Type]
  (∀[F:Type ⟶ Type]
     ∀[f:⋂T:Type. ((T ⟶ partial(A)) ⟶ F[T] ⟶ partial(A))]. (fix(f) ∈ corec(T.F[T]) ⟶ partial(A)) 
     supposing ContinuousMonotone(T.F[T])) supposing 
     (mono(A) and 
     value-type(A))
BY
{ (Auto THEN BLemma `fix-corec-partial1` THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[A:Type]
    (\mforall{}[F:Type  {}\mrightarrow{}  Type]
          \mforall{}[f:\mcap{}T:Type.  ((T  {}\mrightarrow{}  partial(A))  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  partial(A))]
              (fix(f)  \mmember{}  corec(T.F[T])  {}\mrightarrow{}  partial(A)) 
          supposing  ContinuousMonotone(T.F[T]))  supposing 
          (mono(A)  and 
          value-type(A))


By

---

Latex:
(Auto  THEN  BLemma  `fix-corec-partial1`  THEN  Auto)

---

Home Index