---

Step * 1 1 1 of Lemma corec-ext


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])])
BY
{ ((D 0 THEN Auto)
   THEN SubsumeC ⌜primrec(n + 1;Top;λj,T. F[T])⌝⋅
   THEN Auto
   THEN (RW (AddrC [1] (LemmaC `primrec-unroll`)) 0⋅ THENA Auto)
   THEN AutoSplit
   THEN ArithSimp 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  Monotone(T.F[T])
3.  \mforall{}[X:\mBbbN{}  {}\mrightarrow{}  Type].  ((\mcap{}n:\mBbbN{}.  F[X  n])  \msubseteq{}r  F[\mcap{}n:\mBbbN{}.  (X  n)])
4.  \mforall{}n:\mBbbN{}.  (primrec(n  +  1;Top;\mlambda{}j,T.  F[T])  \msubseteq{}r  primrec(n;Top;\mlambda{}j,T.  F[T]))
5.  (\mcap{}n:\mBbbN{}.  F[primrec(n;Top;\mlambda{}j,T.  F[T])])  \msubseteq{}r  F[\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{}j,T.  F[T])]
\mvdash{}  (\mcap{}n:\mBbbN{}.  primrec(n;Top;\mlambda{},T.  F[T]))  \msubseteq{}r  (\mcap{}n:\mBbbN{}.  F[primrec(n;Top;\mlambda{}j,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
  THEN  (RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  ArithSimp  0
  THEN  Auto)

---

Home Index