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