%% ask eval(3*a+2*b+c, Val ,[val(a,4),val(b,5),val(c,7)]).
%% ask update(b,9,[val(a,4),val(b,5),val(c,7)],E2).

addato(X,Y) <= Y is X+a.
foo(X,Y) <= X is a+3 & assign(a,X) & Y is a+3.

%% ask arprove(addato(3,Y),[val(a,4),val(b,5),val(c,7)],E2).
%% ask arprove(foo(X,Y),[val(a,4),val(b,5),val(c,7)],E2).

sumsq(X,Y)=X*X+Y*Y <= true.
fact(N)=N*fact(N1) <= N>0 & N1 is N-1.
fact(0)=1 <= true.

%% ask arprove(X is sumsq(3,4)-fact(4),[],E2).