---

Step * 1 of Lemma corec-ext


1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. ∀n:ℕ. (primrec(n + 1;Top;λj,T. F[T]) ⊆r primrec(n;Top;λj,T. F[T]))
⊢ corec(T.F[T]) ≡ F[corec(T.F[T])]
BY
{ (D 0 THEN All (Unfold `corec`))⋅ }

1
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. ∀n:ℕ. (primrec(n + 1;Top;λj,T. F[T]) ⊆r primrec(n;Top;λj,T. F[T]))
⊢ (⋂n:ℕ. primrec(n;Top;λ,T. F[T])) ⊆r F[⋂n:ℕ. primrec(n;Top;λ,T. F[T])]

2
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. ∀n:ℕ. (primrec(n + 1;Top;λj,T. F[T]) ⊆r primrec(n;Top;λj,T. F[T]))
⊢ F[⋂n:ℕ. primrec(n;Top;λ,T. F[T])] ⊆r (⋂n:ℕ. primrec(n;Top;λ,T. F[T]))

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  ContinuousMonotone(T.F[T])
3.  \mforall{}n:\mBbbN{}.  (primrec(n  +  1;Top;\mlambda{}j,T.  F[T])  \msubseteq{}r  primrec(n;Top;\mlambda{}j,T.  F[T]))
\mvdash{}  corec(T.F[T])  \mequiv{}  F[corec(T.F[T])]


By

---

Latex:
(D  0  THEN  All  (Unfold  `corec`))\mcdot{}

---

Home Index