---

Step * 1 1 1 1 1 of Lemma unique-corec-solution


1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. I : Type
4. G : ⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])
5. corec(T.F[T]) ⊆r F[corec(T.F[T])]
6. F[corec(T.F[T])] ⊆r corec(T.F[T])
7. G ∈ (I ⟶ corec(T.F[T])) ⟶ I ⟶ corec(T.F[T])
8. fix(G) ∈ I ⟶ corec(T.F[T])
9. ∀i:I. ((fix(G) i) = (G fix(G) i) ∈ corec(T.F[T]))
10. s' : I ⟶ corec(T.F[T])
11. s' = (G s') ∈ (I ⟶ corec(T.F[T]))
12. s : I ⟶ corec(T.F[T])
13. fix(G) = s ∈ (I ⟶ corec(T.F[T]))
14. s = (G s) ∈ (I ⟶ corec(T.F[T]))
15. corec(T.F[T]) ≡ F[corec(T.F[T])]
16. T : Type
17. F[T] ⊆r T
18. corec(T.F[T]) ⊆r T
19. ∀x,y:I ⟶ corec(T.F[T]).
      ((∀i:I. (((x i) = (G x i) ∈ corec(T.F[T])) ∧ ((y i) = (G y i) ∈ corec(T.F[T])))) ⇒ (x = y ∈ (I ⟶ T)))
20. x : I ⟶ corec(T.F[T])
21. y : I ⟶ corec(T.F[T])
22. ∀i:I. (((x i) = (G x i) ∈ corec(T.F[T])) ∧ ((y i) = (G y i) ∈ corec(T.F[T])))
⊢ x = y ∈ (I ⟶ F[T])
BY
{ ((Ext THEN Auto) THEN RenameVar `i' (-1)) }

1
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. I : Type
4. G : ⋂T:{T:Type| (F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T)} . ((I ⟶ T) ⟶ I ⟶ F[T])
5. corec(T.F[T]) ⊆r F[corec(T.F[T])]
6. F[corec(T.F[T])] ⊆r corec(T.F[T])
7. G ∈ (I ⟶ corec(T.F[T])) ⟶ I ⟶ corec(T.F[T])
8. fix(G) ∈ I ⟶ corec(T.F[T])
9. ∀i:I. ((fix(G) i) = (G fix(G) i) ∈ corec(T.F[T]))
10. s' : I ⟶ corec(T.F[T])
11. s' = (G s') ∈ (I ⟶ corec(T.F[T]))
12. s : I ⟶ corec(T.F[T])
13. fix(G) = s ∈ (I ⟶ corec(T.F[T]))
14. s = (G s) ∈ (I ⟶ corec(T.F[T]))
15. corec(T.F[T]) ≡ F[corec(T.F[T])]
16. T : Type
17. F[T] ⊆r T
18. corec(T.F[T]) ⊆r T
19. ∀x,y:I ⟶ corec(T.F[T]).
      ((∀i:I. (((x i) = (G x i) ∈ corec(T.F[T])) ∧ ((y i) = (G y i) ∈ corec(T.F[T])))) ⇒ (x = y ∈ (I ⟶ T)))
20. x : I ⟶ corec(T.F[T])
21. y : I ⟶ corec(T.F[T])
22. ∀i:I. (((x i) = (G x i) ∈ corec(T.F[T])) ∧ ((y i) = (G y i) ∈ corec(T.F[T])))
23. i : I
⊢ (x i) = (y i) ∈ F[T]

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  ContinuousMonotone(T.F[T])
3.  I  :  Type
4.  G  :  \mcap{}T:\{T:Type|  (F[T]  \msubseteq{}r  T)  \mwedge{}  (corec(T.F[T])  \msubseteq{}r  T)\}  .  ((I  {}\mrightarrow{}  T)  {}\mrightarrow{}  I  {}\mrightarrow{}  F[T])
5.  corec(T.F[T])  \msubseteq{}r  F[corec(T.F[T])]
6.  F[corec(T.F[T])]  \msubseteq{}r  corec(T.F[T])
7.  G  \mmember{}  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  I  {}\mrightarrow{}  corec(T.F[T])
8.  fix(G)  \mmember{}  I  {}\mrightarrow{}  corec(T.F[T])
9.  \mforall{}i:I.  ((fix(G)  i)  =  (G  fix(G)  i))
10.  s'  :  I  {}\mrightarrow{}  corec(T.F[T])
11.  s'  =  (G  s')
12.  s  :  I  {}\mrightarrow{}  corec(T.F[T])
13.  fix(G)  =  s
14.  s  =  (G  s)
15.  corec(T.F[T])  \mequiv{}  F[corec(T.F[T])]
16.  T  :  Type
17.  F[T]  \msubseteq{}r  T
18.  corec(T.F[T])  \msubseteq{}r  T
19.  \mforall{}x,y:I  {}\mrightarrow{}  corec(T.F[T]).    ((\mforall{}i:I.  (((x  i)  =  (G  x  i))  \mwedge{}  ((y  i)  =  (G  y  i))))  {}\mRightarrow{}  (x  =  y))
20.  x  :  I  {}\mrightarrow{}  corec(T.F[T])
21.  y  :  I  {}\mrightarrow{}  corec(T.F[T])
22.  \mforall{}i:I.  (((x  i)  =  (G  x  i))  \mwedge{}  ((y  i)  =  (G  y  i)))
\mvdash{}  x  =  y


By

---

Latex:
((Ext  THEN  Auto)  THEN  RenameVar  `i'  (-1))

---

Home Index