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