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