:- op(800,xfx,=>).
:- op(800,xfx,==>).
:- op(800,xfx,==>*).

A+(B+C) => (A+B)+C.

A ==> B :-
    A => B.
A+C ==> B+C :-
    A ==> B.
A+B ==> A+C :-
    B ==> C.

A ==>* C :-
    A ==> B,
    B ==>* C.
A ==>* A.

% ?- a+(b+c+a)+(c+d)+(a+(b+c)) ==>* X.
