Skip to content

Instantly share code, notes, and snippets.

@agacek

agacek/test.lus

Created January 6, 2016 14:39
Show Gist options
  • Save agacek/af61097b9ddeb2da777c to your computer and use it in GitHub Desktop.
Save agacek/af61097b9ddeb2da777c to your computer and use it in GitHub Desktop.
Download ZIP
Raw
test.lus
node initial(a : bool) returns (holds : bool);
let
holds = a -> true ;
tel ;
node before_always(p : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if p
then 1
else if(not p and a)
then 0
else if(not p and not a)
then 2
else -1
else if(pre_state = 1)
then 1
else if(pre_state = 2)
then
if(not p)
then 2
else if p
then 3
else -1
else if(pre_state = 3)
then 3
else -1;
holds = (state <> 3);
tel;
node before_exists(p : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if p
then 2
else if(not p and not a)
then 0
else if(not p and a)
then 1
else -1
else if(pre_state = 1)
then 1
else if(pre_state = 2)
then 2
else -1;
holds = (state <> 2);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node before_precedes(p : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if p
then 1
else if a
then 1
else if (not p and not a and b)
then 2
else if (not p and not a and not b)
then 0
else -1
else if (pre_state = 1)
then 1
else if (pre_state = 2)
then
if p
then 3
else if (not p)
then 2
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node before_responds(p : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if p
then 2
else if (not p and not b)
then 0
else if (not p and a and b)
then 0
else if (not p and not a and b)
then 1
else -1
else if (pre_state = 1)
then
if p
then 3
else if (not p and not a)
then 1
else if (not p and a)
then 0
else -1
else if (pre_state = 2)
then 2
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node after_exists(p : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and not a)
then 1
else if (p and a)
then 2
else -1
else if (pre_state = 1)
then
if (not a)
then 1
else if a
then 2
else -1
else if (pre_state = 2)
then 2
else -1;
holds = (state = 0) or (state = 2);
tel;
node after_always(p : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and not a)
then 1
else if (p and a)
then 2
else -1
else if (pre_state = 1)
then 1
else if (pre_state = 2)
then
if a then 2
else 1
else -1;
holds = (state = 0) or (state = 2);
tel;
node after_precedes(p : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and not a and not b)
then 1
else if (p and not a and b)
then 3
else if (p and a)
then 2
else -1
else if (pre_state = 1)
then
if a
then 2
else if (not a and not b)
then 1
else if (not a and b)
then 3
else -1
else if (pre_state = 2)
then 2
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node after_responds(p : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and a)
then 1
else if (p and not a and not b)
then 1
else if (p and not a and b)
then 2
else -1
else if (pre_state = 1)
then
if a
then 1
else if (not a and not b)
then 1
else if (not a and b)
then 2
else -1
else if (pre_state = 2)
then
if a
then 1
else if (not a)
then 2
else -1
else -1;
holds = (state = 0) or (state = 1);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node while_always (p : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,1] of int;
pre_state : subrange [-1,1] of int;
let
pre_state = 0 -> pre state;
state =
if(pre_state = 0)
then
if (not p)
then 0
else if (p and a)
then 0
else if (p and not a)
then 1
else -1
else if(pre_state = 1)
then 1
else -1;
holds = (state <> 1);
tel;
node while_exists(p : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and not a)
then 1
else if (p and a)
then 2
else -1
else if (pre_state = 1)
then
if (not p)
then 3
else if (p and not a)
then 1
else if (p and a)
then 2
else -1
else if (pre_state = 2)
then
if (not p)
then 0
else if p
then 2
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node while_precedes(p : bool; a : bool; b : bool) returns (holds : bool);
var
state,pre_state : subrange [-1,2] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if(pre_state = 0)
then
if(not p)
then 0
else if (p and a)
then 0
else if (p and not a and not b)
then 1
else if (p and not a and b)
then 2
else -1
else if (pre_state = 1)
then
if (not p)
then 0
else if a
then 0
else if(p and not a and not b)
then 1
else if(p and not a and b)
then 2
else -1
else if (pre_state = 2)
then 2
else -1;
holds = (state <> 2);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node while_responds(p : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and a)
then 1
else if (p and not a and not b)
then 1
else if (p and not a and b)
then 2
else -1
else if (pre_state = 1)
then
if (not p)
then 0
else if (p and a)
then 1
else if (p and not a and not b)
then 1
else if (p and not a and b)
then 2
else -1
else if (pre_state = 2)
then
if (not p)
then 3
else if (p and a)
then 1
else if (p and not a)
then 2
else -1
else if (pre_state = 3)
then 3
else -1 ;
holds = (state = 0) or (state = 1);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node global_always(a : bool) returns (holds : bool );
let
holds = a and (true -> pre holds);
tel;
node global_responds_within(a : bool; b : bool; n : int) returns (holds : bool);
var
state,pre_state : subrange [-1,2] of int;
latch_n : int;
i,pre_i : int;
let
latch_n = n -> pre latch_n;
pre_i = 0 -> pre i;
i =
if (pre_state = 0)
then
if (b and not a)
then 0
else pre_i
else if (pre_state = 1)
then
if (not a)
then pre_i + 1
else pre_i
else if (pre_state = 2)
then pre_i
else pre_i;
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if(not b)
then 0
else if(b and a)
then 0
else if(b and not a and latch_n > 0)
then 1
else if(b and not a and latch_n = 0)
then 2
else -1
else if (pre_state = 1)
then
if a
then 0
else if (not a and i < latch_n)
then 1
else if (not a and i >= latch_n)
then 2
else -1
else if (pre_state = 2)
then 2
else -1;
holds = (state = 0) or (state = 1);
tel;
node global_exists(a : bool) returns (holds : bool);
var
state : subrange [-1,1] of int;
pre_state : subrange [-1,1] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not a)
then 0
else if a
then 1
else -1
else if (pre_state = 1)
then 1
else -1;
holds = (state = 1);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node global_precedes (a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if a
then 1
else if(not a and not b)
then 0
else if(not a and b)
then 2
else -1
else if(pre_state = 1)
then 1
else if(pre_state = 2)
then 2
else -1;
holds = (state <> 2);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node global_responds(a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,1] of int;
pre_state : subrange [-1,1] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not b)
then 0
else if (a and b)
then 0
else if (not a and b)
then 1
else -1
else if (pre_state = 1)
then
if (not a)
then 1
else if a
then 0
else -1
else -1;
holds = (state = 0);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node between_always (p : bool; q : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if(p and q)
then 0
else if(p and not q and a)
then 1
else if(p and not q and not a)
then 2
else -1
else if (pre_state = 1)
then
if q
then 0
else if(not q and a)
then 1
else if(not q and not a)
then 2
else -1
else if (pre_state = 2)
then
if q
then 3
else if (not q)
then 2
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
tel;
node between_exists(p : bool; q : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if q
then 0
else if a
then 0
else if (p and not q and not a)
then 1
else -1
else if (pre_state = 1)
then
if q
then 2
else if (not q and not a)
then 1
else if (not q and a)
then 0
else -1
else if (pre_state = 2)
then 2
else -1;
holds = (state <> 2);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node between_precedes (p : bool; q : bool; a : bool ; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if(pre_state = 0)
then
if not p
then 0
else if (p and q)
then 0
else if (p and a)
then 0
else if (p and not q and not a and not b)
then 1
else if (p and not q and not a and b)
then 2
else -1
else if(pre_state = 1)
then
if q
then 0
else if a
then 0
else if (not q and not a and not b)
then 1
else if (not q and not a and b)
then 2
else -1
else if(pre_state = 2)
then
if q
then 3
else if (not q)
then 2
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node between_responds (p : bool; q : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and q)
then 0
else if (p and not q and not b)
then 1
else if (p and not q and a and b)
then 1
else if (p and not q and not a and b)
then 2
else -1
else if (pre_state = 1)
then
if q
then 0
else if (not q and not b)
then 1
else if (not q and a and b)
then 1
else if (not q and not a and b)
then 2
else -1
else if (pre_state = 2)
then
if q
then 3
else if (not q and not a)
then 2
else if (not q and a)
then 1
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state <> 3);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node after_until_always(p : bool; q : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if(not p)
then 0
else if(p and q)
then 0
else if(p and not q and a)
then 1
else if(p and not q and not a)
then 2
else -1
else if(pre_state = 1)
then
if q
then 0
else if (not q and a)
then 1
else if (not q and not a)
then 2
else -1
else if(pre_state = 2)
then 2
else -1;
holds = (state <> 2);
tel;
node after_until_exists(p : bool; q : bool; a : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if(p and q)
then 0
else if(p and not a and not q)
then 1
else if(p and a and not q)
then 2
else -1
else if (pre_state = 1)
then
if q
then 3
else if (not q and a)
then 2
else if (not q and not a)
then 1
else -1
else if (pre_state = 2)
then
if q
then 0
else if (p and not q and a)
then 2
else if (p and not q and not a)
then 1
else if (not p and not q)
then 2
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state = 0) or (state = 2);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node after_until_precedes(p : bool; q : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,2] of int;
pre_state : subrange [-1,2] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if (not p)
then 0
else if (p and q)
then 0
else if (p and not q and a)
then 0
else if (p and not q and not a and not b)
then 1
else if (p and not q and not a and b)
then 2
else -1
else if (pre_state = 1)
then
if q
then 0
else if a
then 0
else if (not q and not a and not b)
then 1
else if (not q and not a and b)
then 2
else -1
else if (pre_state = 2)
then 2
else -1;
holds = (state <> 2);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node after_until_responds(p : bool; q : bool; a : bool; b : bool) returns (holds : bool);
var
state : subrange [-1,3] of int;
pre_state : subrange [-1,3] of int;
prop1 : bool;
let
pre_state = 0 -> pre state;
state =
if (pre_state = 0)
then
if(not p)
then 0
else if(p and q)
then 0
else if(p and not q and a)
then 1
else if(p and not q and not a and not b)
then 1
else if(p and not q and not a and b)
then 2
else -1
else if (pre_state = 1)
then
if q
then 0
else if (not q and a)
then 1
else if (not q and not a and not b)
then 1
else if (not q and not a and b)
then 2
else -1
else if (pre_state = 2)
then
if q
then 3
else if (not q and not a)
then 2
else if (not q and a)
then 1
else -1
else if (pre_state = 3)
then 3
else -1;
holds = (state = 0) or (state = 1);
prop1 = (state <> -1);
--%PROPERTY prop1;
tel;
node H(a : bool) returns (holds : bool);
let
holds = a and Z(holds);
tel;
node O(a : bool) returns (holds : bool);
let
holds = a or Y(holds);
tel;
node Y(a : bool) returns (holds : bool);
let
holds = (false -> pre a);
tel;
node Z(a : bool) returns (holds : bool);
let
holds = (true -> pre a);
tel;
node S(a : bool; b : bool) returns (holds : bool);
let
holds = b or (a and Y(holds));
tel;
node T(a : bool; b : bool) returns (holds : bool);
let
holds = b and (a or Z(holds));
tel;
node holds_while(p : bool; c : bool) returns (holds : bool);
let
holds = (Y(p) and c) => p;
tel;
type TicTacToe_board_col = TicTacToe_value[5];
type TicTacToe_value = enum {TicTacToe_value_blank, TicTacToe_value_oneowns, TicTacToe_value_twoowns};
type TicTacToe_move = struct {x : TicTacToe_indices; y : TicTacToe_indices};
type TicTacToe_board = TicTacToe_board_col[5];
type TicTacToe_player = enum {TicTacToe_player_one, TicTacToe_player_two};
type TicTacToe_indices = subrange [0, 4] of int;
const TicTacToe_n = 5;
node TicTacToe(
b : TicTacToe_board;
p : TicTacToe_player;
m : TicTacToe_move;
game_complete : bool
) returns (
_gen_requirements_0 : bool
);
var
initial_board : bool;
initial_turn : bool;
alternate_turns : bool;
mark_blank_squares : bool;
each_turn_a_player_uses_square : bool;
finished : bool;
low_turn_bound : bool;
high_turn_bound : bool;
let
--%MAIN
initial_board = initial((((((((((((((((((((((((((b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_blank) and (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_blank)));
initial_turn = initial((p = TicTacToe_player_two));
alternate_turns = global_always((true -> (if ((pre p) = TicTacToe_player_one) then (p = TicTacToe_player_two) else (p = TicTacToe_player_one))));
mark_blank_squares = global_always((true -> ((pre b)[m.x][m.y] = TicTacToe_value_blank)));
each_turn_a_player_uses_square = global_always((true -> (if (p = TicTacToe_player_one) then ((pre b)[m.x := (pre b)[m.x][m.y := TicTacToe_value_oneowns]] = b) else ((pre b)[m.x := (pre b)[m.x][m.y := TicTacToe_value_twoowns]] = b))));
finished = global_always((if ((((((((((((((((((((((((((b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] <> TicTacToe_value_blank) and (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] <> TicTacToe_value_blank)) and (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] <> TicTacToe_value_blank)) or (((((((TicTacToe_value_blank <> TicTacToe_value_blank) and (((((((((b[0][0] = TicTacToe_value_blank) and (b[1][0] = TicTacToe_value_blank)) and (b[2][0] = TicTacToe_value_blank)) and (b[3][0] = TicTacToe_value_blank)) and (b[4][0] = TicTacToe_value_blank)) or (((((b[0][1] = TicTacToe_value_blank) and (b[1][1] = TicTacToe_value_blank)) and (b[2][1] = TicTacToe_value_blank)) and (b[3][1] = TicTacToe_value_blank)) and (b[4][1] = TicTacToe_value_blank))) or (((((b[0][2] = TicTacToe_value_blank) and (b[1][2] = TicTacToe_value_blank)) and (b[2][2] = TicTacToe_value_blank)) and (b[3][2] = TicTacToe_value_blank)) and (b[4][2] = TicTacToe_value_blank))) or (((((b[0][3] = TicTacToe_value_blank) and (b[1][3] = TicTacToe_value_blank)) and (b[2][3] = TicTacToe_value_blank)) and (b[3][3] = TicTacToe_value_blank)) and (b[4][3] = TicTacToe_value_blank))) or (((((b[0][4] = TicTacToe_value_blank) and (b[1][4] = TicTacToe_value_blank)) and (b[2][4] = TicTacToe_value_blank)) and (b[3][4] = TicTacToe_value_blank)) and (b[4][4] = TicTacToe_value_blank)))) or ((TicTacToe_value_oneowns <> TicTacToe_value_blank) and (((((((((b[0][0] = TicTacToe_value_oneowns) and (b[1][0] = TicTacToe_value_oneowns)) and (b[2][0] = TicTacToe_value_oneowns)) and (b[3][0] = TicTacToe_value_oneowns)) and (b[4][0] = TicTacToe_value_oneowns)) or (((((b[0][1] = TicTacToe_value_oneowns) and (b[1][1] = TicTacToe_value_oneowns)) and (b[2][1] = TicTacToe_value_oneowns)) and (b[3][1] = TicTacToe_value_oneowns)) and (b[4][1] = TicTacToe_value_oneowns))) or (((((b[0][2] = TicTacToe_value_oneowns) and (b[1][2] = TicTacToe_value_oneowns)) and (b[2][2] = TicTacToe_value_oneowns)) and (b[3][2] = TicTacToe_value_oneowns)) and (b[4][2] = TicTacToe_value_oneowns))) or (((((b[0][3] = TicTacToe_value_oneowns) and (b[1][3] = TicTacToe_value_oneowns)) and (b[2][3] = TicTacToe_value_oneowns)) and (b[3][3] = TicTacToe_value_oneowns)) and (b[4][3] = TicTacToe_value_oneowns))) or (((((b[0][4] = TicTacToe_value_oneowns) and (b[1][4] = TicTacToe_value_oneowns)) and (b[2][4] = TicTacToe_value_oneowns)) and (b[3][4] = TicTacToe_value_oneowns)) and (b[4][4] = TicTacToe_value_oneowns))))) or ((TicTacToe_value_twoowns <> TicTacToe_value_blank) and (((((((((b[0][0] = TicTacToe_value_twoowns) and (b[1][0] = TicTacToe_value_twoowns)) and (b[2][0] = TicTacToe_value_twoowns)) and (b[3][0] = TicTacToe_value_twoowns)) and (b[4][0] = TicTacToe_value_twoowns)) or (((((b[0][1] = TicTacToe_value_twoowns) and (b[1][1] = TicTacToe_value_twoowns)) and (b[2][1] = TicTacToe_value_twoowns)) and (b[3][1] = TicTacToe_value_twoowns)) and (b[4][1] = TicTacToe_value_twoowns))) or (((((b[0][2] = TicTacToe_value_twoowns) and (b[1][2] = TicTacToe_value_twoowns)) and (b[2][2] = TicTacToe_value_twoowns)) and (b[3][2] = TicTacToe_value_twoowns)) and (b[4][2] = TicTacToe_value_twoowns))) or (((((b[0][3] = TicTacToe_value_twoowns) and (b[1][3] = TicTacToe_value_twoowns)) and (b[2][3] = TicTacToe_value_twoowns)) and (b[3][3] = TicTacToe_value_twoowns)) and (b[4][3] = TicTacToe_value_twoowns))) or (((((b[0][4] = TicTacToe_value_twoowns) and (b[1][4] = TicTacToe_value_twoowns)) and (b[2][4] = TicTacToe_value_twoowns)) and (b[3][4] = TicTacToe_value_twoowns)) and (b[4][4] = TicTacToe_value_twoowns))))) or ((((TicTacToe_value_blank <> TicTacToe_value_blank) and (((((((((b[0][0] = TicTacToe_value_blank) and (b[0][1] = TicTacToe_value_blank)) and (b[0][2] = TicTacToe_value_blank)) and (b[0][3] = TicTacToe_value_blank)) and (b[0][4] = TicTacToe_value_blank)) or (((((b[1][0] = TicTacToe_value_blank) and (b[1][1] = TicTacToe_value_blank)) and (b[1][2] = TicTacToe_value_blank)) and (b[1][3] = TicTacToe_value_blank)) and (b[1][4] = TicTacToe_value_blank))) or (((((b[2][0] = TicTacToe_value_blank) and (b[2][1] = TicTacToe_value_blank)) and (b[2][2] = TicTacToe_value_blank)) and (b[2][3] = TicTacToe_value_blank)) and (b[2][4] = TicTacToe_value_blank))) or (((((b[3][0] = TicTacToe_value_blank) and (b[3][1] = TicTacToe_value_blank)) and (b[3][2] = TicTacToe_value_blank)) and (b[3][3] = TicTacToe_value_blank)) and (b[3][4] = TicTacToe_value_blank))) or (((((b[4][0] = TicTacToe_value_blank) and (b[4][1] = TicTacToe_value_blank)) and (b[4][2] = TicTacToe_value_blank)) and (b[4][3] = TicTacToe_value_blank)) and (b[4][4] = TicTacToe_value_blank)))) or ((TicTacToe_value_oneowns <> TicTacToe_value_blank) and (((((((((b[0][0] = TicTacToe_value_oneowns) and (b[0][1] = TicTacToe_value_oneowns)) and (b[0][2] = TicTacToe_value_oneowns)) and (b[0][3] = TicTacToe_value_oneowns)) and (b[0][4] = TicTacToe_value_oneowns)) or (((((b[1][0] = TicTacToe_value_oneowns) and (b[1][1] = TicTacToe_value_oneowns)) and (b[1][2] = TicTacToe_value_oneowns)) and (b[1][3] = TicTacToe_value_oneowns)) and (b[1][4] = TicTacToe_value_oneowns))) or (((((b[2][0] = TicTacToe_value_oneowns) and (b[2][1] = TicTacToe_value_oneowns)) and (b[2][2] = TicTacToe_value_oneowns)) and (b[2][3] = TicTacToe_value_oneowns)) and (b[2][4] = TicTacToe_value_oneowns))) or (((((b[3][0] = TicTacToe_value_oneowns) and (b[3][1] = TicTacToe_value_oneowns)) and (b[3][2] = TicTacToe_value_oneowns)) and (b[3][3] = TicTacToe_value_oneowns)) and (b[3][4] = TicTacToe_value_oneowns))) or (((((b[4][0] = TicTacToe_value_oneowns) and (b[4][1] = TicTacToe_value_oneowns)) and (b[4][2] = TicTacToe_value_oneowns)) and (b[4][3] = TicTacToe_value_oneowns)) and (b[4][4] = TicTacToe_value_oneowns))))) or ((TicTacToe_value_twoowns <> TicTacToe_value_blank) and (((((((((b[0][0] = TicTacToe_value_twoowns) and (b[0][1] = TicTacToe_value_twoowns)) and (b[0][2] = TicTacToe_value_twoowns)) and (b[0][3] = TicTacToe_value_twoowns)) and (b[0][4] = TicTacToe_value_twoowns)) or (((((b[1][0] = TicTacToe_value_twoowns) and (b[1][1] = TicTacToe_value_twoowns)) and (b[1][2] = TicTacToe_value_twoowns)) and (b[1][3] = TicTacToe_value_twoowns)) and (b[1][4] = TicTacToe_value_twoowns))) or (((((b[2][0] = TicTacToe_value_twoowns) and (b[2][1] = TicTacToe_value_twoowns)) and (b[2][2] = TicTacToe_value_twoowns)) and (b[2][3] = TicTacToe_value_twoowns)) and (b[2][4] = TicTacToe_value_twoowns))) or (((((b[3][0] = TicTacToe_value_twoowns) and (b[3][1] = TicTacToe_value_twoowns)) and (b[3][2] = TicTacToe_value_twoowns)) and (b[3][3] = TicTacToe_value_twoowns)) and (b[3][4] = TicTacToe_value_twoowns))) or (((((b[4][0] = TicTacToe_value_twoowns) and (b[4][1] = TicTacToe_value_twoowns)) and (b[4][2] = TicTacToe_value_twoowns)) and (b[4][3] = TicTacToe_value_twoowns)) and (b[4][4] = TicTacToe_value_twoowns)))))) or ((((TicTacToe_value_blank <> TicTacToe_value_blank) and ((((((((((((((((((((((((((TicTacToe_move {x = 0; y = 0}.x = TicTacToe_move {x = 0; y = 0}.y) => (b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_blank)) and ((TicTacToe_move {x = 0; y = 1}.x = TicTacToe_move {x = 0; y = 1}.y) => (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 0; y = 2}.x = TicTacToe_move {x = 0; y = 2}.y) => (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 0; y = 3}.x = TicTacToe_move {x = 0; y = 3}.y) => (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 0; y = 4}.x = TicTacToe_move {x = 0; y = 4}.y) => (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 1; y = 0}.x = TicTacToe_move {x = 1; y = 0}.y) => (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 1; y = 1}.x = TicTacToe_move {x = 1; y = 1}.y) => (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 1; y = 2}.x = TicTacToe_move {x = 1; y = 2}.y) => (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 1; y = 3}.x = TicTacToe_move {x = 1; y = 3}.y) => (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 1; y = 4}.x = TicTacToe_move {x = 1; y = 4}.y) => (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 2; y = 0}.x = TicTacToe_move {x = 2; y = 0}.y) => (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 2; y = 1}.x = TicTacToe_move {x = 2; y = 1}.y) => (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 2; y = 2}.x = TicTacToe_move {x = 2; y = 2}.y) => (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 2; y = 3}.x = TicTacToe_move {x = 2; y = 3}.y) => (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 2; y = 4}.x = TicTacToe_move {x = 2; y = 4}.y) => (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 3; y = 0}.x = TicTacToe_move {x = 3; y = 0}.y) => (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 3; y = 1}.x = TicTacToe_move {x = 3; y = 1}.y) => (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 3; y = 2}.x = TicTacToe_move {x = 3; y = 2}.y) => (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 3; y = 3}.x = TicTacToe_move {x = 3; y = 3}.y) => (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 3; y = 4}.x = TicTacToe_move {x = 3; y = 4}.y) => (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 4; y = 0}.x = TicTacToe_move {x = 4; y = 0}.y) => (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 4; y = 1}.x = TicTacToe_move {x = 4; y = 1}.y) => (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 4; y = 2}.x = TicTacToe_move {x = 4; y = 2}.y) => (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 4; y = 3}.x = TicTacToe_move {x = 4; y = 3}.y) => (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_blank))) and ((TicTacToe_move {x = 4; y = 4}.x = TicTacToe_move {x = 4; y = 4}.y) => (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_blank)))) or ((TicTacToe_value_oneowns <> TicTacToe_value_blank) and ((((((((((((((((((((((((((TicTacToe_move {x = 0; y = 0}.x = TicTacToe_move {x = 0; y = 0}.y) => (b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_oneowns)) and ((TicTacToe_move {x = 0; y = 1}.x = TicTacToe_move {x = 0; y = 1}.y) => (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 0; y = 2}.x = TicTacToe_move {x = 0; y = 2}.y) => (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 0; y = 3}.x = TicTacToe_move {x = 0; y = 3}.y) => (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 0; y = 4}.x = TicTacToe_move {x = 0; y = 4}.y) => (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 1; y = 0}.x = TicTacToe_move {x = 1; y = 0}.y) => (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 1; y = 1}.x = TicTacToe_move {x = 1; y = 1}.y) => (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 1; y = 2}.x = TicTacToe_move {x = 1; y = 2}.y) => (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 1; y = 3}.x = TicTacToe_move {x = 1; y = 3}.y) => (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 1; y = 4}.x = TicTacToe_move {x = 1; y = 4}.y) => (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 2; y = 0}.x = TicTacToe_move {x = 2; y = 0}.y) => (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 2; y = 1}.x = TicTacToe_move {x = 2; y = 1}.y) => (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 2; y = 2}.x = TicTacToe_move {x = 2; y = 2}.y) => (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 2; y = 3}.x = TicTacToe_move {x = 2; y = 3}.y) => (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 2; y = 4}.x = TicTacToe_move {x = 2; y = 4}.y) => (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 3; y = 0}.x = TicTacToe_move {x = 3; y = 0}.y) => (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 3; y = 1}.x = TicTacToe_move {x = 3; y = 1}.y) => (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 3; y = 2}.x = TicTacToe_move {x = 3; y = 2}.y) => (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 3; y = 3}.x = TicTacToe_move {x = 3; y = 3}.y) => (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 3; y = 4}.x = TicTacToe_move {x = 3; y = 4}.y) => (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 4; y = 0}.x = TicTacToe_move {x = 4; y = 0}.y) => (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 4; y = 1}.x = TicTacToe_move {x = 4; y = 1}.y) => (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 4; y = 2}.x = TicTacToe_move {x = 4; y = 2}.y) => (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 4; y = 3}.x = TicTacToe_move {x = 4; y = 3}.y) => (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_oneowns))) and ((TicTacToe_move {x = 4; y = 4}.x = TicTacToe_move {x = 4; y = 4}.y) => (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_oneowns))))) or ((TicTacToe_value_twoowns <> TicTacToe_value_blank) and ((((((((((((((((((((((((((TicTacToe_move {x = 0; y = 0}.x = TicTacToe_move {x = 0; y = 0}.y) => (b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_twoowns)) and ((TicTacToe_move {x = 0; y = 1}.x = TicTacToe_move {x = 0; y = 1}.y) => (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 0; y = 2}.x = TicTacToe_move {x = 0; y = 2}.y) => (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 0; y = 3}.x = TicTacToe_move {x = 0; y = 3}.y) => (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 0; y = 4}.x = TicTacToe_move {x = 0; y = 4}.y) => (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 1; y = 0}.x = TicTacToe_move {x = 1; y = 0}.y) => (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 1; y = 1}.x = TicTacToe_move {x = 1; y = 1}.y) => (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 1; y = 2}.x = TicTacToe_move {x = 1; y = 2}.y) => (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 1; y = 3}.x = TicTacToe_move {x = 1; y = 3}.y) => (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 1; y = 4}.x = TicTacToe_move {x = 1; y = 4}.y) => (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 2; y = 0}.x = TicTacToe_move {x = 2; y = 0}.y) => (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 2; y = 1}.x = TicTacToe_move {x = 2; y = 1}.y) => (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 2; y = 2}.x = TicTacToe_move {x = 2; y = 2}.y) => (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 2; y = 3}.x = TicTacToe_move {x = 2; y = 3}.y) => (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 2; y = 4}.x = TicTacToe_move {x = 2; y = 4}.y) => (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 3; y = 0}.x = TicTacToe_move {x = 3; y = 0}.y) => (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 3; y = 1}.x = TicTacToe_move {x = 3; y = 1}.y) => (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 3; y = 2}.x = TicTacToe_move {x = 3; y = 2}.y) => (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 3; y = 3}.x = TicTacToe_move {x = 3; y = 3}.y) => (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 3; y = 4}.x = TicTacToe_move {x = 3; y = 4}.y) => (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 4; y = 0}.x = TicTacToe_move {x = 4; y = 0}.y) => (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 4; y = 1}.x = TicTacToe_move {x = 4; y = 1}.y) => (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 4; y = 2}.x = TicTacToe_move {x = 4; y = 2}.y) => (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 4; y = 3}.x = TicTacToe_move {x = 4; y = 3}.y) => (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_twoowns))) and ((TicTacToe_move {x = 4; y = 4}.x = TicTacToe_move {x = 4; y = 4}.y) => (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_twoowns)))))) or ((((TicTacToe_value_blank <> TicTacToe_value_blank) and (((((((((((((((((((((((((((TicTacToe_move {x = 0; y = 0}.x + TicTacToe_move {x = 0; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_blank)) and (((TicTacToe_move {x = 0; y = 1}.x + TicTacToe_move {x = 0; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 0; y = 2}.x + TicTacToe_move {x = 0; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 0; y = 3}.x + TicTacToe_move {x = 0; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 0; y = 4}.x + TicTacToe_move {x = 0; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 1; y = 0}.x + TicTacToe_move {x = 1; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 1; y = 1}.x + TicTacToe_move {x = 1; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 1; y = 2}.x + TicTacToe_move {x = 1; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 1; y = 3}.x + TicTacToe_move {x = 1; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 1; y = 4}.x + TicTacToe_move {x = 1; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 2; y = 0}.x + TicTacToe_move {x = 2; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 2; y = 1}.x + TicTacToe_move {x = 2; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 2; y = 2}.x + TicTacToe_move {x = 2; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 2; y = 3}.x + TicTacToe_move {x = 2; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 2; y = 4}.x + TicTacToe_move {x = 2; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 3; y = 0}.x + TicTacToe_move {x = 3; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 3; y = 1}.x + TicTacToe_move {x = 3; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 3; y = 2}.x + TicTacToe_move {x = 3; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 3; y = 3}.x + TicTacToe_move {x = 3; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 3; y = 4}.x + TicTacToe_move {x = 3; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 4; y = 0}.x + TicTacToe_move {x = 4; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 4; y = 1}.x + TicTacToe_move {x = 4; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 4; y = 2}.x + TicTacToe_move {x = 4; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 4; y = 3}.x + TicTacToe_move {x = 4; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_blank))) and (((TicTacToe_move {x = 4; y = 4}.x + TicTacToe_move {x = 4; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_blank)))) or ((TicTacToe_value_oneowns <> TicTacToe_value_blank) and (((((((((((((((((((((((((((TicTacToe_move {x = 0; y = 0}.x + TicTacToe_move {x = 0; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_oneowns)) and (((TicTacToe_move {x = 0; y = 1}.x + TicTacToe_move {x = 0; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 0; y = 2}.x + TicTacToe_move {x = 0; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 0; y = 3}.x + TicTacToe_move {x = 0; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 0; y = 4}.x + TicTacToe_move {x = 0; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 1; y = 0}.x + TicTacToe_move {x = 1; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 1; y = 1}.x + TicTacToe_move {x = 1; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 1; y = 2}.x + TicTacToe_move {x = 1; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 1; y = 3}.x + TicTacToe_move {x = 1; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 1; y = 4}.x + TicTacToe_move {x = 1; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 2; y = 0}.x + TicTacToe_move {x = 2; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 2; y = 1}.x + TicTacToe_move {x = 2; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 2; y = 2}.x + TicTacToe_move {x = 2; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 2; y = 3}.x + TicTacToe_move {x = 2; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 2; y = 4}.x + TicTacToe_move {x = 2; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 3; y = 0}.x + TicTacToe_move {x = 3; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 3; y = 1}.x + TicTacToe_move {x = 3; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 3; y = 2}.x + TicTacToe_move {x = 3; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 3; y = 3}.x + TicTacToe_move {x = 3; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 3; y = 4}.x + TicTacToe_move {x = 3; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 4; y = 0}.x + TicTacToe_move {x = 4; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 4; y = 1}.x + TicTacToe_move {x = 4; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 4; y = 2}.x + TicTacToe_move {x = 4; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 4; y = 3}.x + TicTacToe_move {x = 4; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_oneowns))) and (((TicTacToe_move {x = 4; y = 4}.x + TicTacToe_move {x = 4; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_oneowns))))) or ((TicTacToe_value_twoowns <> TicTacToe_value_blank) and (((((((((((((((((((((((((((TicTacToe_move {x = 0; y = 0}.x + TicTacToe_move {x = 0; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 0}.x][TicTacToe_move {x = 0; y = 0}.y] = TicTacToe_value_twoowns)) and (((TicTacToe_move {x = 0; y = 1}.x + TicTacToe_move {x = 0; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 1}.x][TicTacToe_move {x = 0; y = 1}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 0; y = 2}.x + TicTacToe_move {x = 0; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 2}.x][TicTacToe_move {x = 0; y = 2}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 0; y = 3}.x + TicTacToe_move {x = 0; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 3}.x][TicTacToe_move {x = 0; y = 3}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 0; y = 4}.x + TicTacToe_move {x = 0; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 0; y = 4}.x][TicTacToe_move {x = 0; y = 4}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 1; y = 0}.x + TicTacToe_move {x = 1; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 0}.x][TicTacToe_move {x = 1; y = 0}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 1; y = 1}.x + TicTacToe_move {x = 1; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 1}.x][TicTacToe_move {x = 1; y = 1}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 1; y = 2}.x + TicTacToe_move {x = 1; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 2}.x][TicTacToe_move {x = 1; y = 2}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 1; y = 3}.x + TicTacToe_move {x = 1; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 3}.x][TicTacToe_move {x = 1; y = 3}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 1; y = 4}.x + TicTacToe_move {x = 1; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 1; y = 4}.x][TicTacToe_move {x = 1; y = 4}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 2; y = 0}.x + TicTacToe_move {x = 2; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 0}.x][TicTacToe_move {x = 2; y = 0}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 2; y = 1}.x + TicTacToe_move {x = 2; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 1}.x][TicTacToe_move {x = 2; y = 1}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 2; y = 2}.x + TicTacToe_move {x = 2; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 2}.x][TicTacToe_move {x = 2; y = 2}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 2; y = 3}.x + TicTacToe_move {x = 2; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 3}.x][TicTacToe_move {x = 2; y = 3}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 2; y = 4}.x + TicTacToe_move {x = 2; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 2; y = 4}.x][TicTacToe_move {x = 2; y = 4}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 3; y = 0}.x + TicTacToe_move {x = 3; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 0}.x][TicTacToe_move {x = 3; y = 0}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 3; y = 1}.x + TicTacToe_move {x = 3; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 1}.x][TicTacToe_move {x = 3; y = 1}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 3; y = 2}.x + TicTacToe_move {x = 3; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 2}.x][TicTacToe_move {x = 3; y = 2}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 3; y = 3}.x + TicTacToe_move {x = 3; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 3}.x][TicTacToe_move {x = 3; y = 3}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 3; y = 4}.x + TicTacToe_move {x = 3; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 3; y = 4}.x][TicTacToe_move {x = 3; y = 4}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 4; y = 0}.x + TicTacToe_move {x = 4; y = 0}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 0}.x][TicTacToe_move {x = 4; y = 0}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 4; y = 1}.x + TicTacToe_move {x = 4; y = 1}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 1}.x][TicTacToe_move {x = 4; y = 1}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 4; y = 2}.x + TicTacToe_move {x = 4; y = 2}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 2}.x][TicTacToe_move {x = 4; y = 2}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 4; y = 3}.x + TicTacToe_move {x = 4; y = 3}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 3}.x][TicTacToe_move {x = 4; y = 3}.y] = TicTacToe_value_twoowns))) and (((TicTacToe_move {x = 4; y = 4}.x + TicTacToe_move {x = 4; y = 4}.y) = (5 - 1)) => (b[TicTacToe_move {x = 4; y = 4}.x][TicTacToe_move {x = 4; y = 4}.y] = TicTacToe_value_twoowns))))))) then game_complete else (not game_complete)));
low_turn_bound = (_gen_requirements_0 => global_always((game_complete => (((2 * 5) - 1) <= (((((((((if (b[0][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[0][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[0][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[0][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[0][4] <> TicTacToe_value_blank) then 1 else 0)) + (((((if (b[1][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[1][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[1][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[1][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[1][4] <> TicTacToe_value_blank) then 1 else 0))) + (((((if (b[2][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[2][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[2][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[2][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[2][4] <> TicTacToe_value_blank) then 1 else 0))) + (((((if (b[3][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[3][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[3][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[3][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[3][4] <> TicTacToe_value_blank) then 1 else 0))) + (((((if (b[4][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[4][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[4][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[4][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[4][4] <> TicTacToe_value_blank) then 1 else 0)))))));
high_turn_bound = (_gen_requirements_0 => global_always((game_complete => ((((((((((if (b[0][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[0][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[0][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[0][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[0][4] <> TicTacToe_value_blank) then 1 else 0)) + (((((if (b[1][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[1][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[1][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[1][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[1][4] <> TicTacToe_value_blank) then 1 else 0))) + (((((if (b[2][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[2][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[2][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[2][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[2][4] <> TicTacToe_value_blank) then 1 else 0))) + (((((if (b[3][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[3][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[3][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[3][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[3][4] <> TicTacToe_value_blank) then 1 else 0))) + (((((if (b[4][0] <> TicTacToe_value_blank) then 1 else 0) + (if (b[4][1] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[4][2] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[4][3] <> TicTacToe_value_blank) then 1 else 0)) + (if (b[4][4] <> TicTacToe_value_blank) then 1 else 0))) <= (5 * 5)))));
_gen_requirements_0 = H((((((initial_board and initial_turn) and alternate_turns) and mark_blank_squares) and each_turn_a_player_uses_square) and finished));
--%PROPERTY low_turn_bound;
-- %PROPERTY high_turn_bound;
tel;
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment