Runtime Complexity proof of /tmp/tmpw0yDGO/prefix-fb.pl

Runtime Complexity of the query pattern
prefix(a,g)
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), 50 ms)

↳4 CdtProblem

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

    ↳6 CdtProblem

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

    ↳8 CdtProblem

    ↳9 CdtKnowledgeProof (⇔, 0 ms)

    ↳10 CdtProblem

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

    ↳12 CdtProblem

    ↳13 SIsEmptyProof (⇔, 0 ms)

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

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

↳16 CdtProblem

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

    ↳18 CdtProblem

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

    ↳20 CdtProblem

    ↳21 CdtKnowledgeProof (⇔, 0 ms)

    ↳22 CdtProblem

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

    ↳24 CdtProblem

(0) Obligation:

Clauses:

prefix(Xs, Ys) :- app(Xs, X1, Ys).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: prefix(a,g)

(1) LPReorderTransformerProof (EQUIVALENT transformation)

Reordered facts before rules in definite LP [PROLOG].

(2) Obligation:

Clauses:

app([], X, X).
prefix(Xs, Ys) :- app(Xs, X1, Ys).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: prefix(a,g)

(3) 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: prefix(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: prefix(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: app(T12, X13, T11)\n\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: app(T12, X13, T11), SCOPE: 2, CLAUSE: 0 | app(T12, X13, T11), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: true | app(T12, X13, T17), SCOPE: 2, CLAUSE: 2\n\nT17 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: app(T12, X13, T11), SCOPE: 2, CLAUSE: 2\n\nT11 is ground\nX13 is free\nX22 is free\napp(T12, X13, T11) !=? app([], X22, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: app(T12, X13, T17), SCOPE: 2, CLAUSE: 2\n\nT17 is ground\nX13 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: app(T27, X38, T26)\n\nT26 is ground\nX38 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: app(T39, X57, T38)\n\nT36 is ground\nT38 is ground\nX13 is free\nX22 is free\nX57 is free\napp(T12, X13, .(T36, T38)) !=? app([], X22, X22)", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 23 [arrowhead = none ];
23 -> 3;

24 [label="ONLY EVAL with clause\nprefix(X11, X12) :- app(X11, X13, X12).\nand substitutionT1 -> T12,\nX11 -> T12,\nT2 -> T11,\nX12 -> T11,\nT10 -> T12", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 24 [arrowhead = none ];
24 -> 7;

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

26 [label="EVAL with clause\napp([], X22, X22).\nand substitutionT12 -> [],\nX13 -> T17,\nX22 -> T17,\nT11 -> T17,\nX23 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 26 [arrowhead = none ];
26 -> 14;

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

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

29 [label="EVAL with clause\napp(.(X53, X54), X55, .(X53, X56)) :- app(X54, X55, X56).\nand substitutionX53 -> T36,\nX54 -> T39,\nT12 -> .(T36, T39),\nX13 -> X57,\nX55 -> X57,\nX56 -> T38,\nT11 -> .(T36, T38),\nT37 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 29 [arrowhead = none ];
29 -> 21;

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

31 [label="EVAL with clause\napp(.(X34, X35), X36, .(X34, X37)) :- app(X35, X36, X37).\nand substitutionX34 -> T24,\nX35 -> T27,\nT12 -> .(T24, T27),\nX13 -> X38,\nX36 -> X38,\nX37 -> T26,\nT17 -> .(T24, T26),\nT25 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
18 -> 31 [arrowhead = none ];
31 -> 19;

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

33 [label="INSTANCE with matching:\nT12 -> T27\nX13 -> X38\nT11 -> T26", fontsize=14, style = filled, fillcolor = lightgrey];
19 -> 33 [arrowhead = none , style=dashed];
33 -> 7[style=dashed];

34 [label="INSTANCE with matching:\nT12 -> T39\nX13 -> X57\nT11 -> T38", fontsize=14, style = filled, fillcolor = lightgrey];
21 -> 34 [arrowhead = none , style=dashed];
34 -> 7[style=dashed];

}

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1), z2) → f2_out1(z0)
f7_in(z0) → f7_out1([], z0)
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
f7_in(.(z0, z1)) → U3(f7_in(z1), .(z0, z1))
U2(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)
U3(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)

Tuples:

F2_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F7_IN(.(z0, z1)) → c4(U3'(f7_in(z1), .(z0, z1)), F7_IN(z1))

S tuples:

F2_IN(z0) → c(U1'(f7_in(z0), z0), F7_IN(z0))
F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F7_IN(.(z0, z1)) → c4(U3'(f7_in(z1), .(z0, z1)), F7_IN(z1))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f7_in, U2, U3

Defined Pair Symbols:

F2_IN, F7_IN

Compound Symbols:

c, c3, c4

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

Split RHS of tuples not part of any SCC

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1), z2) → f2_out1(z0)
f7_in(z0) → f7_out1([], z0)
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
f7_in(.(z0, z1)) → U3(f7_in(z1), .(z0, z1))
U2(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)
U3(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)

Tuples:

F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F7_IN(.(z0, z1)) → c4(U3'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F2_IN(z0) → c1(U1'(f7_in(z0), z0))
F2_IN(z0) → c1(F7_IN(z0))

S tuples:

F7_IN(.(z0, z1)) → c3(U2'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F7_IN(.(z0, z1)) → c4(U3'(f7_in(z1), .(z0, z1)), F7_IN(z1))
F2_IN(z0) → c1(U1'(f7_in(z0), z0))
F2_IN(z0) → c1(F7_IN(z0))

K tuples:none
Defined Rule Symbols:

f2_in, U1, f7_in, U2, U3

Defined Pair Symbols:

F7_IN, F2_IN

Compound Symbols:

c3, c4, c1

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

Removed 3 trailing tuple parts

(8) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1), z2) → f2_out1(z0)
f7_in(z0) → f7_out1([], z0)
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
f7_in(.(z0, z1)) → U3(f7_in(z1), .(z0, z1))
U2(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)
U3(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)

Tuples:

F2_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))
F2_IN(z0) → c1

S tuples:

F2_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))
F2_IN(z0) → c1

K tuples:none
Defined Rule Symbols:

f2_in, U1, f7_in, U2, U3

Defined Pair Symbols:

F2_IN, F7_IN

Compound Symbols:

c1, c3, c4, c1

(9) CdtKnowledgeProof (EQUIVALENT transformation)

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

F2_IN(z0) → c1(F7_IN(z0))
F2_IN(z0) → c1

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1), z2) → f2_out1(z0)
f7_in(z0) → f7_out1([], z0)
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
f7_in(.(z0, z1)) → U3(f7_in(z1), .(z0, z1))
U2(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)
U3(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)

Tuples:

F2_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))
F2_IN(z0) → c1

S tuples:

F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))

K tuples:

F2_IN(z0) → c1(F7_IN(z0))
F2_IN(z0) → c1

Defined Rule Symbols:

f2_in, U1, f7_in, U2, U3

Defined Pair Symbols:

F2_IN, F7_IN

Compound Symbols:

c1, c3, c4, c1

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

F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))

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

F2_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))
F2_IN(z0) → c1

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

POL(.(x₁, x₂)) = [2] + x₂
POL(F2_IN(x₁)) = [2] + x₁
POL(F7_IN(x₁)) = [1] + x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(z0) → U1(f7_in(z0), z0)
U1(f7_out1(z0, z1), z2) → f2_out1(z0)
f7_in(z0) → f7_out1([], z0)
f7_in(.(z0, z1)) → U2(f7_in(z1), .(z0, z1))
f7_in(.(z0, z1)) → U3(f7_in(z1), .(z0, z1))
U2(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)
U3(f7_out1(z0, z1), .(z2, z3)) → f7_out1(.(z2, z0), z1)

Tuples:

F2_IN(z0) → c1(F7_IN(z0))
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))
F2_IN(z0) → c1

S tuples:none
K tuples:

F2_IN(z0) → c1(F7_IN(z0))
F2_IN(z0) → c1
F7_IN(.(z0, z1)) → c3(F7_IN(z1))
F7_IN(.(z0, z1)) → c4(F7_IN(z1))

Defined Rule Symbols:

f2_in, U1, f7_in, U2, U3

Defined Pair Symbols:

F2_IN, F7_IN

Compound Symbols:

c1, c3, c4, c1

(13) SIsEmptyProof (EQUIVALENT transformation)

The set 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];
1 [label="1: prefix(T1, T2)\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: prefix(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT2 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: app(T7, X6, T6)\n\nT6 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: app(T7, X6, T6), SCOPE: 2, CLAUSE: 0 | app(T7, X6, T6), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: true | app(T7, X6, T10), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: app(T7, X6, T6), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nX6 is free\nX11 is free\napp(T7, X6, T6) !=? app([], X11, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: app(T7, X6, T10), SCOPE: 2, CLAUSE: 2\n\nT10 is ground\nX6 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: app(T20, X27, T19)\n\nT19 is ground\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: app(T32, X46, T31)\n\nT29 is ground\nT31 is ground\nX6 is free\nX11 is free\nX46 is free\napp(T7, X6, .(T29, T31)) !=? app([], X11, X11)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 18 [arrowhead = none ];
18 -> 4;

19 [label="ONLY EVAL with clause\nprefix(X4, X5) :- app(X4, X6, X5).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T6,\nX5 -> T6,\nT5 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 19 [arrowhead = none ];
19 -> 5;

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

21 [label="EVAL with clause\napp([], X11, X11).\nand substitutionT7 -> [],\nX6 -> T10,\nX11 -> T10,\nT6 -> T10,\nX12 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 21 [arrowhead = none ];
21 -> 8;

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

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

24 [label="EVAL with clause\napp(.(X42, X43), X44, .(X42, X45)) :- app(X43, X44, X45).\nand substitutionX42 -> T29,\nX43 -> T32,\nT7 -> .(T29, T32),\nX6 -> X46,\nX44 -> X46,\nX45 -> T31,\nT6 -> .(T29, T31),\nT30 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
9 -> 24 [arrowhead = none ];
24 -> 16;

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

26 [label="EVAL with clause\napp(.(X23, X24), X25, .(X23, X26)) :- app(X24, X25, X26).\nand substitutionX23 -> T17,\nX24 -> T20,\nT7 -> .(T17, T20),\nX6 -> X27,\nX25 -> X27,\nX26 -> T19,\nT10 -> .(T17, T19),\nT18 -> T20", fontsize=14, style = filled, fillcolor = lightblue];
10 -> 26 [arrowhead = none ];
26 -> 11;

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

28 [label="INSTANCE with matching:\nT7 -> T20\nX6 -> X27\nT6 -> T19", fontsize=14, style = filled, fillcolor = lightgrey];
11 -> 28 [arrowhead = none , style=dashed];
28 -> 5[style=dashed];

29 [label="INSTANCE with matching:\nT7 -> T32\nX6 -> X46\nT6 -> T31", fontsize=14, style = filled, fillcolor = lightgrey];
16 -> 29 [arrowhead = none , style=dashed];
29 -> 5[style=dashed];

}

(16) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1(z0, z1), z2) → f1_out1(z0)
f5_in(z0) → f5_out1([], z0)
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
f5_in(.(z0, z1)) → U3(f5_in(z1), .(z0, z1))
U2(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)
U3(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)

Tuples:

F1_IN(z0) → c(U1'(f5_in(z0), z0), F5_IN(z0))
F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F5_IN(.(z0, z1)) → c4(U3'(f5_in(z1), .(z0, z1)), F5_IN(z1))

S tuples:

F1_IN(z0) → c(U1'(f5_in(z0), z0), F5_IN(z0))
F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F5_IN(.(z0, z1)) → c4(U3'(f5_in(z1), .(z0, z1)), F5_IN(z1))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f5_in, U2, U3

Defined Pair Symbols:

F1_IN, F5_IN

Compound Symbols:

c, c3, c4

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

Split RHS of tuples not part of any SCC

(18) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1(z0, z1), z2) → f1_out1(z0)
f5_in(z0) → f5_out1([], z0)
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
f5_in(.(z0, z1)) → U3(f5_in(z1), .(z0, z1))
U2(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)
U3(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)

Tuples:

F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F5_IN(.(z0, z1)) → c4(U3'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F1_IN(z0) → c1(U1'(f5_in(z0), z0))
F1_IN(z0) → c1(F5_IN(z0))

S tuples:

F5_IN(.(z0, z1)) → c3(U2'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F5_IN(.(z0, z1)) → c4(U3'(f5_in(z1), .(z0, z1)), F5_IN(z1))
F1_IN(z0) → c1(U1'(f5_in(z0), z0))
F1_IN(z0) → c1(F5_IN(z0))

K tuples:none
Defined Rule Symbols:

f1_in, U1, f5_in, U2, U3

Defined Pair Symbols:

F5_IN, F1_IN

Compound Symbols:

c3, c4, c1

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

Removed 3 trailing tuple parts

(20) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1(z0, z1), z2) → f1_out1(z0)
f5_in(z0) → f5_out1([], z0)
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
f5_in(.(z0, z1)) → U3(f5_in(z1), .(z0, z1))
U2(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)
U3(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)

Tuples:

F1_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))
F1_IN(z0) → c1

S tuples:

F1_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))
F1_IN(z0) → c1

K tuples:none
Defined Rule Symbols:

f1_in, U1, f5_in, U2, U3

Defined Pair Symbols:

F1_IN, F5_IN

Compound Symbols:

c1, c3, c4, c1

(21) CdtKnowledgeProof (EQUIVALENT transformation)

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

F1_IN(z0) → c1(F5_IN(z0))
F1_IN(z0) → c1

(22) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1(z0, z1), z2) → f1_out1(z0)
f5_in(z0) → f5_out1([], z0)
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
f5_in(.(z0, z1)) → U3(f5_in(z1), .(z0, z1))
U2(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)
U3(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)

Tuples:

F1_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))
F1_IN(z0) → c1

S tuples:

F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))

K tuples:

F1_IN(z0) → c1(F5_IN(z0))
F1_IN(z0) → c1

Defined Rule Symbols:

f1_in, U1, f5_in, U2, U3

Defined Pair Symbols:

F1_IN, F5_IN

Compound Symbols:

c1, c3, c4, c1

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

F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))

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

F1_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))
F1_IN(z0) → c1

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

POL(.(x₁, x₂)) = [2] + x₂
POL(F1_IN(x₁)) = [2] + x₁
POL(F5_IN(x₁)) = [1] + x₁
POL(c1) = 0
POL(c1(x₁)) = x₁
POL(c3(x₁)) = x₁
POL(c4(x₁)) = x₁

(24) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(z0) → U1(f5_in(z0), z0)
U1(f5_out1(z0, z1), z2) → f1_out1(z0)
f5_in(z0) → f5_out1([], z0)
f5_in(.(z0, z1)) → U2(f5_in(z1), .(z0, z1))
f5_in(.(z0, z1)) → U3(f5_in(z1), .(z0, z1))
U2(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)
U3(f5_out1(z0, z1), .(z2, z3)) → f5_out1(.(z2, z0), z1)

Tuples:

F1_IN(z0) → c1(F5_IN(z0))
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))
F1_IN(z0) → c1

S tuples:none
K tuples:

F1_IN(z0) → c1(F5_IN(z0))
F1_IN(z0) → c1
F5_IN(.(z0, z1)) → c3(F5_IN(z1))
F5_IN(.(z0, z1)) → c4(F5_IN(z1))

Defined Rule Symbols:

f1_in, U1, f5_in, U2, U3

Defined Pair Symbols:

F1_IN, F5_IN

Compound Symbols:

c1, c3, c4, c1