---

Step * 1 of Lemma coinduction-principle


1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. R : corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ
4. x,y.R[x;y] is an T.F[T]-bisimulation
⊢ ∀[x,y:corec(T.F[T])].  x = y ∈ corec(T.F[T]) supposing R[x;y]
BY
{ Assert ⌜∀n:ℕ. ∀[x,y:corec(T.F[T])].  x = y ∈ primrec(n;Top;λ,T. F[T]) supposing R[x;y]⌝⋅ }

1
.....assertion..... 
1. F : Type ⟶ Type
2. ContinuousMonotone(T.F[T])
3. R : corec(T.F[T]) ⟶ corec(T.F[T]) ⟶ ℙ
4. x,y.R[x;y] is an T.F[T]-bisimulation
⊢ ∀n:ℕ. ∀[x,y:corec(T.F[T])].  x = y ∈ primrec(n;Top;λ,T. F[T]) supposing R[x;y]

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

---

Latex:

---

Latex:

1.  F  :  Type  {}\mrightarrow{}  Type
2.  ContinuousMonotone(T.F[T])
3.  R  :  corec(T.F[T])  {}\mrightarrow{}  corec(T.F[T])  {}\mrightarrow{}  \mBbbP{}
4.  x,y.R[x;y]  is  an  T.F[T]-bisimulation
\mvdash{}  \mforall{}[x,y:corec(T.F[T])].    x  =  y  supposing  R[x;y]


By

---

Latex:
Assert  \mkleeneopen{}\mforall{}n:\mBbbN{}.  \mforall{}[x,y:corec(T.F[T])].    x  =  y  supposing  R[x;y]\mkleeneclose{}\mcdot{}

---

Home Index