Nuprl Definition : coW-equiv

The bisimulation relation on coW-types is defined to be 
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