(VAR X X1 X2 X3)
(RULES 
a__f(a,X,X) -> a__f(X,a__b,b)
a__b -> a
mark(f(X1,X2,X3)) -> a__f(X1,mark(X2),X3)
mark(b) -> a__b
mark(a) -> a
a__f(X1,X2,X3) -> f(X1,X2,X3)
a__b -> b
)

Proving termination of rewriting for Ex9_Luc06_GM:

-> Dependency pairs:
nF_a__f(a,X,X) -> nF_a__f(X,a__b,b)
nF_a__f(a,X,X) -> nF_a__b
nF_mark(f(X1,X2,X3)) -> nF_a__f(X1,mark(X2),X3)
nF_mark(f(X1,X2,X3)) -> nF_mark(X2)
nF_mark(b) -> nF_a__b

-> Proof of termination for Ex9_Luc06_GM_1_1:
-> -> Dependency pairs in cycle:
nF_mark(f(X1,X2,X3)) -> nF_mark(X2)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex9_Luc06_GM_1_2:
-> -> Dependency pairs in cycle:
nF_a__f(a,X,X) -> nF_a__f(X,a__b,b)

Usable Rules:
a__b -> a
a__b -> b

Polynomial Interpretation:

[f](X1,X2,X3) = 0
[a] = 1
[b] = 0
[a__f](X1,X2,X3) = 0
[a__b] = 1
[mark](X) = 0
[nF_a__f](X1,X2,X3) = X1 + X3

TIME: 1.5999e-2


SETTINGS:
Base ordering: Polynomial ordering
Proof mode: SCCs in DG + base ordering
Upper bound for coeffs: 1
Rationals below 1 for all non-replacing args: No
Polynomial interpretation: Linear
Coeffs in polynomials: No rationals
Delta: automatic



Termination was proved succesfully.