var2 P,Q; assert 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; assert A & x notin P; even(x);
var2 P,Q; assert 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; assert A & x notin P; even(x);