hide throw, stop, again, tie type Tries = {1..3} type Die = {1..6} X(n:Tries) = throw.psum(first:Die, 1/6 : n > 1 => again . X[n - 1] ++ stop . Y[first, 4 - n]) Y(first:Die, n:Tries) = throw.psum(second:Die, 1/6 : second > first => p2win.Z[] ++ n = 1 & first > second => p1win.Z[] ++ first = second => tie.X[3] ++ n > 1 & first >= second => tau.Y[first, n-1]) Z = done.Z[] init X[3]