# 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 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: var2 a_3; var2 a_2; var2 a_1; var2 a_0; var1 len_a; ((Peq(((0) in a_3), ((0) in a_2), ((0) in a_1), ((0) in a_0), false, false, false, false)) & ((0) < (len_a))) & (all1 i: (((i) < (10)) => ((Peqplus(((i + 1) in a_3), ((i + 1) in a_2), ((i + 1) in a_1), ((i + 1) in a_0), ((i) in a_3), ((i) in a_2), ((i) in a_1), ((i) in a_0), false, false, false, true)) & ((i + 1) < (len_a)) & ((i) < (len_a)))));