Runtime Complexity proof of /tmp/tmpXkzM3D/less2.pl

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

0 Prolog

↳1 BuiltinConflictTransformerProof (BOTH BOUNDS(ID, ID), 0 ms)

↳2 Prolog

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

↳4 CdtProblem

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

    ↳6 CdtProblem

    ↳7 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 130 ms)

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 2 ms)

    ↳10 CdtProblem

    ↳11 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))), 42 ms)

    ↳12 CdtProblem

    ↳13 CdtKnowledgeProof (⇔, 0 ms)

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

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

↳16 CdtProblem

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

    ↳18 CdtProblem

    ↳19 CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^1))), 109 ms)

    ↳20 CdtProblem

    ↳21 CdtKnowledgeProof (⇔, 3 ms)

    ↳22 CdtProblem

(0) Obligation:

Clauses:

less(0, Y) :- ','(!, =(Y, s(X2))).
less(X, Y) :- ','(p(X, X1), ','(p(Y, Y1), less(X1, Y1))).
p(0, 0).
p(s(X), X).
=(X, X).

Query: less(g,a)

(1) BuiltinConflictTransformerProof (BOTH BOUNDS(ID, ID) transformation)

Renamed defined predicates conflicting with built-in predicates [PROLOG].

(2) Obligation:

Clauses:

less(0, Y) :- ','(!, user_defined_=(Y, s(X2))).
less(X, Y) :- ','(p(X, X1), ','(p(Y, Y1), less(X1, Y1))).
p(0, 0).
p(s(X), X).
user_defined_=(X, X).

Query: less(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: less(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: less(T1, T2), SCOPE: 1, CLAUSE: 0 | less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_1, user_defined_=(T6, s(X7))) | less(0, T2), SCOPE: 1, CLAUSE: 1\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX6 is free\nless(T1, T2) !=? less(0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: user_defined_=(T6, s(X7))\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: user_defined_=(T6, s(X7)), SCOPE: 2, CLAUSE: 4\n\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(p(T18, X22), ','(p(T20, X23), less(X22, X23)))\n\nT18 is ground\nX6 is free\nX22 is free\nX23 is free\nless(T18, T2) !=? less(0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(p(T18, X22), ','(p(T20, X23), less(X22, X23))), SCOPE: 3, CLAUSE: 2 | ','(p(T18, X22), ','(p(T20, X23), less(X22, X23))), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nX6 is free\nX22 is free\nX23 is free\nless(T18, T2) !=? less(0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: ','(p(T18, X22), ','(p(T20, X23), less(X22, X23))), SCOPE: 3, CLAUSE: 3\n\nT18 is ground\nX6 is free\nX22 is free\nX23 is free\nless(T18, T2) !=? less(0, X6)", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(p(T20, X23), less(T23, X23))\n\nT23 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(p(T20, X23), less(T23, X23)), SCOPE: 4, CLAUSE: 2 | ','(p(T20, X23), less(T23, X23)), SCOPE: 4, CLAUSE: 3\n\nT23 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: less(T23, 0) | ','(p(T20, X23), less(T23, X23)), SCOPE: 4, CLAUSE: 3\n\nT23 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(p(T20, X23), less(T23, X23)), SCOPE: 4, CLAUSE: 3\n\nT23 is ground\nX23 is free\np(T20, X23) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: less(T23, 0)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: ','(p(T20, X23), less(T23, X23)), SCOPE: 4, CLAUSE: 3\n\nT23 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: less(T23, 0), SCOPE: 5, CLAUSE: 0 | less(T23, 0), SCOPE: 5, CLAUSE: 1\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(!_5, user_defined_=(0, s(X41))) | less(0, 0), SCOPE: 5, CLAUSE: 1\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: less(T23, 0), SCOPE: 5, CLAUSE: 1\n\nT23 is ground\nX40 is free\nless(T23, 0) !=? less(0, X40)", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: user_defined_=(0, s(X41))\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: user_defined_=(0, s(X41)), SCOPE: 6, CLAUSE: 4\n\nX41 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: ','(p(T26, X54), ','(p(0, X55), less(X54, X55)))\n\nT26 is ground\nX40 is free\nX54 is free\nX55 is free\nless(T26, 0) !=? less(0, X40)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(p(T26, X54), ','(p(0, X55), less(X54, X55))), SCOPE: 7, CLAUSE: 2 | ','(p(T26, X54), ','(p(0, X55), less(X54, X55))), SCOPE: 7, CLAUSE: 3\n\nT26 is ground\nX40 is free\nX54 is free\nX55 is free\nless(T26, 0) !=? less(0, X40)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(p(T26, X54), ','(p(0, X55), less(X54, X55))), SCOPE: 7, CLAUSE: 3\n\nT26 is ground\nX40 is free\nX54 is free\nX55 is free\nless(T26, 0) !=? less(0, X40)", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(p(0, X55), less(T29, X55))\n\nT29 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(p(0, X55), less(T29, X55)), SCOPE: 8, CLAUSE: 2 | ','(p(0, X55), less(T29, X55)), SCOPE: 8, CLAUSE: 3\n\nT29 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: less(T29, 0) | ','(p(0, X55), less(T29, X55)), SCOPE: 8, CLAUSE: 3\n\nT29 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: less(T29, 0)\n\nT29 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(p(0, X55), less(T29, X55)), SCOPE: 8, CLAUSE: 3\n\nT29 is ground\nX55 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: less(T23, T33)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: less(T23, T38)\n\nT23 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 78 [arrowhead = none ];
78 -> 4;

79 [label="EVAL with clause\nless(0, X6) :- ','(!_1, user_defined_=(X6, s(X7))).\nand substitutionT1 -> 0,\nT2 -> T6,\nX6 -> T6,\nT5 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 79 [arrowhead = none ];
79 -> 5;

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

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

82 [label="ONLY EVAL with clause\nless(X20, X21) :- ','(p(X20, X22), ','(p(X21, X23), less(X22, X23))).\nand substitutionT1 -> T18,\nX20 -> T18,\nT2 -> T20,\nX21 -> T20,\nT19 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 82 [arrowhead = none ];
82 -> 20;

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

84 [label="EVAL with clause\nuser_defined_=(X10, X10).\nand substitutionT6 -> s(T12),\nX10 -> s(T12),\nX7 -> T12,\nT11 -> s(T12)", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 84 [arrowhead = none ];
84 -> 13;

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

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

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

88 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T18, T2), less(0, X6))", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 88 [arrowhead = none ];
88 -> 24;

89 [label="EVAL with clause\np(s(X29), X29).\nand substitutionX29 -> T23,\nT18 -> s(T23),\nX22 -> T23", fontsize=14, style = filled, fillcolor = lightblue];
24 -> 89 [arrowhead = none ];
89 -> 25;

90 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 90 [arrowhead = none ];
90 -> 27;

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

92 [label="EVAL with clause\np(0, 0).\nand substitutionT20 -> 0,\nX23 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
29 -> 92 [arrowhead = none ];
92 -> 31;

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

94 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 94 [arrowhead = none ];
94 -> 35;

95 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
31 -> 95 [arrowhead = none ];
95 -> 37;

96 [label="EVAL with clause\np(s(X79), X79).\nand substitutionX79 -> T38,\nT20 -> s(T38),\nX23 -> T38,\nT37 -> T38", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 96 [arrowhead = none ];
96 -> 76;

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

98 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
35 -> 98 [arrowhead = none ];
98 -> 39;

99 [label="EVAL with clause\np(s(X74), X74).\nand substitutionX74 -> T33,\nT20 -> s(T33),\nX23 -> T33,\nT32 -> T33", fontsize=14, style = filled, fillcolor = lightblue];
37 -> 99 [arrowhead = none ];
99 -> 71;

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

101 [label="EVAL with clause\nless(0, X40) :- ','(!_5, user_defined_=(X40, s(X41))).\nand substitutionT23 -> 0,\nX40 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
39 -> 101 [arrowhead = none ];
101 -> 42;

102 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
39 -> 102 [arrowhead = none ];
102 -> 44;

103 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 103 [arrowhead = none ];
103 -> 45;

104 [label="ONLY EVAL with clause\nless(X52, X53) :- ','(p(X52, X54), ','(p(X53, X55), less(X54, X55))).\nand substitutionT23 -> T26,\nX52 -> T26,\nX53 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 104 [arrowhead = none ];
104 -> 52;

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

106 [label="BACKTRACK\nfor clause: user_defined_=(X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
47 -> 106 [arrowhead = none ];
106 -> 49;

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

108 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T26, 0), less(0, X40))", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 108 [arrowhead = none ];
108 -> 56;

109 [label="EVAL with clause\np(s(X61), X61).\nand substitutionX61 -> T29,\nT26 -> s(T29),\nX54 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 109 [arrowhead = none ];
109 -> 58;

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

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

112 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX55 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 112 [arrowhead = none ];
112 -> 64;

113 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 113 [arrowhead = none ];
113 -> 67;

114 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
64 -> 114 [arrowhead = none ];
114 -> 68;

115 [label="INSTANCE with matching:\nT23 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
67 -> 115 [arrowhead = none , style=dashed];
115 -> 35[style=dashed];

116 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
68 -> 116 [arrowhead = none ];
116 -> 69;

117 [label="INSTANCE with matching:\nT1 -> T23\nT2 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
71 -> 117 [arrowhead = none , style=dashed];
117 -> 1[style=dashed];

118 [label="INSTANCE with matching:\nT1 -> T23\nT2 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 118 [arrowhead = none , style=dashed];
118 -> 1[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f31_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f31_out1, s(z0)) → f1_out1
U1(f31_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f35_in(s(z0)) → U3(f64_in(z0), s(z0))
U3(f64_out1, s(z0)) → f35_out1
U3(f64_out2(z0), s(z1)) → f35_out1
f37_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f37_out1
f31_in(z0) → U5(f35_in(z0), f37_in(z0), z0)
U5(f35_out1, z0, z1) → f31_out1
U5(z0, f37_out1, z1) → f31_out2
f64_in(z0) → U6(f35_in(z0), f68_in(z0), z0)
U6(f35_out1, z0, z1) → f64_out1
U6(z0, f68_out1(z1), z2) → f64_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(U1'(f31_in(z0), s(z0)), F31_IN(z0))
F1_IN(s(z0)) → c2(U2'(f1_in(z0), s(z0)), F1_IN(z0))
F35_IN(s(z0)) → c6(U3'(f64_in(z0), s(z0)), F64_IN(z0))
F37_IN(z0) → c9(U4'(f1_in(z0), z0), F1_IN(z0))
F31_IN(z0) → c11(U5'(f35_in(z0), f37_in(z0), z0), F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(U6'(f35_in(z0), f68_in(z0), z0), F35_IN(z0))

S tuples:

F1_IN(s(z0)) → c1(U1'(f31_in(z0), s(z0)), F31_IN(z0))
F1_IN(s(z0)) → c2(U2'(f1_in(z0), s(z0)), F1_IN(z0))
F35_IN(s(z0)) → c6(U3'(f64_in(z0), s(z0)), F64_IN(z0))
F37_IN(z0) → c9(U4'(f1_in(z0), z0), F1_IN(z0))
F31_IN(z0) → c11(U5'(f35_in(z0), f37_in(z0), z0), F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(U6'(f35_in(z0), f68_in(z0), z0), F35_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f35_in, U3, f37_in, U4, f31_in, U5, f64_in, U6

Defined Pair Symbols:

F1_IN, F35_IN, F37_IN, F31_IN, F64_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

Removed 6 trailing tuple parts

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f31_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f31_out1, s(z0)) → f1_out1
U1(f31_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f35_in(s(z0)) → U3(f64_in(z0), s(z0))
U3(f64_out1, s(z0)) → f35_out1
U3(f64_out2(z0), s(z1)) → f35_out1
f37_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f37_out1
f31_in(z0) → U5(f35_in(z0), f37_in(z0), z0)
U5(f35_out1, z0, z1) → f31_out1
U5(z0, f37_out1, z1) → f31_out2
f64_in(z0) → U6(f35_in(z0), f68_in(z0), z0)
U6(f35_out1, z0, z1) → f64_out1
U6(z0, f68_out1(z1), z2) → f64_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

S tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2, f35_in, U3, f37_in, U4, f31_in, U5, f64_in, U6

Defined Pair Symbols:

F1_IN, F35_IN, F37_IN, F31_IN, F64_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

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

POL(F1_IN(x₁)) = x₁
POL(F31_IN(x₁)) = x₁
POL(F35_IN(x₁)) = 0
POL(F37_IN(x₁)) = x₁
POL(F64_IN(x₁)) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f31_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f31_out1, s(z0)) → f1_out1
U1(f31_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f35_in(s(z0)) → U3(f64_in(z0), s(z0))
U3(f64_out1, s(z0)) → f35_out1
U3(f64_out2(z0), s(z1)) → f35_out1
f37_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f37_out1
f31_in(z0) → U5(f35_in(z0), f37_in(z0), z0)
U5(f35_out1, z0, z1) → f31_out1
U5(z0, f37_out1, z1) → f31_out2
f64_in(z0) → U6(f35_in(z0), f68_in(z0), z0)
U6(f35_out1, z0, z1) → f64_out1
U6(z0, f68_out1(z1), z2) → f64_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

S tuples:

F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

K tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))

Defined Rule Symbols:

f1_in, U1, U2, f35_in, U3, f37_in, U4, f31_in, U5, f64_in, U6

Defined Pair Symbols:

F1_IN, F35_IN, F37_IN, F31_IN, F64_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f31_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f31_out1, s(z0)) → f1_out1
U1(f31_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f35_in(s(z0)) → U3(f64_in(z0), s(z0))
U3(f64_out1, s(z0)) → f35_out1
U3(f64_out2(z0), s(z1)) → f35_out1
f37_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f37_out1
f31_in(z0) → U5(f35_in(z0), f37_in(z0), z0)
U5(f35_out1, z0, z1) → f31_out1
U5(z0, f37_out1, z1) → f31_out2
f64_in(z0) → U6(f35_in(z0), f68_in(z0), z0)
U6(f35_out1, z0, z1) → f64_out1
U6(z0, f68_out1(z1), z2) → f64_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

S tuples:

F35_IN(s(z0)) → c6(F64_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

K tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))

Defined Rule Symbols:

f1_in, U1, U2, f35_in, U3, f37_in, U4, f31_in, U5, f64_in, U6

Defined Pair Symbols:

F1_IN, F35_IN, F37_IN, F31_IN, F64_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(11) CdtPolyRedPairProof (UPPER BOUND (ADD(O(n^2))) transformation)

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

F35_IN(s(z0)) → c6(F64_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

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

POL(F1_IN(x₁)) = x₁²
POL(F31_IN(x₁)) = x₁ + x₁²
POL(F35_IN(x₁)) = x₁
POL(F37_IN(x₁)) = x₁²
POL(F64_IN(x₁)) = x₁
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(0) → f1_out1
f1_in(s(z0)) → U1(f31_in(z0), s(z0))
f1_in(s(z0)) → U2(f1_in(z0), s(z0))
U1(f31_out1, s(z0)) → f1_out1
U1(f31_out2, s(z0)) → f1_out1
U2(f1_out1, s(z0)) → f1_out1
f35_in(s(z0)) → U3(f64_in(z0), s(z0))
U3(f64_out1, s(z0)) → f35_out1
U3(f64_out2(z0), s(z1)) → f35_out1
f37_in(z0) → U4(f1_in(z0), z0)
U4(f1_out1, z0) → f37_out1
f31_in(z0) → U5(f35_in(z0), f37_in(z0), z0)
U5(f35_out1, z0, z1) → f31_out1
U5(z0, f37_out1, z1) → f31_out2
f64_in(z0) → U6(f35_in(z0), f68_in(z0), z0)
U6(f35_out1, z0, z1) → f64_out1
U6(z0, f68_out1(z1), z2) → f64_out2(z1)

Tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F64_IN(z0) → c14(F35_IN(z0))

S tuples:

F64_IN(z0) → c14(F35_IN(z0))

K tuples:

F1_IN(s(z0)) → c1(F31_IN(z0))
F1_IN(s(z0)) → c2(F1_IN(z0))
F31_IN(z0) → c11(F35_IN(z0), F37_IN(z0))
F37_IN(z0) → c9(F1_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))

Defined Rule Symbols:

f1_in, U1, U2, f35_in, U3, f37_in, U4, f31_in, U5, f64_in, U6

Defined Pair Symbols:

F1_IN, F35_IN, F37_IN, F31_IN, F64_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(13) CdtKnowledgeProof (EQUIVALENT transformation)

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

F64_IN(z0) → c14(F35_IN(z0))
F35_IN(s(z0)) → c6(F64_IN(z0))

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: less(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: less(T1, T2), SCOPE: 1, CLAUSE: 0 | less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(!_1, user_defined_=(T5, s(X5))) | less(0, T2), SCOPE: 1, CLAUSE: 1\n\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: less(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nX4 is free\nless(T1, T2) !=? less(0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: user_defined_=(T5, s(X5))\n\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: user_defined_=(T5, s(X5)), SCOPE: 2, CLAUSE: 4\n\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(p(T14, X13), ','(p(T16, X14), less(X13, X14)))\n\nT14 is ground\nX4 is free\nX13 is free\nX14 is free\nless(T14, T2) !=? less(0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: ','(p(T14, X13), ','(p(T16, X14), less(X13, X14))), SCOPE: 3, CLAUSE: 2 | ','(p(T14, X13), ','(p(T16, X14), less(X13, X14))), SCOPE: 3, CLAUSE: 3\n\nT14 is ground\nX4 is free\nX13 is free\nX14 is free\nless(T14, T2) !=? less(0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(p(T14, X13), ','(p(T16, X14), less(X13, X14))), SCOPE: 3, CLAUSE: 3\n\nT14 is ground\nX4 is free\nX13 is free\nX14 is free\nless(T14, T2) !=? less(0, X4)", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(p(T16, X14), less(T19, X14))\n\nT19 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(p(T16, X14), less(T19, X14)), SCOPE: 4, CLAUSE: 2 | ','(p(T16, X14), less(T19, X14)), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: less(T19, 0) | ','(p(T16, X14), less(T19, X14)), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: ','(p(T16, X14), less(T19, X14)), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nX14 is free\np(T16, X14) !=? p(0, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: less(T19, 0)\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: ','(p(T16, X14), less(T19, X14)), SCOPE: 4, CLAUSE: 3\n\nT19 is ground\nX14 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: less(T19, 0), SCOPE: 5, CLAUSE: 0 | less(T19, 0), SCOPE: 5, CLAUSE: 1\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(!_5, user_defined_=(0, s(X29))) | less(0, 0), SCOPE: 5, CLAUSE: 1\n\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: less(T19, 0), SCOPE: 5, CLAUSE: 1\n\nT19 is ground\nX28 is free\nless(T19, 0) !=? less(0, X28)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: user_defined_=(0, s(X29))\n\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: user_defined_=(0, s(X29)), SCOPE: 6, CLAUSE: 4\n\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(p(T22, X42), ','(p(0, X43), less(X42, X43)))\n\nT22 is ground\nX28 is free\nX42 is free\nX43 is free\nless(T22, 0) !=? less(0, X28)", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(p(T22, X42), ','(p(0, X43), less(X42, X43))), SCOPE: 7, CLAUSE: 2 | ','(p(T22, X42), ','(p(0, X43), less(X42, X43))), SCOPE: 7, CLAUSE: 3\n\nT22 is ground\nX28 is free\nX42 is free\nX43 is free\nless(T22, 0) !=? less(0, X28)", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ','(p(T22, X42), ','(p(0, X43), less(X42, X43))), SCOPE: 7, CLAUSE: 3\n\nT22 is ground\nX28 is free\nX42 is free\nX43 is free\nless(T22, 0) !=? less(0, X28)", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(p(0, X43), less(T25, X43))\n\nT25 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(p(0, X43), less(T25, X43)), SCOPE: 8, CLAUSE: 2 | ','(p(0, X43), less(T25, X43)), SCOPE: 8, CLAUSE: 3\n\nT25 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: less(T25, 0) | ','(p(0, X43), less(T25, X43)), SCOPE: 8, CLAUSE: 3\n\nT25 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: less(T25, 0)\n\nT25 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(p(0, X43), less(T25, X43)), SCOPE: 8, CLAUSE: 3\n\nT25 is ground\nX43 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: less(T19, T29)\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: less(T19, T34)\n\nT19 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 79 [arrowhead = none ];
79 -> 3;

80 [label="EVAL with clause\nless(0, X4) :- ','(!_1, user_defined_=(X4, s(X5))).\nand substitutionT1 -> 0,\nT2 -> T5,\nX4 -> T5,\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 80 [arrowhead = none ];
80 -> 6;

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

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

83 [label="ONLY EVAL with clause\nless(X11, X12) :- ','(p(X11, X13), ','(p(X12, X14), less(X13, X14))).\nand substitutionT1 -> T14,\nX11 -> T14,\nT2 -> T16,\nX12 -> T16,\nT15 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 83 [arrowhead = none ];
83 -> 19;

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

85 [label="EVAL with clause\nuser_defined_=(X8, X8).\nand substitutionT5 -> s(T11),\nX8 -> s(T11),\nX5 -> T11,\nT10 -> s(T11)", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 85 [arrowhead = none ];
85 -> 14;

86 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
11 -> 86 [arrowhead = none ];
86 -> 16;

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

88 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
19 -> 88 [arrowhead = none ];
88 -> 21;

89 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T14, T2), less(0, X4))", fontsize=14, style = filled, fillcolor = lightgreen];
21 -> 89 [arrowhead = none ];
89 -> 23;

90 [label="EVAL with clause\np(s(X17), X17).\nand substitutionX17 -> T19,\nT14 -> s(T19),\nX13 -> T19", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 90 [arrowhead = none ];
90 -> 26;

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

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

93 [label="EVAL with clause\np(0, 0).\nand substitutionT16 -> 0,\nX14 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 93 [arrowhead = none ];
93 -> 32;

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

95 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 95 [arrowhead = none ];
95 -> 36;

96 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
32 -> 96 [arrowhead = none ];
96 -> 38;

97 [label="EVAL with clause\np(s(X67), X67).\nand substitutionX67 -> T34,\nT16 -> s(T34),\nX14 -> T34,\nT33 -> T34", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 97 [arrowhead = none ];
97 -> 75;

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

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

100 [label="EVAL with clause\np(s(X62), X62).\nand substitutionX62 -> T29,\nT16 -> s(T29),\nX14 -> T29,\nT28 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 100 [arrowhead = none ];
100 -> 72;

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

102 [label="EVAL with clause\nless(0, X28) :- ','(!_5, user_defined_=(X28, s(X29))).\nand substitutionT19 -> 0,\nX28 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
40 -> 102 [arrowhead = none ];
102 -> 41;

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

104 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 104 [arrowhead = none ];
104 -> 46;

105 [label="ONLY EVAL with clause\nless(X40, X41) :- ','(p(X40, X42), ','(p(X41, X43), less(X42, X43))).\nand substitutionT19 -> T22,\nX40 -> T22,\nX41 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 105 [arrowhead = none ];
105 -> 51;

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

107 [label="BACKTRACK\nfor clause: user_defined_=(X, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
48 -> 107 [arrowhead = none ];
107 -> 50;

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

109 [label="BACKTRACK\nfor clause: p(0, 0)\nwith clash: (less(T22, 0), less(0, X28))", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 109 [arrowhead = none ];
109 -> 55;

110 [label="EVAL with clause\np(s(X49), X49).\nand substitutionX49 -> T25,\nT22 -> s(T25),\nX42 -> T25", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 110 [arrowhead = none ];
110 -> 57;

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

112 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
57 -> 112 [arrowhead = none ];
112 -> 61;

113 [label="ONLY EVAL with clause\np(0, 0).\nand substitutionX43 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
61 -> 113 [arrowhead = none ];
113 -> 63;

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

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

116 [label="INSTANCE with matching:\nT19 -> T25", fontsize=14, style = filled, fillcolor = lightgrey];
65 -> 116 [arrowhead = none , style=dashed];
116 -> 36[style=dashed];

117 [label="BACKTRACK\nfor clause: p(s(X), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
66 -> 117 [arrowhead = none ];
117 -> 70;

118 [label="INSTANCE with matching:\nT1 -> T19\nT2 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 118 [arrowhead = none , style=dashed];
118 -> 2[style=dashed];

119 [label="INSTANCE with matching:\nT1 -> T19\nT2 -> T34", fontsize=14, style = filled, fillcolor = lightgrey];
75 -> 119 [arrowhead = none , style=dashed];
119 -> 2[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f32_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f32_out1, s(z0)) → f2_out1
U1(f32_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f36_in(s(z0)) → U3(f63_in(z0), s(z0))
U3(f63_out1, s(z0)) → f36_out1
U3(f63_out2(z0), s(z1)) → f36_out1
f38_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f38_out1
f32_in(z0) → U5(f36_in(z0), f38_in(z0), z0)
U5(f36_out1, z0, z1) → f32_out1
U5(z0, f38_out1, z1) → f32_out2
f63_in(z0) → U6(f36_in(z0), f66_in(z0), z0)
U6(f36_out1, z0, z1) → f63_out1
U6(z0, f66_out1(z1), z2) → f63_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(U1'(f32_in(z0), s(z0)), F32_IN(z0))
F2_IN(s(z0)) → c2(U2'(f2_in(z0), s(z0)), F2_IN(z0))
F36_IN(s(z0)) → c6(U3'(f63_in(z0), s(z0)), F63_IN(z0))
F38_IN(z0) → c9(U4'(f2_in(z0), z0), F2_IN(z0))
F32_IN(z0) → c11(U5'(f36_in(z0), f38_in(z0), z0), F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(U6'(f36_in(z0), f66_in(z0), z0), F36_IN(z0))

S tuples:

F2_IN(s(z0)) → c1(U1'(f32_in(z0), s(z0)), F32_IN(z0))
F2_IN(s(z0)) → c2(U2'(f2_in(z0), s(z0)), F2_IN(z0))
F36_IN(s(z0)) → c6(U3'(f63_in(z0), s(z0)), F63_IN(z0))
F38_IN(z0) → c9(U4'(f2_in(z0), z0), F2_IN(z0))
F32_IN(z0) → c11(U5'(f36_in(z0), f38_in(z0), z0), F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(U6'(f36_in(z0), f66_in(z0), z0), F36_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f36_in, U3, f38_in, U4, f32_in, U5, f63_in, U6

Defined Pair Symbols:

F2_IN, F36_IN, F38_IN, F32_IN, F63_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

Removed 6 trailing tuple parts

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f32_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f32_out1, s(z0)) → f2_out1
U1(f32_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f36_in(s(z0)) → U3(f63_in(z0), s(z0))
U3(f63_out1, s(z0)) → f36_out1
U3(f63_out2(z0), s(z1)) → f36_out1
f38_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f38_out1
f32_in(z0) → U5(f36_in(z0), f38_in(z0), z0)
U5(f36_out1, z0, z1) → f32_out1
U5(z0, f38_out1, z1) → f32_out2
f63_in(z0) → U6(f36_in(z0), f66_in(z0), z0)
U6(f36_out1, z0, z1) → f63_out1
U6(z0, f66_out1(z1), z2) → f63_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F36_IN(s(z0)) → c6(F63_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

S tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F36_IN(s(z0)) → c6(F63_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2, f36_in, U3, f38_in, U4, f32_in, U5, f63_in, U6

Defined Pair Symbols:

F2_IN, F36_IN, F38_IN, F32_IN, F63_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

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

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))

We considered the (Usable) Rules:none
And the Tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F36_IN(s(z0)) → c6(F63_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

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

POL(F2_IN(x₁)) = x₁
POL(F32_IN(x₁)) = x₁
POL(F36_IN(x₁)) = 0
POL(F38_IN(x₁)) = x₁
POL(F63_IN(x₁)) = 0
POL(c1(x₁)) = x₁
POL(c11(x₁, x₂)) = x₁ + x₂
POL(c14(x₁)) = x₁
POL(c2(x₁)) = x₁
POL(c6(x₁)) = x₁
POL(c9(x₁)) = x₁
POL(s(x₁)) = [1] + x₁

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f32_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f32_out1, s(z0)) → f2_out1
U1(f32_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f36_in(s(z0)) → U3(f63_in(z0), s(z0))
U3(f63_out1, s(z0)) → f36_out1
U3(f63_out2(z0), s(z1)) → f36_out1
f38_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f38_out1
f32_in(z0) → U5(f36_in(z0), f38_in(z0), z0)
U5(f36_out1, z0, z1) → f32_out1
U5(z0, f38_out1, z1) → f32_out2
f63_in(z0) → U6(f36_in(z0), f66_in(z0), z0)
U6(f36_out1, z0, z1) → f63_out1
U6(z0, f66_out1(z1), z2) → f63_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F36_IN(s(z0)) → c6(F63_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

S tuples:

F36_IN(s(z0)) → c6(F63_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

K tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))

Defined Rule Symbols:

f2_in, U1, U2, f36_in, U3, f38_in, U4, f32_in, U5, f63_in, U6

Defined Pair Symbols:

F2_IN, F36_IN, F38_IN, F32_IN, F63_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(0) → f2_out1
f2_in(s(z0)) → U1(f32_in(z0), s(z0))
f2_in(s(z0)) → U2(f2_in(z0), s(z0))
U1(f32_out1, s(z0)) → f2_out1
U1(f32_out2, s(z0)) → f2_out1
U2(f2_out1, s(z0)) → f2_out1
f36_in(s(z0)) → U3(f63_in(z0), s(z0))
U3(f63_out1, s(z0)) → f36_out1
U3(f63_out2(z0), s(z1)) → f36_out1
f38_in(z0) → U4(f2_in(z0), z0)
U4(f2_out1, z0) → f38_out1
f32_in(z0) → U5(f36_in(z0), f38_in(z0), z0)
U5(f36_out1, z0, z1) → f32_out1
U5(z0, f38_out1, z1) → f32_out2
f63_in(z0) → U6(f36_in(z0), f66_in(z0), z0)
U6(f36_out1, z0, z1) → f63_out1
U6(z0, f66_out1(z1), z2) → f63_out2(z1)

Tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F36_IN(s(z0)) → c6(F63_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

S tuples:

F36_IN(s(z0)) → c6(F63_IN(z0))
F63_IN(z0) → c14(F36_IN(z0))

K tuples:

F2_IN(s(z0)) → c1(F32_IN(z0))
F2_IN(s(z0)) → c2(F2_IN(z0))
F32_IN(z0) → c11(F36_IN(z0), F38_IN(z0))
F38_IN(z0) → c9(F2_IN(z0))

Defined Rule Symbols:

f2_in, U1, U2, f36_in, U3, f38_in, U4, f32_in, U5, f63_in, U6

Defined Pair Symbols:

F2_IN, F36_IN, F38_IN, F32_IN, F63_IN

Compound Symbols:

c1, c2, c6, c9, c11, c14