```    1:- module(arith_partial_eval,[]).    2
3% ?- arith_partial_eval(0, X).
4%@ X = 0.
5% ?- arith_partial_eval(0+A+0, X).%@ A = X.
6%@ A = X.
7% ?- arith_partial_eval(1+(A+B)*0, X).
8%@ X = 1.
9% ?- arith_partial_eval(0+ (X<<((2*A*1 + 4*B*1)*0))*(1+2), R).
10%@ R = X+X*2.
11%@ R = X+X*2.
12% ?- arith_partial_eval(0+ X<<(((((2*A*1 + 4*B*1)*0)))*(1+2)), R).
13%@ X = R.
14% ?- arith_partial_eval(X+Y+Z -(Y + Z), R).
15%@ X = R.
16% ?- arith_partial_eval(X - Y + Z -(Y + Z), R).
17%@ R = X+ -Y+ -Y.
18% ?- arith_partial_eval(X << (Y - Y + Z - Z), R).
19%@ X = R.
20% ?- arith_partial_eval(X ^ (1-1), R).
21
22% ?- arith_partial_eval(0 ^ (1-1), R).
23% ?- arith_partial_eval(X + X + X, R).
24%@ R = X+X+X.
25% ?- arith_partial_eval(X + X + Y + X , R).
26
27
28% ?- listing(arith_rule).
29
30elim_term(A, B, 0)	:- A==B.
31elim_term(A, B, X)	:- nonvar(B, X+Y), A==Y.
32elim_term(A, B, Z+Y):- nonvar(B, X+Y), elim_term(A, X, Z).
33%
34nonvar(X, Y):- nonvar(X), Y=X.
35%
36ground_compound_basic_exp(E):- compound(E),
37	arg(1, E, A),
38	integer(A),
39	(	arg(2, E, B) -> integer(B)
40	;	true
41	).
42%
43arith_partial_eval(X, Y):- arith_rule(X, X0), !,
44	arith_partial_eval(X0, Y).
45arith_partial_eval(X, X).
46%
47arith_rule(A, _)			:- var(A), !, fail.
48arith_rule(A - B, A + -(B)).
49arith_rule(E*C, A*C+B*C)	:- nonvar(E, A+B).
50arith_rule(C*E, C*A+C*B)	:- nonvar(E, A+B).
51arith_rule(A+E, (A+B)+C)	:- nonvar(E, B+C).
52arith_rule(A*E, (A*B)*C)	:- nonvar(E, B*C).
53arith_rule(A+B, A0+B)		:- arith_rule(A, A0).
54arith_rule(A+B, A+B0)		:- arith_rule(B, B0).
55arith_rule(+(A), +(A0))		:- arith_rule(A, A0).
56arith_rule(-E, -A + -B)		:- nonvar(E, A+B).
57arith_rule(-E, A)			:- nonvar(E, -A).
58arith_rule(-(A), -(A0))		:- arith_rule(A, A0).
59arith_rule(E, V)			:- ground_compound_basic_exp(E), V is E.
60arith_rule(A*B, A0*B)		:- arith_rule(A, A0).
61arith_rule(A*B, A*B0)		:- arith_rule(B, B0).
62arith_rule(A//B, A0//B)		:- arith_rule(A, A0).
63arith_rule(A//B, A//B0)		:- arith_rule(B, B0).
64arith_rule(A<<B, A0<<B)		:- arith_rule(A, A0).
65arith_rule(A<<B, A<<B0)		:- arith_rule(B, B0).
66arith_rule(A>>B, A0>>B)		:- arith_rule(A, A0).
67arith_rule(A>>B, A>>B0)		:- arith_rule(B, B0).
68arith_rule(A^B, A0^B)		:- arith_rule(A, A0).
69arith_rule(A^B, A^B0)		:- arith_rule(B, B0).
70arith_rule(A mod B, A0 mod B)	 :- arith_rule(A, A0).
71arith_rule(A mod B, A mod B0)	 :- arith_rule(B, B0).
72arith_rule(E*_, 0)		:- E == 0.
73arith_rule(_*E, 0)		:- E == 0.
74arith_rule(E+X, X)		:- E == 0.
75arith_rule(X+E, X)		:- E == 0.
76arith_rule(X>>E, X)		:- E == 0.
77arith_rule(X<<E, X)		:- E == 0.
78arith_rule(E//_, 0)		:- E == 0.
79arith_rule(E*X, X)		:- E == 1.
80arith_rule(X*E, X)		:- E == 1.
81arith_rule(_^E, 1)		:- E == 0.
82arith_rule(A^E, A)		:- E == 1.
83arith_rule(E^_, 1)		:- E == 1.
84arith_rule(A+B, B+A)	:- integer(A).
85arith_rule(A*B, B*A)	:- integer(A).
86arith_rule(A+B, B+A)	:- nonvar(A, A0*H), nonvar(B, B0*K),
87	integer(H), integer(K),
88	A0 @< B0.
89arith_rule(A+B, A0*D)	:- nonvar(A, A0*H), nonvar(B, B0*K),
90					A0 == B0,
91					D is H+K.
92arith_rule(A+B, B+A)	:- arith_mono_compare(<, A, B).
93arith_rule(A+B, (U+B)+V)	:- nonvar(A, U+V),
94	arith_mono_compare(<, V, B).
95
96%
97arith_mono_compare(=, A, B):-integer(A), integer(B).
98arith_mono_compare(<, A, _):-integer(A).
99arith_mono_compare(>, _, B):-integer(B).
100arith_mono_compare(C, A, B):- nonvar(A, A0*I), nonvar(B, B0*K),
101	integer(I),
102	integer(K),
103	compare(C, B0, A0).
104arith_mono_compare(C, A, B):- nonvar(A, A0*I),
105	integer(I),
106	B0 = B,
107	compare(C, B0, A0).
108arith_mono_compare(C, A, B):- nonvar(B, B0*I),
109	integer(I),
110	A0 = A,
111	compare(C, B0, A0).
112arith_mono_compare(C, A, B):- compare(C, A, B)```