YES
(VAR X)
(RULES 
active(f(f(a))) -> mark(c(f(g(f(a)))))
mark(f(X)) -> active(f(mark(X)))
mark(a) -> active(a)
mark(c(X)) -> active(c(X))
mark(g(X)) -> active(g(mark(X)))
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
c(mark(X)) -> c(X)
c(active(X)) -> c(X)
g(mark(X)) -> g(X)
g(active(X)) -> g(X)
)

Proving termination of rewriting for Ex23_Luc06_iGM:

-> Dependency pairs:
nF_active(f(f(a))) -> nF_mark(c(f(g(f(a)))))
nF_active(f(f(a))) -> nF_c(f(g(f(a))))
nF_active(f(f(a))) -> nF_f(g(f(a)))
nF_active(f(f(a))) -> nF_g(f(a))
nF_active(f(f(a))) -> nF_f(a)
nF_mark(f(X)) -> nF_active(f(mark(X)))
nF_mark(f(X)) -> nF_f(mark(X))
nF_mark(f(X)) -> nF_mark(X)
nF_mark(a) -> nF_active(a)
nF_mark(c(X)) -> nF_active(c(X))
nF_mark(c(X)) -> nF_c(X)
nF_mark(g(X)) -> nF_active(g(mark(X)))
nF_mark(g(X)) -> nF_g(mark(X))
nF_mark(g(X)) -> nF_mark(X)
nF_f(mark(X)) -> nF_f(X)
nF_f(active(X)) -> nF_f(X)
nF_c(mark(X)) -> nF_c(X)
nF_c(active(X)) -> nF_c(X)
nF_g(mark(X)) -> nF_g(X)
nF_g(active(X)) -> nF_g(X)

-> Dependency pairs narrowed: 
nF_mark(f(X)) -> nF_active(f(mark(X)))
nF_mark(g(X)) -> nF_active(g(mark(X)))

-> New dependency pairs: 
nF_mark(f(X)) -> nF_active(f(X))
nF_mark(g(X)) -> nF_active(g(X))

-> Proof of termination for Ex23_Luc06_iGM_1_1:
-> -> Dependency pairs in cycle:
nF_active(f(f(a))) -> nF_mark(c(f(g(f(a)))))
nF_mark(g(X)) -> nF_active(g(X))
nF_mark(g(X)) -> nF_mark(X)
nF_mark(f(X)) -> nF_mark(X)
nF_mark(f(X)) -> nF_active(f(X))
nF_mark(c(X)) -> nF_active(c(X))

UsableRules:
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
c(mark(X)) -> c(X)
c(active(X)) -> c(X)
g(mark(X)) -> g(X)
g(active(X)) -> g(X)

Polynomial Interpretation:

[active](X) = 0
[f](X) = 1
[a] = 0
[mark](X) = 0
[c](X) = 0
[g](X) = 1
[nF_active](X) = X
[nF_mark](X) = 1

TIME: 5.8023e-2

-> -> Dependency pairs in cycle:
nF_active(f(f(a))) -> nF_mark(c(f(g(f(a)))))
nF_mark(f(X)) -> nF_active(f(X))
nF_mark(f(X)) -> nF_mark(X)
nF_mark(g(X)) -> nF_mark(X)
nF_mark(g(X)) -> nF_active(g(X))

UsableRules:
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
c(mark(X)) -> c(X)
c(active(X)) -> c(X)
g(mark(X)) -> g(X)
g(active(X)) -> g(X)

Polynomial Interpretation:

[active](X) = 0
[f](X) = 1
[a] = 0
[mark](X) = 0
[c](X) = 0
[g](X) = 0
[nF_active](X) = X
[nF_mark](X) = 1

TIME: 5.4393e-2

-> -> Dependency pairs in cycle:
nF_active(f(f(a))) -> nF_mark(c(f(g(f(a)))))
nF_mark(f(X)) -> nF_active(f(X))
nF_mark(g(X)) -> nF_mark(X)
nF_mark(f(X)) -> nF_mark(X)

UsableRules:
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
c(mark(X)) -> c(X)
c(active(X)) -> c(X)
g(mark(X)) -> g(X)
g(active(X)) -> g(X)

Polynomial Interpretation:

[active](X) = X
[f](X) = X + 1
[a] = 0
[mark](X) = X
[c](X) = 0
[g](X) = X
[nF_active](X) = X
[nF_mark](X) = X

TIME: 5.2092e-2

-> -> Dependency pairs in cycle:
nF_active(f(f(a))) -> nF_mark(c(f(g(f(a)))))
nF_mark(f(X)) -> nF_active(f(X))
nF_mark(g(X)) -> nF_mark(X)

UsableRules:
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
c(mark(X)) -> c(X)
c(active(X)) -> c(X)
g(mark(X)) -> g(X)
g(active(X)) -> g(X)

Polynomial Interpretation:

[active](X) = X
[f](X) = X + 1
[a] = 0
[mark](X) = X
[c](X) = 0
[g](X) = X + 1
[nF_active](X) = X
[nF_mark](X) = X

TIME: 5.2747e-2

-> -> Dependency pairs in cycle:
nF_active(f(f(a))) -> nF_mark(c(f(g(f(a)))))
nF_mark(f(X)) -> nF_active(f(X))

UsableRules:
f(mark(X)) -> f(X)
f(active(X)) -> f(X)
c(mark(X)) -> c(X)
c(active(X)) -> c(X)
g(mark(X)) -> g(X)
g(active(X)) -> g(X)

Polynomial Interpretation:

[active](X) = 0
[f](X) = 1
[a] = 0
[mark](X) = 0
[c](X) = 0
[g](X) = 0
[nF_active](X) = 0
[nF_mark](X) = X

TIME: 5.1673e-2


-> Proof of termination for Ex23_Luc06_iGM_1_2:
-> -> Dependency pairs in cycle:
nF_c(active(X)) -> nF_c(X)
nF_c(mark(X)) -> nF_c(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex23_Luc06_iGM_1_3:
-> -> Dependency pairs in cycle:
nF_f(active(X)) -> nF_f(X)
nF_f(mark(X)) -> nF_f(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex23_Luc06_iGM_1_4:
-> -> Dependency pairs in cycle:
nF_g(active(X)) -> nF_g(X)
nF_g(mark(X)) -> nF_g(X)

Termination proved: Cycles verify subterm criterion.

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.