---

Step * of Lemma fix-mutual-corec-partial1

∀[A:Type]
  (∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type]. ∀[f:(i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A))
                                                ⟶ i:ℕk
                                                ⟶ m-corec(T.F[T];i)
                                                ⟶ partial(A)].
     (fix(f) ∈ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A))) supposing 
     (mono(A) and 
     value-type(A))
BY
{ (Auto THEN (ExtWith [`i'] [⌜Void ⟶ Void⌝]⋅ THENA Auto) THEN (ExtWith [`x'] [⌜Void ⟶ Void⌝]⋅ THENA Auto)) }

1
1. A : Type
2. value-type(A)
3. mono(A)
4. k : ℕ
5. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
6. f : (i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)) ⟶ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)
7. i : ℕk
8. x : m-corec(T.F[T];i)
⊢ fix(f) i x ∈ partial(A)

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (ExtWith  [`i']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (ExtWith  [`x']  [\mkleeneopen{}Void  {}\mrightarrow{}  Void\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index