---

Step * 1 2 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]))
⊢ F[⋂n:ℕ. primrec(n;Top;λ,T. F[T])] ⊆r (⋂n:ℕ. primrec(n;Top;λ,T. F[T]))
BY
{ ((D 0 THEN Auto) THEN SubsumeC ⌜primrec(n + 1;Top;λj,T. F[T])⌝⋅ THEN Auto)⋅ }

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]))
4. x : F[⋂n:ℕ. primrec(n;Top;λ,T. F[T])]
5. n : ℕ
⊢ x ∈ primrec(n + 1;Top;λj,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{}  F[\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T])]  \msubseteq{}r  (\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T]))


By

---

Latex:
((D  0  THEN  Auto)  THEN  SubsumeC  \mkleeneopen{}primrec(n  +  1;Top;\mlambda{}j,T.  F[T])\mkleeneclose{}\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index