---

Step * 1 of Lemma fix_wf_mutual-corec-partial1


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)
BY
{ SubsumeC ⌜(i:ℕk ⟶ (mutual-corec(T.F[T]) i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[mutual-corec(T.F[T])] i) ⟶ partial(A)⌝⋅ }

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 ⟶ (mutual-corec(T.F[T]) i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[mutual-corec(T.F[T])] i) ⟶ partial(A)

2
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])]
10. f = f ∈ ((i:ℕk ⟶ (mutual-corec(T.F[T]) i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[mutual-corec(T.F[T])] i) ⟶ partial(A))
⊢ ((i:ℕk ⟶ (mutual-corec(T.F[T]) i) ⟶ partial(A)) ⟶ i:ℕk ⟶ (F[mutual-corec(T.F[T])] i) ⟶ partial(A))
    ⊆r ((i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A)) ⟶ i:ℕk ⟶ m-corec(T.F[T];i) ⟶ partial(A))

---

Latex:

---

Latex:

1.  A  :  Type
2.  value-type(A)
3.  mono(A)
4.  k  :  \mBbbN{}
5.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
6.  k-Monotone(T.F[T])
7.  \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)
8.  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))
9.  mutual-corec(T.F[T])  \mequiv{}  F[mutual-corec(T.F[T])]
\mvdash{}  f  \mmember{}  (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)


By

---

Latex:
SubsumeC  \mkleeneopen{}(i:\mBbbN{}k  {}\mrightarrow{}  (mutual-corec(T.F[T])  i)  {}\mrightarrow{}  partial(A))
                    {}\mrightarrow{}  i:\mBbbN{}k
                    {}\mrightarrow{}  (F[mutual-corec(T.F[T])]  i)
                    {}\mrightarrow{}  partial(A)\mkleeneclose{}\mcdot{}

---

Home Index