YES
(VAR x y)
(RULES 
active(f(x)) -> mark(x)
top(active(c)) -> top(mark(c))
top(mark(x)) -> top(check(x))
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X),x))
match(f(x),f(y)) -> f(match(x,y))
match(X,x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
start(ok(x)) -> found(x)
f(found(x)) -> found(f(x))
top(found(x)) -> top(active(x))
active(f(x)) -> f(active(x))
f(mark(x)) -> mark(f(x))
)

Proving termination of rewriting for Liveness8:

-> Dependency pairs:
nF_top(active(c)) -> nF_top(mark(c))
nF_top(mark(x)) -> nF_top(check(x))
nF_top(mark(x)) -> nF_check(x)
nF_check(f(x)) -> nF_f(check(x))
nF_check(f(x)) -> nF_check(x)
nF_check(x) -> nF_start(match(f(X),x))
nF_check(x) -> nF_match(f(X),x)
nF_check(x) -> nF_f(X)
nF_match(f(x),f(y)) -> nF_f(match(x,y))
nF_match(f(x),f(y)) -> nF_match(x,y)
nF_match(X,x) -> nF_proper(x)
nF_proper(f(x)) -> nF_f(proper(x))
nF_proper(f(x)) -> nF_proper(x)
nF_f(ok(x)) -> nF_f(x)
nF_f(found(x)) -> nF_f(x)
nF_top(found(x)) -> nF_top(active(x))
nF_top(found(x)) -> nF_active(x)
nF_active(f(x)) -> nF_f(active(x))
nF_active(f(x)) -> nF_active(x)
nF_f(mark(x)) -> nF_f(x)

-> Proof of termination for Liveness8_1_1:
-> -> Dependency pairs in cycle:
nF_top(active(c)) -> nF_top(mark(c))
nF_top(found(x)) -> nF_top(active(x))
nF_top(mark(x)) -> nF_top(check(x))

UsableRules:
active(f(x)) -> mark(x)
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X),x))
match(f(x),f(y)) -> f(match(x,y))
match(X,x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
start(ok(x)) -> found(x)
f(found(x)) -> found(f(x))
active(f(x)) -> f(active(x))
f(mark(x)) -> mark(f(x))

Polynomial Interpretation:

[active](X) = X
[f](X) = 0
[mark](X) = 0
[top](X) = 0
[c] = 1
[check](X) = 0
[start](X) = X
[match](X1,X2) = X1
[X] = 1
[proper](X) = 1
[ok](X) = X
[found](X) = X
[nF_top](X) = X

TIME: 4.6753000000000045e-2

-> -> Dependency pairs in cycle:
nF_top(found(x)) -> nF_top(active(x))
nF_top(mark(x)) -> nF_top(check(x))

UsableRules:
active(f(x)) -> mark(x)
check(f(x)) -> f(check(x))
check(x) -> start(match(f(X),x))
match(f(x),f(y)) -> f(match(x,y))
match(X,x) -> proper(x)
proper(c) -> ok(c)
proper(f(x)) -> f(proper(x))
f(ok(x)) -> ok(f(x))
start(ok(x)) -> found(x)
f(found(x)) -> found(f(x))
active(f(x)) -> f(active(x))
f(mark(x)) -> mark(f(x))

Polynomial Interpretation:

[active](X) = X
[f](X) = X + 1
[mark](X) = X + 1
[top](X) = 0
[c] = 1
[check](X) = X
[start](X) = X
[match](X1,X2) = X2
[X] = 0
[proper](X) = X
[ok](X) = X
[found](X) = X
[nF_top](X) = X

TIME: 4.6712e-2

-> -> Dependency pairs in cycle:
nF_top(found(x)) -> nF_top(active(x))

UsableRules:
active(f(x)) -> mark(x)
f(ok(x)) -> ok(f(x))
f(found(x)) -> found(f(x))
active(f(x)) -> f(active(x))
f(mark(x)) -> mark(f(x))

Polynomial Interpretation:

[active](X) = 0
[f](X) = X
[mark](X) = 0
[top](X) = 0
[c] = 0
[check](X) = 0
[start](X) = 0
[match](X1,X2) = 0
[X] = 0
[proper](X) = 0
[ok](X) = 0
[found](X) = 1
[nF_top](X) = X

TIME: 4.583e-2


-> Proof of termination for Liveness8_1_2:
-> -> Dependency pairs in cycle:
nF_active(f(x)) -> nF_active(x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Liveness8_1_3:
-> -> Dependency pairs in cycle:
nF_check(f(x)) -> nF_check(x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Liveness8_1_4:
-> -> Dependency pairs in cycle:
nF_match(f(x),f(y)) -> nF_match(x,y)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Liveness8_1_5:
-> -> Dependency pairs in cycle:
nF_proper(f(x)) -> nF_proper(x)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Liveness8_1_6:
-> -> Dependency pairs in cycle:
nF_f(mark(x)) -> nF_f(x)
nF_f(found(x)) -> nF_f(x)
nF_f(ok(x)) -> nF_f(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.