Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/Rubio_04/wst99)

The rewrite relation of the following TRS is considered.

din(der(plus(X,Y))) → u21(din(der(X)),X,Y) (1)
u21(dout(DX),X,Y) → u22(din(der(Y)),X,Y,DX) (2)
u22(dout(DY),X,Y,DX) → dout(plus(DX,DY)) (3)
din(der(times(X,Y))) → u31(din(der(X)),X,Y) (4)
u31(dout(DX),X,Y) → u32(din(der(Y)),X,Y,DX) (5)
u32(dout(DY),X,Y,DX) → dout(plus(times(X,DY),times(Y,DX))) (6)
din(der(der(X))) → u41(din(der(X)),X) (7)
u41(dout(DX),X) → u42(din(der(DX)),X,DX) (8)
u42(dout(DDX),X,DX) → dout(DDX) (9)
The evaluation strategy is innermost.

Property / Task

Determine bounds on the runtime complexity.

Answer / Result

An upperbound for the complexity is O(n2).

Proof (by AProVE @ termCOMP 2023)

1 Dependency Tuples

We get the following set of dependency tuples:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
originates from
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
originates from
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
originates from
din(der(der(z0))) → u41(din(der(z0)),z0) (14)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
originates from
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
u22#(dout(z0),z1,z2,z3) → c4 (19)
originates from
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
originates from
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u32#(dout(z0),z1,z2,z3) → c6 (23)
originates from
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
originates from
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
u42#(dout(z0),z1,z2) → c8 (27)
originates from
u42(dout(z0),z1,z2) → dout(z0) (26)
Moreover, we add the following terms to the innermost strategy.
din#(der(plus(z0,z1)))
din#(der(times(z0,z1)))
din#(der(der(z0)))
u21#(dout(z0),z1,z2)
u22#(dout(z0),z1,z2,z3)
u31#(dout(z0),z1,z2)
u32#(dout(z0),z1,z2,z3)
u41#(dout(z0),z1)
u42#(dout(z0),z1,z2)

1.1 Rule Shifting

The rules
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 3 · x1 + 0
[u22(x1,...,x4)] = 1 + 3 · x1 + 3 · x4
[u31(x1, x2, x3)] = 1 · x1 + 0
[u32(x1,...,x4)] = 3 · x1 + 0 + 1 · x4
[u41(x1, x2)] = 2 · x1 + 0
[u42(x1, x2, x3)] = 1 + 1 · x1 + 1 · x3
[din#(x1)] = 3 · x1 + 0
[u21#(x1, x2, x3)] = 1 · x1 + 0
[u22#(x1,...,x4)] = 1 + 1 · x4
[u31#(x1, x2, x3)] = 0
[u32#(x1,...,x4)] = 0
[u41#(x1, x2)] = 0
[u42#(x1, x2, x3)] = 0
[der(x1)] = 0
[plus(x1, x2)] = 1 + 1 · x2
[times(x1, x2)] = 2
[dout(x1)] = 3 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

1.1.1 Rule Shifting

The rules
u42#(dout(z0),z1,z2) → c8 (27)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 2 · x1 + 0
[u22(x1,...,x4)] = 2
[u31(x1, x2, x3)] = 2 · x1 + 0
[u32(x1,...,x4)] = 2 + 1 · x1
[u41(x1, x2)] = 1 · x1 + 0
[u42(x1, x2, x3)] = 2
[din#(x1)] = 3 · x1 + 0
[u21#(x1, x2, x3)] = 0
[u22#(x1,...,x4)] = 0
[u31#(x1, x2, x3)] = 0
[u32#(x1,...,x4)] = 0
[u41#(x1, x2)] = 0
[u42#(x1, x2, x3)] = 2 · x1 + 0
[der(x1)] = 0
[plus(x1, x2)] = 0
[times(x1, x2)] = 0
[dout(x1)] = 2
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

1.1.1.1 Rule Shifting

The rules
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 0
[u22(x1,...,x4)] = 1 · x1 + 0
[u31(x1, x2, x3)] = 0
[u32(x1,...,x4)] = 1 · x1 + 0
[u41(x1, x2)] = 0
[u42(x1, x2, x3)] = 1 · x1 + 0
[din#(x1)] = 1 · x1 + 0
[u21#(x1, x2, x3)] = 0
[u22#(x1,...,x4)] = 1 · x1 + 0
[u31#(x1, x2, x3)] = 0
[u32#(x1,...,x4)] = 0
[u41#(x1, x2)] = 1 · x1 + 0
[u42#(x1, x2, x3)] = 1 · x1 + 0
[der(x1)] = 0
[plus(x1, x2)] = 1
[times(x1, x2)] = 0
[dout(x1)] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

1.1.1.1.1 Rule Shifting

The rules
u32#(dout(z0),z1,z2,z3) → c6 (23)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 1 · x1 + 0
[u22(x1,...,x4)] = 1
[u31(x1, x2, x3)] = 0
[u32(x1,...,x4)] = 1 · x1 + 0
[u41(x1, x2)] = 0
[u42(x1, x2, x3)] = 1 · x1 + 0
[din#(x1)] = 1 · x1 + 0
[u21#(x1, x2, x3)] = 0
[u22#(x1,...,x4)] = 1 · x1 + 0
[u31#(x1, x2, x3)] = 0
[u32#(x1,...,x4)] = 1 · x1 + 0
[u41#(x1, x2)] = 0
[u42#(x1, x2, x3)] = 1 · x1 + 0
[der(x1)] = 0
[plus(x1, x2)] = 1
[times(x1, x2)] = 0
[dout(x1)] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

1.1.1.1.1.1 Rule Shifting

The rules
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 0
[u22(x1,...,x4)] = 1 · x1 + 0
[u31(x1, x2, x3)] = 0
[u32(x1,...,x4)] = 1 · x1 + 0
[u41(x1, x2)] = 1 · x1 + 0
[u42(x1, x2, x3)] = 1
[din#(x1)] = 1 · x1 + 0
[u21#(x1, x2, x3)] = 0
[u22#(x1,...,x4)] = 1 · x1 + 0
[u31#(x1, x2, x3)] = 1 · x1 + 0
[u32#(x1,...,x4)] = 1 · x1 + 0
[u41#(x1, x2)] = 0
[u42#(x1, x2, x3)] = 1 · x1 + 0
[der(x1)] = 0
[plus(x1, x2)] = 1
[times(x1, x2)] = 0
[dout(x1)] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

1.1.1.1.1.1.1 Rule Shifting

The rules
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 1 · x1 + 0
[u22(x1,...,x4)] = 2 + 2 · x1 · x4 + 2 · x1 · x1
[u31(x1, x2, x3)] = 1 · x1 + 0 + 1 · x1 · x3 + 1 · x1 · x1 + 2 · x2 · x1
[u32(x1,...,x4)] = 1 · x2 + 0 + 2 · x2 · x4 + 2 · x1 · x1
[u41(x1, x2)] = 0
[u42(x1, x2, x3)] = 2 · x1 + 0
[din#(x1)] = 1 · x1 + 0
[u21#(x1, x2, x3)] = 2 · x1 · x3 + 0
[u22#(x1,...,x4)] = 1 · x3 · x4 + 0
[u31#(x1, x2, x3)] = 1 · x3 + 0
[u32#(x1,...,x4)] = 0
[u41#(x1, x2)] = 1 · x1 · x1 + 0
[u42#(x1, x2, x3)] = 2
[der(x1)] = 1 · x1 + 0
[plus(x1, x2)] = 2 + 1 · x1
[times(x1, x2)] = 1 + 1 · x1 + 1 · x2
[dout(x1)] = 2 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c2(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c3(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6] = 0
[c7(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c8] = 0
[din(x1)] = 0
[u21(x1, x2, x3)] = 0
[u22(x1,...,x4)] = 2 · x1 + 0 + 2 · x1 · x4
[u31(x1, x2, x3)] = 2 · x1 + 0 + 2 · x1 · x3 + 2 · x1 · x1 + 2 · x2 · x1
[u32(x1,...,x4)] = 2 · x1 + 0 + 1 · x2 + 1 · x3 + 2 · x4 + 2 · x4 · x4
[u41(x1, x2)] = 1 · x1 + 0 + 1 · x1 · x1
[u42(x1, x2, x3)] = 2 · x1 + 0 + 2 · x3
[din#(x1)] = 2 · x1 + 0 + 1 · x1 · x1
[u21#(x1, x2, x3)] = 2 · x1 + 0 + 2 · x3 + 1 · x3 · x3 + 2 · x1 · x3 + 1 · x1 · x1
[u22#(x1,...,x4)] = 1 · x3 · x4 + 0
[u31#(x1, x2, x3)] = 2 · x3 + 0 + 1 · x3 · x3 + 2 · x1 · x3 + 2 · x1 · x1
[u32#(x1,...,x4)] = 2 · x4 + 0 + 1 · x3 · x4
[u41#(x1, x2)] = 2 · x2 + 0 + 2 · x1 · x1
[u42#(x1, x2, x3)] = 2 · x2 + 0 + 1 · x3 · x3
[der(x1)] = 2 + 1 · x1
[plus(x1, x2)] = 1 · x1 + 0 + 1 · x2
[times(x1, x2)] = 1 · x1 + 0 + 1 · x2
[dout(x1)] = 2 + 1 · x1
which has the intended complexity. Here, only the following usable rules have been considered:
din#(der(plus(z0,z1))) → c(u21#(din(der(z0)),z0,z1),din#(der(z0))) (11)
din#(der(times(z0,z1))) → c1(u31#(din(der(z0)),z0,z1),din#(der(z0))) (13)
din#(der(der(z0))) → c2(u41#(din(der(z0)),z0),din#(der(z0))) (15)
u21#(dout(z0),z1,z2) → c3(u22#(din(der(z2)),z1,z2,z0),din#(der(z2))) (17)
u22#(dout(z0),z1,z2,z3) → c4 (19)
u31#(dout(z0),z1,z2) → c5(u32#(din(der(z2)),z1,z2,z0),din#(der(z2))) (21)
u32#(dout(z0),z1,z2,z3) → c6 (23)
u41#(dout(z0),z1) → c7(u42#(din(der(z0)),z1,z0),din#(der(z0))) (25)
u42#(dout(z0),z1,z2) → c8 (27)
u32(dout(z0),z1,z2,z3) → dout(plus(times(z1,z0),times(z2,z3))) (22)
din(der(times(z0,z1))) → u31(din(der(z0)),z0,z1) (12)
u22(dout(z0),z1,z2,z3) → dout(plus(z3,z0)) (18)
u31(dout(z0),z1,z2) → u32(din(der(z2)),z1,z2,z0) (20)
u41(dout(z0),z1) → u42(din(der(z0)),z1,z0) (24)
din(der(plus(z0,z1))) → u21(din(der(z0)),z0,z1) (10)
u42(dout(z0),z1,z2) → dout(z0) (26)
u21(dout(z0),z1,z2) → u22(din(der(z2)),z1,z2,z0) (16)
din(der(der(z0))) → u41(din(der(z0)),z0) (14)

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).