---

Step * of Lemma corec-ext

∀[F:Type ⟶ Type]. corec(T.F[T]) ≡ F[corec(T.F[T])] supposing ContinuousMonotone(T.F[T])
BY
{ (Auto
   THEN (Assert ∀n:ℕ. (primrec(n + 1;Top;λj,T. F[T]) ⊆r primrec(n;Top;λj,T. F[T])) BY
               (InductionOnNat
                THEN Reduce 0
                THEN Try (Complete (Auto))
                THEN (RW (AddrC [1] (LemmaC `primrec-unroll`)) 0⋅ THENA Auto)
                THEN AutoSplit
                THEN (Subst' (n + 1) - 1 ~ n 0
                      THEN Try (Complete (Auto))
                      THEN (D 2 THEN Unfold `type-monotone` 2)
                      THEN InstHyp [⌜primrec(n;Top;λj,T. F[T])⌝;⌜primrec(n - 1;Top;λj,T. F[T])⌝] 2⋅
                      THEN Try (Complete (Auto))
                      THEN NthHypEq (-1)
                      THEN EqCD
                      THEN Auto
                      THEN (RW (AddrC [2] (LemmaC `primrec-unroll`)) 0⋅ THENA Auto)
                      THEN AutoSplit)⋅))
   ) }

1
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. ∀n:ℕ. (primrec(n + 1;Top;λj,T. F[T]) ⊆r primrec(n;Top;λj,T. F[T]))
⊢ corec(T.F[T]) ≡ F[corec(T.F[T])]

---

Latex:

---

Latex:
\mforall{}[F:Type  {}\mrightarrow{}  Type].  corec(T.F[T])  \mequiv{}  F[corec(T.F[T])]  supposing  ContinuousMonotone(T.F[T])


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (primrec(n  +  1;Top;\mlambda{}j,T.  F[T])  \msubseteq{}r  primrec(n;Top;\mlambda{}j,T.  F[T]))  BY
                          (InductionOnNat
                            THEN  Reduce  0
                            THEN  Try  (Complete  (Auto))
                            THEN  (RW  (AddrC  [1]  (LemmaC  `primrec-unroll`))  0\mcdot{}  THENA  Auto)
                            THEN  AutoSplit
                            THEN  (Subst'  (n  +  1)  -  1  \msim{}  n  0
                                        THEN  Try  (Complete  (Auto))
                                        THEN  (D  2  THEN  Unfold  `type-monotone`  2)
                                        THEN  InstHyp  [\mkleeneopen{}primrec(n;Top;\mlambda{}j,T.  F[T])\mkleeneclose{};\mkleeneopen{}primrec(n  -  1;Top;\mlambda{}j,T.  F[T])\mkleeneclose{}]  2\mcdot{}
                                        THEN  Try  (Complete  (Auto))
                                        THEN  NthHypEq  (-1)
                                        THEN  EqCD
                                        THEN  Auto
                                        THEN  (RW  (AddrC  [2]  (LemmaC  `primrec-unroll`))  0\mcdot{}  THENA  Auto)
                                        THEN  AutoSplit)\mcdot{}))
  )

---

Home Index