Runtime Complexity proof of /tmp/tmp34nvUv/length1.pl

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

0 Prolog

↳1 LPReorderTransformerProof (⇔, 0 ms)

↳2 Prolog

↳3 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 63 ms)

↳4 CdtProblem

    ↳5 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳6 CdtProblem

    ↳7 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 5 ms)

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 0 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 340 ms)

    ↳12 CdtProblem

    ↳13 CdtKnowledgeProof (⇔, 0 ms)

    ↳14 BOUNDS(O(1), O(1))

↳15 PrologToCdtProblemTransformerProof (UPPER BOUND (ID), 62 ms)

↳16 CdtProblem

    ↳17 CdtGraphSplitRhsProof (BOTH BOUNDS(ID, ID), 0 ms)

    ↳18 CdtProblem

    ↳19 CdtGraphRemoveTrailingTuplepartsProof (BOTH BOUNDS(ID, ID), 2 ms)

    ↳20 CdtProblem

    ↳21 CdtKnowledgeProof (⇔, 0 ms)

    ↳22 CdtProblem

    ↳23 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 326 ms)

    ↳24 CdtProblem

(0) Obligation:

Clauses:

len1([], 0).
len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M))).
eq(X, X).

Query: len1(g,a)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

len1([], 0).
eq(X, X).
len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M))).

Query: len1(g,a)

(3) 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: len1(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: len1(T1, T2), SCOPE: 1, CLAUSE: 0 | len1(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: true | len1([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: len1(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nlen1(T1, T2) !=? len1([], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: len1([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(len1(T10, X15), eq(T12, s(X15)))\n\nT10 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: len1(T10, X15)\n\nT10 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: eq(T12, s(T13))\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: len1(T10, X15), SCOPE: 2, CLAUSE: 0 | len1(T10, X15), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: true | len1([], X15), SCOPE: 2, CLAUSE: 2\n\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: len1(T10, X15), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nX15 is free\nlen1(T10, X15) !=? len1([], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: len1([], X15), SCOPE: 2, CLAUSE: 2\n\nX15 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(len1(T19, X31), eq(X32, s(X31)))\n\nT19 is ground\nX32 is free\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: len1(T19, X31)\n\nT19 is ground\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: eq(X32, s(T20))\n\nT20 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: eq(X32, s(T20)), SCOPE: 3, CLAUSE: 1\n\nT20 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: eq(T12, s(T13)), SCOPE: 4, CLAUSE: 1\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 63 [arrowhead = none ];
63 -> 4;

64 [label="EVAL with clause\nlen1([], 0).\nand substitutionT1 -> [],\nT2 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 64 [arrowhead = none ];
64 -> 5;

65 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
4 -> 65 [arrowhead = none ];
65 -> 7;

66 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
5 -> 66 [arrowhead = none ];
66 -> 10;

67 [label="EVAL with clause\nlen1(.(X12, X13), X14) :- ','(len1(X13, X15), eq(X14, s(X15))).\nand substitutionX12 -> T9,\nX13 -> T10,\nT1 -> .(T9, T10),\nT2 -> T12,\nX14 -> T12,\nT11 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 67 [arrowhead = none ];
67 -> 16;

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

69 [label="BACKTRACK\nfor clause: len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 69 [arrowhead = none ];
69 -> 12;

70 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
16 -> 70 [arrowhead = none ];
70 -> 31;

71 [label="SPLIT 2\nnew knowledge:\nT10 is ground\nT13 is ground\nreplacements:X15 -> T13", fontsize=14, style = filled, fillcolor = violet];
16 -> 71 [arrowhead = none ];
71 -> 33;

72 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
31 -> 72 [arrowhead = none ];
72 -> 36;

73 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
33 -> 73 [arrowhead = none ];
73 -> 59;

74 [label="EVAL with clause\nlen1([], 0).\nand substitutionT10 -> [],\nX15 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 74 [arrowhead = none ];
74 -> 39;

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

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

77 [label="EVAL with clause\nlen1(.(X28, X29), X30) :- ','(len1(X29, X31), eq(X30, s(X31))).\nand substitutionX28 -> T18,\nX29 -> T19,\nT10 -> .(T18, T19),\nX15 -> X32,\nX30 -> X32", fontsize=14, style = filled, fillcolor = lightblue];
41 -> 77 [arrowhead = none ];
77 -> 46;

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

79 [label="BACKTRACK\nfor clause: len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 79 [arrowhead = none ];
79 -> 43;

80 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
46 -> 80 [arrowhead = none ];
80 -> 50;

81 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT20 is ground\nreplacements:X31 -> T20", fontsize=14, style = filled, fillcolor = violet];
46 -> 81 [arrowhead = none ];
81 -> 51;

82 [label="INSTANCE with matching:\nT10 -> T19\nX15 -> X31", fontsize=14, style = filled, fillcolor = lightgrey];
50 -> 82 [arrowhead = none , style=dashed];
82 -> 31[style=dashed];

83 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
51 -> 83 [arrowhead = none ];
83 -> 52;

84 [label="ONLY EVAL with clause\neq(X37, X37).\nand substitutionX32 -> s(T23),\nX37 -> s(T23),\nT20 -> T23,\nX38 -> s(T23)", fontsize=14, style = filled, fillcolor = lightblue];
52 -> 84 [arrowhead = none ];
84 -> 56;

85 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
56 -> 85 [arrowhead = none ];
85 -> 57;

86 [label="EVAL with clause\neq(X41, X41).\nand substitutionT12 -> s(T29),\nX41 -> s(T29),\nT13 -> T29,\nT28 -> s(T29)", fontsize=14, style = filled, fillcolor = lightblue];
59 -> 86 [arrowhead = none ];
86 -> 60;

87 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
59 -> 87 [arrowhead = none ];
87 -> 61;

88 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
60 -> 88 [arrowhead = none ];
88 -> 62;

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1(0)
f1_in(.(z0, z1)) → U1(f16_in(z1), .(z0, z1))
U1(f16_out1(z0, z1), .(z2, z3)) → f1_out1(z1)
f31_in([]) → f31_out1(0)
f31_in(.(z0, z1)) → U2(f46_in(z1), .(z0, z1))
U2(f46_out1(z0, z1), .(z2, z3)) → f31_out1(z1)
f33_in(z0) → f33_out1(s(z0))
f51_in(z0) → f51_out1(s(z0))
f16_in(z0) → U3(f31_in(z0), z0)
U3(f31_out1(z0), z1) → U4(f33_in(z0), z1, z0)
U4(f33_out1(z0), z1, z2) → f16_out1(z2, z0)
f46_in(z0) → U5(f31_in(z0), z0)
U5(f31_out1(z0), z1) → U6(f51_in(z0), z1, z0)
U6(f51_out1(z0), z1, z2) → f46_out1(z2, z0)

Tuples:

F1_IN(.(z0, z1)) → c1(U1'(f16_in(z1), .(z0, z1)), F16_IN(z1))
F31_IN(.(z0, z1)) → c4(U2'(f46_in(z1), .(z0, z1)), F46_IN(z1))
F16_IN(z0) → c8(U3'(f31_in(z0), z0), F31_IN(z0))
U3'(f31_out1(z0), z1) → c9(U4'(f33_in(z0), z1, z0), F33_IN(z0))
F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
U5'(f31_out1(z0), z1) → c12(U6'(f51_in(z0), z1, z0), F51_IN(z0))

S tuples:

F1_IN(.(z0, z1)) → c1(U1'(f16_in(z1), .(z0, z1)), F16_IN(z1))
F31_IN(.(z0, z1)) → c4(U2'(f46_in(z1), .(z0, z1)), F46_IN(z1))
F16_IN(z0) → c8(U3'(f31_in(z0), z0), F31_IN(z0))
U3'(f31_out1(z0), z1) → c9(U4'(f33_in(z0), z1, z0), F33_IN(z0))
F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
U5'(f31_out1(z0), z1) → c12(U6'(f51_in(z0), z1, z0), F51_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f31_in, U2, f33_in, f51_in, f16_in, U3, U4, f46_in, U5, U6

Defined Pair Symbols:

F1_IN, F31_IN, F16_IN, U3', F46_IN, U5'

Compound Symbols:

c1, c4, c8, c9, c11, c12

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1(0)
f1_in(.(z0, z1)) → U1(f16_in(z1), .(z0, z1))
U1(f16_out1(z0, z1), .(z2, z3)) → f1_out1(z1)
f31_in([]) → f31_out1(0)
f31_in(.(z0, z1)) → U2(f46_in(z1), .(z0, z1))
U2(f46_out1(z0, z1), .(z2, z3)) → f31_out1(z1)
f33_in(z0) → f33_out1(s(z0))
f51_in(z0) → f51_out1(s(z0))
f16_in(z0) → U3(f31_in(z0), z0)
U3(f31_out1(z0), z1) → U4(f33_in(z0), z1, z0)
U4(f33_out1(z0), z1, z2) → f16_out1(z2, z0)
f46_in(z0) → U5(f31_in(z0), z0)
U5(f31_out1(z0), z1) → U6(f51_in(z0), z1, z0)
U6(f51_out1(z0), z1, z2) → f46_out1(z2, z0)

Tuples:

F31_IN(.(z0, z1)) → c4(U2'(f46_in(z1), .(z0, z1)), F46_IN(z1))
F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(U1'(f16_in(z1), .(z0, z1)))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
U3'(f31_out1(z0), z1) → c(U4'(f33_in(z0), z1, z0))
U3'(f31_out1(z0), z1) → c(F33_IN(z0))
U5'(f31_out1(z0), z1) → c(U6'(f51_in(z0), z1, z0))
U5'(f31_out1(z0), z1) → c(F51_IN(z0))

S tuples:

F31_IN(.(z0, z1)) → c4(U2'(f46_in(z1), .(z0, z1)), F46_IN(z1))
F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(U1'(f16_in(z1), .(z0, z1)))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
U3'(f31_out1(z0), z1) → c(U4'(f33_in(z0), z1, z0))
U3'(f31_out1(z0), z1) → c(F33_IN(z0))
U5'(f31_out1(z0), z1) → c(U6'(f51_in(z0), z1, z0))
U5'(f31_out1(z0), z1) → c(F51_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f31_in, U2, f33_in, f51_in, f16_in, U3, U4, f46_in, U5, U6

Defined Pair Symbols:

F31_IN, F46_IN, F1_IN, F16_IN, U3', U5'

Compound Symbols:

c4, c11, c

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

Removed 6 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1(0)
f1_in(.(z0, z1)) → U1(f16_in(z1), .(z0, z1))
U1(f16_out1(z0, z1), .(z2, z3)) → f1_out1(z1)
f31_in([]) → f31_out1(0)
f31_in(.(z0, z1)) → U2(f46_in(z1), .(z0, z1))
U2(f46_out1(z0, z1), .(z2, z3)) → f31_out1(z1)
f33_in(z0) → f33_out1(s(z0))
f51_in(z0) → f51_out1(s(z0))
f16_in(z0) → U3(f31_in(z0), z0)
U3(f31_out1(z0), z1) → U4(f33_in(z0), z1, z0)
U4(f33_out1(z0), z1, z2) → f16_out1(z2, z0)
f46_in(z0) → U5(f31_in(z0), z0)
U5(f31_out1(z0), z1) → U6(f51_in(z0), z1, z0)
U6(f51_out1(z0), z1, z2) → f46_out1(z2, z0)

Tuples:

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
U5'(f31_out1(z0), z1) → c

S tuples:

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
U5'(f31_out1(z0), z1) → c

K tuples:none
Defined Rule Symbols:

f1_in, U1, f31_in, U2, f33_in, f51_in, f16_in, U3, U4, f46_in, U5, U6

Defined Pair Symbols:

F46_IN, F1_IN, F16_IN, F31_IN, U3', U5'

Compound Symbols:

c11, c, c4, c

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
U3'(f31_out1(z0), z1) → c
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
U3'(f31_out1(z0), z1) → c
U3'(f31_out1(z0), z1) → c

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1(0)
f1_in(.(z0, z1)) → U1(f16_in(z1), .(z0, z1))
U1(f16_out1(z0, z1), .(z2, z3)) → f1_out1(z1)
f31_in([]) → f31_out1(0)
f31_in(.(z0, z1)) → U2(f46_in(z1), .(z0, z1))
U2(f46_out1(z0, z1), .(z2, z3)) → f31_out1(z1)
f33_in(z0) → f33_out1(s(z0))
f51_in(z0) → f51_out1(s(z0))
f16_in(z0) → U3(f31_in(z0), z0)
U3(f31_out1(z0), z1) → U4(f33_in(z0), z1, z0)
U4(f33_out1(z0), z1, z2) → f16_out1(z2, z0)
f46_in(z0) → U5(f31_in(z0), z0)
U5(f31_out1(z0), z1) → U6(f51_in(z0), z1, z0)
U6(f51_out1(z0), z1, z2) → f46_out1(z2, z0)

Tuples:

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
U5'(f31_out1(z0), z1) → c

S tuples:

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))
U5'(f31_out1(z0), z1) → c

K tuples:

F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c

Defined Rule Symbols:

f1_in, U1, f31_in, U2, f33_in, f51_in, f16_in, U3, U4, f46_in, U5, U6

Defined Pair Symbols:

F46_IN, F1_IN, F16_IN, F31_IN, U3', U5'

Compound Symbols:

c11, c, c4, c

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

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))

We considered the (Usable) Rules:

f31_in([]) → f31_out1(0)
f31_in(.(z0, z1)) → U2(f46_in(z1), .(z0, z1))
f46_in(z0) → U5(f31_in(z0), z0)
U2(f46_out1(z0, z1), .(z2, z3)) → f31_out1(z1)
U5(f31_out1(z0), z1) → U6(f51_in(z0), z1, z0)
f51_in(z0) → f51_out1(s(z0))
U6(f51_out1(z0), z1, z2) → f46_out1(z2, z0)

And the Tuples:

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
U5'(f31_out1(z0), z1) → c

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

POL(.(x₁, x₂)) = [3] + x₂
POL(0) = 0
POL(F16_IN(x₁)) = [2] + [2]x₁
POL(F1_IN(x₁)) = [3] + [2]x₁
POL(F31_IN(x₁)) = [1] + x₁
POL(F46_IN(x₁)) = [2] + x₁
POL(U2(x₁, x₂)) = 0
POL(U3'(x₁, x₂)) = [1] + x₂
POL(U5(x₁, x₂)) = [3]x₁ + [2]x₂
POL(U5'(x₁, x₂)) = 0
POL(U6(x₁, x₂, x₃)) = [2] + [2]x₁ + x₂ + [2]x₃
POL([]) = 0
POL(c) = 0
POL(c(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c4(x₁)) = x₁
POL(f31_in(x₁)) = 0
POL(f31_out1(x₁)) = [3] + x₁
POL(f46_in(x₁)) = [2] + [3]x₁
POL(f46_out1(x₁, x₂)) = [2] + x₁
POL(f51_in(x₁)) = [2]
POL(f51_out1(x₁)) = x₁
POL(s(x₁)) = 0

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in([]) → f1_out1(0)
f1_in(.(z0, z1)) → U1(f16_in(z1), .(z0, z1))
U1(f16_out1(z0, z1), .(z2, z3)) → f1_out1(z1)
f31_in([]) → f31_out1(0)
f31_in(.(z0, z1)) → U2(f46_in(z1), .(z0, z1))
U2(f46_out1(z0, z1), .(z2, z3)) → f31_out1(z1)
f33_in(z0) → f33_out1(s(z0))
f51_in(z0) → f51_out1(s(z0))
f16_in(z0) → U3(f31_in(z0), z0)
U3(f31_out1(z0), z1) → U4(f33_in(z0), z1, z0)
U4(f33_out1(z0), z1, z2) → f16_out1(z2, z0)
f46_in(z0) → U5(f31_in(z0), z0)
U5(f31_out1(z0), z1) → U6(f51_in(z0), z1, z0)
U6(f51_out1(z0), z1, z2) → f46_out1(z2, z0)

Tuples:

F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
U5'(f31_out1(z0), z1) → c

S tuples:

U5'(f31_out1(z0), z1) → c

K tuples:

F1_IN(.(z0, z1)) → c(F16_IN(z1))
F16_IN(z0) → c(U3'(f31_in(z0), z0))
F16_IN(z0) → c(F31_IN(z0))
F1_IN(.(z0, z1)) → c
U3'(f31_out1(z0), z1) → c
F46_IN(z0) → c11(U5'(f31_in(z0), z0), F31_IN(z0))
F31_IN(.(z0, z1)) → c4(F46_IN(z1))

Defined Rule Symbols:

f1_in, U1, f31_in, U2, f33_in, f51_in, f16_in, U3, U4, f46_in, U5, U6

Defined Pair Symbols:

F46_IN, F1_IN, F16_IN, F31_IN, U3', U5'

Compound Symbols:

c11, c, c4, c

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

U5'(f31_out1(z0), z1) → c
U5'(f31_out1(z0), z1) → c

Now S is empty

(14) BOUNDS(O(1), O(1))

(15) 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: len1(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: len1(T1, T2), SCOPE: 1, CLAUSE: 0 | len1(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: true | len1([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: len1(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nlen1(T1, T2) !=? len1([], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: len1([], T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(len1(T7, X11), eq(T9, s(X11)))\n\nT7 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(len1(T7, X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 0 | ','(len1(T7, X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: eq(T9, s(0)) | ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(len1(T7, X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nT7 is ground\nX11 is free\nlen1(T7, X11) !=? len1([], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: eq(T9, s(0)), SCOPE: 3, CLAUSE: 1 | ?_3 | ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true | ?_3 | ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ?_3 | ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free\nX14 is free\neq(T9, s(0)) !=? eq(X14, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ?_3 | ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(len1([], X11), eq(T9, s(X11))), SCOPE: 2, CLAUSE: 2\n\nX11 is free\nX14 is free\neq(T9, s(0)) !=? eq(X14, X14)", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(','(len1(T18, X33), eq(X34, s(X33))), eq(T9, s(X34)))\n\nT18 is ground\nX34 is free\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: len1(T18, X33)\n\nT18 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(eq(X34, s(T19)), eq(T9, s(X34)))\n\nT19 is ground\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: len1(T18, X33), SCOPE: 4, CLAUSE: 0 | len1(T18, X33), SCOPE: 4, CLAUSE: 2\n\nT18 is ground\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: true | len1([], X33), SCOPE: 4, CLAUSE: 2\n\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: len1(T18, X33), SCOPE: 4, CLAUSE: 2\n\nT18 is ground\nX33 is free\nlen1(T18, X33) !=? len1([], 0)", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: len1([], X33), SCOPE: 4, CLAUSE: 2\n\nX33 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: ','(len1(T25, X50), eq(X51, s(X50)))\n\nT25 is ground\nX51 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: len1(T25, X50)\n\nT25 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: eq(X51, s(T26))\n\nT26 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: eq(X51, s(T26)), SCOPE: 5, CLAUSE: 1\n\nT26 is ground\nX51 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(eq(X34, s(T19)), eq(T9, s(X34))), SCOPE: 6, CLAUSE: 1\n\nT19 is ground\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: eq(T9, s(s(T32)))\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: eq(T9, s(s(T32))), SCOPE: 7, CLAUSE: 1\n\nT32 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 68 [arrowhead = none ];
68 -> 3;

69 [label="EVAL with clause\nlen1([], 0).\nand substitutionT1 -> [],\nT2 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 69 [arrowhead = none ];
69 -> 6;

70 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
3 -> 70 [arrowhead = none ];
70 -> 8;

71 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
6 -> 71 [arrowhead = none ];
71 -> 9;

72 [label="EVAL with clause\nlen1(.(X8, X9), X10) :- ','(len1(X9, X11), eq(X10, s(X11))).\nand substitutionX8 -> T6,\nX9 -> T7,\nT1 -> .(T6, T7),\nT2 -> T9,\nX10 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 72 [arrowhead = none ];
72 -> 13;

73 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
8 -> 73 [arrowhead = none ];
73 -> 14;

74 [label="BACKTRACK\nfor clause: len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
9 -> 74 [arrowhead = none ];
74 -> 11;

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

76 [label="EVAL with clause\nlen1([], 0).\nand substitutionT7 -> [],\nX11 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 76 [arrowhead = none ];
76 -> 17;

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

78 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
17 -> 78 [arrowhead = none ];
78 -> 20;

79 [label="EVAL with clause\nlen1(.(X30, X31), X32) :- ','(len1(X31, X33), eq(X32, s(X33))).\nand substitutionX30 -> T17,\nX31 -> T18,\nT7 -> .(T17, T18),\nX11 -> X34,\nX32 -> X34", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 79 [arrowhead = none ];
79 -> 28;

80 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
18 -> 80 [arrowhead = none ];
80 -> 29;

81 [label="EVAL with clause\neq(X14, X14).\nand substitutionT9 -> s(0),\nX14 -> s(0),\nT12 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
20 -> 81 [arrowhead = none ];
81 -> 21;

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

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

84 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 84 [arrowhead = none ];
84 -> 26;

85 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
23 -> 85 [arrowhead = none ];
85 -> 24;

86 [label="BACKTRACK\nfor clause: len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 86 [arrowhead = none ];
86 -> 25;

87 [label="BACKTRACK\nfor clause: len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
26 -> 87 [arrowhead = none ];
87 -> 27;

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

89 [label="SPLIT 2\nnew knowledge:\nT18 is ground\nT19 is ground\nreplacements:X33 -> T19", fontsize=14, style = filled, fillcolor = violet];
28 -> 89 [arrowhead = none ];
89 -> 32;

90 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
30 -> 90 [arrowhead = none ];
90 -> 34;

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

92 [label="EVAL with clause\nlen1([], 0).\nand substitutionT18 -> [],\nX33 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 92 [arrowhead = none ];
92 -> 35;

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

94 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 94 [arrowhead = none ];
94 -> 38;

95 [label="EVAL with clause\nlen1(.(X47, X48), X49) :- ','(len1(X48, X50), eq(X49, s(X50))).\nand substitutionX47 -> T24,\nX48 -> T25,\nT18 -> .(T24, T25),\nX33 -> X51,\nX49 -> X51", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 95 [arrowhead = none ];
95 -> 44;

96 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 96 [arrowhead = none ];
96 -> 45;

97 [label="BACKTRACK\nfor clause: len1(.(X1, Ts), N) :- ','(len1(Ts, M), eq(N, s(M)))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
38 -> 97 [arrowhead = none ];
97 -> 40;

98 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
44 -> 98 [arrowhead = none ];
98 -> 48;

99 [label="SPLIT 2\nnew knowledge:\nT25 is ground\nT26 is ground\nreplacements:X50 -> T26", fontsize=14, style = filled, fillcolor = violet];
44 -> 99 [arrowhead = none ];
99 -> 49;

100 [label="INSTANCE with matching:\nT18 -> T25\nX33 -> X50", fontsize=14, style = filled, fillcolor = lightgrey];
48 -> 100 [arrowhead = none , style=dashed];
100 -> 30[style=dashed];

101 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
49 -> 101 [arrowhead = none ];
101 -> 53;

102 [label="ONLY EVAL with clause\neq(X56, X56).\nand substitutionX51 -> s(T29),\nX56 -> s(T29),\nT26 -> T29,\nX57 -> s(T29)", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 102 [arrowhead = none ];
102 -> 54;

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

104 [label="ONLY EVAL with clause\neq(X62, X62).\nand substitutionX34 -> s(T32),\nX62 -> s(T32),\nT19 -> T32,\nX63 -> s(T32)", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 104 [arrowhead = none ];
104 -> 63;

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

106 [label="EVAL with clause\neq(X66, X66).\nand substitutionT9 -> s(s(T38)),\nX66 -> s(s(T38)),\nT32 -> T38,\nT37 -> s(s(T38))", fontsize=14, style = filled, fillcolor = lightblue];
64 -> 106 [arrowhead = none ];
106 -> 65;

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

108 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
65 -> 108 [arrowhead = none ];
108 -> 67;

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1(0)
f2_in(.(z0, [])) → f2_out1(s(0))
f2_in(.(z0, .(z1, z2))) → U1(f28_in(z2), .(z0, .(z1, z2)))
U1(f28_out1(z0, z1, z2), .(z3, .(z4, z5))) → f2_out1(z2)
f30_in([]) → f30_out1(0)
f30_in(.(z0, z1)) → U2(f44_in(z1), .(z0, z1))
U2(f44_out1(z0, z1), .(z2, z3)) → f30_out1(z1)
f32_in(z0) → f32_out1(s(z0), s(s(z0)))
f49_in(z0) → f49_out1(s(z0))
f28_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f32_in(z0), z1, z0)
U4(f32_out1(z0, z1), z2, z3) → f28_out1(z3, z0, z1)
f44_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f49_in(z0), z1, z0)
U6(f49_out1(z0), z1, z2) → f44_out1(z2, z0)

Tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f28_in(z2), .(z0, .(z1, z2))), F28_IN(z2))
F30_IN(.(z0, z1)) → c5(U2'(f44_in(z1), .(z0, z1)), F44_IN(z1))
F28_IN(z0) → c9(U3'(f30_in(z0), z0), F30_IN(z0))
U3'(f30_out1(z0), z1) → c10(U4'(f32_in(z0), z1, z0), F32_IN(z0))
F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
U5'(f30_out1(z0), z1) → c13(U6'(f49_in(z0), z1, z0), F49_IN(z0))

S tuples:

F2_IN(.(z0, .(z1, z2))) → c2(U1'(f28_in(z2), .(z0, .(z1, z2))), F28_IN(z2))
F30_IN(.(z0, z1)) → c5(U2'(f44_in(z1), .(z0, z1)), F44_IN(z1))
F28_IN(z0) → c9(U3'(f30_in(z0), z0), F30_IN(z0))
U3'(f30_out1(z0), z1) → c10(U4'(f32_in(z0), z1, z0), F32_IN(z0))
F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
U5'(f30_out1(z0), z1) → c13(U6'(f49_in(z0), z1, z0), F49_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f30_in, U2, f32_in, f49_in, f28_in, U3, U4, f44_in, U5, U6

Defined Pair Symbols:

F2_IN, F30_IN, F28_IN, U3', F44_IN, U5'

Compound Symbols:

c2, c5, c9, c10, c12, c13

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

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1(0)
f2_in(.(z0, [])) → f2_out1(s(0))
f2_in(.(z0, .(z1, z2))) → U1(f28_in(z2), .(z0, .(z1, z2)))
U1(f28_out1(z0, z1, z2), .(z3, .(z4, z5))) → f2_out1(z2)
f30_in([]) → f30_out1(0)
f30_in(.(z0, z1)) → U2(f44_in(z1), .(z0, z1))
U2(f44_out1(z0, z1), .(z2, z3)) → f30_out1(z1)
f32_in(z0) → f32_out1(s(z0), s(s(z0)))
f49_in(z0) → f49_out1(s(z0))
f28_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f32_in(z0), z1, z0)
U4(f32_out1(z0, z1), z2, z3) → f28_out1(z3, z0, z1)
f44_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f49_in(z0), z1, z0)
U6(f49_out1(z0), z1, z2) → f44_out1(z2, z0)

Tuples:

F30_IN(.(z0, z1)) → c5(U2'(f44_in(z1), .(z0, z1)), F44_IN(z1))
F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(U1'(f28_in(z2), .(z0, .(z1, z2))))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
U3'(f30_out1(z0), z1) → c(U4'(f32_in(z0), z1, z0))
U3'(f30_out1(z0), z1) → c(F32_IN(z0))
U5'(f30_out1(z0), z1) → c(U6'(f49_in(z0), z1, z0))
U5'(f30_out1(z0), z1) → c(F49_IN(z0))

S tuples:

F30_IN(.(z0, z1)) → c5(U2'(f44_in(z1), .(z0, z1)), F44_IN(z1))
F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(U1'(f28_in(z2), .(z0, .(z1, z2))))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
U3'(f30_out1(z0), z1) → c(U4'(f32_in(z0), z1, z0))
U3'(f30_out1(z0), z1) → c(F32_IN(z0))
U5'(f30_out1(z0), z1) → c(U6'(f49_in(z0), z1, z0))
U5'(f30_out1(z0), z1) → c(F49_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f30_in, U2, f32_in, f49_in, f28_in, U3, U4, f44_in, U5, U6

Defined Pair Symbols:

F30_IN, F44_IN, F2_IN, F28_IN, U3', U5'

Compound Symbols:

c5, c12, c

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

Removed 6 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1(0)
f2_in(.(z0, [])) → f2_out1(s(0))
f2_in(.(z0, .(z1, z2))) → U1(f28_in(z2), .(z0, .(z1, z2)))
U1(f28_out1(z0, z1, z2), .(z3, .(z4, z5))) → f2_out1(z2)
f30_in([]) → f30_out1(0)
f30_in(.(z0, z1)) → U2(f44_in(z1), .(z0, z1))
U2(f44_out1(z0, z1), .(z2, z3)) → f30_out1(z1)
f32_in(z0) → f32_out1(s(z0), s(s(z0)))
f49_in(z0) → f49_out1(s(z0))
f28_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f32_in(z0), z1, z0)
U4(f32_out1(z0, z1), z2, z3) → f28_out1(z3, z0, z1)
f44_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f49_in(z0), z1, z0)
U6(f49_out1(z0), z1, z2) → f44_out1(z2, z0)

Tuples:

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F30_IN(.(z0, z1)) → c5(F44_IN(z1))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
U5'(f30_out1(z0), z1) → c

S tuples:

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F30_IN(.(z0, z1)) → c5(F44_IN(z1))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
U5'(f30_out1(z0), z1) → c

K tuples:none
Defined Rule Symbols:

f2_in, U1, f30_in, U2, f32_in, f49_in, f28_in, U3, U4, f44_in, U5, U6

Defined Pair Symbols:

F44_IN, F2_IN, F28_IN, F30_IN, U3', U5'

Compound Symbols:

c12, c, c5, c

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
U3'(f30_out1(z0), z1) → c
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
U3'(f30_out1(z0), z1) → c
U3'(f30_out1(z0), z1) → c

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1(0)
f2_in(.(z0, [])) → f2_out1(s(0))
f2_in(.(z0, .(z1, z2))) → U1(f28_in(z2), .(z0, .(z1, z2)))
U1(f28_out1(z0, z1, z2), .(z3, .(z4, z5))) → f2_out1(z2)
f30_in([]) → f30_out1(0)
f30_in(.(z0, z1)) → U2(f44_in(z1), .(z0, z1))
U2(f44_out1(z0, z1), .(z2, z3)) → f30_out1(z1)
f32_in(z0) → f32_out1(s(z0), s(s(z0)))
f49_in(z0) → f49_out1(s(z0))
f28_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f32_in(z0), z1, z0)
U4(f32_out1(z0, z1), z2, z3) → f28_out1(z3, z0, z1)
f44_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f49_in(z0), z1, z0)
U6(f49_out1(z0), z1, z2) → f44_out1(z2, z0)

Tuples:

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F30_IN(.(z0, z1)) → c5(F44_IN(z1))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
U5'(f30_out1(z0), z1) → c

S tuples:

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F30_IN(.(z0, z1)) → c5(F44_IN(z1))
U5'(f30_out1(z0), z1) → c

K tuples:

F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c

Defined Rule Symbols:

f2_in, U1, f30_in, U2, f32_in, f49_in, f28_in, U3, U4, f44_in, U5, U6

Defined Pair Symbols:

F44_IN, F2_IN, F28_IN, F30_IN, U3', U5'

Compound Symbols:

c12, c, c5, c

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

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))

We considered the (Usable) Rules:

f30_in([]) → f30_out1(0)
f30_in(.(z0, z1)) → U2(f44_in(z1), .(z0, z1))
f44_in(z0) → U5(f30_in(z0), z0)
U2(f44_out1(z0, z1), .(z2, z3)) → f30_out1(z1)
U5(f30_out1(z0), z1) → U6(f49_in(z0), z1, z0)
f49_in(z0) → f49_out1(s(z0))
U6(f49_out1(z0), z1, z2) → f44_out1(z2, z0)

And the Tuples:

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F30_IN(.(z0, z1)) → c5(F44_IN(z1))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
U5'(f30_out1(z0), z1) → c

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

POL(.(x₁, x₂)) = [1] + x₂
POL(0) = 0
POL(F28_IN(x₁)) = [2] + [2]x₁
POL(F2_IN(x₁)) = [3]x₁
POL(F30_IN(x₁)) = [2]x₁
POL(F44_IN(x₁)) = [2] + [2]x₁
POL(U2(x₁, x₂)) = 0
POL(U3'(x₁, x₂)) = [1]
POL(U5(x₁, x₂)) = [2] + x₂
POL(U5'(x₁, x₂)) = 0
POL(U6(x₁, x₂, x₃)) = [2]x₁
POL([]) = 0
POL(c) = 0
POL(c(x₁)) = x₁
POL(c12(x₁, x₂)) = x₁ + x₂
POL(c5(x₁)) = x₁
POL(f30_in(x₁)) = 0
POL(f30_out1(x₁)) = 0
POL(f44_in(x₁)) = [2] + x₁
POL(f44_out1(x₁, x₂)) = x₂
POL(f49_in(x₁)) = [1]
POL(f49_out1(x₁)) = x₁
POL(s(x₁)) = 0

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in([]) → f2_out1(0)
f2_in(.(z0, [])) → f2_out1(s(0))
f2_in(.(z0, .(z1, z2))) → U1(f28_in(z2), .(z0, .(z1, z2)))
U1(f28_out1(z0, z1, z2), .(z3, .(z4, z5))) → f2_out1(z2)
f30_in([]) → f30_out1(0)
f30_in(.(z0, z1)) → U2(f44_in(z1), .(z0, z1))
U2(f44_out1(z0, z1), .(z2, z3)) → f30_out1(z1)
f32_in(z0) → f32_out1(s(z0), s(s(z0)))
f49_in(z0) → f49_out1(s(z0))
f28_in(z0) → U3(f30_in(z0), z0)
U3(f30_out1(z0), z1) → U4(f32_in(z0), z1, z0)
U4(f32_out1(z0, z1), z2, z3) → f28_out1(z3, z0, z1)
f44_in(z0) → U5(f30_in(z0), z0)
U5(f30_out1(z0), z1) → U6(f49_in(z0), z1, z0)
U6(f49_out1(z0), z1, z2) → f44_out1(z2, z0)

Tuples:

F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F30_IN(.(z0, z1)) → c5(F44_IN(z1))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
U5'(f30_out1(z0), z1) → c

S tuples:

F30_IN(.(z0, z1)) → c5(F44_IN(z1))
U5'(f30_out1(z0), z1) → c

K tuples:

F2_IN(.(z0, .(z1, z2))) → c(F28_IN(z2))
F28_IN(z0) → c(U3'(f30_in(z0), z0))
F28_IN(z0) → c(F30_IN(z0))
F2_IN(.(z0, .(z1, z2))) → c
U3'(f30_out1(z0), z1) → c
F44_IN(z0) → c12(U5'(f30_in(z0), z0), F30_IN(z0))

Defined Rule Symbols:

f2_in, U1, f30_in, U2, f32_in, f49_in, f28_in, U3, U4, f44_in, U5, U6

Defined Pair Symbols:

F44_IN, F2_IN, F28_IN, F30_IN, U3', U5'

Compound Symbols:

c12, c, c5, c