---

Step * 1 1 of Lemma mutual-corec-ext


1. [k] : ℕ
2. [F] : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. [%] : k-Continuous(T.F[T])
4. [%1] : k-Monotone(T.F[T])
5. ∀n:ℕ. primrec(n + 1;λi.Top;λj,T. F[T]) ⊆ primrec(n;λi.Top;λj,T. F[T])
⊢ SqStable(⋂n. primrec(n;λi.Top;λ,T. F[T]) ⊆ F[⋂n. primrec(n;λi.Top;λ,T. F[T])])
BY
{ RepeatFor 3 ((D 0 THEN Auto)) }

---

Latex:

---

Latex:

1.  [k]  :  \mBbbN{}
2.  [F]  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
3.  [\%]  :  k-Continuous(T.F[T])
4.  [\%1]  :  k-Monotone(T.F[T])
5.  \mforall{}n:\mBbbN{}.  primrec(n  +  1;\mlambda{}i.Top;\mlambda{}j,T.  F[T])  \msubseteq{}  primrec(n;\mlambda{}i.Top;\mlambda{}j,T.  F[T])
\mvdash{}  SqStable(\mcap{}n.  primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])  \msubseteq{}  F[\mcap{}n.  primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])])


By

---

Latex:
RepeatFor  3  ((D  0  THEN  Auto))

---

Home Index