---

Step * 1 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]
⊢ fix(G) ∈ ⋂n:ℕ. H[primrec(n;Top;λ,T. F[T])]
BY
{ TACTIC:(((MemTypeCD THENM NatInd (-1)) THENA Auto)
          THEN (Reduce 0 THEN (RW (SweepUpC UnrollRecursionC) 0 THENA Auto))⋅
          ) }

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]
5. n : ℤ
⊢ G fix(G) ∈ H[Top]

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

---

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]
\mvdash{}  fix(G)  \mmember{}  \mcap{}n:\mBbbN{}.  H[primrec(n;Top;\mlambda{},T.  F[T])]


By

---

Latex:
TACTIC:(((MemTypeCD  THENM  NatInd  (-1))  THENA  Auto)
                THEN  (Reduce  0  THEN  (RW  (SweepUpC  UnrollRecursionC)  0  THENA  Auto))\mcdot{}
                )

---

Home Index