enrich
int-basic1
with
functions
. + . : int × int → int;
variables
i : int;
j : int;
axioms
add-zero: i + 0 = i;
add-succ: i + j +1 = (i + j)+1;
add-pred: i + j -1 = (i + j)-1;
end enrich