---

Step * of Lemma indexed-coinduction-principle

∀[I:Type]. ∀[F:Type ⟶ Type].
  ∀[R:(I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ]
    ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ corec(T.F[T])) supposing R[x;y] 
    supposing x,y.R[x;y] is an T.F[T]-bisimulation (indexed I) 
  supposing ContinuousMonotone(T.F[T])
BY
{ RepeatFor 5 ((D 0 THENA Auto)) }

1
1. I : Type
2. F : Type ⟶ Type
3. ContinuousMonotone(T.F[T])
4. R : (I ⟶ corec(T.F[T])) ⟶ (I ⟶ corec(T.F[T])) ⟶ ℙ
5. x,y.R[x;y] is an T.F[T]-bisimulation (indexed I)
⊢ ∀[x,y:I ⟶ corec(T.F[T])].  x = y ∈ (I ⟶ corec(T.F[T])) supposing R[x;y]

---

Latex:

---

Latex:
\mforall{}[I:Type].  \mforall{}[F:Type  {}\mrightarrow{}  Type].
    \mforall{}[R:(I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  (I  {}\mrightarrow{}  corec(T.F[T]))  {}\mrightarrow{}  \mBbbP{}]
        \mforall{}[x,y:I  {}\mrightarrow{}  corec(T.F[T])].    x  =  y  supposing  R[x;y] 
        supposing  x,y.R[x;y]  is  an  T.F[T]-bisimulation  (indexed  I) 
    supposing  ContinuousMonotone(T.F[T])


By

---

Latex:
RepeatFor  5  ((D  0  THENA  Auto))

---

Home Index