# 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;
var2 const_beta_4;
var2 const_beta_5;
var2 const_beta_6;

# definition:
pred def_beta() = (len_const_beta = 128) & 
	const_beta_0 = {1, 3, 5, 7, 9, 11, 13, 15, 17, 19, 21, 23, 25, 27, 29, 31, 33, 35, 37, 39, 41, 43, 45, 47, 49, 51, 53, 55, 57, 59, 61, 63, 65, 67, 69, 71, 73, 75, 77, 79, 81, 83, 85, 87, 89, 91, 93, 95, 97, 99, 101, 103, 105, 107, 109, 111, 113, 115, 117, 119, 121, 123, 125, 127} & 
	const_beta_1 = {2, 3, 6, 7, 10, 11, 14, 15, 18, 19, 22, 23, 26, 27, 30, 31, 34, 35, 38, 39, 42, 43, 46, 47, 50, 51, 54, 55, 58, 59, 62, 63, 66, 67, 70, 71, 74, 75, 78, 79, 82, 83, 86, 87, 90, 91, 94, 95, 98, 99, 102, 103, 106, 107, 110, 111, 114, 115, 118, 119, 122, 123, 126, 127} & 
	const_beta_2 = {4, 5, 6, 7, 12, 13, 14, 15, 20, 21, 22, 23, 28, 29, 30, 31, 36, 37, 38, 39, 44, 45, 46, 47, 52, 53, 54, 55, 60, 61, 62, 63, 68, 69, 70, 71, 76, 77, 78, 79, 84, 85, 86, 87, 92, 93, 94, 95, 100, 101, 102, 103, 108, 109, 110, 111, 116, 117, 118, 119, 124, 125, 126, 127} & 
	const_beta_3 = {8, 9, 10, 11, 12, 13, 14, 15, 24, 25, 26, 27, 28, 29, 30, 31, 40, 41, 42, 43, 44, 45, 46, 47, 56, 57, 58, 59, 60, 61, 62, 63, 72, 73, 74, 75, 76, 77, 78, 79, 88, 89, 90, 91, 92, 93, 94, 95, 104, 105, 106, 107, 108, 109, 110, 111, 120, 121, 122, 123, 124, 125, 126, 127} & 
	const_beta_4 = {16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127} & 
	const_beta_5 = {32, 33, 34, 35, 36, 37, 38, 39, 40, 41, 42, 43, 44, 45, 46, 47, 48, 49, 50, 51, 52, 53, 54, 55, 56, 57, 58, 59, 60, 61, 62, 63, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127} & 
	const_beta_6 = {64, 65, 66, 67, 68, 69, 70, 71, 72, 73, 74, 75, 76, 77, 78, 79, 80, 81, 82, 83, 84, 85, 86, 87, 88, 89, 90, 91, 92, 93, 94, 95, 96, 97, 98, 99, 100, 101, 102, 103, 104, 105, 106, 107, 108, 109, 110, 111, 112, 113, 114, 115, 116, 117, 118, 119, 120, 121, 122, 123, 124, 125, 126, 127};

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 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0) = (x0 <=> y0) & (x1 <=> y1) & (x2 <=> y2) & (x3 <=> y3) & (x4 <=> y4) & (x5 <=> y5) & (x6 <=> y6);

pred Ple(var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0) = (~x6 & y6) | (x6 <=> y6) & ((~x5 & y5) | (x5 <=> y5) & ((~x4 & y4) | (x4 <=> y4) & ((~x3 & y3) | (x3 <=> y3) & ((~x2 & y2) | (x2 <=> y2) & ((~x1 & y1) | (x1 <=> y1) & ((~x0 & y0) | (x0 <=> y0)))))));

pred Plt(var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0) = (~x6 & y6) | (x6 <=> y6) & ((~x5 & y5) | (x5 <=> y5) & ((~x4 & y4) | (x4 <=> y4) & ((~x3 & y3) | (x3 <=> y3) & ((~x2 & y2) | (x2 <=> y2) & ((~x1 & y1) | (x1 <=> y1) & ((~x0 & y0)))))));

pred Peqplus(var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0, var0 z6, var0 z5, var0 z4, var0 z3, var0 z2, var0 z1, var0 z0) = ex2 c: (~(0 in c) & ~(7 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)) &
((5 in c) <=> Pgt2(4 in c, y4, z4)) &
((6 in c) <=> Pgt2(5 in c, y5, z5)) &
((7 in c) <=> Pgt2(6 in c, y6, z6)) &
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) &
Pxoreq(x4, y4, z4, 4 in c) &
Pxoreq(x5, y5, z5, 5 in c) &
Pxoreq(x6, y6, z6, 6 in c)
);

# global variable declaration:
var2 x;
var2 a_6;
var2 a_5;
var2 a_4;
var2 a_3;
var2 a_2;
var2 a_1;
var2 a_0;
var1 len_a;

def_beta => 
(Peq(((6) in x), ((5) in x), ((4) in x), ((3) in x), ((2) in x), ((1) in x), ((0) in x), false, false, false, false, false, true, true)) & 
(ex1 i_1: (((Peq(((i_1) in a_6), ((i_1) in a_5), ((i_1) in a_4), ((i_1) in a_3), ((i_1) in a_2), ((i_1) in a_1), ((i_1) in a_0), false, false, false, false, false, false, true)) & ((i_1) < (len_a))) & ((Peq(((i_1) in const_beta_6), ((i_1) in const_beta_5), ((i_1) in const_beta_4), ((i_1) in const_beta_3), ((i_1) in const_beta_2), ((i_1) in const_beta_1), ((i_1) in const_beta_0), ((6) in x), ((5) in x), ((4) in x), ((3) in x), ((2) in x), ((1) in x), ((0) in x))) & ((i_1) < (len_const_beta)))));