Nuprl Definition : coW-equiv
The bisimulation relation on coW-types is defined to be 
a winning strategy for the second player in the game ⌜coW-game(a.B[a];w;w')⌝.
This is an equivalence relation on the coW-type ⌜coW(A;a.B[a])⌝.⋅
coW-equiv(a.B[a];w;w') ==  win2(coW-game(a.B[a];w;w'))
Definitions occuring in Statement : 
coW-game: coW-game(a.B[a];w;w')
, 
win2: win2(g)
Definitions occuring in definition : 
win2: win2(g)
, 
coW-game: coW-game(a.B[a];w;w')
FDL editor aliases : 
coW-equiv
Latex:
coW-equiv(a.B[a];w;w')  ==    win2(coW-game(a.B[a];w;w'))
Date html generated:
2019_06_20-PM-00_57_52
Last ObjectModification:
2019_01_02-PM-01_34_30
Theory : co-recursion-2
Home
Index