 This position is a win for Spoiler if and only if some atomic formula (of one of the forms ‘\(\R(v_0 ,\ldots ,v_{k-1})\)’ or ‘\(\mathrm{F}(v_0 ,\ldots ,v_{k-1}) = v_k\)’ or ‘\(v_0 =v_1\)’, or one of these with different variables) is satisfied by \((a_0 ,\ldots ,a_{n-1})\) in \(A\) but not by \((b_0 ,\ldots ,b_{n-1})\) in \(B\), or vice versa. The condition for Duplicator to win is different in different forms of the game. In the simplest form, \(\EF(A, B)\), a play is a win for Duplicator if and only if no initial part of it is a win for Spoiler (i.e. she wins if she hasn’t lost by any finite stage). For each natural number \(m\) there is a game \(\EF_m (A, B)\); in this game Duplicator wins after \(m\) steps provided she has not yet lost. All these games are determined, by the Gale-Stewart Theorem. The two structures \(A\) and \(B\) are said to be back-and-forth equivalent if Duplicator has a winning strategy for \(\EF(A, B)\), and m-equivalent if she has a winning strategy for \(\EF_m (A, B)\).