YES

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

The following DP Processors were used


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

Problem 1: DependencyGraph



Dependency Pair Problem

Dependency Pairs

remove#(x, .(y, z))remove#(x, z)purge#(.(x, y))remove#(x, y)
purge#(.(x, y))purge#(remove(x, y))

Rewrite Rules

purge(nil)nilpurge(.(x, y)).(x, purge(remove(x, y)))
remove(x, nil)nilremove(x, .(y, z))if(=(x, y), remove(x, z), .(y, remove(x, z)))

Original Signature

Termination of terms over the following signature is verified: remove, if, ., purge, =, nil

Strategy


The following SCCs where found

remove#(x, .(y, z)) → remove#(x, z)

purge#(.(x, y)) → purge#(remove(x, y))

Problem 2: PolynomialLinearRange4iUR



Dependency Pair Problem

Dependency Pairs

purge#(.(x, y))purge#(remove(x, y))

Rewrite Rules

purge(nil)nilpurge(.(x, y)).(x, purge(remove(x, y)))
remove(x, nil)nilremove(x, .(y, z))if(=(x, y), remove(x, z), .(y, remove(x, z)))

Original Signature

Termination of terms over the following signature is verified: remove, if, ., purge, =, nil

Strategy


Polynomial Interpretation

Improved Usable rules

remove(x, nil)nilremove(x, .(y, z))if(=(x, y), remove(x, z), .(y, remove(x, z)))

The following dependency pairs are strictly oriented by an ordering on the given polynomial interpretation, thus they are removed:

purge#(.(x, y))purge#(remove(x, y))

Problem 3: SubtermCriterion



Dependency Pair Problem

Dependency Pairs

remove#(x, .(y, z))remove#(x, z)

Rewrite Rules

purge(nil)nilpurge(.(x, y)).(x, purge(remove(x, y)))
remove(x, nil)nilremove(x, .(y, z))if(=(x, y), remove(x, z), .(y, remove(x, z)))

Original Signature

Termination of terms over the following signature is verified: remove, if, ., purge, =, nil

Strategy


Projection

The following projection was used:

Thus, the following dependency pairs are removed:

remove#(x, .(y, z))remove#(x, z)