# 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;
var2 const_beta_2;
var2 const_beta_3;

# definition:
pred def_beta() = (len_const_beta = 16) & 
	const_beta_0 = {1, 3, 5, 7, 9, 11, 13, 15} & 
	const_beta_1 = {2, 3, 6, 7, 10, 11, 14, 15} & 
	const_beta_2 = {4, 5, 6, 7, 12, 13, 14, 15} & 
	const_beta_3 = {8, 9, 10, 11, 12, 13, 14, 15};

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 x3, var0 x2, var0 x1, var0 x0, var0 y3, var0 y2, var0 y1, var0 y0) = (x0 <=> y0) & (x1 <=> y1) & (x2 <=> y2) & (x3 <=> y3);

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

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

pred Peqplus(var0 x3, var0 x2, var0 x1, var0 x0, var0 y3, var0 y2, var0 y1, var0 y0, var0 z3, var0 z2, var0 z1, var0 z0) = ex2 c: (~(0 in c) & ~(4 in c) & 
((1 in c) <=> Pgt2(0 in c, y0, z0)) &
((2 in c) <=> Pgt2(1 in c, y1, z1)) &
((3 in c) <=> Pgt2(2 in c, y2, z2)) &
((4 in c) <=> Pgt2(3 in c, y3, z3)) &
Pxoreq(x0, y0, z0, 0 in c) &
Pxoreq(x1, y1, z1, 1 in c) &
Pxoreq(x2, y2, z2, 2 in c) &
Pxoreq(x3, y3, z3, 3 in c)
);

# global variable declaration:
var1 i;
var2 a_3;
var2 a_2;
var2 a_1;
var2 a_0;
var1 len_a;

def_beta => 
((i) = (1)) & 
((Peq(((i) in a_3), ((i) in a_2), ((i) in a_1), ((i) in a_0), false, false, false, true)) & ((i) < (len_a))) & 
(ex2 e_4: (ex2 e_5: (ex2 e_6: (ex1 i_2: (((Peq(((i_2) in a_3), ((i_2) in a_2), ((i_2) in a_1), ((i_2) in a_0), false, false, true, false)) & ((i_2) < (len_a))) & ((Peq(((3) in e_4), ((2) in e_4), ((1) in e_4), ((0) in e_4), ((i) in const_beta_3), ((i) in const_beta_2), ((i) in const_beta_1), ((i) in const_beta_0))) & ((i) < (len_const_beta))) & ((Peq(((3) in e_5), ((2) in e_5), ((1) in e_5), ((0) in e_5), ((i) in const_beta_3), ((i) in const_beta_2), ((i) in const_beta_1), ((i) in const_beta_0))) & ((i) < (len_const_beta))) & (Peqplus(((3) in e_6), ((2) in e_6), ((1) in e_6), ((0) in e_6), ((3) in e_4), ((2) in e_4), ((1) in e_4), ((0) in e_4), ((3) in e_5), ((2) in e_5), ((1) in e_5), ((0) in e_5))) & ((Peq(((i_2) in const_beta_3), ((i_2) in const_beta_2), ((i_2) in const_beta_1), ((i_2) in const_beta_0), ((3) in e_6), ((2) in e_6), ((1) in e_6), ((0) in e_6))) & ((i_2) < (len_const_beta))))))));