---

Step * of Lemma corec-rel-wf2

∀[F:𝕌' ⟶ 𝕌']
  ∀[G:⋂T:𝕌'. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)]. (corec-rel(G) ∈ corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ) 
  supposing continuous-monotone{i':l}(T.F[T])
BY
{ ((UnivCD THENA Auto)
   THEN (Assert ∀n:ℕ. (G^n (λx,y. True) ∈ primrec(n;Top;λ,T. F[T]) ⟶ primrec(n;Top;λ,T. F[T]) ⟶ ℙ) BY
               (InductionOnNat
                THEN (RWO "fun_exp_unroll" 0 THENA Auto)
                THEN (RWO "primrec-unroll" 0 THENA Auto)
                THEN Reduce 0
                THEN Try ((((Subst' (n =z 0) ~ ff 0 THENA Complete (Auto))
                            THEN (Subst' n <z 1 ~ ff 0 THENA Complete (Auto))
                            )
                           THEN Reduce 0
                           THEN Auto))
                THEN Auto))
   ) }

1
1. F : 𝕌' ⟶ 𝕌'
2. continuous-monotone{i':l}(T.F[T])
3. G : ⋂T:𝕌'. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)
4. ∀n:ℕ. (G^n (λx,y. True) ∈ primrec(n;Top;λ,T. F[T]) ⟶ primrec(n;Top;λ,T. F[T]) ⟶ ℙ)
⊢ corec-rel(G) ∈ corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ

---

Latex:

---

Latex:
\mforall{}[F:\mBbbU{}'  {}\mrightarrow{}  \mBbbU{}']
    \mforall{}[G:\mcap{}T:\mBbbU{}'.  ((T  {}\mrightarrow{}  T  {}\mrightarrow{}  \mBbbP{})  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  F[T]  {}\mrightarrow{}  \mBbbP{})]
        (corec-rel(G)  \mmember{}  corec(T.F[T])  {}\mrightarrow{}  corec(T.F[T])  {}\mrightarrow{}  \mBbbP{}) 
    supposing  continuous-monotone\{i':l\}(T.F[T])


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (Assert  \mforall{}n:\mBbbN{}.  (G\^{}n  (\mlambda{}x,y.  True)  \mmember{}  primrec(n;Top;\mlambda{},T.  F[T])  {}\mrightarrow{}  primrec(n;Top;\mlambda{},T.  F[T])  {}\mrightarrow{}  \mBbbP{})  B\000CY
                          (InductionOnNat
                            THEN  (RWO  "fun\_exp\_unroll"  0  THENA  Auto)
                            THEN  (RWO  "primrec-unroll"  0  THENA  Auto)
                            THEN  Reduce  0
                            THEN  Try  ((((Subst'  (n  =\msubz{}  0)  \msim{}  ff  0  THENA  Complete  (Auto))
                                                    THEN  (Subst'  n  <z  1  \msim{}  ff  0  THENA  Complete  (Auto))
                                                    )
                                                  THEN  Reduce  0
                                                  THEN  Auto))
                            THEN  Auto))
  )

---

Home Index