YES Termination w.r.t. Q proof of TCT_12_polycounter-10.ari

Termination w.r.t. Q of the given QTRS could be proven:

0 QTRS
↳1 QTRSRRRProof (⇔, 168 ms)
↳2 QTRS
↳3 RisEmptyProof (⇔, 0 ms)
↳4 YES

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

f(s(x1), x2, x3, x4, x5, x6, x7, x8, x9, x10) → f(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
f(0, s(x2), x3, x4, x5, x6, x7, x8, x9, x10) → f(x2, x2, x3, x4, x5, x6, x7, x8, x9, x10)
f(0, 0, s(x3), x4, x5, x6, x7, x8, x9, x10) → f(x3, x3, x3, x4, x5, x6, x7, x8, x9, x10)
f(0, 0, 0, s(x4), x5, x6, x7, x8, x9, x10) → f(x4, x4, x4, x4, x5, x6, x7, x8, x9, x10)
f(0, 0, 0, 0, s(x5), x6, x7, x8, x9, x10) → f(x5, x5, x5, x5, x5, x6, x7, x8, x9, x10)
f(0, 0, 0, 0, 0, s(x6), x7, x8, x9, x10) → f(x6, x6, x6, x6, x6, x6, x7, x8, x9, x10)
f(0, 0, 0, 0, 0, 0, s(x7), x8, x9, x10) → f(x7, x7, x7, x7, x7, x7, x7, x8, x9, x10)
f(0, 0, 0, 0, 0, 0, 0, s(x8), x9, x10) → f(x8, x8, x8, x8, x8, x8, x8, x8, x9, x10)
f(0, 0, 0, 0, 0, 0, 0, 0, s(x9), x10) → f(x9, x9, x9, x9, x9, x9, x9, x9, x9, x10)
f(0, 0, 0, 0, 0, 0, 0, 0, 0, s(x10)) → f(x10, x10, x10, x10, x10, x10, x10, x10, x10, x10)
f(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) → 0

Q is empty.

(1) QTRSRRRProof (EQUIVALENT transformation)

Used ordering:
Recursive path order with status [RPO].
Quasi-Precedence:
s1 > [f10, 0]

Status:
f10: [10,9,8,7,6,5,4,3,2,1]
s1: [1]
0: multiset

With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:

f(s(x1), x2, x3, x4, x5, x6, x7, x8, x9, x10) → f(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)
f(0, s(x2), x3, x4, x5, x6, x7, x8, x9, x10) → f(x2, x2, x3, x4, x5, x6, x7, x8, x9, x10)
f(0, 0, s(x3), x4, x5, x6, x7, x8, x9, x10) → f(x3, x3, x3, x4, x5, x6, x7, x8, x9, x10)
f(0, 0, 0, s(x4), x5, x6, x7, x8, x9, x10) → f(x4, x4, x4, x4, x5, x6, x7, x8, x9, x10)
f(0, 0, 0, 0, s(x5), x6, x7, x8, x9, x10) → f(x5, x5, x5, x5, x5, x6, x7, x8, x9, x10)
f(0, 0, 0, 0, 0, s(x6), x7, x8, x9, x10) → f(x6, x6, x6, x6, x6, x6, x7, x8, x9, x10)
f(0, 0, 0, 0, 0, 0, s(x7), x8, x9, x10) → f(x7, x7, x7, x7, x7, x7, x7, x8, x9, x10)
f(0, 0, 0, 0, 0, 0, 0, s(x8), x9, x10) → f(x8, x8, x8, x8, x8, x8, x8, x8, x9, x10)
f(0, 0, 0, 0, 0, 0, 0, 0, s(x9), x10) → f(x9, x9, x9, x9, x9, x9, x9, x9, x9, x10)
f(0, 0, 0, 0, 0, 0, 0, 0, 0, s(x10)) → f(x10, x10, x10, x10, x10, x10, x10, x10, x10, x10)
f(0, 0, 0, 0, 0, 0, 0, 0, 0, 0) → 0


(2) Obligation:

Q restricted rewrite system:
R is empty.
Q is empty.

(3) RisEmptyProof (EQUIVALENT transformation)

The TRS R is empty. Hence, termination is trivially proven.

(4) YES