---

Step * of Lemma fix_wf_mutual-corec-partial1

∀[A:Type]
  (∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
     ∀[f:⋂T:ℕk ⟶ Type. ((i:ℕk ⟶ (T i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[T] i) ⟶ partial(A))]
       (fix(f) ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)) 
     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))) supposing 
     (mono(A) and 
     value-type(A))
BY
{ (Auto THEN BLemma `fix-mutual-corec-partial1` THEN Auto THEN (InstLemma `mutual-corec-ext2` [⌜k⌝;⌜F⌝]⋅ THENA Auto)) }

1
1. A : Type
2. value-type(A)
3. mono(A)
4. k : ℕ
5. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
6. k-Monotone(T.F[T])
7. ∀i,j:ℕk. ∀Z:ℕk ⟶ Type.  Continuous(X.F[λi.if (i =z j) then X else Z i fi ] i)
8. f : ⋂T:ℕk ⟶ Type. ((i:ℕk ⟶ (T i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[T] i) ⟶ partial(A))
9. mutual-corec(T.F[T]) ≡ F[mutual-corec(T.F[T])]
⊢ f ∈ (i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)) ⟶ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)

---

Latex:

---

Latex:
\mforall{}[A:Type]
    (\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(A))  {}\mrightarrow{}  i:\mBbbN{}k  {}\mrightarrow{}  (F[T]  i)  {}\mrightarrow{}  partial(A))]
              (fix(f)  \mmember{}  i:\mBbbN{}k  {}\mrightarrow{}  m-corec(T.F[T];i)  {}\mrightarrow{}  partial(A)) 
          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)))  supposing 
          (mono(A)  and 
          value-type(A))


By

---

Latex:
(Auto
  THEN  BLemma  `fix-mutual-corec-partial1`
  THEN  Auto
  THEN  (InstLemma  `mutual-corec-ext2`  [\mkleeneopen{}k\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index