Step
*
2
of Lemma
fix_wf_corec1
1. F : Type ⟶ Type
2. H : Type ⟶ Type
3. Continuous(T.H[T]) ∧ Monotone(T.F[T])
4. G : ⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]
5. fix(G) = fix(G) ∈ (⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])])
⊢ (⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])]) ⊆r H[⋂n:ℕ. primrec(n;Top;λ,T. F[T])]
BY
{ TACTIC:(TACTIC:Auto THEN (With ⌜λn.primrec(n;Top;λ,T. F[T])⌝ (D 3)⋅ THEN Reduce (-1) THEN Auto)⋅) }
Latex:
Latex:
1. F : Type {}\mrightarrow{} Type
2. H : Type {}\mrightarrow{} Type
3. Continuous(T.H[T]) \mwedge{} Monotone(T.F[T])
4. G : \mcap{}T:\{T:Type| (F[T] \msubseteq{}r T) \mwedge{} (corec(T.F[T]) \msubseteq{}r T)\} . (H[T] {}\mrightarrow{} H[F[T]]) \mcap{} Top {}\mrightarrow{} H[Top]
5. fix(G) = fix(G)
\mvdash{} (\mcap{}n:\mBbbN{}. H[primrec(n;Top;\mlambda{},T. F[T])]) \msubseteq{}r H[\mcap{}n:\mBbbN{}. primrec(n;Top;\mlambda{},T. F[T])]
By
Latex:
TACTIC:(TACTIC:Auto THEN (With \mkleeneopen{}\mlambda{}n.primrec(n;Top;\mlambda{},T. F[T])\mkleeneclose{} (D 3)\mcdot{} THEN Reduce (-1) THEN Auto)\mcdot{})
Home
Index