Certification Problem

Input (TPDB Runtime_Complexity_Innermost_Rewriting/raML/subtrees.raml)

The rewrite relation of the following TRS is considered.

append(@l1,@l2) → append#1(@l1,@l2) (1)
append#1(::(@x,@xs),@l2) → ::(@x,append(@xs,@l2)) (2)
append#1(nil,@l2) → @l2 (3)
subtrees(@t) → subtrees#1(@t) (4)
subtrees#1(leaf) → nil (5)
subtrees#1(node(@x,@t1,@t2)) → subtrees#2(subtrees(@t1),@t1,@t2,@x) (6)
subtrees#2(@l1,@t1,@t2,@x) → subtrees#3(subtrees(@t2),@l1,@t1,@t2,@x) (7)
subtrees#3(@l2,@l1,@t1,@t2,@x) → ::(node(@x,@t1,@t2),append(@l1,@l2)) (8)
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:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
originates from
append(z0,z1) → append#1(z0,z1) (9)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
originates from
append#1(::(z0,z1),z2) → ::(z0,append(z1,z2)) (11)
append#1#(nil,z0) → c2 (14)
originates from
append#1(nil,z0) → z0 (13)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
originates from
subtrees(z0) → subtrees#1(z0) (15)
subtrees#1#(leaf) → c4 (17)
originates from
subtrees#1(leaf) → nil (5)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
originates from
subtrees#1(node(z0,z1,z2)) → subtrees#2(subtrees(z1),z1,z2,z0) (18)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
originates from
subtrees#2(z0,z1,z2,z3) → subtrees#3(subtrees(z2),z0,z1,z2,z3) (20)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)
originates from
subtrees#3(z0,z1,z2,z3,z4) → ::(node(z4,z2,z3),append(z1,z0)) (22)
Moreover, we add the following terms to the innermost strategy.
append#(z0,z1)
append#1#(::(z0,z1),z2)
append#1#(nil,z0)
subtrees#(z0)
subtrees#1#(leaf)
subtrees#1#(node(z0,z1,z2))
subtrees#2#(z0,z1,z2,z3)
subtrees#3#(z0,z1,z2,z3,z4)

1.1 Rule Shifting

The rules
append#1#(nil,z0) → c2 (14)
subtrees#1#(leaf) → c4 (17)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[append#1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[subtrees(x1)] = 0
[subtrees#1(x1)] = 0
[subtrees#2(x1,...,x4)] = 1 · x1 + 0
[subtrees#3(x1,...,x5)] = 1 · x1 + 0 + 1 · x2
[append#(x1, x2)] = 1 + 1 · x1 + 1 · x2
[append#1#(x1, x2)] = 1 + 1 · x1 + 1 · x2
[subtrees#(x1)] = 1 · x1 + 0
[subtrees#1#(x1)] = 1 · x1 + 0
[subtrees#2#(x1,...,x4)] = 1 + 1 · x1 + 1 · x3 + 1 · x4
[subtrees#3#(x1,...,x5)] = 1 + 1 · x1 + 1 · x2 + 1 · x5
[leaf] = 1
[nil] = 0
[node(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[::(x1, x2)] = 1 · x2 + 0
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)
subtrees#3(z0,z1,z2,z3,z4) → ::(node(z4,z2,z3),append(z1,z0)) (22)
subtrees#2(z0,z1,z2,z3) → subtrees#3(subtrees(z2),z0,z1,z2,z3) (20)
append(z0,z1) → append#1(z0,z1) (9)
append#1(nil,z0) → z0 (13)
subtrees(z0) → subtrees#1(z0) (15)
subtrees#1(node(z0,z1,z2)) → subtrees#2(subtrees(z1),z1,z2,z0) (18)
subtrees#1(leaf) → nil (5)
append#1(::(z0,z1),z2) → ::(z0,append(z1,z2)) (11)

1.1.1 Rule Shifting

The rules
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 3 · x1 + 0 + 3 · x2
[append#1(x1, x2)] = 2 · x1 + 0 + 3 · x2
[subtrees(x1)] = 0
[subtrees#1(x1)] = 3 + 3 · x1
[subtrees#2(x1,...,x4)] = 3 + 3 · x1 + 3 · x2 + 3 · x3 + 3 · x4
[subtrees#3(x1,...,x5)] = 3 + 3 · x1 + 3 · x2 + 3 · x3 + 3 · x4 + 3 · x5
[append#(x1, x2)] = 0
[append#1#(x1, x2)] = 0
[subtrees#(x1)] = 2 · x1 + 0
[subtrees#1#(x1)] = 2 · x1 + 0
[subtrees#2#(x1,...,x4)] = 2 · x3 + 0 + 2 · x4
[subtrees#3#(x1,...,x5)] = 2 · x5 + 0
[leaf] = 3
[nil] = 3
[node(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[::(x1, x2)] = 2
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)

1.1.1.1 Rule Shifting

The rules
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 + 1 · x1 + 1 · x2
[append#1(x1, x2)] = 1 + 1 · x1 + 1 · x2
[subtrees(x1)] = 1 + 1 · x1
[subtrees#1(x1)] = 1 + 1 · x1
[subtrees#2(x1,...,x4)] = 1 + 1 · x1 + 1 · x3 + 1 · x4
[subtrees#3(x1,...,x5)] = 1 + 1 · x2 + 1 · x4 + 1 · x5
[append#(x1, x2)] = 0
[append#1#(x1, x2)] = 0
[subtrees#(x1)] = 1 · x1 + 0
[subtrees#1#(x1)] = 1 · x1 + 0
[subtrees#2#(x1,...,x4)] = 1 + 1 · x3 + 1 · x4
[subtrees#3#(x1,...,x5)] = 1 + 1 · x5
[leaf] = 1
[nil] = 0
[node(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[::(x1, x2)] = 1
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)

1.1.1.1.1 Rule Shifting

The rules
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0
[append#1(x1, x2)] = 1 + 1 · x1 + 1 · x2
[subtrees(x1)] = 1 + 1 · x1
[subtrees#1(x1)] = 1 + 1 · x1
[subtrees#2(x1,...,x4)] = 1 + 1 · x1 + 1 · x3 + 1 · x4
[subtrees#3(x1,...,x5)] = 1 + 1 · x2 + 1 · x4 + 1 · x5
[append#(x1, x2)] = 0
[append#1#(x1, x2)] = 0
[subtrees#(x1)] = 1 · x1 + 0
[subtrees#1#(x1)] = 1 · x1 + 0
[subtrees#2#(x1,...,x4)] = 1 + 1 · x3 + 1 · x4
[subtrees#3#(x1,...,x5)] = 1 · x5 + 0
[leaf] = 1
[nil] = 0
[node(x1, x2, x3)] = 1 + 1 · x1 + 1 · x2 + 1 · x3
[::(x1, x2)] = 1 + 1 · x2
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)

1.1.1.1.1.1 Rule Shifting

The rules
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
are strictly oriented by the following linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 + 3 · x1 + 3 · x2
[append#1(x1, x2)] = 1 + 3 · x1 + 3 · x2
[subtrees(x1)] = 0
[subtrees#1(x1)] = 3 + 3 · x1
[subtrees#2(x1,...,x4)] = 3 + 3 · x1 + 3 · x2 + 3 · x3 + 3 · x4
[subtrees#3(x1,...,x5)] = 3 + 3 · x1 + 3 · x2 + 3 · x3 + 3 · x4 + 3 · x5
[append#(x1, x2)] = 0
[append#1#(x1, x2)] = 0
[subtrees#(x1)] = 2 + 3 · x1
[subtrees#1#(x1)] = 3 · x1 + 0
[subtrees#2#(x1,...,x4)] = 2 + 3 · x3 + 2 · x4
[subtrees#3#(x1,...,x5)] = 2 · x5 + 0
[leaf] = 3
[nil] = 3
[node(x1, x2, x3)] = 3 + 1 · x1 + 1 · x2 + 1 · x3
[::(x1, x2)] = 3 + 1 · x2
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)

1.1.1.1.1.1.1 Rule Shifting

The rules
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[append#1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[subtrees(x1)] = 2 · x1 + 0
[subtrees#1(x1)] = 2 · x1 + 0
[subtrees#2(x1,...,x4)] = 2 + 1 · x1 + 2 · x3
[subtrees#3(x1,...,x5)] = 2 + 1 · x1 + 1 · x2
[append#(x1, x2)] = 2 · x1 + 0
[append#1#(x1, x2)] = 2 · x1 + 0
[subtrees#(x1)] = 1 · x1 · x1 + 0
[subtrees#1#(x1)] = 1 · x1 · x1 + 0
[subtrees#2#(x1,...,x4)] = 2 · x1 + 0 + 1 · x3 · x3 + 2 · x2 · x3
[subtrees#3#(x1,...,x5)] = 2 · x2 + 0 + 1 · x3 · x4
[leaf] = 0
[nil] = 0
[node(x1, x2, x3)] = 2 + 1 · x2 + 1 · x3
[::(x1, x2)] = 2 + 1 · x2
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)
subtrees#3(z0,z1,z2,z3,z4) → ::(node(z4,z2,z3),append(z1,z0)) (22)
subtrees#2(z0,z1,z2,z3) → subtrees#3(subtrees(z2),z0,z1,z2,z3) (20)
append(z0,z1) → append#1(z0,z1) (9)
append#1(nil,z0) → z0 (13)
subtrees(z0) → subtrees#1(z0) (15)
subtrees#1(node(z0,z1,z2)) → subtrees#2(subtrees(z1),z1,z2,z0) (18)
subtrees#1(leaf) → nil (5)
append#1(::(z0,z1),z2) → ::(z0,append(z1,z2)) (11)

1.1.1.1.1.1.1.1 Rule Shifting

The rules
append#(z0,z1) → c(append#1#(z0,z1)) (10)
are strictly oriented by the following non-linear polynomial interpretation over the naturals
[c(x1)] = 1 · x1 + 0
[c1(x1)] = 1 · x1 + 0
[c2] = 0
[c3(x1)] = 1 · x1 + 0
[c4] = 0
[c5(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c6(x1, x2)] = 1 · x1 + 0 + 1 · x2
[c7(x1)] = 1 · x1 + 0
[append(x1, x2)] = 1 · x1 + 0 + 1 · x2
[append#1(x1, x2)] = 1 · x1 + 0 + 1 · x2
[subtrees(x1)] = 2 · x1 + 0
[subtrees#1(x1)] = 2 · x1 + 0
[subtrees#2(x1,...,x4)] = 1 + 1 · x1 + 2 · x3
[subtrees#3(x1,...,x5)] = 1 + 1 · x1 + 1 · x2
[append#(x1, x2)] = 2 + 2 · x1
[append#1#(x1, x2)] = 2 · x1 + 0
[subtrees#(x1)] = 2 · x1 · x1 + 0
[subtrees#1#(x1)] = 2 · x1 · x1 + 0
[subtrees#2#(x1,...,x4)] = 2 + 2 · x1 + 2 · x3 · x1 + 2 · x3 · x3
[subtrees#3#(x1,...,x5)] = 2 + 2 · x2 + 1 · x2 · x4
[leaf] = 0
[nil] = 0
[node(x1, x2, x3)] = 2 + 1 · x2 + 1 · x3
[::(x1, x2)] = 1 + 1 · x2
which has the intended complexity. Here, only the following usable rules have been considered:
append#(z0,z1) → c(append#1#(z0,z1)) (10)
append#1#(::(z0,z1),z2) → c1(append#(z1,z2)) (12)
append#1#(nil,z0) → c2 (14)
subtrees#(z0) → c3(subtrees#1#(z0)) (16)
subtrees#1#(leaf) → c4 (17)
subtrees#1#(node(z0,z1,z2)) → c5(subtrees#2#(subtrees(z1),z1,z2,z0),subtrees#(z1)) (19)
subtrees#2#(z0,z1,z2,z3) → c6(subtrees#3#(subtrees(z2),z0,z1,z2,z3),subtrees#(z2)) (21)
subtrees#3#(z0,z1,z2,z3,z4) → c7(append#(z1,z0)) (23)
subtrees#3(z0,z1,z2,z3,z4) → ::(node(z4,z2,z3),append(z1,z0)) (22)
subtrees#2(z0,z1,z2,z3) → subtrees#3(subtrees(z2),z0,z1,z2,z3) (20)
append(z0,z1) → append#1(z0,z1) (9)
append#1(nil,z0) → z0 (13)
subtrees(z0) → subtrees#1(z0) (15)
subtrees#1(node(z0,z1,z2)) → subtrees#2(subtrees(z1),z1,z2,z0) (18)
subtrees#1(leaf) → nil (5)
append#1(::(z0,z1),z2) → ::(z0,append(z1,z2)) (11)

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