YES
(VAR X Y X1 X2)
(RULES 
a__from(X) -> cons(mark(X),from(s(X)))
a__length(nil) -> 0
a__length(cons(X,Y)) -> s(a__length1(Y))
a__length1(X) -> a__length(X)
mark(from(X)) -> a__from(mark(X))
mark(length(X)) -> a__length(X)
mark(length1(X)) -> a__length1(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
a__from(X) -> from(X)
a__length(X) -> length(X)
a__length1(X) -> length1(X)
)

Proving termination of rewriting for Ex14_AEGL02_GM:

-> Dependency pairs:
nF_a__from(X) -> nF_mark(X)
nF_a__length(cons(X,Y)) -> nF_a__length1(Y)
nF_a__length1(X) -> nF_a__length(X)
nF_mark(from(X)) -> nF_a__from(mark(X))
nF_mark(from(X)) -> nF_mark(X)
nF_mark(length(X)) -> nF_a__length(X)
nF_mark(length1(X)) -> nF_a__length1(X)
nF_mark(cons(X1,X2)) -> nF_mark(X1)
nF_mark(s(X)) -> nF_mark(X)

-> Proof of termination for Ex14_AEGL02_GM_1_1:
-> -> Dependency pairs in cycle:
nF_a__from(X) -> nF_mark(X)
nF_mark(from(X)) -> nF_a__from(mark(X))
nF_mark(s(X)) -> nF_mark(X)
nF_mark(cons(X1,X2)) -> nF_mark(X1)
nF_mark(from(X)) -> nF_mark(X)

UsableRules:
a__from(X) -> cons(mark(X),from(s(X)))
a__length(nil) -> 0
a__length(cons(X,Y)) -> s(a__length1(Y))
a__length1(X) -> a__length(X)
mark(from(X)) -> a__from(mark(X))
mark(length(X)) -> a__length(X)
mark(length1(X)) -> a__length1(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
a__from(X) -> from(X)
a__length(X) -> length(X)
a__length1(X) -> length1(X)

Polynomial Interpretation:

[a__from](X) = X + 1
[cons](X1,X2) = X1
[mark](X) = X
[from](X) = X + 1
[s](X) = X
[a__length](X) = 1
[nil] = 1
[0] = 1
[a__length1](X) = 1
[length](X) = 1
[length1](X) = 1
[nF_a__from](X) = X
[nF_mark](X) = X

TIME: 5.165e-2

-> -> Dependency pairs in cycle:
nF_a__from(X) -> nF_mark(X)
nF_mark(from(X)) -> nF_a__from(mark(X))
nF_mark(cons(X1,X2)) -> nF_mark(X1)
nF_mark(s(X)) -> nF_mark(X)

UsableRules:
a__from(X) -> cons(mark(X),from(s(X)))
a__length(nil) -> 0
a__length(cons(X,Y)) -> s(a__length1(Y))
a__length1(X) -> a__length(X)
mark(from(X)) -> a__from(mark(X))
mark(length(X)) -> a__length(X)
mark(length1(X)) -> a__length1(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
a__from(X) -> from(X)
a__length(X) -> length(X)
a__length1(X) -> length1(X)

Polynomial Interpretation:

[a__from](X) = X + 1
[cons](X1,X2) = X1 + 1
[mark](X) = X
[from](X) = X + 1
[s](X) = X
[a__length](X) = 1
[nil] = 1
[0] = 1
[a__length1](X) = 1
[length](X) = 1
[length1](X) = 1
[nF_a__from](X) = X
[nF_mark](X) = X

TIME: 4.2733e-2

-> -> Dependency pairs in cycle:
nF_a__from(X) -> nF_mark(X)
nF_mark(from(X)) -> nF_a__from(mark(X))
nF_mark(s(X)) -> nF_mark(X)

UsableRules:
a__from(X) -> cons(mark(X),from(s(X)))
a__length(nil) -> 0
a__length(cons(X,Y)) -> s(a__length1(Y))
a__length1(X) -> a__length(X)
mark(from(X)) -> a__from(mark(X))
mark(length(X)) -> a__length(X)
mark(length1(X)) -> a__length1(X)
mark(cons(X1,X2)) -> cons(mark(X1),X2)
mark(s(X)) -> s(mark(X))
mark(nil) -> nil
mark(0) -> 0
a__from(X) -> from(X)
a__length(X) -> length(X)
a__length1(X) -> length1(X)

Polynomial Interpretation:

[a__from](X) = X + 1
[cons](X1,X2) = X2
[mark](X) = X
[from](X) = X + 1
[s](X) = X
[a__length](X) = X
[nil] = 1
[0] = 0
[a__length1](X) = X
[length](X) = X
[length1](X) = X
[nF_a__from](X) = X
[nF_mark](X) = X

TIME: 4.6769e-2

-> -> Dependency pairs in cycle:
nF_mark(s(X)) -> nF_mark(X)

Termination proved: Cycles verify subterm criterion.

-> Proof of termination for Ex14_AEGL02_GM_1_2:
-> -> Dependency pairs in cycle:
nF_a__length1(X) -> nF_a__length(X)
nF_a__length(cons(X,Y)) -> nF_a__length1(Y)

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.