var2 P,Q; P\Q = {0,4} union {1,2}; pred even(var1 p) = ex2 Q: p in Q & (all1 q: (0 < q & q <= p) => (q in Q => q - 1 notin Q) & (q notin Q => q - 1 in Q)) & 0 in Q; var1 x; var0 A; A & even(x) & x notin P;
var2 P,Q; P\Q = {0,4} union {1,2}; pred even(var1 p) = ex2 Q: p in Q & (all1 q: (0 < q & q <= p) => (q in Q => q - 1 notin Q) & (q notin Q => q - 1 in Q)) & 0 in Q; var1 x; var0 A; A & even(x) & x notin P;