# Automatically generated code
# Translator Version: v0.1
# Data: XXXX

# Definition of the constant array variable: 'beta'
# declaration:
var1 len_const_beta;
var2 const_beta_0;
var2 const_beta_1;

# definition:
pred def_beta() = (len_const_beta = 4) & 
	const_beta_0 = {1, 3} & 
	const_beta_1 = {2, 3};

pred Pxoreq(var0 r, var0 x, var0 y, var0 z) = (r <=> ~(~(x <=> y) <=> z));

pred Pgt2(var0 x, var0 y, var0 z) = (x & y) | (y & z) | (z & x);

pred Peq(var0 x1, var0 x0, var0 y1, var0 y0) = (x0 <=> y0) & (x1 <=> y1);

pred Ple(var0 x1, var0 x0, var0 y1, var0 y0) = (~x1 & y1) | (x1 <=> y1) & ((~x0 & y0) | (x0 <=> y0));

pred Plt(var0 x1, var0 x0, var0 y1, var0 y0) = (~x1 & y1) | (x1 <=> y1) & ((~x0 & y0));

pred Peqplus(var0 x1, var0 x0, var0 y1, var0 y0, var0 z1, var0 z0) = ex2 c: (~(0 in c) & ~(2 in c) & 
((1 in c) <=> Pgt2(0 in c, y0, z0)) &
((2 in c) <=> Pgt2(1 in c, y1, z1)) &
Pxoreq(x0, y0, z0, 0 in c) &
Pxoreq(x1, y1, z1, 1 in c)
);

# global variable declaration:
var2 a_1;
var2 a_0;
var1 len_a;

def_beta => 
((4) <= (len_a)) & 
((all1 i: (((i) < (4)) => (ex2 e_0: (((Plt(((i) in a_1), ((i) in a_0), ((1) in e_0), ((0) in e_0))) & ((i) < (len_a))) & ((Peq(((1) in e_0), ((0) in e_0), ((i) in const_beta_1), ((i) in const_beta_0))) & ((i) < (len_const_beta))))))) => (all1 i: (((i) < (4)) => (ex1 i_0: (ex2 e_1: (((Plt(((i_0) in a_1), ((i_0) in a_0), ((1) in e_1), ((0) in e_1))) & ((i_0) < (len_a))) & ((Peq(((i_0) in const_beta_1), ((i_0) in const_beta_0), ((i) in a_1), ((i) in a_0))) & ((i_0) < (len_const_beta)) & ((i) < (len_a))) & ((Peq(((1) in e_1), ((0) in e_1), ((i) in const_beta_1), ((i) in const_beta_0))) & ((i) < (len_const_beta)))))))));