# auxiliary predicates pred xor(var0 x,y) = x&~y | ~x&y; pred at_least_two(var0 x,y,z) = x&y | x&z | y&z; # addition relation (p "+" q = r) pred plus(var2 p,q,r) = ex2 c: # carry track 0 notin c # no carry-in & all1 t: (t+1 in c <=> at_least_two(t in p, t in q, t in c)) # propagate carry & (t in r <=> xor(xor(t in p, t in q), t in c)); # calculate result # less-than relation (p "<" q) pred less(var2 p,q) = ex2 t: t ~= empty & plus(p,t,q); pred leq(var2 p,q) = ex2 t: plus(p,t,q); pred plusar3(var2 x1,x2,x3,x4) = ex2 c: plus(x1,x2,c) & plus(c,x3,x4); pred plusar4(var2 x1,x2,x3,x4,x5) = ex2 c: plusar3(x1,x2,x3,c) & plus(c,x4,x5); pred shiftback(var2 x,y) = all1 i: i in y <=> (i + 2) in x; pred closed(var2 s) = all1 x: (x + 4) in s => x in s; pred divisibleBy4(var1 i) = all2 s: (i in s & closed(s)) => 0 in s; pred createNumber(var0 b0,b1,b2,b3, var2 n) = (b0 <=> 0 in n) & (b1 <=> 1 in n) & (b2 <=> 2 in n) & (b3 <=> 3 in n) & all1 i: i > 3 => i notin n; pred smoothing(var2 a,b) = 0 notin b & 1 notin b & 2 notin b & 3 notin b & all1 i: divisibleBy4(i) => ( ex2 x,y,z,t,tDiv4: ex0 x0,x1,x2,x3,y0,y1,y2,y3,z0,z1,z2,z3,t0,t1,t2,t3: (x0 <=> i in a) & (x1 <=> (i+1) in a) & (x2 <=> (i+2) in a) & (x3 <=> (i+3) in a) & (y0 <=> (i+4) in a) & (y1 <=> (i+5) in a) & (y2 <=> (i+6) in a) & (y3 <=> (i+7) in a) & (z0 <=> (i+8) in a) & (z1 <=> (i+9) in a) & (z2 <=> (i+10) in a) & (z3 <=> (i+11) in a) & createNumber(x0,x1,x2,x3,x) & createNumber(y0,y1,y2,y3,y) & createNumber(z0,z1,z2,z3,z) & plusar4(x,y,y,z,t) & shiftback(t,tDiv4) & createNumber(t0,t1,t2,t3,tDiv4) & (t0 <=> (i+4) in b) & (t1 <=> (i+5) in b) & (t2 <=> (i+6) in b) & (t3 <=> (i+7) in b) ); ex2 a,b: smoothing(a,b);