Step
*
of Lemma
corec-rel_wf
∀[F:Type ⟶ Type]
  ∀[G:⋂T:Type. ((T ⟶ T ⟶ ℙ) ⟶ F[T] ⟶ F[T] ⟶ ℙ)]. (corec-rel(G) ∈ corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ) 
  supposing ContinuousMonotone(T.F[T])
BY
{ (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 : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. G : ⋂T:Type. ((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:Type  {}\mrightarrow{}  Type]
    \mforall{}[G:\mcap{}T:Type.  ((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  ContinuousMonotone(T.F[T])
By
Latex:
(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