---

Step * 1 2 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]))
4. x : F[⋂n:ℕ. primrec(n;Top;λ,T. F[T])]
5. n : ℕ
⊢ x ∈ primrec(n + 1;Top;λj,T. F[T])
BY
{ (((RWO "primrec-unroll" 0 THENA Auto) THEN AutoSplit) THEN DoSubsume THEN Try (Complete (Auto))) }

---

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]))
4.  x  :  F[\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T])]
5.  n  :  \mBbbN{}
\mvdash{}  x  \mmember{}  primrec(n  +  1;Top;\mlambda{}j,T.  F[T])


By

---

Latex:
(((RWO  "primrec-unroll"  0  THENA  Auto)  THEN  AutoSplit)  THEN  DoSubsume  THEN  Try  (Complete  (Auto)))

---

Home Index