YES
0 QTRS
↳1 QTRSRRRProof (⇔, 79 ms)
↳2 QTRS
↳3 RisEmptyProof (⇔, 0 ms)
↳4 YES
f(s(x1), x2, x3, x4, x5) → f(x1, x2, x3, x4, x5)
f(0, s(x2), x3, x4, x5) → f(x2, x2, x3, x4, x5)
f(0, 0, s(x3), x4, x5) → f(x3, x3, x3, x4, x5)
f(0, 0, 0, s(x4), x5) → f(x4, x4, x4, x4, x5)
f(0, 0, 0, 0, s(x5)) → f(x5, x5, x5, x5, x5)
f(0, 0, 0, 0, 0) → 0
s1 > [f5, 0]
f5: [4,3,2,1,5]
s1: [1]
0: multiset
f(s(x1), x2, x3, x4, x5) → f(x1, x2, x3, x4, x5)
f(0, s(x2), x3, x4, x5) → f(x2, x2, x3, x4, x5)
f(0, 0, s(x3), x4, x5) → f(x3, x3, x3, x4, x5)
f(0, 0, 0, s(x4), x5) → f(x4, x4, x4, x4, x5)
f(0, 0, 0, 0, s(x5)) → f(x5, x5, x5, x5, x5)
f(0, 0, 0, 0, 0) → 0