Runtime Complexity of the query pattern
sublist(a,g)
w.r.t. the given Prolog program could be shown to be BOUNDS(O(1), O(n^2)).

(0) Obligation:

Clauses:

append([], Ys, Ys).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).
sublist(X, Y) :- ','(append(P, X1, Y), append(X2, X, P)).

Query: sublist(a,g)

(1) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="1: sublist(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: sublist(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: ','(append(X15, X16, T11), append(X17, T12, X15))\n\nT11 is ground\nX15 is free\nX16 is free\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: append(X15, X16, T11)\n\nT11 is ground\nX15 is free\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: append(X17, T12, T15)\n\nT15 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: append(X15, X16, T11), SCOPE: 2, CLAUSE: 0 | append(X15, X16, T11), SCOPE: 2, CLAUSE: 1\n\nT11 is ground\nX15 is free\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: true | append(X15, X16, T20), SCOPE: 2, CLAUSE: 1\n\nT20 is ground\nX15 is free\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: append(X15, X16, T20), SCOPE: 2, CLAUSE: 1\n\nT20 is ground\nX15 is free\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: append(X48, X49, T26)\n\nT26 is ground\nX48 is free\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: append(X17, T12, T15), SCOPE: 3, CLAUSE: 0 | append(X17, T12, T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: true | append(X17, T12, T32), SCOPE: 3, CLAUSE: 1\n\nT32 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: append(X17, T12, T15), SCOPE: 3, CLAUSE: 1\n\nT15 is ground\nX17 is free\nX56 is free\nappend(X17, T12, T15) !=? append([], X56, X56)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: append(X17, T12, T32), SCOPE: 3, CLAUSE: 1\n\nT32 is ground\nX17 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: append(X74, T42, T41)\n\nT41 is ground\nX74 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: append(X94, T54, T53)\n\nT52 is ground\nT53 is ground\nX17 is free\nX56 is free\nX94 is free\nappend(X17, T12, .(T52, T53)) !=? append([], X56, X56)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 41 [arrowhead = none ];
41 -> 4;

42 [label="ONLY EVAL with clause\nsublist(X13, X14) :- ','(append(X15, X16, X14), append(X17, X13, X15)).\nand substitutionT1 -> T12,\nX13 -> T12,\nT2 -> T11,\nX14 -> T11,\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 42 [arrowhead = none ];
42 -> 7;

43 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
7 -> 43 [arrowhead = none ];
43 -> 11;

44 [label="SPLIT 2\nnew knowledge:\nT15 is ground\nT16 is ground\nT11 is ground\nreplacements:X15 -> T15,\nX16 -> T16", fontsize=14, style = filled, fillcolor = violet];
7 -> 44 [arrowhead = none ];
44 -> 13;

45 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
11 -> 45 [arrowhead = none ];
45 -> 16;

46 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
13 -> 46 [arrowhead = none ];
46 -> 26;

47 [label="ONLY EVAL with clause\nappend([], X27, X27).\nand substitutionX15 -> [],\nX16 -> T20,\nX27 -> T20,\nT11 -> T20,\nX28 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 47 [arrowhead = none ];
47 -> 18;

48 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 48 [arrowhead = none ];
48 -> 20;

49 [label="EVAL with clause\nappend(.(X43, X44), X45, .(X43, X46)) :- append(X44, X45, X46).\nand substitutionX43 -> T25,\nX44 -> X48,\nX15 -> .(T25, X48),\nX16 -> X49,\nX45 -> X49,\nX47 -> T25,\nX46 -> T26,\nT20 -> .(T25, T26)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 49 [arrowhead = none ];
49 -> 22;

50 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
20 -> 50 [arrowhead = none ];
50 -> 23;

51 [label="INSTANCE with matching:\nX15 -> X48\nX16 -> X49\nT11 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
22 -> 51 [arrowhead = none , style=dashed];
51 -> 11[style=dashed];

52 [label="EVAL with clause\nappend([], X56, X56).\nand substitutionX17 -> [],\nT12 -> T32,\nX56 -> T32,\nT15 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
26 -> 52 [arrowhead = none ];
52 -> 27;

53 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 53 [arrowhead = none ];
53 -> 30;

54 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
27 -> 54 [arrowhead = none ];
54 -> 31;

55 [label="EVAL with clause\nappend(.(X89, X90), X91, .(X89, X92)) :- append(X90, X91, X92).\nand substitutionX89 -> T52,\nX90 -> X94,\nX17 -> .(T52, X94),\nT12 -> T54,\nX91 -> T54,\nX93 -> T52,\nX92 -> T53,\nT15 -> .(T52, T53),\nT51 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 55 [arrowhead = none ];
55 -> 39;

56 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
30 -> 56 [arrowhead = none ];
56 -> 40;

57 [label="EVAL with clause\nappend(.(X69, X70), X71, .(X69, X72)) :- append(X70, X71, X72).\nand substitutionX69 -> T40,\nX70 -> X74,\nX17 -> .(T40, X74),\nT12 -> T42,\nX71 -> T42,\nX73 -> T40,\nX72 -> T41,\nT32 -> .(T40, T41),\nT39 -> T42", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 57 [arrowhead = none ];
57 -> 35;

58 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 58 [arrowhead = none ];
58 -> 36;

59 [label="INSTANCE with matching:\nX17 -> X74\nT12 -> T42\nT15 -> T41", fontsize=14, style = filled, fillcolor = lightgrey];
35 -> 59 [arrowhead = none , style=dashed];
59 -> 13[style=dashed];

60 [label="INSTANCE with matching:\nX17 -> X94\nT12 -> T54\nT15 -> T53", fontsize=14, style = filled, fillcolor = lightgrey];
39 -> 60 [arrowhead = none , style=dashed];
60 -> 13[style=dashed];

}

(2) Obligation:

Complex Complexity Dependency Tuples Problem
MAX

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

Complex Complexity Dependency Tuples Problem
MULTIPLY

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(3) MaxProof (BOTH BOUNDS(ID, ID) transformation)

Took the maximum complexity of the problems.

(4) Complex Obligation (MAX)

(5) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(6) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(7) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(U1'(f7_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(U10'(f13_in(z0), z2, z0, z1))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))

S tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F1_IN(z0) → c7(U1'(f7_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, U2', F11_IN, U5', F13_IN, F1_IN, U9'

Compound Symbols:

c2, c3, c1, c4, c2, c5, c7

(8) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing tuple parts

(9) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F1_IN(z0) → c7

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(10) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F1_IN(z0) → c7(F7_IN(z0))
F1_IN(z0) → c7
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7
U5'(f11_out1(z0, z1), z2) → c4

Now S is empty

(11) BOUNDS(O(1), O(1))

(12) Obligation:

Complex Complexity Dependency Tuples Problem
MULTIPLY

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(13) MultiplicationProof (BOTH BOUNDS(ID, ID) transformation)

Multiplied the complexity of the problems.

(14) Complex Obligation (MULT)

(15) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(16) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(17) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(U1'(f7_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(U10'(f13_in(z0), z2, z0, z1))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))

S tuples:

F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, U2', F11_IN, U5', F13_IN, F1_IN, U9'

Compound Symbols:

c2, c3, c1, c4, c2, c5, c7

(18) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing tuple parts

(19) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:

F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(20) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4

We considered the (Usable) Rules:

f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)

And the Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = 0   
POL(F11_IN(x₁)) = 0   
POL(F13_IN(x₁)) = 0   
POL(F1_IN(x₁)) = [3] + [2]x₁   
POL(F7_IN(x₁)) = [3] + x₁   
POL(U2'(x₁, x₂)) = [3]   
POL(U4(x₁, x₂)) = 0   
POL(U5'(x₁, x₂)) = [2]   
POL(U9'(x₁, x₂)) = [1] + x₂   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3) = 0   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c7) = 0   
POL(c7(x₁)) = x₁   
POL(f11_in(x₁)) = 0   
POL(f11_out1(x₁, x₂)) = 0   

(21) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:

F11_IN(.(z0, z1)) → c1(F11_IN(z1))

K tuples:

F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(22) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F11_IN(.(z0, z1)) → c1(F11_IN(z1))

We considered the (Usable) Rules:

f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)

And the Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [2] + x₂   
POL(F11_IN(x₁)) = [1] + [2]x₁   
POL(F13_IN(x₁)) = [1]   
POL(F1_IN(x₁)) = [3] + [2]x₁   
POL(F7_IN(x₁)) = [2] + [2]x₁   
POL(U2'(x₁, x₂)) = [1] + x₂   
POL(U4(x₁, x₂)) = 0   
POL(U5'(x₁, x₂)) = [2] + x₂   
POL(U9'(x₁, x₂)) = [2] + x₂   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3) = 0   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c7) = 0   
POL(c7(x₁)) = x₁   
POL(f11_in(x₁)) = 0   
POL(f11_out1(x₁, x₂)) = 0   

(23) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:none
K tuples:

F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4
F11_IN(.(z0, z1)) → c1(F11_IN(z1))

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(24) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(25) BOUNDS(O(1), O(1))

(26) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F1_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
F7_IN(z0) → c3(U5'(f11_in(z0), z0), F11_IN(z0))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

S tuples:

F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c6(U10'(f13_in(z0), z2, z0, z1), F13_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F1_IN, F7_IN, U2', F11_IN, U5', F13_IN, U9'

Compound Symbols:

c, c2, c3, c1, c3, c4, c2, c5, c6

(27) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(28) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
U2'(f11_out1(z0, z1), z2) → c3(U3'(f13_in(z0), z2, z0, z1))
F11_IN(.(z0, z1)) → c1(U4'(f11_in(z1), .(z0, z1)), F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4(U6'(f13_in(z0), z2, z0, z1))
F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(U1'(f7_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(U10'(f13_in(z0), z2, z0, z1))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))

S tuples:

F13_IN(.(z0, z1)) → c1(U7'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F13_IN(.(z0, z1)) → c2(U8'(f13_in(z1), .(z0, z1)), F13_IN(z1))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c7(U10'(f13_in(z0), z2, z0, z1))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, U2', F11_IN, U5', F13_IN, F1_IN, U9'

Compound Symbols:

c2, c3, c1, c4, c2, c5, c7

(29) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 7 trailing tuple parts

(30) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:

F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
U9'(f11_out1(z0, z1), z2) → c7

K tuples:none
Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(31) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7

We considered the (Usable) Rules:

f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)

And the Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = 0   
POL(F11_IN(x₁)) = [3]   
POL(F13_IN(x₁)) = 0   
POL(F1_IN(x₁)) = [3] + [3]x₁   
POL(F7_IN(x₁)) = [3] + [3]x₁   
POL(U2'(x₁, x₂)) = x₂   
POL(U4(x₁, x₂)) = 0   
POL(U5'(x₁, x₂)) = [3]x₂   
POL(U9'(x₁, x₂)) = [1] + [2]x₂   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3) = 0   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c7) = 0   
POL(c7(x₁)) = x₁   
POL(f11_in(x₁)) = 0   
POL(f11_out1(x₁, x₂)) = 0   

(32) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:

F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))

K tuples:

F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(33) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))

We considered the (Usable) Rules:

f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)

And the Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₂   
POL(F11_IN(x₁)) = [1] + x₁   
POL(F13_IN(x₁)) = x₁   
POL(F1_IN(x₁)) = [2] + [3]x₁   
POL(F7_IN(x₁)) = [1] + [3]x₁   
POL(U2'(x₁, x₂)) = [1] + x₂   
POL(U4(x₁, x₂)) = [1] + x₁   
POL(U5'(x₁, x₂)) = [1]   
POL(U9'(x₁, x₂)) = [2]x₁   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c3) = 0   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c7) = 0   
POL(c7(x₁)) = x₁   
POL(f11_in(x₁)) = x₁   
POL(f11_out1(x₁, x₂)) = x₁   

(34) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1, z2, z3), z4) → f1_out1(z3)
f7_in(z0) → U2(f11_in(z0), z0)
f7_in(z0) → U5(f11_in(z0), z0)
f7_in(z0) → U9(f11_in(z0), z0)
U2(f11_out1(z0, z1), z2) → U3(f13_in(z0), z2, z0, z1)
U3(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f11_in(z0) → f11_out1([], z0)
f11_in(.(z0, z1)) → U4(f11_in(z1), .(z0, z1))
U4(f11_out1(z0, z1), .(z2, z3)) → f11_out1(.(z2, z0), z1)
U5(f11_out1(z0, z1), z2) → U6(f13_in(z0), z2, z0, z1)
U6(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)
f13_in(z0) → f13_out1([], z0)
f13_in(.(z0, z1)) → U7(f13_in(z1), .(z0, z1))
f13_in(.(z0, z1)) → U8(f13_in(z1), .(z0, z1))
U7(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U8(f13_out1(z0, z1), .(z2, z3)) → f13_out1(.(z2, z0), z1)
U9(f11_out1(z0, z1), z2) → U10(f13_in(z0), z2, z0, z1)
U10(f13_out1(z0, z1), z2, z3, z4) → f7_out1(z3, z4, z0, z1)

Tuples:

F7_IN(z0) → c2(U2'(f11_in(z0), z0))
F7_IN(z0) → c5(U9'(f11_in(z0), z0))
F1_IN(z0) → c7(F7_IN(z0))
F7_IN(z0) → c7(U5'(f11_in(z0), z0))
F7_IN(z0) → c7(F11_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U2'(f11_out1(z0, z1), z2) → c3
F11_IN(.(z0, z1)) → c1(F11_IN(z1))
U5'(f11_out1(z0, z1), z2) → c4
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))
F1_IN(z0) → c7
U9'(f11_out1(z0, z1), z2) → c7

S tuples:none
K tuples:

F7_IN(z0) → c5(U9'(f11_in(z0), z0))
U9'(f11_out1(z0, z1), z2) → c7(F13_IN(z0))
U9'(f11_out1(z0, z1), z2) → c7
F13_IN(.(z0, z1)) → c1(F13_IN(z1))
F13_IN(.(z0, z1)) → c2(F13_IN(z1))

Defined Rule Symbols:

f1_in, U1, f7_in, U2, U3, f11_in, U4, U5, U6, f13_in, U7, U8, U9, U10

Defined Pair Symbols:

F7_IN, F1_IN, U9', U2', F11_IN, U5', F13_IN

Compound Symbols:

c2, c5, c7, c3, c1, c4, c7

(35) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(36) BOUNDS(O(1), O(1))

(37) PrologToCdtProblemTransformerProof (UPPER BOUND (ID) transformation)

Built complexity over-approximating cdt problems from derivation graph.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="2: sublist(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: sublist(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(append(X7, X8, T6), append(X9, T7, X7))\n\nT6 is ground\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(append(X7, X8, T6), append(X9, T7, X7)), SCOPE: 2, CLAUSE: 0 | ','(append(X7, X8, T6), append(X9, T7, X7)), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: append(X9, T7, []) | ','(append(X7, X8, T12), append(X9, T7, X7)), SCOPE: 2, CLAUSE: 1\n\nT12 is ground\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: append(X9, T7, [])\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(append(X7, X8, T12), append(X9, T7, X7)), SCOPE: 2, CLAUSE: 1\n\nT12 is ground\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: append(X9, T7, []), SCOPE: 3, CLAUSE: 0 | append(X9, T7, []), SCOPE: 3, CLAUSE: 1\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true | append(X9, T7, []), SCOPE: 3, CLAUSE: 1\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: append(X9, T7, []), SCOPE: 3, CLAUSE: 1\n\nX9 is free\nX24 is free\nappend(X9, T7, []) !=? append([], X24, X24)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: append(X9, T7, []), SCOPE: 3, CLAUSE: 1\n\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(append(X56, X57, T27), append(X9, T7, .(T26, X56)))\n\nT26 is ground\nT27 is ground\nX9 is free\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: append(X56, X57, T27)\n\nT27 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: append(X9, T7, .(T26, T35))\n\nT26 is ground\nT35 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: append(X56, X57, T27), SCOPE: 4, CLAUSE: 0 | append(X56, X57, T27), SCOPE: 4, CLAUSE: 1\n\nT27 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: true | append(X56, X57, T40), SCOPE: 4, CLAUSE: 1\n\nT40 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: append(X56, X57, T40), SCOPE: 4, CLAUSE: 1\n\nT40 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: append(X89, X90, T46)\n\nT46 is ground\nX89 is free\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: append(X9, T7, .(T26, T35)), SCOPE: 5, CLAUSE: 0 | append(X9, T7, .(T26, T35)), SCOPE: 5, CLAUSE: 1\n\nT26 is ground\nT35 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true | append(X9, T7, .(T61, T62)), SCOPE: 5, CLAUSE: 1\n\nT61 is ground\nT62 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: append(X9, T7, .(T26, T35)), SCOPE: 5, CLAUSE: 1\n\nT26 is ground\nT35 is ground\nX9 is free\nX97 is free\nappend(X9, T7, .(T26, T35)) !=? append([], X97, X97)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: append(X9, T7, .(T61, T62)), SCOPE: 5, CLAUSE: 1\n\nT61 is ground\nT62 is ground\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: append(X117, T75, T74)\n\nT74 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: append(X117, T75, T74), SCOPE: 6, CLAUSE: 0 | append(X117, T75, T74), SCOPE: 6, CLAUSE: 1\n\nT74 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true | append(X117, T75, T80), SCOPE: 6, CLAUSE: 1\n\nT80 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: append(X117, T75, T74), SCOPE: 6, CLAUSE: 1\n\nT74 is ground\nX117 is free\nX122 is free\nappend(X117, T75, T74) !=? append([], X122, X122)", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: append(X117, T75, T80), SCOPE: 6, CLAUSE: 1\n\nT80 is ground\nX117 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: append(X140, T90, T89)\n\nT89 is ground\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: append(X160, T102, T101)\n\nT100 is ground\nT101 is ground\nX117 is free\nX122 is free\nX160 is free\nappend(X117, T75, .(T100, T101)) !=? append([], X122, X122)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: append(X182, T117, T116)\n\nT115 is ground\nT116 is ground\nX9 is free\nX97 is free\nX182 is free\nappend(X9, T7, .(T115, T116)) !=? append([], X97, X97)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 58 [arrowhead = none ];
58 -> 3;

59 [label="ONLY EVAL with clause\nsublist(X5, X6) :- ','(append(X7, X8, X6), append(X9, X5, X7)).\nand substitutionT1 -> T7,\nX5 -> T7,\nT2 -> T6,\nX6 -> T6,\nT5 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 59 [arrowhead = none ];
59 -> 5;

60 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
5 -> 60 [arrowhead = none ];
60 -> 6;

61 [label="ONLY EVAL with clause\nappend([], X16, X16).\nand substitutionX7 -> [],\nX8 -> T12,\nX16 -> T12,\nT6 -> T12,\nX17 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 61 [arrowhead = none ];
61 -> 8;

62 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
8 -> 62 [arrowhead = none ];
62 -> 9;

63 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
8 -> 63 [arrowhead = none ];
63 -> 10;

64 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
9 -> 64 [arrowhead = none ];
64 -> 12;

65 [label="EVAL with clause\nappend(.(X51, X52), X53, .(X51, X54)) :- append(X52, X53, X54).\nand substitutionX51 -> T26,\nX52 -> X56,\nX7 -> .(T26, X56),\nX8 -> X57,\nX53 -> X57,\nX55 -> T26,\nX54 -> T27,\nT12 -> .(T26, T27)", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 65 [arrowhead = none ];
65 -> 24;

66 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 66 [arrowhead = none ];
66 -> 25;

67 [label="EVAL with clause\nappend([], X24, X24).\nand substitutionX9 -> [],\nT7 -> [],\nX24 -> [],\nT19 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 67 [arrowhead = none ];
67 -> 14;

68 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
12 -> 68 [arrowhead = none ];
68 -> 15;

69 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 69 [arrowhead = none ];
69 -> 17;

70 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
15 -> 70 [arrowhead = none ];
70 -> 21;

71 [label="BACKTRACK\nfor clause: append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 71 [arrowhead = none ];
71 -> 19;

72 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
24 -> 72 [arrowhead = none ];
72 -> 28;

73 [label="SPLIT 2\nnew knowledge:\nT35 is ground\nT36 is ground\nT27 is ground\nreplacements:X56 -> T35,\nX57 -> T36", fontsize=14, style = filled, fillcolor = violet];
24 -> 73 [arrowhead = none ];
73 -> 29;

74 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
28 -> 74 [arrowhead = none ];
74 -> 32;

75 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
29 -> 75 [arrowhead = none ];
75 -> 41;

76 [label="ONLY EVAL with clause\nappend([], X68, X68).\nand substitutionX56 -> [],\nX57 -> T40,\nX68 -> T40,\nT27 -> T40,\nX69 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 76 [arrowhead = none ];
76 -> 33;

77 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
33 -> 77 [arrowhead = none ];
77 -> 34;

78 [label="EVAL with clause\nappend(.(X84, X85), X86, .(X84, X87)) :- append(X85, X86, X87).\nand substitutionX84 -> T45,\nX85 -> X89,\nX56 -> .(T45, X89),\nX57 -> X90,\nX86 -> X90,\nX88 -> T45,\nX87 -> T46,\nT40 -> .(T45, T46)", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 78 [arrowhead = none ];
78 -> 37;

79 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
34 -> 79 [arrowhead = none ];
79 -> 38;

80 [label="INSTANCE with matching:\nX56 -> X89\nX57 -> X90\nT27 -> T46", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 80 [arrowhead = none , style=dashed];
80 -> 28[style=dashed];

81 [label="EVAL with clause\nappend([], X97, X97).\nand substitutionX9 -> [],\nT7 -> .(T61, T62),\nX97 -> .(T61, T62),\nT26 -> T61,\nT35 -> T62,\nT60 -> .(T61, T62)", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 81 [arrowhead = none ];
81 -> 42;

82 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 82 [arrowhead = none ];
82 -> 43;

83 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 83 [arrowhead = none ];
83 -> 44;

84 [label="ONLY EVAL with clause\nappend(.(X177, X178), X179, .(X177, X180)) :- append(X178, X179, X180).\nand substitutionX177 -> T115,\nX178 -> X182,\nX9 -> .(T115, X182),\nT7 -> T117,\nX179 -> T117,\nT26 -> T115,\nX181 -> T115,\nT35 -> T116,\nX180 -> T116,\nT114 -> T117", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 84 [arrowhead = none ];
84 -> 57;

85 [label="ONLY EVAL with clause\nappend(.(X112, X113), X114, .(X112, X115)) :- append(X113, X114, X115).\nand substitutionX112 -> T73,\nX113 -> X117,\nX9 -> .(T73, X117),\nT7 -> T75,\nX114 -> T75,\nT61 -> T73,\nX116 -> T73,\nT62 -> T74,\nX115 -> T74,\nT72 -> T75", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 85 [arrowhead = none ];
85 -> 45;

86 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
45 -> 86 [arrowhead = none ];
86 -> 46;

87 [label="EVAL with clause\nappend([], X122, X122).\nand substitutionX117 -> [],\nT75 -> T80,\nX122 -> T80,\nT74 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 87 [arrowhead = none ];
87 -> 47;

88 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
46 -> 88 [arrowhead = none ];
88 -> 48;

89 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 89 [arrowhead = none ];
89 -> 49;

90 [label="EVAL with clause\nappend(.(X155, X156), X157, .(X155, X158)) :- append(X156, X157, X158).\nand substitutionX155 -> T100,\nX156 -> X160,\nX117 -> .(T100, X160),\nT75 -> T102,\nX157 -> T102,\nX159 -> T100,\nX158 -> T101,\nT74 -> .(T100, T101),\nT99 -> T102", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 90 [arrowhead = none ];
90 -> 52;

91 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 91 [arrowhead = none ];
91 -> 53;

92 [label="EVAL with clause\nappend(.(X135, X136), X137, .(X135, X138)) :- append(X136, X137, X138).\nand substitutionX135 -> T88,\nX136 -> X140,\nX117 -> .(T88, X140),\nT75 -> T90,\nX137 -> T90,\nX139 -> T88,\nX138 -> T89,\nT80 -> .(T88, T89),\nT87 -> T90", fontsize=14, style = filled, fillcolor = lightblue];
49 -> 92 [arrowhead = none ];
92 -> 50;

93 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 93 [arrowhead = none ];
93 -> 51;

94 [label="INSTANCE with matching:\nX117 -> X140\nT75 -> T90\nT74 -> T89", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 94 [arrowhead = none , style=dashed];
94 -> 45[style=dashed];

95 [label="INSTANCE with matching:\nX117 -> X160\nT75 -> T102\nT74 -> T101", fontsize=14, style = filled, fillcolor = lightgrey];
52 -> 95 [arrowhead = none , style=dashed];
95 -> 45[style=dashed];

96 [label="INSTANCE with matching:\nX117 -> X182\nT75 -> T117\nT74 -> T116", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 96 [arrowhead = none , style=dashed];
96 -> 45[style=dashed];

}

(38) Obligation:

Complex Complexity Dependency Tuples Problem
MAX

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

Complex Complexity Dependency Tuples Problem
MULTIPLY

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

(39) MaxProof (BOTH BOUNDS(ID, ID) transformation)

Took the maximum complexity of the problems.

(40) Complex Obligation (MAX)

(41) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

(42) CdtGraphRemoveDanglingProof (ComplexityIfPolyImplication transformation)

Removed 4 of 14 dangling nodes:

U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))

(43) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))

S tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2

(44) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(45) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F2_IN(z0) → c5(U1'(f8_in(z0), z0))
F2_IN(z0) → c5(F8_IN(z0))
F10_IN(.(z0, z1)) → c5(U2'(f24_in(z1, z0), .(z0, z1)))
F10_IN(.(z0, z1)) → c5(F24_IN(z1, z0))
F8_IN(z0) → c5(U5'(f9_in, f10_in(z0), z0))
F8_IN(z0) → c5(F9_IN)
F8_IN(z0) → c5(F10_IN(z0))
F24_IN(z0, z1) → c5(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(F28_IN(z0))

S tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F2_IN(z0) → c5(U1'(f8_in(z0), z0))
F2_IN(z0) → c5(F8_IN(z0))
F10_IN(.(z0, z1)) → c5(U2'(f24_in(z1, z0), .(z0, z1)))
F10_IN(.(z0, z1)) → c5(F24_IN(z1, z0))
F8_IN(z0) → c5(U5'(f9_in, f10_in(z0), z0))
F8_IN(z0) → c5(F9_IN)
F8_IN(z0) → c5(F10_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, U3', F28_IN, U7', F45_IN, F2_IN, F10_IN, F8_IN

Compound Symbols:

c6, c7, c1, c4, c2, c5

(46) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 9 trailing tuple parts

(47) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F2_IN(z0) → c5(F8_IN(z0))
F10_IN(.(z0, z1)) → c5(F24_IN(z1, z0))
F8_IN(z0) → c5(F10_IN(z0))
F24_IN(z0, z1) → c5(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
F2_IN(z0) → c5
F10_IN(.(z0, z1)) → c5
F8_IN(z0) → c5

S tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F2_IN(z0) → c5(F8_IN(z0))
F10_IN(.(z0, z1)) → c5(F24_IN(z1, z0))
F8_IN(z0) → c5(F10_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F2_IN(z0) → c5
F10_IN(.(z0, z1)) → c5
F8_IN(z0) → c5

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, F2_IN, F10_IN, F8_IN, U3', F28_IN, U7', F45_IN

Compound Symbols:

c6, c5, c7, c1, c4, c2, c5

(48) CdtKnowledgeProof (EQUIVALENT transformation)

The following tuples could be moved from S to K by knowledge propagation:

F2_IN(z0) → c5(F8_IN(z0))
F8_IN(z0) → c5(F10_IN(z0))
F2_IN(z0) → c5
F10_IN(.(z0, z1)) → c5
F8_IN(z0) → c5
F8_IN(z0) → c5
F8_IN(z0) → c5(F10_IN(z0))
F8_IN(z0) → c5
F8_IN(z0) → c5
F10_IN(.(z0, z1)) → c5(F24_IN(z1, z0))
F10_IN(.(z0, z1)) → c5
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
U7'(f28_out1(z0, z1), z2, z3) → c4

Now S is empty

(49) BOUNDS(O(1), O(1))

(50) Obligation:

Complex Complexity Dependency Tuples Problem
MULTIPLY

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

(51) MultiplicationProof (BOTH BOUNDS(ID, ID) transformation)

Multiplied the complexity of the problems.

(52) Complex Obligation (MULT)

(53) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

(54) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(55) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))
F2_IN(z0) → c10(U1'(f8_in(z0), z0))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(U2'(f24_in(z1, z0), .(z0, z1)))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(U5'(f9_in, f10_in(z0), z0))
F8_IN(z0) → c10(F9_IN)
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))

S tuples:

F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, U3', F28_IN, U7', F8_IN, F45_IN, U12', F2_IN, F10_IN

Compound Symbols:

c6, c7, c1, c4, c2, c5, c8, c10

(56) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 12 trailing tuple parts

(57) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

S tuples:

F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, F2_IN, F10_IN, F8_IN, U3', F28_IN, U7', F45_IN, U12'

Compound Symbols:

c6, c5, c10, c7, c1, c4, c6, c2, c8, c10

(58) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F24_IN(z0, z1) → c10(F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6

We considered the (Usable) Rules:

f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)

And the Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1]   
POL(F10_IN(x₁)) = [1] + x₁   
POL(F24_IN(x₁, x₂)) = [2]   
POL(F28_IN(x₁)) = [1]   
POL(F2_IN(x₁)) = [2] + [2]x₁   
POL(F45_IN(x₁)) = 0   
POL(F8_IN(x₁)) = [2] + x₁   
POL(U12'(x₁, x₂, x₃)) = 0   
POL(U3'(x₁, x₂, x₃)) = [1]   
POL(U6(x₁, x₂)) = 0   
POL(U7'(x₁, x₂, x₃)) = [2]   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c10) = 0   
POL(c10(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c6) = 0   
POL(c6(x₁)) = x₁   
POL(c7) = 0   
POL(c8) = 0   
POL(f28_in(x₁)) = 0   
POL(f28_out1(x₁, x₂)) = 0   

(59) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

S tuples:

F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F28_IN(.(z0, z1)) → c1(F28_IN(z1))

K tuples:

F24_IN(z0, z1) → c10(F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6

Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, F2_IN, F10_IN, F8_IN, U3', F28_IN, U7', F45_IN, U12'

Compound Symbols:

c6, c5, c10, c7, c1, c4, c6, c2, c8, c10

(60) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))

We considered the (Usable) Rules:

f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)

And the Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₁   
POL(F10_IN(x₁)) = [2] + x₁   
POL(F24_IN(x₁, x₂)) = [2] + x₂   
POL(F28_IN(x₁)) = [1]   
POL(F2_IN(x₁)) = [3] + [3]x₁   
POL(F45_IN(x₁)) = 0   
POL(F8_IN(x₁)) = [3] + [2]x₁   
POL(U12'(x₁, x₂, x₃)) = [1]   
POL(U3'(x₁, x₂, x₃)) = x₃   
POL(U6(x₁, x₂)) = [2] + x₂   
POL(U7'(x₁, x₂, x₃)) = 0   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c10) = 0   
POL(c10(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c6) = 0   
POL(c6(x₁)) = x₁   
POL(c7) = 0   
POL(c8) = 0   
POL(f28_in(x₁)) = [3] + x₁   
POL(f28_out1(x₁, x₂)) = 0   

(61) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

S tuples:

F28_IN(.(z0, z1)) → c1(F28_IN(z1))

K tuples:

F24_IN(z0, z1) → c10(F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))

Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, F2_IN, F10_IN, F8_IN, U3', F28_IN, U7', F45_IN, U12'

Compound Symbols:

c6, c5, c10, c7, c1, c4, c6, c2, c8, c10

(62) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))) transformation)

Found a reduction pair which oriented the following tuples strictly. Hence they can be removed from S.

F28_IN(.(z0, z1)) → c1(F28_IN(z1))

We considered the (Usable) Rules:

f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)

And the Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

The order we found is given by the following interpretation:
Polynomial interpretation :

POL(.(x₁, x₂)) = [1] + x₁ + x₂   
POL(F10_IN(x₁)) = [2] + [3]x₁   
POL(F24_IN(x₁, x₂)) = [1] + [2]x₁ + [3]x₂   
POL(F28_IN(x₁)) = x₁   
POL(F2_IN(x₁)) = [2] + [3]x₁   
POL(F45_IN(x₁)) = 0   
POL(F8_IN(x₁)) = [2] + [3]x₁   
POL(U12'(x₁, x₂, x₃)) = [1] + [2]x₃   
POL(U3'(x₁, x₂, x₃)) = [1]   
POL(U6(x₁, x₂)) = 0   
POL(U7'(x₁, x₂, x₃)) = x₂ + [3]x₃   
POL([]) = 0   
POL(c1(x₁)) = x₁   
POL(c10) = 0   
POL(c10(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(c4) = 0   
POL(c5(x₁)) = x₁   
POL(c6) = 0   
POL(c6(x₁)) = x₁   
POL(c7) = 0   
POL(c8) = 0   
POL(f28_in(x₁)) = 0   
POL(f28_out1(x₁, x₂)) = 0   

(63) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

S tuples:none
K tuples:

F24_IN(z0, z1) → c10(F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F28_IN(.(z0, z1)) → c1(F28_IN(z1))

Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, F2_IN, F10_IN, F8_IN, U3', F28_IN, U7', F45_IN, U12'

Compound Symbols:

c6, c5, c10, c7, c1, c4, c6, c2, c8, c10

(64) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(65) BOUNDS(O(1), O(1))

(66) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F2_IN(z0) → c(U1'(f8_in(z0), z0), F8_IN(z0))
F10_IN(.(z0, z1)) → c4(U2'(f24_in(z1, z0), .(z0, z1)), F24_IN(z1, z0))
F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c9(U5'(f9_in, f10_in(z0), z0), F9_IN, F10_IN(z0))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
F24_IN(z0, z1) → c3(U7'(f28_in(z0), z0, z1), F28_IN(z0))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

S tuples:

F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F2_IN, F10_IN, F24_IN, U3', F8_IN, F28_IN, U7', F45_IN, U12'

Compound Symbols:

c, c4, c6, c7, c9, c1, c3, c4, c2, c5, c8

(67) CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID) transformation)

Split RHS of tuples not part of any SCC

(68) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
U3'(f28_out1(z0, z1), z2, z3) → c7(U4'(f29_in(z3, z0), z2, z3, z0, z1))
F28_IN(.(z0, z1)) → c1(U6'(f28_in(z1), .(z0, z1)), F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4(U8'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c6(U9'(f9_in, f10_in(z0), z0))
F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))
F2_IN(z0) → c10(U1'(f8_in(z0), z0))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(U2'(f24_in(z1, z0), .(z0, z1)))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(U5'(f9_in, f10_in(z0), z0))
F8_IN(z0) → c10(F9_IN)
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))

S tuples:

F45_IN(.(z0, z1)) → c1(U10'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F45_IN(.(z0, z1)) → c2(U11'(f45_in(z1), .(z0, z1)), F45_IN(z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
U12'(f28_out1(z0, z1), z2, z3) → c6(U13'(f29_in(z3, z0), z2, z3, z0, z1))
F8_IN(z0) → c8(U14'(f9_in, f10_in(z0), z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, U3', F28_IN, U7', F8_IN, F45_IN, U12', F2_IN, F10_IN

Compound Symbols:

c6, c7, c1, c4, c2, c5, c8, c10

(69) CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID) transformation)

Removed 12 trailing tuple parts

(70) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f8_in(z0), z0)
U1(f8_out1(z0, z1), z2) → f2_out1(z1)
U1(f8_out2(z0, z1, z2, z3), z4) → f2_out1(z3)
f9_in → f9_out1([], [])
f10_in(.(z0, z1)) → U2(f24_in(z1, z0), .(z0, z1))
U2(f24_out1(z0, z1, z2, z3), .(z4, z5)) → f10_out1(.(z4, z0), z1, z2, z3)
f24_in(z0, z1) → U3(f28_in(z0), z0, z1)
f24_in(z0, z1) → U7(f28_in(z0), z0, z1)
f24_in(z0, z1) → U12(f28_in(z0), z0, z1)
U3(f28_out1(z0, z1), z2, z3) → U4(f29_in(z3, z0), z2, z3, z0, z1)
U4(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
f8_in(z0) → U5(f9_in, f10_in(z0), z0)
f8_in(z0) → U9(f9_in, f10_in(z0), z0)
f8_in(z0) → U14(f9_in, f10_in(z0), z0)
U5(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U5(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f28_in(z0) → f28_out1([], z0)
f28_in(.(z0, z1)) → U6(f28_in(z1), .(z0, z1))
U6(f28_out1(z0, z1), .(z2, z3)) → f28_out1(.(z2, z0), z1)
U7(f28_out1(z0, z1), z2, z3) → U8(f29_in(z3, z0), z2, z3, z0, z1)
U8(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U9(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U9(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)
f45_in(z0) → f45_out1([], z0)
f45_in(.(z0, z1)) → U10(f45_in(z1), .(z0, z1))
f45_in(.(z0, z1)) → U11(f45_in(z1), .(z0, z1))
U10(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U11(f45_out1(z0, z1), .(z2, z3)) → f45_out1(.(z2, z0), z1)
U12(f28_out1(z0, z1), z2, z3) → U13(f29_in(z3, z0), z2, z3, z0, z1)
U13(f29_out1(z0, z1), z2, z3, z4, z5) → f24_out1(z4, z5, z0, z1)
U14(f9_out1(z0, z1), z2, z3) → f8_out1(z0, z1)
U14(z0, f10_out1(z1, z2, z3, z4), z5) → f8_out2(z1, z2, z3, z4)

Tuples:

F24_IN(z0, z1) → c6(U3'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F2_IN(z0) → c10(F8_IN(z0))
F10_IN(.(z0, z1)) → c10(F24_IN(z1, z0))
F8_IN(z0) → c10(F10_IN(z0))
F24_IN(z0, z1) → c10(U7'(f28_in(z0), z0, z1))
F24_IN(z0, z1) → c10(F28_IN(z0))
U3'(f28_out1(z0, z1), z2, z3) → c7
F28_IN(.(z0, z1)) → c1(F28_IN(z1))
U7'(f28_out1(z0, z1), z2, z3) → c4
F8_IN(z0) → c6
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8
F2_IN(z0) → c10
F10_IN(.(z0, z1)) → c10
F8_IN(z0) → c10

S tuples:

F24_IN(z0, z1) → c5(U12'(f28_in(z0), z0, z1))
F45_IN(.(z0, z1)) → c1(F45_IN(z1))
F45_IN(.(z0, z1)) → c2(F45_IN(z1))
U12'(f28_out1(z0, z1), z2, z3) → c6
F8_IN(z0) → c8

K tuples:none
Defined Rule Symbols:

f2_in, U1, f9_in, f10_in, U2, f24_in, U3, U4, f8_in, U5, f28_in, U6, U7, U8, U9, f45_in, U10, U11, U12, U13, U14

Defined Pair Symbols:

F24_IN, F2_IN, F10_IN, F8_IN, U3', F28_IN, U7', F45_IN, U12'

Compound Symbols:

c6, c5, c10, c7, c1, c4, c6, c2, c8, c10