Nuprl Definition : indexed-F-bisimulation
x,y.R[x; y] is an T.F[T]-bisimulation (indexed I) ==
∀T:Type
(((F[T] ⊆r T) ∧ (corec(T.F[T]) ⊆r T))
⇒ (∀x,y:I ⟶ corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ (I ⟶ T))))
⇒ (∀x,y:I ⟶ corec(T.F[T]). (R[x; y] ⇒ (x = y ∈ (I ⟶ 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,
function: x:A ⟶ B[x],
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,
function: x:A ⟶ B[x]
FDL editor aliases :
indexed-F-bisimulation
Latex:
x,y.R[x; y] is an T.F[T]-bisimulation (indexed I) ==
\mforall{}T:Type
(((F[T] \msubseteq{}r T) \mwedge{} (corec(T.F[T]) \msubseteq{}r T))
{}\mRightarrow{} (\mforall{}x,y:I {}\mrightarrow{} corec(T.F[T]). (R[x; y] {}\mRightarrow{} (x = y)))
{}\mRightarrow{} (\mforall{}x,y:I {}\mrightarrow{} corec(T.F[T]). (R[x; y] {}\mRightarrow{} (x = y))))
Date html generated:
2016_05_14-AM-06_21_14
Last ObjectModification:
2015_09_22-PM-05_47_47
Theory : co-recursion
Home
Index