---

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


1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. k-Continuous(T.F[T])
4. k-Monotone(T.F[T])
5. ∀n:ℕ. primrec(n + 1;λi.Top;λj,T. F[T]) ⊆ primrec(n;λi.Top;λj,T. F[T])
6. i : ℕk
7. x : F[⋂n. primrec(n;λi.Top;λ,T. F[T])] i
8. n : ℕ
9. n + 1 ≠ 0
10. x = x ∈ (F[⋂n. primrec(n;λi.Top;λ,T. F[T])] i)
⊢ (F[⋂n. primrec(n;λi.Top;λ,T. F[T])] i) ⊆r (F[primrec((n + 1) - 1;λi.Top;λj,T. F[T])] i)
BY
{ (Assert ⌜F[λi.⋂n:ℕ. (primrec(n;λi.Top;λ,T. F[T]) i)] ⊆ F[primrec((n + 1) - 1;λi.Top;λj,T. F[T])]⌝⋅ THEN Auto) }

1
.....assertion..... 
1. k : ℕ
2. F : (ℕk ⟶ Type) ⟶ ℕk ⟶ Type
3. k-Continuous(T.F[T])
4. k-Monotone(T.F[T])
5. ∀n:ℕ. primrec(n + 1;λi.Top;λj,T. F[T]) ⊆ primrec(n;λi.Top;λj,T. F[T])
6. i : ℕk
7. x : F[⋂n. primrec(n;λi.Top;λ,T. F[T])] i
8. n : ℕ
9. n + 1 ≠ 0
10. x = x ∈ (F[⋂n. primrec(n;λi.Top;λ,T. F[T])] i)
⊢ F[λi.⋂n:ℕ. (primrec(n;λi.Top;λ,T. F[T]) i)] ⊆ F[primrec((n + 1) - 1;λi.Top;λj,T. F[T])]

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

---

Latex:

---

Latex:

1.  k  :  \mBbbN{}
2.  F  :  (\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type
3.  k-Continuous(T.F[T])
4.  k-Monotone(T.F[T])
5.  \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])
6.  i  :  \mBbbN{}k
7.  x  :  F[\mcap{}n.  primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])]  i
8.  n  :  \mBbbN{}
9.  n  +  1  \mneq{}  0
10.  x  =  x
\mvdash{}  (F[\mcap{}n.  primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])]  i)  \msubseteq{}r  (F[primrec((n  +  1)  -  1;\mlambda{}i.Top;\mlambda{}j,T.  F[T])]  i)


By

---

Latex:
(Assert  \mkleeneopen{}F[\mlambda{}i.\mcap{}n:\mBbbN{}.  (primrec(n;\mlambda{}i.Top;\mlambda{},T.  F[T])  i)]  \msubseteq{}  F[primrec((n  +  1)  -  1;\mlambda{}i.Top;\mlambda{}j,T.  F[T])]\mkleeneclose{}\mcdot{}
  THEN  Auto
  )

---

Home Index