Certification Problem

Input (TPDB TRS_Standard/TCT_12/polycounter-10)

The rewrite relation of the following TRS is considered.

f(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10) → f(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) (1)
f(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10) → f(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10) (2)
f(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10) → f(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10) (3)
f(0,0,0,s(x4),x5,x6,x7,x8,x9,x10) → f(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10) (4)
f(0,0,0,0,s(x5),x6,x7,x8,x9,x10) → f(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10) (5)
f(0,0,0,0,0,s(x6),x7,x8,x9,x10) → f(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10) (6)
f(0,0,0,0,0,0,s(x7),x8,x9,x10) → f(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10) (7)
f(0,0,0,0,0,0,0,s(x8),x9,x10) → f(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10) (8)
f(0,0,0,0,0,0,0,0,s(x9),x10) → f(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10) (9)
f(0,0,0,0,0,0,0,0,0,s(x10)) → f(x10,x10,x10,x10,x10,x10,x10,x10,x10,x10) (10)
f(0,0,0,0,0,0,0,0,0,0) → 0 (11)

Property / Task

Prove or disprove termination.

Answer / Result

Yes.

Proof (by AProVE @ termCOMP 2023)

1 Rule Removal

Using the
prec(f) = 0 stat(f) = lex
prec(s) = 1 stat(s) = lex
prec(0) = 0 stat(0) = lex

π(f) = [9,10,8,7,6,5,4,3,2,1]
π(s) = [1]
π(0) = []

all of the following rules can be deleted.
f(s(x1),x2,x3,x4,x5,x6,x7,x8,x9,x10) → f(x1,x2,x3,x4,x5,x6,x7,x8,x9,x10) (1)
f(0,s(x2),x3,x4,x5,x6,x7,x8,x9,x10) → f(x2,x2,x3,x4,x5,x6,x7,x8,x9,x10) (2)
f(0,0,s(x3),x4,x5,x6,x7,x8,x9,x10) → f(x3,x3,x3,x4,x5,x6,x7,x8,x9,x10) (3)
f(0,0,0,s(x4),x5,x6,x7,x8,x9,x10) → f(x4,x4,x4,x4,x5,x6,x7,x8,x9,x10) (4)
f(0,0,0,0,s(x5),x6,x7,x8,x9,x10) → f(x5,x5,x5,x5,x5,x6,x7,x8,x9,x10) (5)
f(0,0,0,0,0,s(x6),x7,x8,x9,x10) → f(x6,x6,x6,x6,x6,x6,x7,x8,x9,x10) (6)
f(0,0,0,0,0,0,s(x7),x8,x9,x10) → f(x7,x7,x7,x7,x7,x7,x7,x8,x9,x10) (7)
f(0,0,0,0,0,0,0,s(x8),x9,x10) → f(x8,x8,x8,x8,x8,x8,x8,x8,x9,x10) (8)
f(0,0,0,0,0,0,0,0,s(x9),x10) → f(x9,x9,x9,x9,x9,x9,x9,x9,x9,x10) (9)
f(0,0,0,0,0,0,0,0,0,s(x10)) → f(x10,x10,x10,x10,x10,x10,x10,x10,x10,x10) (10)
f(0,0,0,0,0,0,0,0,0,0) → 0 (11)

1.1 R is empty

There are no rules in the TRS. Hence, it is terminating.