Tic Tac Toe with ReasonML

ReasonML provides an alternative syntax for OCaml, which Imandra can read. Let's walk through an example ReasonML model of Tic Tac Toe and use Imandra to understand and verify some properties of it.

This model is wired into some ReasonReact components in order to produce this final, playable version. You can see the model code and components as a ReasonReact project in this github repo.

Setting up the model

Let's start by adding some definitions for the player, state of a square on the game grid, and the grid itself.

In [1]:
type player =
  | X
  | O;

/* the state of a particular square - None = (no move yet), Some(X/O) = either X or O has moved there */
type square_state = option(player);

/* each letter represents a square on the grid, starting in the top left and going along each row */
type grid = {
  a: square_state,
  b: square_state,
  c: square_state,
  d: square_state,
  e: square_state,
  f: square_state,
  g: square_state,
  h: square_state,
  i: square_state,
};
Out[1]:
type player = X | O
type square_state = player option
type grid = {
  a : square_state;
  b : square_state;
  c : square_state;
  d : square_state;
  e : square_state;
  f : square_state;
  g : square_state;
  h : square_state;
  i : square_state;
}

(NB: we're inputting in Reason syntax, but Imandra currently outputs OCaml syntax - this is something we'll have resolved very soon!).

Grid document printer

Here's an example grid:

In [2]:
let a_grid = {
  a: Some(O),
  b: Some(X),
  c: Some(O),
  d: None,
  e: None,
  f: Some(X),
  g: None,
  h: None,
  i: None,
};
Out[2]:
val a_grid : grid =
  {a = Some O; b = Some X; c = Some O; d = None; e = None; f = Some X;
   g = None; h = None; i = None}

As you can tell, it's not the easiest thing to interpret from Imandra's output given the way we've described the grid. Let's setup a custom document mapping for the grid type. Imandra will render the Document data structures as richer output to display our types in a clearer way:

In [3]:
[@program] let doc_of_square_state = (s : square_state) =>
  Document.s(switch (s) {
  | Some(X) => "❌" /* emojis! */
  | Some(O) => "⭕"
  | None => "·"
});

[@program] let doc_of_grid = (g: grid) => {
  let f = doc_of_square_state;
  Document.tbl([[f(g.a), f(g.b), f(g.c)], [f(g.d), f(g.e), f(g.f)], [f(g.g), f(g.h), f(g.i)]])
};
[@install_doc doc_of_grid];
Out[3]:
val doc_of_square_state : square_state -> Document.t = <fun>
val doc_of_grid : grid -> Document.t = <fun>
In [4]:
a_grid
Out[4]:
- : grid = <document>
··
···

Much better! The [@program] annotation tells Imandra that we're only going to be using these functions for non-analytical (and potentially side-effecting) operations, and that it doesn't have to worry about analysing them. See Logic and program modes for more information.

More definitions

Let's continue adding some more definitions:

In [5]:
/* maps to the grid entries */
type move =
  | A
  | B
  | C
  | D
  | E
  | F
  | G
  | H
  | I;

/* the full game state - the current grid, and who went last */
type game_state = {
  grid,
  last_player: option(player),
};

type game_status =
  | Won(player)
  | InProgress
  | InvalidMove(move)
  | Tied;

let initial_game = {
  grid: {
    a: None,
    b: None,
    c: None,
    d: None,
    e: None,
    f: None,
    g: None,
    h: None,
    i: None,
  },
  last_player: None,
};

let initial_player = X;

/* convenience function from our move variant to the value in that grid position */
let value = ({grid: {a, b, c, d, e, f, g, h, i}, _}) =>
  fun
  | A => a
  | B => b
  | C => c
  | D => d
  | E => e
  | F => f
  | G => g
  | H => h
  | I => i;
Out[5]:
type move = A | B | C | D | E | F | G | H | I
type game_state = { grid : grid; last_player : player option; }
type game_status = Won of player | InProgress | InvalidMove of move | Tied
val initial_game : game_state = {grid = <document>; last_player = None}
val initial_player : player = X
val value : game_state -> move -> square_state = <fun>
···
···
···

Game state document printer

Let's also add another document for printing game_states, showing both the grid and who went last:

In [6]:
[@program] let doc_of_game_state = (gs: game_state) => {
  Document.tbl([[doc_of_grid(gs.grid), Document.s("Last:"), doc_of_square_state(gs.last_player)]])
};

[@install_doc doc_of_game_state];

initial_game;
Out[6]:
val doc_of_game_state : game_state -> Document.t = <fun>
- : game_state = <document>
···
···
···
Last:·

Some logic and our first instance

Now for our first bit of proper logic - whether or not a game is won for a particular player:

In [7]:
let is_winning = ({grid: {a, b, c, d, e, f, g, h, i}, _}, player) => {
  let winning_state = (Some(player), Some(player), Some(player));
  (a, b, c) == winning_state
  || (d, e, f) == winning_state
  || (g, h, i) == winning_state
  || (a, d, g) == winning_state
  || (b, e, h) == winning_state
  || (c, f, i) == winning_state
  || (a, e, i) == winning_state
  || (c, e, g) == winning_state;
};
Out[7]:
val is_winning : game_state -> player -> bool = <fun>

Let's use Imandra to get a feel for this function - let's ask for an instance of a game where the game is being won by the player X. We use Imandra's instance mechanism, and ask for a game g where the predicate is_winning(g, X) is true:

In [8]:
instance((g : game_state) => is_winning(g, X));
Out[8]:
- : game_state -> bool = <fun>
module CX : sig val g : game_state end
Instance (after 0 steps, 0.028s):
 let (g : game_state) =
   {grid =
     {a = (Some X); b = (Some X); c = (Some X); d = (Some X); e = (Some X);
      f = (Some X); g = (Some X); h = None; i = None};
    last_player = None}
Instance
proof attempt
ground_instances0
definitions0
inductions0
search_time
0.028s
details
Expand
smt_stats
num checks1
rlimit count1594
mk clause40
datatype occurs check1
mk bool var149
datatype splits41
decisions39
propagations32
conflicts7
datatype accessor ax7
datatype constructor ax58
num allocs1071086103
final checks1
added eqs275
memory20.290000
max memory26.910000
Expand
  • start[0.028s]
      (:var_0:.grid.a, :var_0:.grid.b, :var_0:.grid.c) = (Some X, Some X, Some X)
      || (:var_0:.grid.d, :var_0:.grid.e, :var_0:.grid.f) =
         (Some X, Some X, Some X)
         || (:var_0:.grid.g, :var_0:.grid.h, :var_0:.grid.i) =
            (Some X, Some X, Some X)
            || (:var_0:.grid.a, :var_0:.grid.d, :var_0:.grid.g) =
               (Some X, Some X, Some X)
               || (:var_0:.grid.b, :var_0:.grid.e, :var_0:.grid.h) =
                  (Some X, Some X, Some X)
                  || (:var_0:.grid.c, :var_0:.grid.f, :var_0:.grid.i) =
                     (Some X, Some X, Some X)
                     || (:var_0:.grid.a, :var_0:.grid.e, :var_0:.grid.i) =
                        (Some X, Some X, Some X)
                        || (:var_0:.grid.c, :var_0:.grid.e, :var_0:.grid.g) =
                           (Some X, Some X, Some X)
  • simplify

    into
    (((((((:var_0:.grid.a = Some X && :var_0:.grid.b = Some X)
          && :var_0:.grid.c = Some X
          || (:var_0:.grid.d = Some X && :var_0:.grid.e = Some X)
             && :var_0:.grid.f = Some X)
         || (:var_0:.grid.g = Some X && :var_0:.grid.h = Some X)
            && :var_0:.grid.i = Some X)
        || (:var_0:.grid.a = Some X && :var_0:.grid.d = Some X)
           && :var_0:.grid.g = Some X)
       || (:var_0:.grid.b = Some X && :var_0:.grid.e = Some X)
          && :var_0:.grid.h = Some X)
      || (:var_0:.grid.c = Some X && :var_0:.grid.f = Some X)
         && :var_0:.grid.i = Some X)
     || (:var_0:.grid.a = Some X && :var_0:.grid.e = Some X)
        && :var_0:.grid.i = Some X)
    || (:var_0:.grid.c = Some X && :var_0:.grid.e = Some X)
       && :var_0:.grid.g = Some X
    expansions
    []
    rewrite_steps
      forward_chaining
      • Sat (Some let (g : game_state) = {grid = {a = (Some X); b = (Some X); c = (Some X); d = (Some X); e = (Some X); f = (Some X); g = (Some X); h = None; i = None}; last_player = None} )

      Rather than executing our function with random inputs as you might imagine, Imandra has examined our definitions mathematically, and generated an instance that matches what we asked for based on the code itself, without executing it directly. This means we don't have to write generators as we would if we were using a library like QuickCheck for example. We can also use Imandra's other tools, such as state space decomposition, to identify edge cases we may not have thought about. See the other documentation pages/notebooks for more detail.

      In this case we explicitly annotated the type of g as game_state, but if this can be inferred using the usual ReasonML/OCaml inference rules, it can be omitted.

      instance has also reflected the value it found back into our Imandra session, so we can take a look at it:

      In [9]:
      CX.g
      
      Out[9]:
      - : game_state = <document>
      
      ··
      Last:·

      and compute with it:

      In [10]:
      is_winning(CX.g, X)
      
      Out[10]:
      - : bool = true
      

      We can see here that X is definitely 'winning', although the game doesn't look particularly valid. O hasn't made any moves, and the game state hasn't got a last_player set. That's fine for now though, we'll build up additional layers in our logic to handle these other cases. It can be very useful to see a concrete example of our function in action!

      Valid grids

      Let's continue:

      In [11]:
      let other_player =
        fun
        | X => O
        | O => X;
      
      /* count up the number of moves for each player across the whole grid - sounds useful! */
      let move_counts = ({a, b, c, d, e, f, g, h, i}) =>
        List.fold_right(
          (el, (x, o)) =>
            switch (el) {
            | None => (x, o)
            | Some(X) => (x + 1, o)
            | Some(O) => (x, o + 1)
            },
          ~base=(0, 0),
          [a, b, c, d, e, f, g, h, i],
        );
      
      /* whether a grid is 'valid' - the difference between move totals should never be more than 1 */
      let is_valid_grid = (grid, last_player) => {
        let (x, o) = move_counts(grid);
      
        (x + o == 0 && last_player == None) ||
        (x - o == 1 && last_player == Some(X)) ||
        (x == o && last_player == Some(O));
      };
      
      Out[11]:
      val other_player : player -> player = <fun>
      val move_counts : grid -> int * int = <fun>
      val is_valid_grid : grid -> player option -> bool = <fun>
      

      Let's grab a game where the grid is valid:

      In [12]:
      instance((game) => is_valid_grid(game.grid, game.last_player));
      
      Out[12]:
      - : game_state -> bool = <fun>
      module CX : sig val game : game_state end
      
      Instance (after 10 steps, 0.053s):
       let (game : game_state) =
         {grid =
           {a = (Some O); b = None; c = None; d = None; e = (Some O); f = (Some X);
            g = (Some X); h = None; i = None};
          last_player = (Some O)}
      
      Instance
      proof attempt
      ground_instances10
      definitions0
      inductions0
      search_time
      0.053s
      details
      Expand
      smt_stats
      arith offset eqs290
      num checks21
      arith assert lower256
      arith patches_succ2
      arith pivots142
      rlimit count49010
      mk clause426
      datatype occurs check459
      mk bool var1703
      arith gcd tests52
      arith assert upper329
      datatype splits121
      decisions689
      arith add rows878
      arith bound prop89
      propagations1252
      arith patches2
      interface eqs21
      conflicts48
      arith fixed eqs376
      datatype accessor ax109
      minimized lits2
      arith conflicts1
      arith assert diseq35
      datatype constructor ax723
      num allocs1200189368
      final checks32
      added eqs4695
      del clause178
      arith eq adapter234
      memory15.830000
      max memory26.910000
      Expand
      • start[0.053s]
          (List.fold_right
           (fun el _x
            -> let (x : int) = _x.0 and (o : int) = _x.1 in
               if el = None then (x, o)
               else
               if Is_a(Some, el) && Option.get el = X then (x + 1, o) else (x, o + 1))
           (0, 0) (….a :: (… :: …))).0
          + (List.fold_right
             (fun el _x
              -> let (x : int) = _x.0 and (o : int) = _x.1 in
                 if el = None then (x, o)
                 else
                 if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                 else (x, o + 1))
             (0, 0) (….a :: (… :: …))).1
          = 0 && :var_0:.last_player = None
          || (List.fold_right
              (fun el _x
               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                  if el = None then (x, o)
                  else
                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                  else (x, o + 1))
              (0, 0) (….a :: (… :: …))).0
             -
             (List.fold_right
              (fun el _x
               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                  if el = None then (x, o)
                  else
                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                  else (x, o + 1))
              (0, 0) (….a :: (… :: …))).1
             = 1 && :var_0:.last_player = Some X
             || (List.fold_right
                 (fun el _x
                  -> let (x : int) = _x.0 and (o : int) = _x.1 in
                     if el = None then (x, o)
                     else
                     if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                     else (x, o + 1))
                 (0, 0) (….a :: (… :: …))).0
                =
                (List.fold_right
                 (fun el _x
                  -> let (x : int) = _x.0 and (o : int) = _x.1 in
                     if el = None then (x, o)
                     else
                     if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                     else (x, o + 1))
                 (0, 0) (….a :: (… :: …))).1
                && :var_0:.last_player = Some O
      • simplify

        into
        ((List.fold_right
          (fun el _x
           -> let (x : int) = _x.0 and (o : int) = _x.1 in
              if el = None then (x, o)
              else
              if Is_a(Some, el) && Option.get el = X then (x + 1, o) else (x, o + 1))
          (0, 0) (….a :: (… :: …))).0
         + (List.fold_right
            (fun el _x
             -> let (x : int) = _x.0 and (o : int) = _x.1 in
                if el = None then (x, o)
                else
                if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                else (x, o + 1))
            (0, 0) (….a :: (… :: …))).1
         = 0 && :var_0:.last_player = None
         || (List.fold_right
             (fun el _x
              -> let (x : int) = _x.0 and (o : int) = _x.1 in
                 if el = None then (x, o)
                 else
                 if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                 else (x, o + 1))
             (0, 0) (….a :: (… :: …))).0
            + -1
              * (List.fold_right
                 (fun el _x
                  -> let (x : int) = _x.0 and (o : int) = _x.1 in
                     if el = None then (x, o)
                     else
                     if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                     else (x, o + 1))
                 (0, 0) (….a :: (… :: …))).1
            = 1 && :var_0:.last_player = Some X)
        || (List.fold_right
            (fun el _x
             -> let (x : int) = _x.0 and (o : int) = _x.1 in
                if el = None then (x, o)
                else
                if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                else (x, o + 1))
            (0, 0) (….a :: (… :: …))).0
           =
           (List.fold_right
            (fun el _x
             -> let (x : int) = _x.0 and (o : int) = _x.1 in
                if el = None then (x, o)
                else
                if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                else (x, o + 1))
            (0, 0) (….a :: (… :: …))).1
           && :var_0:.last_player = Some O
        expansions
        []
        rewrite_steps
          forward_chaining
          • unroll
            expr
            (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                               (|::_3| (i_27 (grid_40 game_99)) |[]_…
            expansions
            • unroll
              expr
              (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                 (|::_3| (i_27 (grid_40 game_99)) |[]_…
              expansions
              • unroll
                expr
                (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                   (|::_3| (i_27 (grid_40 game_99)) |[]_…
                expansions
                • unroll
                  expr
                  (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                     (|::_3| (i_27 (grid_40 game_99)) |[]_…
                  expansions
                  • unroll
                    expr
                    (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                       (|::_3| (i_27 (grid_40 game_99)) |[]_…
                    expansions
                    • unroll
                      expr
                      (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                         (|::_3| (i_27 (grid_40 game_99)) |[]_…
                      expansions
                      • unroll
                        expr
                        (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                           (|::_3| (i_27 (grid_40 game_99)) |[]_…
                        expansions
                        • unroll
                          expr
                          (let ((a!1 (|::_3| (h_26 (grid_40 game_99))
                                             (|::_3| (i_27 (grid_40 game_99)) |[]_…
                          expansions
                          • unroll
                            expr
                            (|`List.fold_right anon_fun.move_counts.0[0]`_1989|
                              (tuple_mk_1983 0 0)
                              (|::_3| (i_27 (grid_40 g…
                            expansions
                            • unroll
                              expr
                              (|`List.fold_right anon_fun.move_counts.0[0]`_1989| (tuple_mk_1983 0 0) |[]_2|)
                              expansions
                              • Sat (Some let (game : game_state) = {grid = {a = (Some O); b = None; c = None; d = None; e = (Some O); f = (Some X); g = (Some X); h = None; i = None}; last_player = (Some O)} )
                              In [13]:
                              CX.game;
                              
                              Out[13]:
                              - : game_state = <document>
                              
                              ··
                              ·
                              ··
                              Last:

                              This is a bit better - the grid looks more like a real game of Tic Tac Toe now.

                              Let's also see what happens if we ask for an instance that we know shouldn't be possible - if player X is more than 1 move ahead:

                              In [14]:
                              instance((game) => {
                                 let (x, o) = move_counts(game.grid);
                                 is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2)
                              });
                              
                              Out[14]:
                              - : game_state -> bool = <fun>
                              
                              Unsatisfiable
                              proof
                              ground_instances10
                              definitions0
                              inductions0
                              search_time
                              0.071s
                              details
                              Expand
                              smt_stats
                              arith offset eqs645
                              num checks21
                              arith assert lower543
                              arith pivots310
                              rlimit count121569
                              mk clause1212
                              datatype occurs check318
                              restarts1
                              mk bool var2873
                              arith assert upper710
                              datatype splits165
                              decisions1089
                              arith add rows2910
                              arith bound prop150
                              propagations2911
                              interface eqs14
                              conflicts153
                              arith fixed eqs794
                              datatype accessor ax154
                              minimized lits82
                              arith conflicts18
                              arith assert diseq115
                              datatype constructor ax804
                              num allocs1258141119
                              final checks24
                              added eqs8103
                              del clause782
                              arith eq adapter662
                              memory19.370000
                              max memory26.910000
                              Expand
                              • start[0.071s]
                                  ((List.fold_right
                                    (fun el _x
                                     -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                        if el = None then (x, o)
                                        else
                                        if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                        else (x, o + 1))
                                    (0, 0) (….a :: (… :: …))).0
                                   + (List.fold_right
                                      (fun el _x
                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                          if el = None then (x, o)
                                          else
                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                          else (x, o + 1))
                                      (0, 0) (….a :: (… :: …))).1
                                   = 0 && :var_0:.last_player = None
                                   || (List.fold_right
                                       (fun el _x
                                        -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                           if el = None then (x, o)
                                           else
                                           if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                           else (x, o + 1))
                                       (0, 0) (….a :: (… :: …))).0
                                      -
                                      (List.fold_right
                                       (fun el _x
                                        -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                           if el = None then (x, o)
                                           else
                                           if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                           else (x, o + 1))
                                       (0, 0) (….a :: (… :: …))).1
                                      = 1 && :var_0:.last_player = Some X
                                      || (List.fold_right
                                          (fun el _x
                                           -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                              if el = None then (x, o)
                                              else
                                              if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                              else (x, o + 1))
                                          (0, 0) (….a :: (… :: …))).0
                                         =
                                         (List.fold_right
                                          (fun el _x
                                           -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                              if el = None then (x, o)
                                              else
                                              if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                              else (x, o + 1))
                                          (0, 0) (….a :: (… :: …))).1
                                         && :var_0:.last_player = Some O)
                                  && ((List.fold_right
                                       (fun el _x
                                        -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                           if el = None then (x, o)
                                           else
                                           if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                           else (x, o + 1))
                                       (0, 0) (….a :: (… :: …))).0
                                      -
                                      (List.fold_right
                                       (fun el _x
                                        -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                           if el = None then (x, o)
                                           else
                                           if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                           else (x, o + 1))
                                       (0, 0) (….a :: (… :: …))).1)
                                     >= 2
                              • simplify

                                into
                                (((List.fold_right
                                   (fun el _x
                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                       if el = None then (x, o)
                                       else
                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o) else (x, o + 1))
                                   (0, 0) (….a :: (… :: …))).0
                                  + (List.fold_right
                                     (fun el _x
                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                         if el = None then (x, o)
                                         else
                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                         else (x, o + 1))
                                     (0, 0) (….a :: (… :: …))).1
                                  = 0 && :var_0:.last_player = None
                                  || (List.fold_right
                                      (fun el _x
                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                          if el = None then (x, o)
                                          else
                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                          else (x, o + 1))
                                      (0, 0) (….a :: (… :: …))).0
                                     + -1
                                       * (List.fold_right
                                          (fun el _x
                                           -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                              if el = None then (x, o)
                                              else
                                              if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                              else (x, o + 1))
                                          (0, 0) (….a :: (… :: …))).1
                                     = 1 && :var_0:.last_player = Some X)
                                 || (List.fold_right
                                     (fun el _x
                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                         if el = None then (x, o)
                                         else
                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                         else (x, o + 1))
                                     (0, 0) (….a :: (… :: …))).0
                                    =
                                    (List.fold_right
                                     (fun el _x
                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                         if el = None then (x, o)
                                         else
                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                         else (x, o + 1))
                                     (0, 0) (….a :: (… :: …))).1
                                    && :var_0:.last_player = Some O)
                                && ((List.fold_right
                                     (fun el _x
                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                         if el = None then (x, o)
                                         else
                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                         else (x, o + 1))
                                     (0, 0) (….a :: (… :: …))).0
                                    + -1
                                      * (List.fold_right
                                         (fun el _x
                                          -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                             if el = None then (x, o)
                                             else
                                             if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                             else (x, o + 1))
                                         (0, 0) (….a :: (… :: …))).1)
                                   >= 2
                                expansions
                                []
                                rewrite_steps
                                  forward_chaining
                                  • unroll
                                    expr
                                    (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                       (|::_3| (i_27 (grid_40 game_101)) |[…
                                    expansions
                                    • unroll
                                      expr
                                      (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                         (|::_3| (i_27 (grid_40 game_101)) |[…
                                      expansions
                                      • unroll
                                        expr
                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                           (|::_3| (i_27 (grid_40 game_101)) |[…
                                        expansions
                                        • unroll
                                          expr
                                          (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                             (|::_3| (i_27 (grid_40 game_101)) |[…
                                          expansions
                                          • unroll
                                            expr
                                            (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                               (|::_3| (i_27 (grid_40 game_101)) |[…
                                            expansions
                                            • unroll
                                              expr
                                              (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                                 (|::_3| (i_27 (grid_40 game_101)) |[…
                                              expansions
                                              • unroll
                                                expr
                                                (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                                   (|::_3| (i_27 (grid_40 game_101)) |[…
                                                expansions
                                                • unroll
                                                  expr
                                                  (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                                     (|::_3| (i_27 (grid_40 game_101)) |[…
                                                  expansions
                                                  • unroll
                                                    expr
                                                    (|`List.fold_right anon_fun.move_counts.0[0]`_2123|
                                                      (tuple_mk_2117 0 0)
                                                      (|::_3| (i_27 (grid_40 g…
                                                    expansions
                                                    • unroll
                                                      expr
                                                      (|`List.fold_right anon_fun.move_counts.0[0]`_2123| (tuple_mk_2117 0 0) |[]_2|)
                                                      expansions
                                                      • unsat

                                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_101))
                                                                           (|::_3| (i_27 (grid_40 game_101)) |[…

                                                      As this is invalid according to the description we've provided, Imandra can't find an instance. In fact, this Unsatisfiable judgment tells us that Imandra has actually constructed a mathematical proof that no such instance exists.

                                                      Verifying

                                                      We can invert this question, and turn it into a verification statement and ask Imandra to check it for us - similar to a test, but mathematically checked for all possible games (as game is the free argument to the verification function).

                                                      In [15]:
                                                      verify((game) => {
                                                         let (x, o) = move_counts(game.grid);
                                                         not(is_valid_grid(game.grid, game.last_player) && ((x - o) >= 2))
                                                      });
                                                      
                                                      Out[15]:
                                                      - : game_state -> bool = <fun>
                                                      
                                                      Proved
                                                      proof
                                                      ground_instances10
                                                      definitions0
                                                      inductions0
                                                      search_time
                                                      0.059s
                                                      details
                                                      Expand
                                                      smt_stats
                                                      arith offset eqs645
                                                      num checks21
                                                      arith assert lower543
                                                      arith pivots310
                                                      rlimit count121577
                                                      mk clause1212
                                                      datatype occurs check318
                                                      restarts1
                                                      mk bool var2873
                                                      arith assert upper710
                                                      datatype splits165
                                                      decisions1089
                                                      arith add rows2910
                                                      arith bound prop150
                                                      propagations2911
                                                      interface eqs14
                                                      conflicts153
                                                      arith fixed eqs794
                                                      datatype accessor ax154
                                                      minimized lits82
                                                      arith conflicts18
                                                      arith assert diseq115
                                                      datatype constructor ax804
                                                      num allocs1372822374
                                                      final checks24
                                                      added eqs8103
                                                      del clause782
                                                      arith eq adapter662
                                                      memory25.980000
                                                      max memory26.910000
                                                      Expand
                                                      • start[0.059s]
                                                          not
                                                          (((List.fold_right
                                                             (fun el _x
                                                              -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                 if el = None then (x, o)
                                                                 else
                                                                 if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                 else (x, o + 1))
                                                             (0, 0) (….a :: (… :: …))).0
                                                            + (List.fold_right
                                                               (fun el _x
                                                                -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                   if el = None then (x, o)
                                                                   else
                                                                   if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                   else (x, o + 1))
                                                               (0, 0) (….a :: (… :: …))).1
                                                            = 0 && :var_0:.last_player = None
                                                            || (List.fold_right
                                                                (fun el _x
                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                    if el = None then (x, o)
                                                                    else
                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                    else (x, o + 1))
                                                                (0, 0) (….a :: (… :: …))).0
                                                               -
                                                               (List.fold_right
                                                                (fun el _x
                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                    if el = None then (x, o)
                                                                    else
                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                    else (x, o + 1))
                                                                (0, 0) (….a :: (… :: …))).1
                                                               = 1 && :var_0:.last_player = Some X
                                                               || (List.fold_right
                                                                   (fun el _x
                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                       if el = None then (x, o)
                                                                       else
                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                       else (x, o + 1))
                                                                   (0, 0) (….a :: (… :: …))).0
                                                                  =
                                                                  (List.fold_right
                                                                   (fun el _x
                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                       if el = None then (x, o)
                                                                       else
                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                       else (x, o + 1))
                                                                   (0, 0) (….a :: (… :: …))).1
                                                                  && :var_0:.last_player = Some O)
                                                           && ((List.fold_right
                                                                (fun el _x
                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                    if el = None then (x, o)
                                                                    else
                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                    else (x, o + 1))
                                                                (0, 0) (….a :: (… :: …))).0
                                                               -
                                                               (List.fold_right
                                                                (fun el _x
                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                    if el = None then (x, o)
                                                                    else
                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                    else (x, o + 1))
                                                                (0, 0) (….a :: (… :: …))).1)
                                                              >= 2)
                                                      • simplify

                                                        into
                                                        not
                                                        ((((List.fold_right
                                                            (fun el _x
                                                             -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                if el = None then (x, o)
                                                                else
                                                                if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                else (x, o + 1))
                                                            (0, 0) (….a :: (… :: …))).0
                                                           + (List.fold_right
                                                              (fun el _x
                                                               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                  if el = None then (x, o)
                                                                  else
                                                                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                  else (x, o + 1))
                                                              (0, 0) (….a :: (… :: …))).1
                                                           = 0 && :var_0:.last_player = None
                                                           || (List.fold_right
                                                               (fun el _x
                                                                -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                   if el = None then (x, o)
                                                                   else
                                                                   if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                   else (x, o + 1))
                                                               (0, 0) (….a :: (… :: …))).0
                                                              + -1
                                                                * (List.fold_right
                                                                   (fun el _x
                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                       if el = None then (x, o)
                                                                       else
                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                       else (x, o + 1))
                                                                   (0, 0) (….a :: (… :: …))).1
                                                              = 1 && :var_0:.last_player = Some X)
                                                          || (List.fold_right
                                                              (fun el _x
                                                               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                  if el = None then (x, o)
                                                                  else
                                                                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                  else (x, o + 1))
                                                              (0, 0) (….a :: (… :: …))).0
                                                             =
                                                             (List.fold_right
                                                              (fun el _x
                                                               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                  if el = None then (x, o)
                                                                  else
                                                                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                  else (x, o + 1))
                                                              (0, 0) (….a :: (… :: …))).1
                                                             && :var_0:.last_player = Some O)
                                                         && ((List.fold_right
                                                              (fun el _x
                                                               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                  if el = None then (x, o)
                                                                  else
                                                                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                  else (x, o + 1))
                                                              (0, 0) (….a :: (… :: …))).0
                                                             + -1
                                                               * (List.fold_right
                                                                  (fun el _x
                                                                   -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                      if el = None then (x, o)
                                                                      else
                                                                      if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                      else (x, o + 1))
                                                                  (0, 0) (….a :: (… :: …))).1)
                                                            >= 2)
                                                        expansions
                                                        []
                                                        rewrite_steps
                                                          forward_chaining
                                                          • unroll
                                                            expr
                                                            (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                               (|::_3| (i_27 (grid_40 game_105)) |[…
                                                            expansions
                                                            • unroll
                                                              expr
                                                              (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                 (|::_3| (i_27 (grid_40 game_105)) |[…
                                                              expansions
                                                              • unroll
                                                                expr
                                                                (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                   (|::_3| (i_27 (grid_40 game_105)) |[…
                                                                expansions
                                                                • unroll
                                                                  expr
                                                                  (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                     (|::_3| (i_27 (grid_40 game_105)) |[…
                                                                  expansions
                                                                  • unroll
                                                                    expr
                                                                    (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                       (|::_3| (i_27 (grid_40 game_105)) |[…
                                                                    expansions
                                                                    • unroll
                                                                      expr
                                                                      (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                         (|::_3| (i_27 (grid_40 game_105)) |[…
                                                                      expansions
                                                                      • unroll
                                                                        expr
                                                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                           (|::_3| (i_27 (grid_40 game_105)) |[…
                                                                        expansions
                                                                        • unroll
                                                                          expr
                                                                          (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                             (|::_3| (i_27 (grid_40 game_105)) |[…
                                                                          expansions
                                                                          • unroll
                                                                            expr
                                                                            (|`List.fold_right anon_fun.move_counts.0[0]`_2286|
                                                                              (tuple_mk_2280 0 0)
                                                                              (|::_3| (i_27 (grid_40 g…
                                                                            expansions
                                                                            • unroll
                                                                              expr
                                                                              (|`List.fold_right anon_fun.move_counts.0[0]`_2286| (tuple_mk_2280 0 0) |[]_2|)
                                                                              expansions
                                                                              • unsat

                                                                                (let ((a!1 (|::_3| (h_26 (grid_40 game_105))
                                                                                                   (|::_3| (i_27 (grid_40 game_105)) |[…

                                                                              Valid games

                                                                              Let's continue adding some more definitions - we haven't really covered winning criteria as part of is_valid_grid, so let's include a few:

                                                                              In [16]:
                                                                              let is_tie = ({grid: {a, b, c, d, e, f, g, h, i}, _}) =>
                                                                                List.for_all((!=)(None), [a, b, c, d, e, f, g, h, i]);
                                                                              
                                                                              Out[16]:
                                                                              val is_tie : game_state -> bool = <fun>
                                                                              
                                                                              In [17]:
                                                                              let is_valid_game = game => {
                                                                                let winning_X = is_winning(game, X);
                                                                                let winning_O = is_winning(game, O);
                                                                                is_valid_grid(game.grid, game.last_player)
                                                                                && (! winning_X && ! winning_O || winning_X != winning_O);
                                                                              };
                                                                              
                                                                              Out[17]:
                                                                              val is_valid_game : game_state -> bool = <fun>
                                                                              

                                                                              ... and let's ask for a valid game where O is winning:

                                                                              In [18]:
                                                                              instance((game) => is_valid_game(game) && is_winning(game, O));
                                                                              
                                                                              Out[18]:
                                                                              - : game_state -> bool = <fun>
                                                                              module CX : sig val game : game_state end
                                                                              
                                                                              Instance (after 10 steps, 0.049s):
                                                                               let (game : game_state) =
                                                                                 {grid =
                                                                                   {a = None; b = (Some X); c = None; d = (Some O); e = (Some O);
                                                                                    f = (Some O); g = None; h = (Some X); i = (Some X)};
                                                                                  last_player = (Some O)}
                                                                              
                                                                              Instance
                                                                              proof attempt
                                                                              ground_instances10
                                                                              definitions0
                                                                              inductions0
                                                                              search_time
                                                                              0.049s
                                                                              details
                                                                              Expand
                                                                              smt_stats
                                                                              arith offset eqs319
                                                                              num checks21
                                                                              arith assert lower282
                                                                              arith patches_succ3
                                                                              arith pivots198
                                                                              rlimit count82383
                                                                              mk clause542
                                                                              datatype occurs check346
                                                                              mk bool var1635
                                                                              arith gcd tests14
                                                                              arith assert upper393
                                                                              datatype splits111
                                                                              decisions981
                                                                              arith add rows1574
                                                                              arith bound prop113
                                                                              propagations1933
                                                                              arith patches3
                                                                              interface eqs13
                                                                              conflicts103
                                                                              arith fixed eqs390
                                                                              datatype accessor ax92
                                                                              minimized lits14
                                                                              arith conflicts4
                                                                              arith assert diseq69
                                                                              datatype constructor ax645
                                                                              num allocs1542326878
                                                                              final checks24
                                                                              added eqs5693
                                                                              del clause179
                                                                              arith eq adapter254
                                                                              memory32.680000
                                                                              max memory32.680000
                                                                              Expand
                                                                              • start[0.049s]
                                                                                  (((List.fold_right
                                                                                     (fun el _x
                                                                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                         if el = None then (x, o)
                                                                                         else
                                                                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                         else (x, o + 1))
                                                                                     (0, 0) (….a :: (… :: …))).0
                                                                                    + (List.fold_right
                                                                                       (fun el _x
                                                                                        -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                           if el = None then (x, o)
                                                                                           else
                                                                                           if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                           else (x, o + 1))
                                                                                       (0, 0) (….a :: (… :: …))).1
                                                                                    = 0 && :var_0:.last_player = None
                                                                                    || (List.fold_right
                                                                                        (fun el _x
                                                                                         -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                            if el = None then (x, o)
                                                                                            else
                                                                                            if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                            else (x, o + 1))
                                                                                        (0, 0) (….a :: (… :: …))).0
                                                                                       -
                                                                                       (List.fold_right
                                                                                        (fun el _x
                                                                                         -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                            if el = None then (x, o)
                                                                                            else
                                                                                            if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                            else (x, o + 1))
                                                                                        (0, 0) (….a :: (… :: …))).1
                                                                                       = 1 && :var_0:.last_player = Some X
                                                                                       || (List.fold_right
                                                                                           (fun el _x
                                                                                            -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                               if el = None then (x, o)
                                                                                               else
                                                                                               if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                               else (x, o + 1))
                                                                                           (0, 0) (….a :: (… :: …))).0
                                                                                          =
                                                                                          (List.fold_right
                                                                                           (fun el _x
                                                                                            -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                               if el = None then (x, o)
                                                                                               else
                                                                                               if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                               else (x, o + 1))
                                                                                           (0, 0) (….a :: (… :: …))).1
                                                                                          && :var_0:.last_player = Some O)
                                                                                   && (not
                                                                                       ((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                        || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                           || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                              || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                 || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                    || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                       || (….a, ….e, ….i) = (Some X, Some X, Some X)
                                                                                                          || (….c, ….e, ….g) = (Some X, Some X, Some X))
                                                                                       && not
                                                                                          ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                           || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                              || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                 || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                    || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                       || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                          || (….a, ….e, ….i) = (Some O, Some O, Some O)
                                                                                                             || (….c, ….e, ….g) =
                                                                                                                (Some O, Some O, Some O))
                                                                                       || not
                                                                                          (((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                            || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                               || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                  || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                     || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                        || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                           || (….a, ….e, ….i) =
                                                                                                              (Some X, Some X, Some X)
                                                                                                              || (….c, ….e, ….g) =
                                                                                                                 (Some X, Some X, Some X))
                                                                                           =
                                                                                           ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                            || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                               || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                  || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                     || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                        || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                           || (….a, ….e, ….i) =
                                                                                                              (Some O, Some O, Some O)
                                                                                                              || (….c, ….e, ….g) =
                                                                                                                 (Some O, Some O, Some O)))))
                                                                                  && ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                      || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                         || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                            || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                               || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                  || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                     || (….a, ….e, ….i) = (Some O, Some O, Some O)
                                                                                                        || (….c, ….e, ….g) = (Some O, Some O, Some O))
                                                                              • simplify

                                                                                into
                                                                                ((((List.fold_right
                                                                                    (fun el _x
                                                                                     -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                        if el = None then (x, o)
                                                                                        else
                                                                                        if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                        else (x, o + 1))
                                                                                    (0, 0) (….a :: (… :: …))).0
                                                                                   + (List.fold_right
                                                                                      (fun el _x
                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                          if el = None then (x, o)
                                                                                          else
                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                          else (x, o + 1))
                                                                                      (0, 0) (….a :: (… :: …))).1
                                                                                   = 0 && :var_0:.last_player = None
                                                                                   || (List.fold_right
                                                                                       (fun el _x
                                                                                        -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                           if el = None then (x, o)
                                                                                           else
                                                                                           if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                           else (x, o + 1))
                                                                                       (0, 0) (….a :: (… :: …))).0
                                                                                      + -1
                                                                                        * (List.fold_right
                                                                                           (fun el _x
                                                                                            -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                               if el = None then (x, o)
                                                                                               else
                                                                                               if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                               else (x, o + 1))
                                                                                           (0, 0) (….a :: (… :: …))).1
                                                                                      = 1 && :var_0:.last_player = Some X)
                                                                                  || (List.fold_right
                                                                                      (fun el _x
                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                          if el = None then (x, o)
                                                                                          else
                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                          else (x, o + 1))
                                                                                      (0, 0) (….a :: (… :: …))).0
                                                                                     =
                                                                                     (List.fold_right
                                                                                      (fun el _x
                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                          if el = None then (x, o)
                                                                                          else
                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                          else (x, o + 1))
                                                                                      (0, 0) (….a :: (… :: …))).1
                                                                                     && :var_0:.last_player = Some O)
                                                                                 && (not
                                                                                     ((((((((….a = Some X && … = Some X) && ….c = Some X
                                                                                            || (….d = Some X && ….e = Some X) && ….f = Some X)
                                                                                           || (….g = Some X && ….h = Some X) && ….i = Some X)
                                                                                          || (….a = Some X && ….d = Some X) && ….g = Some X)
                                                                                         || (… = Some X && ….e = Some X) && ….h = Some X)
                                                                                        || (….c = Some X && ….f = Some X) && ….i = Some X)
                                                                                       || (….a = Some X && ….e = Some X) && ….i = Some X)
                                                                                      || (….c = Some X && ….e = Some X) && ….g = Some X)
                                                                                     && not
                                                                                        ((((((((….a = Some O && … = Some O) && ….c = Some O
                                                                                               || (….d = Some O && ….e = Some O) && ….f = Some O)
                                                                                              || (….g = Some O && ….h = Some O) && ….i = Some O)
                                                                                             || (….a = Some O && ….d = Some O) && ….g = Some O)
                                                                                            || (… = Some O && ….e = Some O) && ….h = Some O)
                                                                                           || (….c = Some O && ….f = Some O) && ….i = Some O)
                                                                                          || (….a = Some O && ….e = Some O) && ….i = Some O)
                                                                                         || (….c = Some O && ….e = Some O) && ….g = Some O)
                                                                                     || not
                                                                                        ((((((((….a = Some X && … = Some X) && ….c = Some X
                                                                                               || (….d = Some X && ….e = Some X) && ….f = Some X)
                                                                                              || (….g = Some X && ….h = Some X) && ….i = Some X)
                                                                                             || (….a = Some X && ….d = Some X) && ….g = Some X)
                                                                                            || (… = Some X && ….e = Some X) && ….h = Some X)
                                                                                           || (….c = Some X && ….f = Some X) && ….i = Some X)
                                                                                          || (….a = Some X && ….e = Some X) && ….i = Some X)
                                                                                         || (….c = Some X && ….e = Some X) && ….g = Some X)
                                                                                        =
                                                                                        ((((((((….a = Some O && … = Some O) && ….c = Some O
                                                                                               || (….d = Some O && ….e = Some O) && ….f = Some O)
                                                                                              || (….g = Some O && ….h = Some O) && ….i = Some O)
                                                                                             || (….a = Some O && ….d = Some O) && ….g = Some O)
                                                                                            || (… = Some O && ….e = Some O) && ….h = Some O)
                                                                                           || (….c = Some O && ….f = Some O) && ….i = Some O)
                                                                                          || (….a = Some O && ….e = Some O) && ….i = Some O)
                                                                                         || (….c = Some O && ….e = Some O) && ….g = Some O)))
                                                                                && ((((((((….a = Some O && … = Some O) && ….c = Some O
                                                                                          || (….d = Some O && ….e = Some O) && ….f = Some O)
                                                                                         || (….g = Some O && ….h = Some O) && ….i = Some O)
                                                                                        || (….a = Some O && ….d = Some O) && ….g = Some O)
                                                                                       || (… = Some O && ….e = Some O) && ….h = Some O)
                                                                                      || (….c = Some O && ….f = Some O) && ….i = Some O)
                                                                                     || (….a = Some O && ….e = Some O) && ….i = Some O)
                                                                                    || (….c = Some O && ….e = Some O) && ….g = Some O)
                                                                                expansions
                                                                                []
                                                                                rewrite_steps
                                                                                  forward_chaining
                                                                                  • unroll
                                                                                    expr
                                                                                    (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                       (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                    expansions
                                                                                    • unroll
                                                                                      expr
                                                                                      (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                         (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                      expansions
                                                                                      • unroll
                                                                                        expr
                                                                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                           (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                        expansions
                                                                                        • unroll
                                                                                          expr
                                                                                          (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                             (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                          expansions
                                                                                          • unroll
                                                                                            expr
                                                                                            (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                               (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                            expansions
                                                                                            • unroll
                                                                                              expr
                                                                                              (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                                 (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                              expansions
                                                                                              • unroll
                                                                                                expr
                                                                                                (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                                   (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                                expansions
                                                                                                • unroll
                                                                                                  expr
                                                                                                  (let ((a!1 (|::_3| (h_26 (grid_40 game_124))
                                                                                                                     (|::_3| (i_27 (grid_40 game_124)) |[…
                                                                                                  expansions
                                                                                                  • unroll
                                                                                                    expr
                                                                                                    (|`List.fold_right anon_fun.move_counts.0[0]`_2490|
                                                                                                      (tuple_mk_2484 0 0)
                                                                                                      (|::_3| (i_27 (grid_40 g…
                                                                                                    expansions
                                                                                                    • unroll
                                                                                                      expr
                                                                                                      (|`List.fold_right anon_fun.move_counts.0[0]`_2490| (tuple_mk_2484 0 0) |[]_2|)
                                                                                                      expansions
                                                                                                      • Sat (Some let (game : game_state) = {grid = {a = None; b = (Some X); c = None; d = (Some O); e = (Some O); f = (Some O); g = None; h = (Some X); i = (Some X)}; last_player = (Some O)} )
                                                                                                      In [19]:
                                                                                                      CX.game;
                                                                                                      
                                                                                                      Out[19]:
                                                                                                      - : game_state = <document>
                                                                                                      
                                                                                                      ··
                                                                                                      ·
                                                                                                      Last:

                                                                                                      Valid moves

                                                                                                      Looks good! We're on the home stretch now - let's add the last few helper functions around playing moves:

                                                                                                      In [20]:
                                                                                                      let is_valid_move = (game, player, move) =>
                                                                                                        ! (is_winning(game, X) || is_winning(game, O) || is_tie(game))
                                                                                                        && is_valid_game(game)
                                                                                                        && (
                                                                                                          game.last_player == None
                                                                                                          && player == initial_player
                                                                                                          || game.last_player == Some(other_player(player))
                                                                                                        );
                                                                                                      
                                                                                                      let play_move = ({grid, _}, player, move) => {
                                                                                                        let play = Some(player);
                                                                                                        let grid =
                                                                                                          switch (move) {
                                                                                                          | A => {...grid, a: play}
                                                                                                          | B => {...grid, b: play}
                                                                                                          | C => {...grid, c: play}
                                                                                                          | D => {...grid, d: play}
                                                                                                          | E => {...grid, e: play}
                                                                                                          | F => {...grid, f: play}
                                                                                                          | G => {...grid, g: play}
                                                                                                          | H => {...grid, h: play}
                                                                                                          | I => {...grid, i: play}
                                                                                                          };
                                                                                                        {grid, last_player: play};
                                                                                                      };
                                                                                                      
                                                                                                      let status = game =>
                                                                                                        if (is_winning(game, X)) {
                                                                                                          Won(X);
                                                                                                        } else if (is_winning(game, O)) {
                                                                                                          Won(O);
                                                                                                        } else if (is_tie(game)) {
                                                                                                          Tied;
                                                                                                        } else {
                                                                                                          InProgress;
                                                                                                        };
                                                                                                      
                                                                                                      Out[20]:
                                                                                                      val is_valid_move : game_state -> player -> 'a -> bool = <fun>
                                                                                                      val play_move : game_state -> player -> move -> game_state = <fun>
                                                                                                      val status : game_state -> game_status = <fun>
                                                                                                      

                                                                                                      And finally, the function we call from the ReasonReact frontend to actually play the game!

                                                                                                      In [21]:
                                                                                                      let play = ({last_player, _} as game, move) => {
                                                                                                        let player =
                                                                                                          switch (last_player) {
                                                                                                          | None => initial_player
                                                                                                          | Some(player) => other_player(player)
                                                                                                          };
                                                                                                        if (is_valid_move(game, player, move)) {
                                                                                                          let game = play_move(game, player, move);
                                                                                                          (game, status(game));
                                                                                                        } else {
                                                                                                          (game, InvalidMove(move));
                                                                                                        };
                                                                                                      };
                                                                                                      
                                                                                                      Out[21]:
                                                                                                      val play : game_state -> move -> game_state * game_status = <fun>
                                                                                                      

                                                                                                      ...and we're done! Let's add one more verification statement to check that these functions work as we expect. If we've got a valid game, and a valid move, then if we play the move on the game, we should still have a valid game.

                                                                                                      verify((game, player, move) =>
                                                                                                        (is_valid_game(game) && is_valid_move(game, player, move))
                                                                                                        ==> is_valid_game(play_move(game, player, move))
                                                                                                      );

                                                                                                      The a ==> b operator here is the logical "implies" - "if a is true, then b is also true". It's defined as a regular infix operator in the Imandra prelude:

                                                                                                      In [22]:
                                                                                                      (==>)
                                                                                                      
                                                                                                      Out[22]:
                                                                                                      - : bool -> bool -> bool = <fun>
                                                                                                      

                                                                                                      Anyway! Let's actually run the statement:

                                                                                                      In [23]:
                                                                                                      verify((game, player, move) =>
                                                                                                        (is_valid_game(game) && is_valid_move(game, player, move))
                                                                                                        ==> is_valid_game(play_move(game, player, move))
                                                                                                      );
                                                                                                      
                                                                                                      Out[23]:
                                                                                                      - : game_state -> player -> move -> bool = <fun>
                                                                                                      module CX : sig val game : game_state val player : player val move : move end
                                                                                                      
                                                                                                      Counterexample (after 24 steps, 0.191s):
                                                                                                       let (game : game_state) =
                                                                                                         {grid =
                                                                                                           {a = None; b = None; c = (Some O); d = None; e = (Some X); f = (Some X);
                                                                                                            g = (Some X); h = None; i = (Some O)};
                                                                                                          last_player = (Some X)}
                                                                                                       let (player : player) = O
                                                                                                       let (move : move) = I
                                                                                                      
                                                                                                      Refuted
                                                                                                      proof attempt
                                                                                                      ground_instances24
                                                                                                      definitions0
                                                                                                      inductions0
                                                                                                      search_time
                                                                                                      0.191s
                                                                                                      details
                                                                                                      Expand
                                                                                                      smt_stats
                                                                                                      arith offset eqs2963
                                                                                                      num checks49
                                                                                                      arith assert lower1331
                                                                                                      arith patches_succ2
                                                                                                      arith pivots508
                                                                                                      rlimit count421857
                                                                                                      mk clause1618
                                                                                                      datatype occurs check5074
                                                                                                      restarts1
                                                                                                      mk bool var10432
                                                                                                      arith gcd tests4
                                                                                                      arith assert upper1697
                                                                                                      datatype splits751
                                                                                                      decisions6742
                                                                                                      arith add rows5794
                                                                                                      arith bound prop269
                                                                                                      propagations11719
                                                                                                      arith patches2
                                                                                                      interface eqs104
                                                                                                      conflicts300
                                                                                                      arith fixed eqs2557
                                                                                                      datatype accessor ax293
                                                                                                      minimized lits94
                                                                                                      arith conflicts13
                                                                                                      arith assert diseq248
                                                                                                      datatype constructor ax7263
                                                                                                      num allocs1899093891
                                                                                                      final checks130
                                                                                                      added eqs47621
                                                                                                      del clause622
                                                                                                      arith eq adapter1192
                                                                                                      memory33.890000
                                                                                                      max memory33.990000
                                                                                                      Expand
                                                                                                      • start[0.191s]
                                                                                                          (((List.fold_right
                                                                                                             (fun el _x
                                                                                                              -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                 if el = None then (x, o)
                                                                                                                 else
                                                                                                                 if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                 else (x, o + 1))
                                                                                                             (0, 0) (….a :: (… :: …))).0
                                                                                                            + (List.fold_right
                                                                                                               (fun el _x
                                                                                                                -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                   if el = None then (x, o)
                                                                                                                   else
                                                                                                                   if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                   else (x, o + 1))
                                                                                                               (0, 0) (….a :: (… :: …))).1
                                                                                                            = 0 && :var_0:.last_player = None
                                                                                                            || (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).0
                                                                                                               -
                                                                                                               (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).1
                                                                                                               = 1 && :var_0:.last_player = Some X
                                                                                                               || (List.fold_right
                                                                                                                   (fun el _x
                                                                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                       if el = None then (x, o)
                                                                                                                       else
                                                                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                       else (x, o + 1))
                                                                                                                   (0, 0) (….a :: (… :: …))).0
                                                                                                                  =
                                                                                                                  (List.fold_right
                                                                                                                   (fun el _x
                                                                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                       if el = None then (x, o)
                                                                                                                       else
                                                                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                       else (x, o + 1))
                                                                                                                   (0, 0) (….a :: (… :: …))).1
                                                                                                                  && :var_0:.last_player = Some O)
                                                                                                           && (not
                                                                                                               ((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                                || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                   || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                      || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                         || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                            || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                                               || (….a, ….e, ….i) = (Some X, Some X, Some X)
                                                                                                                                  || (….c, ….e, ….g) = (Some X, Some X, Some X))
                                                                                                               && not
                                                                                                                  ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                   || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                      || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                         || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                            || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                               || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                                                  || (….a, ….e, ….i) = (Some O, Some O, Some O)
                                                                                                                                     || (….c, ….e, ….g) =
                                                                                                                                        (Some O, Some O, Some O))
                                                                                                               || not
                                                                                                                  (((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                                    || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                       || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                          || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                             || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                                || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                                                   || (….a, ….e, ….i) =
                                                                                                                                      (Some X, Some X, Some X)
                                                                                                                                      || (….c, ….e, ….g) =
                                                                                                                                         (Some X, Some X, Some X))
                                                                                                                   =
                                                                                                                   ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                    || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                       || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                          || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                             || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                                || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                                                   || (….a, ….e, ….i) =
                                                                                                                                      (Some O, Some O, Some O)
                                                                                                                                      || (….c, ….e, ….g) =
                                                                                                                                         (Some O, Some O, Some O)))))
                                                                                                          && not
                                                                                                             (((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                               || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                  || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                     || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                        || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                           || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                                              || (….a, ….e, ….i) = (Some X, Some X, Some X)
                                                                                                                                 || (….c, ….e, ….g) = (Some X, Some X, Some X))
                                                                                                              || ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                  || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                     || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                        || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                           || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                              || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                                                 || (….a, ….e, ….i) = (Some O, Some O, Some O)
                                                                                                                                    || (….c, ….e, ….g) =
                                                                                                                                       (Some O, Some O, Some O))
                                                                                                                 || List.for_all ((<>) None) (….a :: (… :: …)))
                                                                                                             && (((List.fold_right
                                                                                                                   (fun el _x
                                                                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                       if el = None then (x, o)
                                                                                                                       else
                                                                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                       else (x, o + 1))
                                                                                                                   (0, 0) (….a :: (… :: …))).0
                                                                                                                  + (List.fold_right
                                                                                                                     (fun el _x
                                                                                                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                         if el = None then (x, o)
                                                                                                                         else
                                                                                                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                         else (x, o + 1))
                                                                                                                     (0, 0) (….a :: (… :: …))).1
                                                                                                                  = 0 && :var_0:.last_player = None
                                                                                                                  || (List.fold_right
                                                                                                                      (fun el _x
                                                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                          if el = None then (x, o)
                                                                                                                          else
                                                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                          else (x, o + 1))
                                                                                                                      (0, 0) (….a :: (… :: …))).0
                                                                                                                     -
                                                                                                                     (List.fold_right
                                                                                                                      (fun el _x
                                                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                          if el = None then (x, o)
                                                                                                                          else
                                                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                          else (x, o + 1))
                                                                                                                      (0, 0) (….a :: (… :: …))).1
                                                                                                                     = 1 && :var_0:.last_player = Some X
                                                                                                                     || (List.fold_right
                                                                                                                         (fun el _x
                                                                                                                          -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                             if el = None then (x, o)
                                                                                                                             else
                                                                                                                             if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                             else (x, o + 1))
                                                                                                                         (0, 0) (….a :: (… :: …))).0
                                                                                                                        =
                                                                                                                        (List.fold_right
                                                                                                                         (fun el _x
                                                                                                                          -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                             if el = None then (x, o)
                                                                                                                             else
                                                                                                                             if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                             else (x, o + 1))
                                                                                                                         (0, 0) (….a :: (… :: …))).1
                                                                                                                        && :var_0:.last_player = Some O)
                                                                                                                 && (not
                                                                                                                     ((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                                      || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                         || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                            || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                               || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                                  || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                                                     || (….a, ….e, ….i) =
                                                                                                                                        (Some X, Some X, Some X)
                                                                                                                                        || (….c, ….e, ….g) =
                                                                                                                                           (Some X, Some X, Some X))
                                                                                                                     && not
                                                                                                                        ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                         || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                            || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                               || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                                  || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                                     || (….c, ….f, ….i) =
                                                                                                                                        (Some O, Some O, Some O)
                                                                                                                                        || (….a, ….e, ….i) =
                                                                                                                                           (Some O, Some O, Some O)
                                                                                                                                           || (….c, ….e, ….g) =
                                                                                                                                              (Some O, Some O, Some O))
                                                                                                                     || not
                                                                                                                        (((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                                          || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                             || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                                || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                                   || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                                      || (….c, ….f, ….i) =
                                                                                                                                         (Some X, Some X, Some X)
                                                                                                                                         || (….a, ….e, ….i) =
                                                                                                                                            (Some X, Some X, Some X)
                                                                                                                                            || (….c, ….e, ….g) =
                                                                                                                                               (Some X, Some X, Some X))
                                                                                                                         =
                                                                                                                         ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                          || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                             || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                                || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                                   || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                                      || (….c, ….f, ….i) =
                                                                                                                                         (Some O, Some O, Some O)
                                                                                                                                         || (….a, ….e, ….i) =
                                                                                                                                            (Some O, Some O, Some O)
                                                                                                                                            || (….c, ….e, ….g) =
                                                                                                                                               (Some O, Some O, Some O)))))
                                                                                                                && (:var_0:.last_player = None && :var_1: = X
                                                                                                                    || :var_0:.last_player = Some (if :var_1: = X then O else X))
                                                                                                          ==> ((List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).0
                                                                                                               + (List.fold_right
                                                                                                                  (fun el _x
                                                                                                                   -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                      if el = None then (x, o)
                                                                                                                      else
                                                                                                                      if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                      else (x, o + 1))
                                                                                                                  (0, 0) (….a :: (… :: …))).1
                                                                                                               = 0 && … = None
                                                                                                               || (List.fold_right
                                                                                                                   (fun el _x
                                                                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                       if el = None then (x, o)
                                                                                                                       else
                                                                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                       else (x, o + 1))
                                                                                                                   (0, 0) (….a :: (… :: …))).0
                                                                                                                  -
                                                                                                                  (List.fold_right
                                                                                                                   (fun el _x
                                                                                                                    -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                       if el = None then (x, o)
                                                                                                                       else
                                                                                                                       if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                       else (x, o + 1))
                                                                                                                   (0, 0) (….a :: (… :: …))).1
                                                                                                                  = 1 && … = Some X
                                                                                                                  || (List.fold_right
                                                                                                                      (fun el _x
                                                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                          if el = None then (x, o)
                                                                                                                          else
                                                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                          else (x, o + 1))
                                                                                                                      (0, 0) (….a :: (… :: …))).0
                                                                                                                     =
                                                                                                                     (List.fold_right
                                                                                                                      (fun el _x
                                                                                                                       -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                          if el = None then (x, o)
                                                                                                                          else
                                                                                                                          if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                          else (x, o + 1))
                                                                                                                      (0, 0) (….a :: (… :: …))).1
                                                                                                                     && … = Some O)
                                                                                                              && (not
                                                                                                                  ((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                                   || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                      || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                         || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                            || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                               || (….c, ….f, ….i) = (Some X, Some X, Some X)
                                                                                                                                  || (….a, ….e, ….i) = (Some X, Some X, Some X)
                                                                                                                                     || (….c, ….e, ….g) =
                                                                                                                                        (Some X, Some X, Some X))
                                                                                                                  && not
                                                                                                                     ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                      || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                         || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                            || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                               || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                                  || (….c, ….f, ….i) = (Some O, Some O, Some O)
                                                                                                                                     || (….a, ….e, ….i) =
                                                                                                                                        (Some O, Some O, Some O)
                                                                                                                                        || (….c, ….e, ….g) =
                                                                                                                                           (Some O, Some O, Some O))
                                                                                                                  || not
                                                                                                                     (((….a, …, ….c) = (Some X, Some X, Some X)
                                                                                                                       || (….d, ….e, ….f) = (Some X, Some X, Some X)
                                                                                                                          || (….g, ….h, ….i) = (Some X, Some X, Some X)
                                                                                                                             || (….a, ….d, ….g) = (Some X, Some X, Some X)
                                                                                                                                || (…, ….e, ….h) = (Some X, Some X, Some X)
                                                                                                                                   || (….c, ….f, ….i) =
                                                                                                                                      (Some X, Some X, Some X)
                                                                                                                                      || (….a, ….e, ….i) =
                                                                                                                                         (Some X, Some X, Some X)
                                                                                                                                         || (….c, ….e, ….g) =
                                                                                                                                            (Some X, Some X, Some X))
                                                                                                                      =
                                                                                                                      ((….a, …, ….c) = (Some O, Some O, Some O)
                                                                                                                       || (….d, ….e, ….f) = (Some O, Some O, Some O)
                                                                                                                          || (….g, ….h, ….i) = (Some O, Some O, Some O)
                                                                                                                             || (….a, ….d, ….g) = (Some O, Some O, Some O)
                                                                                                                                || (…, ….e, ….h) = (Some O, Some O, Some O)
                                                                                                                                   || (….c, ….f, ….i) =
                                                                                                                                      (Some O, Some O, Some O)
                                                                                                                                      || (….a, ….e, ….i) =
                                                                                                                                         (Some O, Some O, Some O)
                                                                                                                                         || (….c, ….e, ….g) =
                                                                                                                                            (Some O, Some O, Some O))))
                                                                                                      • simplify

                                                                                                        into
                                                                                                        not
                                                                                                        ((((((List.fold_right
                                                                                                              (fun el _x
                                                                                                               -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                  if el = None then (x, o)
                                                                                                                  else
                                                                                                                  if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                  else (x, o + 1))
                                                                                                              (0, 0) (….a :: (… :: …))).0
                                                                                                             + (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).1
                                                                                                             = 0 && :var_0:.last_player = None
                                                                                                             || (List.fold_right
                                                                                                                 (fun el _x
                                                                                                                  -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                     if el = None then (x, o)
                                                                                                                     else
                                                                                                                     if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                     else (x, o + 1))
                                                                                                                 (0, 0) (….a :: (… :: …))).0
                                                                                                                + -1
                                                                                                                  * (List.fold_right
                                                                                                                     (fun el _x
                                                                                                                      -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                         if el = None then (x, o)
                                                                                                                         else
                                                                                                                         if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                         else (x, o + 1))
                                                                                                                     (0, 0) (….a :: (… :: …))).1
                                                                                                                = 1 && :var_0:.last_player = Some X)
                                                                                                            || (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).0
                                                                                                               =
                                                                                                               (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).1
                                                                                                               && :var_0:.last_player = Some O)
                                                                                                           && (not
                                                                                                               ((((((((….a = Some X && … = Some X) && ….c = Some X
                                                                                                                      || (….d = Some X && ….e = Some X) && ….f = Some X)
                                                                                                                     || (….g = Some X && ….h = Some X) && ….i = Some X)
                                                                                                                    || (….a = Some X && ….d = Some X) && ….g = Some X)
                                                                                                                   || (… = Some X && ….e = Some X) && ….h = Some X)
                                                                                                                  || (….c = Some X && ….f = Some X) && ….i = Some X)
                                                                                                                 || (….a = Some X && ….e = Some X) && ….i = Some X)
                                                                                                                || (….c = Some X && ….e = Some X) && ….g = Some X)
                                                                                                               && not
                                                                                                                  ((((((((….a = Some O && … = Some O) && ….c = Some O
                                                                                                                         || (….d = Some O && ….e = Some O) && ….f = Some O)
                                                                                                                        || (….g = Some O && ….h = Some O) && ….i = Some O)
                                                                                                                       || (….a = Some O && ….d = Some O) && ….g = Some O)
                                                                                                                      || (… = Some O && ….e = Some O) && ….h = Some O)
                                                                                                                     || (….c = Some O && ….f = Some O) && ….i = Some O)
                                                                                                                    || (….a = Some O && ….e = Some O) && ….i = Some O)
                                                                                                                   || (….c = Some O && ….e = Some O) && ….g = Some O)
                                                                                                               || not
                                                                                                                  ((((((((….a = Some X && … = Some X) && ….c = Some X
                                                                                                                         || (….d = Some X && ….e = Some X) && ….f = Some X)
                                                                                                                        || (….g = Some X && ….h = Some X) && ….i = Some X)
                                                                                                                       || (….a = Some X && ….d = Some X) && ….g = Some X)
                                                                                                                      || (… = Some X && ….e = Some X) && ….h = Some X)
                                                                                                                     || (….c = Some X && ….f = Some X) && ….i = Some X)
                                                                                                                    || (….a = Some X && ….e = Some X) && ….i = Some X)
                                                                                                                   || (….c = Some X && ….e = Some X) && ….g = Some X)
                                                                                                                  =
                                                                                                                  ((((((((….a = Some O && … = Some O) && ….c = Some O
                                                                                                                         || (….d = Some O && ….e = Some O) && ….f = Some O)
                                                                                                                        || (….g = Some O && ….h = Some O) && ….i = Some O)
                                                                                                                       || (….a = Some O && ….d = Some O) && ….g = Some O)
                                                                                                                      || (… = Some O && ….e = Some O) && ….h = Some O)
                                                                                                                     || (….c = Some O && ….f = Some O) && ….i = Some O)
                                                                                                                    || (….a = Some O && ….e = Some O) && ….i = Some O)
                                                                                                                   || (….c = Some O && ….e = Some O) && ….g = Some O)))
                                                                                                          && not
                                                                                                             (((((((((((((((((….a = Some X && … = Some X) && ….c = Some X
                                                                                                                             || (….d = Some X && ….e = Some X) && ….f = Some X)
                                                                                                                            || (….g = Some X && ….h = Some X) && ….i = Some X)
                                                                                                                           || (….a = Some X && ….d = Some X) && ….g = Some X)
                                                                                                                          || (… = Some X && ….e = Some X) && ….h = Some X)
                                                                                                                         || (….c = Some X && ….f = Some X) && ….i = Some X)
                                                                                                                        || (….a = Some X && ….e = Some X) && ….i = Some X)
                                                                                                                       || (….c = Some X && ….e = Some X) && ….g = Some X)
                                                                                                                      || (….a = Some O && … = Some O) && ….c = Some O)
                                                                                                                     || (….d = Some O && ….e = Some O) && ….f = Some O)
                                                                                                                    || (….g = Some O && ….h = Some O) && ….i = Some O)
                                                                                                                   || (….a = Some O && ….d = Some O) && ….g = Some O)
                                                                                                                  || (… = Some O && ….e = Some O) && ….h = Some O)
                                                                                                                 || (….c = Some O && ….f = Some O) && ….i = Some O)
                                                                                                                || (….a = Some O && ….e = Some O) && ….i = Some O)
                                                                                                               || (….c = Some O && ….e = Some O) && ….g = Some O)
                                                                                                              || List.for_all ((<>) None) (….a :: (… :: …))))
                                                                                                         && (:var_0:.last_player = None && :var_1: = X
                                                                                                             || :var_0:.last_player = Some (if :var_1: = X then O else X)))
                                                                                                        || ((List.fold_right
                                                                                                             (fun el _x
                                                                                                              -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                 if el = None then (x, o)
                                                                                                                 else
                                                                                                                 if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                 else (x, o + 1))
                                                                                                             (0, 0) (….a :: (… :: …))).0
                                                                                                            + -1
                                                                                                              * (List.fold_right
                                                                                                                 (fun el _x
                                                                                                                  -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                     if el = None then (x, o)
                                                                                                                     else
                                                                                                                     if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                     else (x, o + 1))
                                                                                                                 (0, 0) (….a :: (… :: …))).1
                                                                                                            = 1 && :var_1: = X
                                                                                                            || (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).0
                                                                                                               =
                                                                                                               (List.fold_right
                                                                                                                (fun el _x
                                                                                                                 -> let (x : int) = _x.0 and (o : int) = _x.1 in
                                                                                                                    if el = None then (x, o)
                                                                                                                    else
                                                                                                                    if Is_a(Some, el) && Option.get el = X then (x + 1, o)
                                                                                                                    else (x, o + 1))
                                                                                                                (0, 0) (….a :: (… :: …))).1
                                                                                                               && :var_1: = O)
                                                                                                           && (not
                                                                                                               ((((((((….a = Some X && … = Some X)
                                                                                                                      && (if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).c
                                                                                                                         = Some X
                                                                                                                      || ((if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).d
                                                                                                                          = Some X
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).e
                                                                                                                             = Some X)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).f
                                                                                                                            = Some X)
                                                                                                                     || ((if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).g
                                                                                                                         = Some X
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).h
                                                                                                                            = Some X)
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).i
                                                                                                                           = Some X)
                                                                                                                    || (….a = Some X
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).d
                                                                                                                           = Some X)
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).g
                                                                                                                          = Some X)
                                                                                                                   || (… = Some X
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).e
                                                                                                                          = Some X)
                                                                                                                      && (if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).h
                                                                                                                         = Some X)
                                                                                                                  || ((if :var_2: = A
                                                                                                                       then
                                                                                                                         {a = Some :var_1:; b = …; c = ….c; d = ….d; e = ….e;
                                                                                                                          f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                       else
                                                                                                                       if :var_2: = B
                                                                                                                       then
                                                                                                                         {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                          e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                       else if :var_2: = C then … else …).c
                                                                                                                      = Some X
                                                                                                                      && (if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).f
                                                                                                                         = Some X)
                                                                                                                     && (if :var_2: = A
                                                                                                                         then
                                                                                                                           {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                            e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                         else
                                                                                                                         if :var_2: = B
                                                                                                                         then
                                                                                                                           {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                            e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                         else if :var_2: = C then … else …).i
                                                                                                                        = Some X)
                                                                                                                 || (….a = Some X
                                                                                                                     && (if :var_2: = A
                                                                                                                         then
                                                                                                                           {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                            e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                         else
                                                                                                                         if :var_2: = B
                                                                                                                         then
                                                                                                                           {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                            e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                         else if :var_2: = C then … else …).e
                                                                                                                        = Some X)
                                                                                                                    && (if :var_2: = A
                                                                                                                        then
                                                                                                                          {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else
                                                                                                                        if :var_2: = B
                                                                                                                        then
                                                                                                                          {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else if :var_2: = C then … else …).i
                                                                                                                       = Some X)
                                                                                                                || ((if :var_2: = A
                                                                                                                     then
                                                                                                                       {a = Some :var_1:; b = …; c = ….c; d = ….d; e = ….e;
                                                                                                                        f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                     else
                                                                                                                     if :var_2: = B
                                                                                                                     then
                                                                                                                       {a = ….a; b = Some :var_1:; c = ….c; d = ….d; e = ….e;
                                                                                                                        f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                     else if :var_2: = C then … else …).c
                                                                                                                    = Some X
                                                                                                                    && (if :var_2: = A
                                                                                                                        then
                                                                                                                          {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else
                                                                                                                        if :var_2: = B
                                                                                                                        then
                                                                                                                          {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else if :var_2: = C then … else …).e
                                                                                                                       = Some X)
                                                                                                                   && (if :var_2: = A
                                                                                                                       then
                                                                                                                         {a = Some :var_1:; b = …; c = ….c; d = ….d; e = ….e;
                                                                                                                          f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                       else
                                                                                                                       if :var_2: = B
                                                                                                                       then
                                                                                                                         {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                          e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                       else if :var_2: = C then … else …).g
                                                                                                                      = Some X)
                                                                                                               && not
                                                                                                                  ((((((((….a = Some O && … = Some O)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).c
                                                                                                                            = Some O
                                                                                                                         || ((if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).d
                                                                                                                             = Some O
                                                                                                                             && (if :var_2: = A
                                                                                                                                 then
                                                                                                                                   {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                    e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                    i = ….i}
                                                                                                                                 else
                                                                                                                                 if :var_2: = B
                                                                                                                                 then
                                                                                                                                   {a = ….a; b = Some :var_1:; c = ….c;
                                                                                                                                    d = ….d; e = ….e; f = ….f; g = ….g;
                                                                                                                                    h = ….h; i = ….i}
                                                                                                                                 else if :var_2: = C then … else …).e
                                                                                                                                = Some O)
                                                                                                                            && (if :var_2: = A
                                                                                                                                then
                                                                                                                                  {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else
                                                                                                                                if :var_2: = B
                                                                                                                                then
                                                                                                                                  {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else if :var_2: = C then … else …).f
                                                                                                                               = Some O)
                                                                                                                        || ((if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).g
                                                                                                                            = Some O
                                                                                                                            && (if :var_2: = A
                                                                                                                                then
                                                                                                                                  {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else
                                                                                                                                if :var_2: = B
                                                                                                                                then
                                                                                                                                  {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else if :var_2: = C then … else …).h
                                                                                                                               = Some O)
                                                                                                                           && (if :var_2: = A
                                                                                                                               then
                                                                                                                                 {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else
                                                                                                                               if :var_2: = B
                                                                                                                               then
                                                                                                                                 {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else if :var_2: = C then … else …).i
                                                                                                                              = Some O)
                                                                                                                       || (….a = Some O
                                                                                                                           && (if :var_2: = A
                                                                                                                               then
                                                                                                                                 {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else
                                                                                                                               if :var_2: = B
                                                                                                                               then
                                                                                                                                 {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else if :var_2: = C then … else …).d
                                                                                                                              = Some O)
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).g
                                                                                                                             = Some O)
                                                                                                                      || (… = Some O
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).e
                                                                                                                             = Some O)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).h
                                                                                                                            = Some O)
                                                                                                                     || ((if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).c
                                                                                                                         = Some O
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).f
                                                                                                                            = Some O)
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).i
                                                                                                                           = Some O)
                                                                                                                    || (….a = Some O
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).e
                                                                                                                           = Some O)
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).i
                                                                                                                          = Some O)
                                                                                                                   || ((if :var_2: = A
                                                                                                                        then
                                                                                                                          {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else
                                                                                                                        if :var_2: = B
                                                                                                                        then
                                                                                                                          {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else if :var_2: = C then … else …).c
                                                                                                                       = Some O
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).e
                                                                                                                          = Some O)
                                                                                                                      && (if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).g
                                                                                                                         = Some O)
                                                                                                               || not
                                                                                                                  ((((((((….a = Some X && … = Some X)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).c
                                                                                                                            = Some X
                                                                                                                         || ((if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).d
                                                                                                                             = Some X
                                                                                                                             && (if :var_2: = A
                                                                                                                                 then
                                                                                                                                   {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                    e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                    i = ….i}
                                                                                                                                 else
                                                                                                                                 if :var_2: = B
                                                                                                                                 then
                                                                                                                                   {a = ….a; b = Some :var_1:; c = ….c;
                                                                                                                                    d = ….d; e = ….e; f = ….f; g = ….g;
                                                                                                                                    h = ….h; i = ….i}
                                                                                                                                 else if :var_2: = C then … else …).e
                                                                                                                                = Some X)
                                                                                                                            && (if :var_2: = A
                                                                                                                                then
                                                                                                                                  {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else
                                                                                                                                if :var_2: = B
                                                                                                                                then
                                                                                                                                  {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else if :var_2: = C then … else …).f
                                                                                                                               = Some X)
                                                                                                                        || ((if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).g
                                                                                                                            = Some X
                                                                                                                            && (if :var_2: = A
                                                                                                                                then
                                                                                                                                  {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else
                                                                                                                                if :var_2: = B
                                                                                                                                then
                                                                                                                                  {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else if :var_2: = C then … else …).h
                                                                                                                               = Some X)
                                                                                                                           && (if :var_2: = A
                                                                                                                               then
                                                                                                                                 {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else
                                                                                                                               if :var_2: = B
                                                                                                                               then
                                                                                                                                 {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else if :var_2: = C then … else …).i
                                                                                                                              = Some X)
                                                                                                                       || (….a = Some X
                                                                                                                           && (if :var_2: = A
                                                                                                                               then
                                                                                                                                 {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else
                                                                                                                               if :var_2: = B
                                                                                                                               then
                                                                                                                                 {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else if :var_2: = C then … else …).d
                                                                                                                              = Some X)
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).g
                                                                                                                             = Some X)
                                                                                                                      || (… = Some X
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).e
                                                                                                                             = Some X)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).h
                                                                                                                            = Some X)
                                                                                                                     || ((if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).c
                                                                                                                         = Some X
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).f
                                                                                                                            = Some X)
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).i
                                                                                                                           = Some X)
                                                                                                                    || (….a = Some X
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).e
                                                                                                                           = Some X)
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).i
                                                                                                                          = Some X)
                                                                                                                   || ((if :var_2: = A
                                                                                                                        then
                                                                                                                          {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else
                                                                                                                        if :var_2: = B
                                                                                                                        then
                                                                                                                          {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else if :var_2: = C then … else …).c
                                                                                                                       = Some X
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).e
                                                                                                                          = Some X)
                                                                                                                      && (if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).g
                                                                                                                         = Some X)
                                                                                                                  =
                                                                                                                  ((((((((….a = Some O && … = Some O)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).c
                                                                                                                            = Some O
                                                                                                                         || ((if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).d
                                                                                                                             = Some O
                                                                                                                             && (if :var_2: = A
                                                                                                                                 then
                                                                                                                                   {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                    e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                    i = ….i}
                                                                                                                                 else
                                                                                                                                 if :var_2: = B
                                                                                                                                 then
                                                                                                                                   {a = ….a; b = Some :var_1:; c = ….c;
                                                                                                                                    d = ….d; e = ….e; f = ….f; g = ….g;
                                                                                                                                    h = ….h; i = ….i}
                                                                                                                                 else if :var_2: = C then … else …).e
                                                                                                                                = Some O)
                                                                                                                            && (if :var_2: = A
                                                                                                                                then
                                                                                                                                  {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else
                                                                                                                                if :var_2: = B
                                                                                                                                then
                                                                                                                                  {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else if :var_2: = C then … else …).f
                                                                                                                               = Some O)
                                                                                                                        || ((if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).g
                                                                                                                            = Some O
                                                                                                                            && (if :var_2: = A
                                                                                                                                then
                                                                                                                                  {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else
                                                                                                                                if :var_2: = B
                                                                                                                                then
                                                                                                                                  {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                   e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                   i = ….i}
                                                                                                                                else if :var_2: = C then … else …).h
                                                                                                                               = Some O)
                                                                                                                           && (if :var_2: = A
                                                                                                                               then
                                                                                                                                 {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else
                                                                                                                               if :var_2: = B
                                                                                                                               then
                                                                                                                                 {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else if :var_2: = C then … else …).i
                                                                                                                              = Some O)
                                                                                                                       || (….a = Some O
                                                                                                                           && (if :var_2: = A
                                                                                                                               then
                                                                                                                                 {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else
                                                                                                                               if :var_2: = B
                                                                                                                               then
                                                                                                                                 {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                  e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                  i = ….i}
                                                                                                                               else if :var_2: = C then … else …).d
                                                                                                                              = Some O)
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).g
                                                                                                                             = Some O)
                                                                                                                      || (… = Some O
                                                                                                                          && (if :var_2: = A
                                                                                                                              then
                                                                                                                                {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else
                                                                                                                              if :var_2: = B
                                                                                                                              then
                                                                                                                                {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                 e = ….e; f = ….f; g = ….g; h = ….h;
                                                                                                                                 i = ….i}
                                                                                                                              else if :var_2: = C then … else …).e
                                                                                                                             = Some O)
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).h
                                                                                                                            = Some O)
                                                                                                                     || ((if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).c
                                                                                                                         = Some O
                                                                                                                         && (if :var_2: = A
                                                                                                                             then
                                                                                                                               {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else
                                                                                                                             if :var_2: = B
                                                                                                                             then
                                                                                                                               {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                                e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                             else if :var_2: = C then … else …).f
                                                                                                                            = Some O)
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).i
                                                                                                                           = Some O)
                                                                                                                    || (….a = Some O
                                                                                                                        && (if :var_2: = A
                                                                                                                            then
                                                                                                                              {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else
                                                                                                                            if :var_2: = B
                                                                                                                            then
                                                                                                                              {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                               e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                            else if :var_2: = C then … else …).e
                                                                                                                           = Some O)
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).i
                                                                                                                          = Some O)
                                                                                                                   || ((if :var_2: = A
                                                                                                                        then
                                                                                                                          {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else
                                                                                                                        if :var_2: = B
                                                                                                                        then
                                                                                                                          {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                           e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                        else if :var_2: = C then … else …).c
                                                                                                                       = Some O
                                                                                                                       && (if :var_2: = A
                                                                                                                           then
                                                                                                                             {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else
                                                                                                                           if :var_2: = B
                                                                                                                           then
                                                                                                                             {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                              e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                           else if :var_2: = C then … else …).e
                                                                                                                          = Some O)
                                                                                                                      && (if :var_2: = A
                                                                                                                          then
                                                                                                                            {a = Some :var_1:; b = …; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else
                                                                                                                          if :var_2: = B
                                                                                                                          then
                                                                                                                            {a = ….a; b = Some :var_1:; c = ….c; d = ….d;
                                                                                                                             e = ….e; f = ….f; g = ….g; h = ….h; i = ….i}
                                                                                                                          else if :var_2: = C then … else …).g
                                                                                                                         = Some O))
                                                                                                        expansions
                                                                                                        []
                                                                                                        rewrite_steps
                                                                                                          forward_chaining
                                                                                                          • unroll
                                                                                                            expr
                                                                                                            (let ((a!1 (ite (= move_150 H_37)
                                                                                                                            (|rec_mk.grid_2716|
                                                                                                                              (a_19 (grid_…
                                                                                                            expansions
                                                                                                            • unroll
                                                                                                              expr
                                                                                                              (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                 (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                              expansions
                                                                                                              • unroll
                                                                                                                expr
                                                                                                                (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                   (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                expansions
                                                                                                                • unroll
                                                                                                                  expr
                                                                                                                  (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                  (|rec_mk.grid_2716|
                                                                                                                                    (a_19 (grid_…
                                                                                                                  expansions
                                                                                                                  • unroll
                                                                                                                    expr
                                                                                                                    (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                       (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                    expansions
                                                                                                                    • unroll
                                                                                                                      expr
                                                                                                                      (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                         (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                      expansions
                                                                                                                      • unroll
                                                                                                                        expr
                                                                                                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                           (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                        expansions
                                                                                                                        • unroll
                                                                                                                          expr
                                                                                                                          (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                          (|rec_mk.grid_2716|
                                                                                                                                            (a_19 (grid_…
                                                                                                                          expansions
                                                                                                                          • unroll
                                                                                                                            expr
                                                                                                                            (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                            (|rec_mk.grid_2716|
                                                                                                                                              (a_19 (grid_…
                                                                                                                            expansions
                                                                                                                            • unroll
                                                                                                                              expr
                                                                                                                              (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                 (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                              expansions
                                                                                                                              • unroll
                                                                                                                                expr
                                                                                                                                (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                                (|rec_mk.grid_2716|
                                                                                                                                                  (a_19 (grid_…
                                                                                                                                expansions
                                                                                                                                • unroll
                                                                                                                                  expr
                                                                                                                                  (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                                  (|rec_mk.grid_2716|
                                                                                                                                                    (a_19 (grid_…
                                                                                                                                  expansions
                                                                                                                                  • unroll
                                                                                                                                    expr
                                                                                                                                    (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                       (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                    expansions
                                                                                                                                    • unroll
                                                                                                                                      expr
                                                                                                                                      (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                         (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                      expansions
                                                                                                                                      • unroll
                                                                                                                                        expr
                                                                                                                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                           (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                        expansions
                                                                                                                                        • unroll
                                                                                                                                          expr
                                                                                                                                          (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                             (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                          expansions
                                                                                                                                          • unroll
                                                                                                                                            expr
                                                                                                                                            (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                               (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                            expansions
                                                                                                                                            • unroll
                                                                                                                                              expr
                                                                                                                                              (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                                              (|rec_mk.grid_2716|
                                                                                                                                                                (a_19 (grid_…
                                                                                                                                              expansions
                                                                                                                                              • unroll
                                                                                                                                                expr
                                                                                                                                                (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                                                (|rec_mk.grid_2716|
                                                                                                                                                                  (a_19 (grid_…
                                                                                                                                                expansions
                                                                                                                                                • unroll
                                                                                                                                                  expr
                                                                                                                                                  (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                                     (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                                  expansions
                                                                                                                                                  • unroll
                                                                                                                                                    expr
                                                                                                                                                    (let ((a!1 (ite (= move_150 H_37)
                                                                                                                                                                    (|rec_mk.grid_2716|
                                                                                                                                                                      (a_19 (grid_…
                                                                                                                                                    expansions
                                                                                                                                                    • unroll
                                                                                                                                                      expr
                                                                                                                                                      (|`List.fold_right anon_fun.move_counts.0[0]`_2731| (tuple_mk_2725 0 0) |[]_2|)
                                                                                                                                                      expansions
                                                                                                                                                      • unroll
                                                                                                                                                        expr
                                                                                                                                                        (let ((a!1 (|::_3| (h_26 (grid_40 game_148))
                                                                                                                                                                           (|::_3| (i_27 (grid_40 game_148)) |[…
                                                                                                                                                        expansions
                                                                                                                                                        • unroll
                                                                                                                                                          expr
                                                                                                                                                          (|`List.fold_right anon_fun.move_counts.0[0]`_2731|
                                                                                                                                                            (tuple_mk_2725 0 0)
                                                                                                                                                            (|::_3| (i_27 (grid_40 g…
                                                                                                                                                          expansions
                                                                                                                                                          • Sat (Some let (game : game_state) = {grid = {a = None; b = None; c = (Some O); d = None; e = (Some X); f = (Some X); g = (Some X); h = None; i = (Some O)}; last_player = (Some X)} let (player : player) = O let (move : move) = I )

                                                                                                                                                          Uh oh! What's gone wrong?

                                                                                                                                                          In this case, the problem is clear - the player is trying to play a move in a square that's already occupied:

                                                                                                                                                          In [24]:
                                                                                                                                                          value(CX.game, CX.move)
                                                                                                                                                          
                                                                                                                                                          Out[24]:
                                                                                                                                                          - : square_state = Some O
                                                                                                                                                          

                                                                                                                                                          If you try out the initial version of the game based on the code so far, you'll see the bug if you try and make a move in a square that's already filled.

                                                                                                                                                          Imandra has spotted the issue for us from a straightforward statement about the logic of the game!

                                                                                                                                                          The culprit is the is_valid_move function - we don't check that the square is empty. Let's add && value(game, move) == None to our check:

                                                                                                                                                          In [25]:
                                                                                                                                                          let is_valid_move = (game, player, move) =>
                                                                                                                                                            ! (is_winning(game, X) || is_winning(game, O) || is_tie(game))
                                                                                                                                                            && is_valid_game(game)
                                                                                                                                                            && (
                                                                                                                                                              game.last_player == None
                                                                                                                                                              && player == initial_player
                                                                                                                                                              || game.last_player == Some(other_player(player))
                                                                                                                                                            )
                                                                                                                                                            && value(game, move) == None
                                                                                                                                                          ;
                                                                                                                                                          
                                                                                                                                                          Out[25]:
                                                                                                                                                          val is_valid_move : game_state -> player -> move -> bool = <fun>
                                                                                                                                                          

                                                                                                                                                          ... and verify once more (using [@blast] to speed it up):

                                                                                                                                                          In [26]:
                                                                                                                                                          [@blast]
                                                                                                                                                          verify((game, player, move) =>
                                                                                                                                                            (is_valid_game(game) && is_valid_move(game, player, move))
                                                                                                                                                            ==> is_valid_game(play_move(game, player, move))
                                                                                                                                                          );
                                                                                                                                                          
                                                                                                                                                          Out[26]:
                                                                                                                                                          - : game_state -> player -> move -> bool = <fun>
                                                                                                                                                          
                                                                                                                                                          proof from "blast" (after 1.13s)!
                                                                                                                                                          Proved

                                                                                                                                                          Much better! You can play the final version here, and you'll see that the bug is fixed. Hopefully this gives you a feel for an interactive development workflow with Imandra, in particular how seeing concrete examples can be really useful to understanding what's going on.