pred leq (var2 X, Y) = (all1 x: (x in X \ Y) => ex1 y: (y > x & y in Y \ X));

pred xor(var0 x,y) = x&~y | ~x&y;
pred at_least_two(var0 x,y,z) = x&y | x&z | y&z;

#1b
pred add(var2 X,Y,Z) =
 ex2 C:                                                  # carry track
   0 notin C                                             # no carry-in
 & all1 t:
     (t+1 in C <=> at_least_two(t in X, t in Y, t in C)) # propagate carry
   & (t in Z <=> xor(xor(t in X, t in Y), t in C));      # calculate result

#1a
# pred leq(var2 X,Y) = ex2 Z: add(X,Z,Y);

#1c
# pconst == constant 3 as set.

pred frm(var2 Y) =
  ex2 X: add(X,X,Y) & leq(X,pconst(3)) & leq(pconst(3),Y);

# export some automata
var2 X,Y,Z;
add(X,Y,Z);
# frm(Y);