---

Step * 1 2 1 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]
5. n : ℤ
6. n ≠ 0
7. 0 < n
8. fix(G) ∈ H[primrec(n - 1;Top;λ,T. F[T])]
9. v : H[primrec(n - 1;Top;λ,T. F[T])]@i
10. fix(G) = v ∈ H[primrec(n - 1;Top;λ,T. F[T])]
11. v1 : ⋂T:{T:Type| ((F T) ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . (H[T] ⟶ H[F[T]])@i'
12. G = v1 ∈ (⋂T:{T:Type| ((F T) ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . (H[T] ⟶ H[F[T]]))
⊢ v1 v ∈ H[F[primrec(n - 1;Top;λ,T. F[T])]]
BY
{ TACTIC:(ThinVar `G' THEN RenameVar `G' (-1)) }

1
1. F : Type ⟶ Type
2. H : Type ⟶ Type
3. Continuous(T.H[T]) ∧ Monotone(T.F[T])
4. n : ℤ
5. n ≠ 0
6. 0 < n
7. v : H[primrec(n - 1;Top;λ,T. F[T])]@i
8. G : ⋂T:{T:Type| ((F T) ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . (H[T] ⟶ H[F[T]])@i'
⊢ G v ∈ H[F[primrec(n - 1;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]
5.  n  :  \mBbbZ{}
6.  n  \mneq{}  0
7.  0  <  n
8.  fix(G)  \mmember{}  H[primrec(n  -  1;Top;\mlambda{},T.  F[T])]
9.  v  :  H[primrec(n  -  1;Top;\mlambda{},T.  F[T])]@i
10.  fix(G)  =  v
11.  v1  :  \mcap{}T:\{T:Type|  ((F  T)  \msubseteq{}r  T)  \mwedge{}  (corec(T.F[T])  \msubseteq{}r  T)\}  .  (H[T]  {}\mrightarrow{}  H[F[T]])@i'
12.  G  =  v1
\mvdash{}  v1  v  \mmember{}  H[F[primrec(n  -  1;Top;\mlambda{},T.  F[T])]]


By

---

Latex:
TACTIC:(ThinVar  `G'  THEN  RenameVar  `G'  (-1))

---

Home Index