---

Step * 1 2 1 2 of Lemma mutual-corec-ext


1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. k-Monotone(T.F[T])
4. ∀n:ℕ. primrec(n + 1;λi.Top;λj,T. F[T]) ⊆ primrec(n;λi.Top;λj,T. F[T])
5. (∀n:ℕ. primrec(n + 1;λi.Top;λ,T. F[T]) ⊆ primrec(n;λi.Top;λ,T. F[T]))
⇒ ⋂n. F[primrec(n;λi.Top;λ,T. F[T])] ⊆ F[⋂n. primrec(n;λi.Top;λ,T. F[T])]
6. λi.⋂n:ℕ. (primrec(n;λi.Top;λ,T. F[T]) i) ⊆ λi.⋂n:ℕ. (F[primrec(n;λi.Top;λ,T. F[T])] i)
⊢ ⋂n. primrec(n;λi.Top;λ,T. F[T]) ⊆ F[⋂n. primrec(n;λi.Top;λ,T. F[T])]
BY
{ (RepeatFor 2 (ParallelLast) THEN ThinTrivial THEN All Reduce) }

1
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. k-Monotone(T.F[T])
4. ∀n:ℕ. primrec(n + 1;λi.Top;λj,T. F[T]) ⊆ primrec(n;λi.Top;λj,T. F[T])
5. ∀i:ℕk. ((⋂n:ℕ. (primrec(n;λi.Top;λ,T. F[T]) i)) ⊆r (⋂n:ℕ. (F[primrec(n;λi.Top;λ,T. F[T])] i)))
6. i : ℕk
7. (⋂n:ℕ. (primrec(n;λi.Top;λ,T. F[T]) i)) ⊆r (⋂n:ℕ. (F[primrec(n;λi.Top;λ,T. F[T])] i))
8. ⋂n. F[primrec(n;λi.Top;λ,T. F[T])] ⊆ F[⋂n. primrec(n;λi.Top;λ,T. F[T])]
⊢ (⋂n. primrec(n;λi.Top;λ,T. F[T]) i) ⊆r (F[⋂n. primrec(n;λi.Top;λ,T. F[T])] i)

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
3.  k-Monotone(T.F[T])
4.  \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])
5.  (\mforall{}n:\mBbbN{}.  primrec(n  +  1;\mlambda{}i.Top;\mlambda{},T.  F[T])  \msubseteq{}  primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T]))
{}\mRightarrow{}  \mcap{}n.  F[primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])]  \msubseteq{}  F[\mcap{}n.  primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])]
6.  \mlambda{}i.\mcap{}n:\mBbbN{}.  (primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])  i)  \msubseteq{}  \mlambda{}i.\mcap{}n:\mBbbN{}.  (F[primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])]  i)
\mvdash{}  \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  2  (ParallelLast)  THEN  ThinTrivial  THEN  All  Reduce)

---

Home Index