# Automatically generated code # Translator Version: v0.1 # Data: XXXX 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 x7, var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y7, 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) & (x7 <=> y7); pred Ple(var0 x7, var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y7, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0) = (~x7 & y7) | (x7 <=> y7) & ((~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 x7, var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y7, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0) = (~x7 & y7) | (x7 <=> y7) & ((~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 x7, var0 x6, var0 x5, var0 x4, var0 x3, var0 x2, var0 x1, var0 x0, var0 y7, var0 y6, var0 y5, var0 y4, var0 y3, var0 y2, var0 y1, var0 y0, var0 z7, var0 z6, var0 z5, var0 z4, var0 z3, var0 z2, var0 z1, var0 z0) = ex2 c: (~(0 in c) & ~(8 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)) & ((8 in c) <=> Pgt2(7 in c, y7, z7)) & 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) & Pxoreq(x7, y7, z7, 7 in c) ); # global variable declaration: var2 a_7; var2 a_6; var2 a_5; var2 a_4; var2 a_3; var2 a_2; var2 a_1; var2 a_0; var1 len_a; var2 c_7; var2 c_6; var2 c_5; var2 c_4; var2 c_3; var2 c_2; var2 c_1; var2 c_0; var1 len_c; ((Peq(((0) in a_7), ((0) in a_6), ((0) in a_5), ((0) in a_4), ((0) in a_3), ((0) in a_2), ((0) in a_1), ((0) in a_0), false, false, false, false, false, false, false, true)) & ((0) < (len_a))) & ((Peq(((1) in a_7), ((1) in a_6), ((1) in a_5), ((1) in a_4), ((1) in a_3), ((1) in a_2), ((1) in a_1), ((1) in a_0), false, false, false, false, false, false, false, false)) & ((1) < (len_a))) & ((Peq(((2) in a_7), ((2) in a_6), ((2) in a_5), ((2) in a_4), ((2) in a_3), ((2) in a_2), ((2) in a_1), ((2) in a_0), false, false, false, false, false, false, false, true)) & ((2) < (len_a))) & ((Peq(((3) in a_7), ((3) in a_6), ((3) in a_5), ((3) in a_4), ((3) in a_3), ((3) in a_2), ((3) in a_1), ((3) in a_0), false, false, false, false, false, false, false, true)) & ((3) < (len_a))) & ((Peq(((4) in a_7), ((4) in a_6), ((4) in a_5), ((4) in a_4), ((4) in a_3), ((4) in a_2), ((4) in a_1), ((4) in a_0), false, false, false, false, false, false, false, false)) & ((4) < (len_a))) & ((Peq(((5) in a_7), ((5) in a_6), ((5) in a_5), ((5) in a_4), ((5) in a_3), ((5) in a_2), ((5) in a_1), ((5) in a_0), false, false, false, false, false, false, false, true)) & ((5) < (len_a))) & ((Peq(((6) in a_7), ((6) in a_6), ((6) in a_5), ((6) in a_4), ((6) in a_3), ((6) in a_2), ((6) in a_1), ((6) in a_0), false, false, false, false, false, false, false, false)) & ((6) < (len_a))) & ((Peq(((7) in a_7), ((7) in a_6), ((7) in a_5), ((7) in a_4), ((7) in a_3), ((7) in a_2), ((7) in a_1), ((7) in a_0), false, false, false, false, false, false, false, true)) & ((7) < (len_a))) & ((Peq(((0) in c_7), ((0) in c_6), ((0) in c_5), ((0) in c_4), ((0) in c_3), ((0) in c_2), ((0) in c_1), ((0) in c_0), false, false, false, false, false, false, false, false)) & ((0) < (len_c))) & ((len_a) = (8)) & ((len_c) = (9)) & (all1 i: (((i) < (8)) => ((((Peq(((i) in a_7), ((i) in a_6), ((i) in a_5), ((i) in a_4), ((i) in a_3), ((i) in a_2), ((i) in a_1), ((i) in a_0), false, false, false, false, false, false, false, true)) & ((i) < (len_a))) & ((Peqplus(((i + 1) in c_7), ((i + 1) in c_6), ((i + 1) in c_5), ((i + 1) in c_4), ((i + 1) in c_3), ((i + 1) in c_2), ((i + 1) in c_1), ((i + 1) in c_0), ((i) in c_7), ((i) in c_6), ((i) in c_5), ((i) in c_4), ((i) in c_3), ((i) in c_2), ((i) in c_1), ((i) in c_0), false, false, false, false, false, false, false, true)) & ((i + 1) < (len_c)) & ((i) < (len_c)))) | (((Peq(((i) in a_7), ((i) in a_6), ((i) in a_5), ((i) in a_4), ((i) in a_3), ((i) in a_2), ((i) in a_1), ((i) in a_0), false, false, false, false, false, false, false, false)) & ((i) < (len_a))) & ((Peq(((i + 1) in c_7), ((i + 1) in c_6), ((i + 1) in c_5), ((i + 1) in c_4), ((i + 1) in c_3), ((i + 1) in c_2), ((i + 1) in c_1), ((i + 1) in c_0), ((i) in c_7), ((i) in c_6), ((i) in c_5), ((i) in c_4), ((i) in c_3), ((i) in c_2), ((i) in c_1), ((i) in c_0))) & ((i + 1) < (len_c)) & ((i) < (len_c)))))));