theory C = A + B:;

end;