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:
2018_07_25-PM-01_42_31
Last ObjectModification:
2018_07_11-PM-10_57_00
Theory : co-recursion
Home
Index