Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Frederiksen_Others/boolprog)

The rewrite relation of the following TRS is considered.

f4(S(x''),S(x'),x3,x4,S(x))	→	f2(S(x''),x',x3,x4,x)	(1)
f4(S(x'),0,x3,x4,S(x))	→	f3(x',0,x3,x4,x)	(2)
f2(x1,x2,S(x''),S(x'),S(x))	→	f5(x1,x2,S(x''),x',x)	(3)
f2(x1,x2,S(x'),0,S(x))	→	f3(x1,x2,x',0,x)	(4)
f4(S(x'),S(x),x3,x4,0)	→	0	(5)
f4(S(x),0,x3,x4,0)	→	0	(6)
f2(x1,x2,S(x'),S(x),0)	→	0	(7)
f2(x1,x2,S(x),0,0)	→	0	(8)
f0(x1,S(x'),x3,S(x),x5)	→	f1(x',S(x'),x,S(x),S(x))	(9)
f0(x1,S(x),x3,0,x5)	→	0	(10)
f6(x1,x2,x3,x4,S(x))	→	f0(x1,x2,x4,x3,x)	(11)
f5(x1,x2,x3,x4,S(x))	→	f6(x2,x1,x3,x4,x)	(12)
f3(x1,x2,x3,x4,S(x))	→	f4(x1,x2,x4,x3,x)	(13)
f1(x1,x2,x3,x4,S(x))	→	f2(x2,x1,x3,x4,x)	(14)
f6(x1,x2,x3,x4,0)	→	0	(15)
f5(x1,x2,x3,x4,0)	→	0	(16)
f4(0,x2,x3,x4,x5)	→	0	(17)
f3(x1,x2,x3,x4,0)	→	0	(18)
f2(x1,x2,0,x4,x5)	→	0	(19)
f1(x1,x2,x3,x4,0)	→	0	(20)
f0(x1,0,x3,x4,x5)	→	0	(21)

The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:

f4^#(S(z0),S(z1),z2,z3,S(z4))

→

c(f2^#(S(z0),z1,z2,z3,z4))

(23)

originates from

f4(S(z0),S(z1),z2,z3,S(z4))

→

f2(S(z0),z1,z2,z3,z4)

(22)

f4^#(S(z0),0,z1,z2,S(z3))

→

c1(f3^#(z0,0,z1,z2,z3))

(25)

originates from

f4(S(z0),0,z1,z2,S(z3))

→

f3(z0,0,z1,z2,z3)

(24)

f4^#(S(z0),S(z1),z2,z3,0)

→

(27)

originates from

f4(S(z0),S(z1),z2,z3,0)

→

(26)

f4^#(S(z0),0,z1,z2,0)

→

(29)

originates from

f4(S(z0),0,z1,z2,0)

→

(28)

f4^#(0,z0,z1,z2,z3)

→

(31)

originates from

f4(0,z0,z1,z2,z3)

→

(30)

f2^#(z0,z1,S(z2),S(z3),S(z4))

→

c5(f5^#(z0,z1,S(z2),z3,z4))

(33)

originates from

f2(z0,z1,S(z2),S(z3),S(z4))

→

f5(z0,z1,S(z2),z3,z4)

(32)

f2^#(z0,z1,S(z2),0,S(z3))

→

c6(f3^#(z0,z1,z2,0,z3))

(35)

originates from

f2(z0,z1,S(z2),0,S(z3))

→

f3(z0,z1,z2,0,z3)

(34)

f2^#(z0,z1,S(z2),S(z3),0)

→

(37)

originates from

f2(z0,z1,S(z2),S(z3),0)

→

(36)

f2^#(z0,z1,S(z2),0,0)

→

(39)

originates from

f2(z0,z1,S(z2),0,0)

→

(38)

f2^#(z0,z1,0,z2,z3)

→

(41)

originates from

f2(z0,z1,0,z2,z3)

→

(40)

f0^#(z0,S(z1),z2,S(z3),z4)

→

c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))

(43)

originates from

f0(z0,S(z1),z2,S(z3),z4)

→

f1(z1,S(z1),z3,S(z3),S(z3))

(42)

f0^#(z0,S(z1),z2,0,z3)

→

c11

(45)

originates from

f0(z0,S(z1),z2,0,z3)

→

(44)

f0^#(z0,0,z1,z2,z3)

→

c12

(47)

originates from

f0(z0,0,z1,z2,z3)

→

(46)

f6^#(z0,z1,z2,z3,S(z4))

→

c13(f0^#(z0,z1,z3,z2,z4))

(49)

originates from

f6(z0,z1,z2,z3,S(z4))

→

f0(z0,z1,z3,z2,z4)

(48)

f6^#(z0,z1,z2,z3,0)

→

c14

(51)

originates from

f6(z0,z1,z2,z3,0)

→

(50)

f5^#(z0,z1,z2,z3,S(z4))

→

c15(f6^#(z1,z0,z2,z3,z4))

(53)

originates from

f5(z0,z1,z2,z3,S(z4))

→

f6(z1,z0,z2,z3,z4)

(52)

f5^#(z0,z1,z2,z3,0)

→

c16

(55)

originates from

f5(z0,z1,z2,z3,0)

→

(54)

f3^#(z0,z1,z2,z3,S(z4))

→

c17(f4^#(z0,z1,z3,z2,z4))

(57)

originates from

f3(z0,z1,z2,z3,S(z4))

→

f4(z0,z1,z3,z2,z4)

(56)

f3^#(z0,z1,z2,z3,0)

→

c18

(59)

originates from

f3(z0,z1,z2,z3,0)

→

(58)

f1^#(z0,z1,z2,z3,S(z4))

→

c19(f2^#(z1,z0,z2,z3,z4))

(61)

originates from

f1(z0,z1,z2,z3,S(z4))

→

f2(z1,z0,z2,z3,z4)

(60)

f1^#(z0,z1,z2,z3,0)

→

c20

(63)

originates from

f1(z0,z1,z2,z3,0)

→

(62)

Moreover, we add the following terms to the innermost strategy.

f4^#(S(z0),S(z1),z2,z3,S(z4))

f4^#(S(z0),0,z1,z2,S(z3))

f4^#(S(z0),S(z1),z2,z3,0)

f4^#(S(z0),0,z1,z2,0)

f4^#(0,z0,z1,z2,z3)

f2^#(z0,z1,S(z2),S(z3),S(z4))

f2^#(z0,z1,S(z2),0,S(z3))

f2^#(z0,z1,S(z2),S(z3),0)

f2^#(z0,z1,S(z2),0,0)

f2^#(z0,z1,0,z2,z3)

f0^#(z0,S(z1),z2,S(z3),z4)

f0^#(z0,S(z1),z2,0,z3)

f0^#(z0,0,z1,z2,z3)

f6^#(z0,z1,z2,z3,S(z4))

f6^#(z0,z1,z2,z3,0)

f5^#(z0,z1,z2,z3,S(z4))

f5^#(z0,z1,z2,z3,0)

f3^#(z0,z1,z2,z3,S(z4))

f3^#(z0,z1,z2,z3,0)

f1^#(z0,z1,z2,z3,S(z4))

f1^#(z0,z1,z2,z3,0)

1.1 Usable Rules

We remove the following rules since they are not usable.

f4(S(z0),S(z1),z2,z3,S(z4))	→	f2(S(z0),z1,z2,z3,z4)	(22)
f4(S(z0),0,z1,z2,S(z3))	→	f3(z0,0,z1,z2,z3)	(24)
f4(S(z0),S(z1),z2,z3,0)	→	0	(26)
f4(S(z0),0,z1,z2,0)	→	0	(28)
f4(0,z0,z1,z2,z3)	→	0	(30)
f2(z0,z1,S(z2),S(z3),S(z4))	→	f5(z0,z1,S(z2),z3,z4)	(32)
f2(z0,z1,S(z2),0,S(z3))	→	f3(z0,z1,z2,0,z3)	(34)
f2(z0,z1,S(z2),S(z3),0)	→	0	(36)
f2(z0,z1,S(z2),0,0)	→	0	(38)
f2(z0,z1,0,z2,z3)	→	0	(40)
f0(z0,S(z1),z2,S(z3),z4)	→	f1(z1,S(z1),z3,S(z3),S(z3))	(42)
f0(z0,S(z1),z2,0,z3)	→	0	(44)
f0(z0,0,z1,z2,z3)	→	0	(46)
f6(z0,z1,z2,z3,S(z4))	→	f0(z0,z1,z3,z2,z4)	(48)
f6(z0,z1,z2,z3,0)	→	0	(50)
f5(z0,z1,z2,z3,S(z4))	→	f6(z1,z0,z2,z3,z4)	(52)
f5(z0,z1,z2,z3,0)	→	0	(54)
f3(z0,z1,z2,z3,S(z4))	→	f4(z0,z1,z3,z2,z4)	(56)
f3(z0,z1,z2,z3,0)	→	0	(58)
f1(z0,z1,z2,z3,S(z4))	→	f2(z1,z0,z2,z3,z4)	(60)
f1(z0,z1,z2,z3,0)	→	0	(62)

1.1.1 Rule Shifting

The rules

f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	0
[f2^#(x₁,...,x₅)]	=	0
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f5^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f3^#(x₁,...,x₅)]	=	0
[f1^#(x₁,...,x₅)]	=	1 · x₂ + 0 + 1 · x₄ + 1 · x₅
[S(x₁)]	=	0
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1 Rule Shifting

The rules

f0^#(z0,0,z1,z2,z3)

→

c12

(47)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	0
[f2^#(x₁,...,x₅)]	=	1 · x₁ + 0
[f0^#(x₁,...,x₅)]	=	1 · x₂ + 0 + 1 · x₄
[f6^#(x₁,...,x₅)]	=	1 · x₂ + 0 + 1 · x₃
[f5^#(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₃
[f3^#(x₁,...,x₅)]	=	0
[f1^#(x₁,...,x₅)]	=	1 · x₂ + 0 + 1 · x₄ + 1 · x₅
[S(x₁)]	=	0
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1 Rule Shifting

The rules

f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1
[f2^#(x₁,...,x₅)]	=	1
[f0^#(x₁,...,x₅)]	=	1 + 1 · x₄
[f6^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f5^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f3^#(x₁,...,x₅)]	=	1
[f1^#(x₁,...,x₅)]	=	1 + 1 · x₂ + 1 · x₄ + 1 · x₅
[S(x₁)]	=	0
[0]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1 Rule Shifting

The rules

f4^#(S(z0),0,z1,z2,S(z3))

→

c1(f3^#(z0,0,z1,z2,z3))

(25)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 · x₁ + 0
[f2^#(x₁,...,x₅)]	=	1 · x₁ + 0
[f0^#(x₁,...,x₅)]	=	1 · x₂ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₂ + 0
[f5^#(x₁,...,x₅)]	=	1 · x₁ + 0
[f3^#(x₁,...,x₅)]	=	1 · x₁ + 0
[f1^#(x₁,...,x₅)]	=	1 · x₂ + 0
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1 Rule Shifting

The rules

f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 · x₃ + 0 + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f5^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f3^#(x₁,...,x₅)]	=	1 · x₃ + 0 + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 · x₃ + 0
[S(x₁)]	=	1 + 1 · x₁
[0]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1 Rule Shifting

The rules

f1^#(z0,z1,z2,z3,S(z4))

→

c19(f2^#(z1,z0,z2,z3,z4))

(61)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 · x₃ + 0 + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f5^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f3^#(x₁,...,x₅)]	=	1 · x₃ + 0 + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 + 1 · x₃
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

f4^#(S(z0),S(z1),z2,z3,S(z4))

→

c(f2^#(S(z0),z1,z2,z3,z4))

(23)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f5^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f3^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 · x₃ + 0
[S(x₁)]	=	1 + 1 · x₁
[0]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

f6^#(z0,z1,z2,z3,S(z4))

→

c13(f0^#(z0,z1,z3,z2,z4))

(49)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f5^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f3^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 + 1 · x₃
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

f3^#(z0,z1,z2,z3,S(z4))

→

c17(f4^#(z0,z1,z3,z2,z4))

(57)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₃ + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₃
[f0^#(x₁,...,x₅)]	=	1 · x₂ + 0 + 1 · x₄
[f6^#(x₁,...,x₅)]	=	1 · x₂ + 0 + 1 · x₃
[f5^#(x₁,...,x₅)]	=	1 · x₁ + 0 + 1 · x₃
[f3^#(x₁,...,x₅)]	=	1 + 1 · x₁ + 1 · x₃ + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 + 1 · x₂ + 1 · x₃
[S(x₁)]	=	1 + 1 · x₁
[0]	=	0

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

f5^#(z0,z1,z2,z3,S(z4))

→

c15(f6^#(z1,z0,z2,z3,z4))

(53)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f5^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f3^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 + 1 · x₃
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1.1.1.1.1.1 Rule Shifting

The rules

f2^#(z0,z1,S(z2),S(z3),S(z4))

→

c5(f5^#(z0,z1,S(z2),z3,z4))

(33)

are strictly oriented by the following linear polynomial interpretation over the naturals

[c(x₁)]	=	1 · x₁ + 0
[c1(x₁)]	=	1 · x₁ + 0
[c2]	=	0
[c3]	=	0
[c4]	=	0
[c5(x₁)]	=	1 · x₁ + 0
[c6(x₁)]	=	1 · x₁ + 0
[c7]	=	0
[c8]	=	0
[c9]	=	0
[c10(x₁)]	=	1 · x₁ + 0
[c11]	=	0
[c12]	=	0
[c13(x₁)]	=	1 · x₁ + 0
[c14]	=	0
[c15(x₁)]	=	1 · x₁ + 0
[c16]	=	0
[c17(x₁)]	=	1 · x₁ + 0
[c18]	=	0
[c19(x₁)]	=	1 · x₁ + 0
[c20]	=	0
[f4^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f2^#(x₁,...,x₅)]	=	1 + 1 · x₃
[f0^#(x₁,...,x₅)]	=	1 · x₄ + 0
[f6^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f5^#(x₁,...,x₅)]	=	1 · x₃ + 0
[f3^#(x₁,...,x₅)]	=	1 + 1 · x₃ + 1 · x₄
[f1^#(x₁,...,x₅)]	=	1 + 1 · x₃
[S(x₁)]	=	1 + 1 · x₁
[0]	=	1

which has the intended complexity. Here, only the following usable rules have been considered:

f4^#(S(z0),S(z1),z2,z3,S(z4))	→	c(f2^#(S(z0),z1,z2,z3,z4))	(23)
f4^#(S(z0),0,z1,z2,S(z3))	→	c1(f3^#(z0,0,z1,z2,z3))	(25)
f4^#(S(z0),S(z1),z2,z3,0)	→	c2	(27)
f4^#(S(z0),0,z1,z2,0)	→	c3	(29)
f4^#(0,z0,z1,z2,z3)	→	c4	(31)
f2^#(z0,z1,S(z2),S(z3),S(z4))	→	c5(f5^#(z0,z1,S(z2),z3,z4))	(33)
f2^#(z0,z1,S(z2),0,S(z3))	→	c6(f3^#(z0,z1,z2,0,z3))	(35)
f2^#(z0,z1,S(z2),S(z3),0)	→	c7	(37)
f2^#(z0,z1,S(z2),0,0)	→	c8	(39)
f2^#(z0,z1,0,z2,z3)	→	c9	(41)
f0^#(z0,S(z1),z2,S(z3),z4)	→	c10(f1^#(z1,S(z1),z3,S(z3),S(z3)))	(43)
f0^#(z0,S(z1),z2,0,z3)	→	c11	(45)
f0^#(z0,0,z1,z2,z3)	→	c12	(47)
f6^#(z0,z1,z2,z3,S(z4))	→	c13(f0^#(z0,z1,z3,z2,z4))	(49)
f6^#(z0,z1,z2,z3,0)	→	c14	(51)
f5^#(z0,z1,z2,z3,S(z4))	→	c15(f6^#(z1,z0,z2,z3,z4))	(53)
f5^#(z0,z1,z2,z3,0)	→	c16	(55)
f3^#(z0,z1,z2,z3,S(z4))	→	c17(f4^#(z0,z1,z3,z2,z4))	(57)
f3^#(z0,z1,z2,z3,0)	→	c18	(59)
f1^#(z0,z1,z2,z3,S(z4))	→	c19(f2^#(z1,z0,z2,z3,z4))	(61)
f1^#(z0,z1,z2,z3,0)	→	c20	(63)

1.1.1.1.1.1.1.1.1.1.1.1.1.1 R is empty

There are no rules in the TRS R. Hence, R/S has complexity O(1).