---

Step * of Lemma fix_wf_mutual-corec-partial-nat

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
  ∀[f:⋂T:ℕk ⟶ Type. ((i:ℕk ⟶ (T i) ⟶ partial(ℕ)) ⟶ i:ℕk ⟶ (F[T] i) ⟶ partial(ℕ))]
    (fix(f) ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(ℕ)) 
  supposing k-Monotone(T.F[T]) ∧ (∀i,j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i))
BY
{ Auto }

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].
    \mforall{}[f:\mcap{}T:\mBbbN{}k  {}\mrightarrow{}  Type.  ((i:\mBbbN{}k  {}\mrightarrow{}  (T  i)  {}\mrightarrow{}  partial(\mBbbN{}))  {}\mrightarrow{}  i:\mBbbN{}k  {}\mrightarrow{}  (F[T]  i)  {}\mrightarrow{}  partial(\mBbbN{}))]
        (fix(f)  \mmember{}  i:\mBbbN{}k  {}\mrightarrow{}  m-corec(T.F[T];i)  {}\mrightarrow{}  partial(\mBbbN{})) 
    supposing  k-Monotone(T.F[T])
    \mwedge{}  (\mforall{}i,j:\mBbbN{}k.  \mforall{}Z:\mBbbN{}k  {}\mrightarrow{}  Type.    Continuous(X.F[\mlambda{}i.if  (i  =\msubz{}  j)  then  X  else  Z  i  fi  ]  i))


By

---

Latex:
Auto

---

Home Index