---

Step * 1 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]))
⊢ (⋂n:ℕ. primrec(n;Top;λ,T. F[T])) ⊆r F[⋂n:ℕ. primrec(n;Top;λ,T. F[T])]
BY
{ ((Using [`B', ⌜⋂n:ℕ. F[primrec(n;Top;λj,T. F[T])]⌝] (BLemma `subtype_rel_transitivity`)⋅ THEN Try (Complete (Auto)))
   THEN Try ((D -2
              THEN Unfold `type-continuous` -2
              THEN InstHyp [⌜λ2n.primrec(n;Top;λj,T. F[T])⌝] (-2)⋅
              THEN Try (Complete (Auto))))
   )⋅ }

1
1. F : Type ⟶ Type
2. Monotone(T.F[T])
3. ∀[X:ℕ ⟶ Type]. ((⋂n:ℕ. F[X n]) ⊆r F[⋂n:ℕ. (X n)])
4. ∀n:ℕ. (primrec(n + 1;Top;λj,T. F[T]) ⊆r primrec(n;Top;λj,T. F[T]))
5. (⋂n:ℕ. F[primrec(n;Top;λj,T. F[T])]) ⊆r F[⋂n:ℕ. primrec(n;Top;λj,T. F[T])]
⊢ (⋂n:ℕ. primrec(n;Top;λ,T. F[T])) ⊆r (⋂n:ℕ. F[primrec(n;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{}  (\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T]))  \msubseteq{}r  F[\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T])]


By

---

Latex:
((Using  [`B',  \mkleeneopen{}\mcap{}n:\mBbbN{}.  F[primrec(n;Top;\mlambda{}j,T.  F[T])]\mkleeneclose{}]  (BLemma  `subtype\_rel\_transitivity`)\mcdot{}
    THEN  Try  (Complete  (Auto))
    )
  THEN  Try  ((D  -2
                        THEN  Unfold  `type-continuous`  -2
                        THEN  InstHyp  [\mkleeneopen{}\mlambda{}\msubtwo{}n.primrec(n;Top;\mlambda{}j,T.  F[T])\mkleeneclose{}]  (-2)\mcdot{}
                        THEN  Try  (Complete  (Auto))))
  )\mcdot{}

---

Home Index