YES

The TRS could be proven terminating. The proof took 22 ms.

The following DP Processors were used


Problem 1 was processed with processor DependencyGraph (7ms).
 | – Problem 2 was processed with processor SubtermCriterion (1ms).
 |    | – Problem 4 was processed with processor DependencyGraph (1ms).
 | – Problem 3 was processed with processor SubtermCriterion (1ms).

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

int#(s(x), s(y))int_list#(int(x, y))int#(s(x), s(y))int#(x, y)
int#(0, s(y))int#(s(0), s(y))int_list#(.(x, y))int_list#(y)

Rewrite Rules

int(0, 0).(0, nil)int(0, s(y)).(0, int(s(0), s(y)))
int(s(x), 0)nilint(s(x), s(y))int_list(int(x, y))
int_list(nil)nilint_list(.(x, y)).(s(x), int_list(y))

Original Signature

Termination of terms over the following signature is verified: 0, s, int, int_list, ., nil

Strategy


The following SCCs where found

int#(s(x), s(y)) → int#(x, y)int#(0, s(y)) → int#(s(0), s(y))

int_list#(.(x, y)) → int_list#(y)

Problem 2: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

int#(s(x), s(y))int#(x, y)int#(0, s(y))int#(s(0), s(y))

Rewrite Rules

int(0, 0).(0, nil)int(0, s(y)).(0, int(s(0), s(y)))
int(s(x), 0)nilint(s(x), s(y))int_list(int(x, y))
int_list(nil)nilint_list(.(x, y)).(s(x), int_list(y))

Original Signature

Termination of terms over the following signature is verified: 0, s, int, int_list, ., nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

int#(s(x), s(y))int#(x, y)

Problem 4: DependencyGraph



Dependency Pair Problem

Dependency Pairs

int#(0, s(y))int#(s(0), s(y))

Rewrite Rules

int(0, 0).(0, nil)int(0, s(y)).(0, int(s(0), s(y)))
int(s(x), 0)nilint(s(x), s(y))int_list(int(x, y))
int_list(nil)nilint_list(.(x, y)).(s(x), int_list(y))

Original Signature

Termination of terms over the following signature is verified: 0, s, int, int_list, ., nil

Strategy


There are no SCCs!

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

int_list#(.(x, y))int_list#(y)

Rewrite Rules

int(0, 0).(0, nil)int(0, s(y)).(0, int(s(0), s(y)))
int(s(x), 0)nilint(s(x), s(y))int_list(int(x, y))
int_list(nil)nilint_list(.(x, y)).(s(x), int_list(y))

Original Signature

Termination of terms over the following signature is verified: 0, s, int, int_list, ., nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

int_list#(.(x, y))int_list#(y)