# 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 plusar5(var2 x1,x2,x3,x4,x5,x6) = ex2 c: plusar4(x1,x2,x3,x4,c) & plus(c,x5,x6); macro shift(var2 p,q) = plus(p,p,q); macro shift2(var2 p,q) = ex2 t: shift(p,t) & shift(t,q); macro shift3(var2 p,q) = ex2 t: shift2(p,t) & shift(t,q); macro time3(var2 p,q) = ex2 t: shift(p,t) & plus(p,t,q); macro time9(var2 p,q) = ex2 t: shift3(p,t) & plus(p,t,q); macro time27(var2 p,q) = ex2 t1,t2,t3: shift(p,t1) & shift2(t1,t2) & shift(t2,t3) & plusar4(p,t1,t2,t3,q); macro weight(var2 w, w1, w2, w3, w4) = leq(w1,pconst(2)) & leq(w2,pconst(2)) & leq(w3,pconst(2)) & ex2 t2,t3,t4,s: time3(w2,t2) & time9(w3,t3) & time27(w4,t4) & plusar4(w1,t2,t3,t4,s) & plus(w,pconst(40),s); ex2 w, w1, w2, w3, w4: weight(w, w1, w2, w3, w4);