---

Step * of Lemma mutual-corec-ext

∀[k:ℕ]. ∀[F:(ℕk ⟶ Type) ⟶ ℕk ⟶ Type].
  (mutual-corec(T.F[T]) ≡ F[mutual-corec(T.F[T])]) supposing (k-Monotone(T.F[T]) and k-Continuous(T.F[T]))
BY
{ (Intros
   THEN (Assert ∀n:ℕ. primrec(n + 1;λi.Top;λj,T. F[T]) ⊆ primrec(n;λi.Top;λj,T. F[T]) BY
               (InductionOnNat⋅
                THEN Reduce 0
                THEN Try (Complete ((D 0 THEN Auto)))
                THEN (RW (AddrC [2] (LemmaC `primrec-unroll`)) 0⋅ THENA Auto)
                THEN AutoSplit
                THEN ((Subst' (n + 1) - 1 ~ n 0 THENA Auto)
                      THEN Unfold `k-monotone` 4
                      THEN (FHyp 4 [-1] THENA Auto)
                      THEN NthHypEq (-1)
                      THEN EqCD
                      THEN Auto
                      THEN (RW (AddrC [2] (LemmaC `primrec-unroll`)) 0⋅ THENA Auto)
                      THEN AutoSplit)⋅))
   THEN D 0
   THEN Unfold `mutual-corec` 0) }

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

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

---

Latex:

---

Latex:
\mforall{}[k:\mBbbN{}].  \mforall{}[F:(\mBbbN{}k  {}\mrightarrow{}  Type)  {}\mrightarrow{}  \mBbbN{}k  {}\mrightarrow{}  Type].
    (mutual-corec(T.F[T])  \mequiv{}  F[mutual-corec(T.F[T])])  supposing 
          (k-Monotone(T.F[T])  and 
          k-Continuous(T.F[T]))


By

---

Latex:
(Intros
  THEN  (Assert  \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])  BY
                          (InductionOnNat\mcdot{}
                            THEN  Reduce  0
                            THEN  Try  (Complete  ((D  0  THEN  Auto)))
                            THEN  (RW  (AddrC  [2]  (LemmaC  `primrec-unroll`))  0\mcdot{}  THENA  Auto)
                            THEN  AutoSplit
                            THEN  ((Subst'  (n  +  1)  -  1  \msim{}  n  0  THENA  Auto)
                                        THEN  Unfold  `k-monotone`  4
                                        THEN  (FHyp  4  [-1]  THENA  Auto)
                                        THEN  NthHypEq  (-1)
                                        THEN  EqCD
                                        THEN  Auto
                                        THEN  (RW  (AddrC  [2]  (LemmaC  `primrec-unroll`))  0\mcdot{}  THENA  Auto)
                                        THEN  AutoSplit)\mcdot{}))
  THEN  D  0
  THEN  Unfold  `mutual-corec`  0)

---

Home Index