---

Step * 1 2 1 1 1 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. i : ℕk
6. ⋂n. F[primrec(n;λi.Top;λ,T. F[T])] ⊆ F[⋂n. primrec(n;λi.Top;λ,T. F[T])]
7. x : ⋂n:ℕ. (primrec(n;λi.Top;λ,T. F[T]) i)
8. n : ℕ
⊢ x ∈ F[primrec(n;λi.Top;λ,T. F[T])] i
BY
{ (SubsumeC ⌜primrec(n + 1;λi.Top;λj,T. F[T]) i⌝⋅
   THEN Auto
   THEN (RW (AddrC [1;1] (LemmaC `primrec-unroll`)) 0⋅ THENA Auto)
   THEN AutoSplit
   THEN ArithSimp 0
   THEN Auto) }

---

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.  i  :  \mBbbN{}k
6.  \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])]
7.  x  :  \mcap{}n:\mBbbN{}.  (primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])  i)
8.  n  :  \mBbbN{}
\mvdash{}  x  \mmember{}  F[primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])]  i


By

---

Latex:
(SubsumeC  \mkleeneopen{}primrec(n  +  1;\mlambda{}i.Top;\mlambda{}j,T.  F[T])  i\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (RW  (AddrC  [1;1]  (LemmaC  `primrec-unroll`))  0\mcdot{}  THENA  Auto)
  THEN  AutoSplit
  THEN  ArithSimp  0
  THEN  Auto)

---

Home Index