---

Step * 2 of Lemma fix_wf_corec2'


1. F : Type ⟶ Type
2. H : Type ⟶ Type
3. Continuous(T.H[T])
4. G : ⋂T:{T:Type| corec(T.F[T]) ⊆r T} . (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]
5. fix(G) = fix(G) ∈ (⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])])
⊢ (⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])]) ⊆r H[⋂n:ℕ. primrec(n;Top;λ,T. F[T])]
BY
{ (With ⌜λn.primrec(n;Top;λ,T. F[T])⌝ (D 3)⋅ THEN Reduce (-1) THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  H  :  Type  {}\mrightarrow{}  Type
3.  Continuous(T.H[T])
4.  G  :  \mcap{}T:\{T:Type|  corec(T.F[T])  \msubseteq{}r  T\}  .  (H[T]  {}\mrightarrow{}  H[F[T]])  \mcap{}  Top  {}\mrightarrow{}  H[Top]
5.  fix(G)  =  fix(G)
\mvdash{}  (\mcap{}n:\mBbbN{}.  H[primrec(n;Top;\mlambda{},T.  F[T])])  \msubseteq{}r  H[\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T])]


By

---

Latex:
(With  \mkleeneopen{}\mlambda{}n.primrec(n;Top;\mlambda{},T.  F[T])\mkleeneclose{}  (D  3)\mcdot{}  THEN  Reduce  (-1)  THEN  Auto)\mcdot{}

---

Home Index