---

Step * of Lemma fix_wf_corec1

∀[F,H:Type ⟶ Type].
  ∀[G:⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . (H[T] ⟶ H[F[T]]) ⋂ Top ⟶ H[Top]]. (fix(G) ∈ H[corec(T.F[T])]) 
  supposing Continuous(T.H[T]) ∧ Monotone(T.F[T])
BY
{ TACTIC:TACTIC:((UnivCD THENA Auto) THEN Unfold `corec` 0 THEN SubsumeC ⌜⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])]⌝⋅) }

1
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]
⊢ fix(G) ∈ ⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])]

2
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])]

---

Latex:

---

Latex:
\mforall{}[F,H:Type  {}\mrightarrow{}  Type].
    \mforall{}[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]]
        (fix(G)  \mmember{}  H[corec(T.F[T])]) 
    supposing  Continuous(T.H[T])  \mwedge{}  Monotone(T.F[T])


By

---

Latex:
TACTIC:TACTIC:((UnivCD  THENA  Auto)
                              THEN  Unfold  `corec`  0
                              THEN  SubsumeC  \mkleeneopen{}\mcap{}n:\mBbbN{}.  H[primrec(n;Top;\mlambda{},T.  F[T])]\mkleeneclose{}\mcdot{})

---

Home Index