Some implicit constraint

问题:

When i execute this code(shown below) , it always sets implicit kind of constraint.

As you can see below , it always says that D1 = D2 but there is no such explicit constraints nor any pattern matching which forces this.

Or in otherwords there is some reference between D1 and D2 such that whenever D1 gets initialized, D2 gets automatically initialized. I can't see how this is happening. Can someone explain me, i tried ot figure it out with debugger but it did not help.

It's a puzzle "GERALD + DONALD = ROBERT", initially three lists contains these variables.

I add code below if anyone wants to test it:

sum(N1,N2,N):-
    sum1(N1,N2,N,0,0,[0,1,2,3,4,5,6,7,8,9],_).

sum1([],[],[],0,0,Digits,Digits).    
sum1([D1|N1],[D2|N2],[D|N],C1,C,Digs1,Digs2):-
    sum1(N1,N2,N,C1,C2,Digs1,Digs2),
    digitSum(D1,D2,C2,D,C,Digs2,Digs).

digitSum(D1,D2,C1,D,C,Digs1,Digs):-
    del(D1,Digs1,Digs2),
    del(D2,Digs2,Digs3),
    del(D,Digs3,Digs),
    S is D1 + D2 + C1,
    D is S mod 10,
    C is D div 10.

del(A,L,L):-
    nonvar(A),!.
del(A,[A|L],L).
del(A,[B|L],[B|L1]):-
    del(A,L,L1).

Query:

?- sum( [D,O,N,A,L,D], [G,E,R,A,L,D], [R,O,B,E,R,T] ).

回答1:

When it says D1 = D2 then you should see that both D1 and D2 have same variable from the list and List is a functor and one variable is visible in whole functor.

You should see that when the recursion ends, then you have have D's(last element) from GERALD and DONALD , since this D is visible in whole functor, D1 and D2 both refer to same variable.