const int k;

// both users maximise the expected reward before their battery becomes empty
<<user1:user2>>max=? (R{"r1"}[F e1=0] + R{"r2"}[F e2=0])

// both users maximise the expected reward for the first k steps
<<user1:user2>>max=? (R{"r1"}[C<=k] + R{"r2"}[C<=k])