einf(X+Y*X,U):-einf((1+Y)*X,U).
einf(Y*X+X,U):-einf((1+Y)*X,U).
einf(X+X,U):-einf(2*X,U).
einf(Y*X+Z*X,U):-einf((Y+Z)*X,U).
einf(X+Y,Z):-einf(X,U),einf(Y,V),integer(U),integer(V),Z is U+V.
einf(X*Y,Z):-einf(X,U),einf(Y,V),integer(U),integer(V),Z is U*V.
einf(X+Y,U+V):-einf(X,U),einf(Y,V).
einf(X*Y,U*V):-einf(X,U),einf(Y,V).
einf(0*_,0).
einf(1*X,X):-!.
einf(0+X,X):-!.
einf(X,X):-!.