Nuprl Definition : F-bisimulation
x,y.R[x; y] is an T.F[T]-bisimulation ==
∀T:Type
(((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
⇒ (∀x,y:corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ T)))
⇒ (∀x,y:corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ F[T]))))
Definitions occuring in Statement :
corec: corec(T.F[T]),
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
implies: P ⇒ Q,
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T
Definitions occuring in definition :
universe: Type,
and: P ∧ Q,
subtype_rel: A ⊆r B,
all: ∀x:A. B[x],
corec: corec(T.F[T]),
implies: P ⇒ Q,
equal: s = t ∈ T
FDL editor aliases :
F-bisimulation
Latex:
x,y.R[x; y] is an T.F[T]-bisimulation ==
\mforall{}T:Type
(((F[T] \msubseteq{}r T) \mwedge{} (corec(T.F[T]) \msubseteq{}r T))
{}\mRightarrow{} (\mforall{}x,y:corec(T.F[T]). (R[x; y] {}\mRightarrow{} (x = y)))
{}\mRightarrow{} (\mforall{}x,y:corec(T.F[T]). (R[x; y] {}\mRightarrow{} (x = y))))
Date html generated:
2016_05_14-AM-06_21_01
Last ObjectModification:
2015_09_22-PM-05_47_45
Theory : co-recursion
Home
Index