% The following script is a simple test for the following conjecture:

% Let S: N -> N be the sum of the digits of a positive integer.
% For all A and B in N, S(A + B) = S(A) + S(B) - 9k, where k is an integer.

sum_digits(X, Y) :- sum_digits_acc(X, 0, Y).

sum_digits_acc(0, Acc, Acc) :- !.
sum_digits_acc(X, Acc, Y) :-
    Q is X div 10,
    R is X mod 10,
    Acc1 is Acc + R,            % Accumulate value
    sum_digits_acc(Q, Acc1, Y). % Propagate Y (result) from recursion back up

test_pair(A, B) :-
    sum_digits(A, X),
    sum_digits(B, Y),
    sum_digits(A + B, Z),
    D   = Z - X - Y,
    0 =:= D mod 9.

conjecture(Max) :-
    forall(between(0, Max, A), forall(between(0, A, B), test_pair(A, B))).

