---

Step * 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]))
⊢ s' = s ∈ (I ⟶ corec(T.F[T]))
BY
{ TACTIC:((InstLemma `indexed-coinduction-principle` [⌜I⌝;⌜F⌝;⌜λ2s.λ2s'.∀i:I
                                                                          (((s i) = (G s i) ∈ corec(T.F[T]))
                                                                          ∧ ((s' i) = (G s' i) ∈ corec(T.F[T])))⌝]⋅
           THENA Auto
           )
          THEN All Reduce
          THEN Try ((BHyp (-1) THEN Auto))
          THEN (FLemma `corec-ext` [2] THENA Auto)
          THEN (D 0 THEN Auto)
          THEN Try ((D 0 THEN Auto))) }

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])))
⊢ x = 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)
\mvdash{}  s'  =  s


By

---

Latex:
TACTIC:((InstLemma  `indexed-coinduction-principle`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}F\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}s.\mlambda{}\msubtwo{}s'.\mforall{}i:I
                                                                                                                                                (((s  i)  =  (G  s  i))
                                                                                                                                                \mwedge{}  ((s'  i)  =  (G  s'  i)))\mkleeneclose{}]\mcdot{}
                  THENA  Auto
                  )
                THEN  All  Reduce
                THEN  Try  ((BHyp  (-1)  THEN  Auto))
                THEN  (FLemma  `corec-ext`  [2]  THENA  Auto)
                THEN  (D  0  THEN  Auto)
                THEN  Try  ((D  0  THEN  Auto)))

---

Home Index