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

(0) Obligation:

Clauses:

countstack(empty, X) :- ','(!, eq(X, 0)).
countstack(S, X) :- ','(pop(S, nil), ','(!, ','(popped(S, Pd), countstack(Pd, X)))).
countstack(S, s(X)) :- ','(pop(S, P), ','(head(P, H), ','(tail(P, T), ','(popped(S, Pd), countstack(push(H, push(T, Pd)), X))))).
pop(empty, X1).
pop(push(P, X2), P).
popped(empty, empty).
popped(push(X3, Pd), Pd).
head(nil, X4).
head(cons(H, X5), H).
tail(nil, nil).
tail(cons(X6, T), T).
eq(X, X).

Query: countstack(g,a)

(1) 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: countstack(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
3 [label="3: countstack(T1, T2), SCOPE: 1, CLAUSE: 0 | countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
6 [label="6: ','(!_1, eq(T6, 0)) | countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX9 is free\ncountstack(T1, T2) !=? countstack(empty, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
9 [label="9: eq(T6, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: eq(T6, 0), SCOPE: 2, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(pop(T15, nil), ','(!_1, ','(popped(T15, X20), countstack(X20, T17)))) | countstack(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX9 is free\nX20 is free\ncountstack(T15, T2) !=? countstack(empty, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(pop(T15, nil), ','(!_1, ','(popped(T15, X20), countstack(X20, T17)))), SCOPE: 3, CLAUSE: 3 | ','(pop(T15, nil), ','(!_1, ','(popped(T15, X20), countstack(X20, T17)))), SCOPE: 3, CLAUSE: 4 | ?_3 | countstack(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX9 is free\nX20 is free\ncountstack(T15, T2) !=? countstack(empty, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(pop(T15, nil), ','(!_1, ','(popped(T15, X20), countstack(X20, T17)))), SCOPE: 3, CLAUSE: 4 | ?_3 | countstack(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX9 is free\nX20 is free\ncountstack(T15, T2) !=? countstack(empty, X9)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: ','(!_1, ','(popped(push(nil, T23), X20), countstack(X20, T17))) | ?_3 | countstack(push(nil, T23), T2), SCOPE: 1, CLAUSE: 2\n\nT23 is ground\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ?_3 | countstack(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX9 is free\nX26 is free\nX27 is free\ncountstack(T15, T2) !=? countstack(empty, X9)\npop(T15, nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: ','(popped(push(nil, T23), X20), countstack(X20, T17))\n\nT23 is ground\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(popped(push(nil, T23), X20), countstack(X20, T17)), SCOPE: 4, CLAUSE: 5 | ','(popped(push(nil, T23), X20), countstack(X20, T17)), SCOPE: 4, CLAUSE: 6\n\nT23 is ground\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(popped(push(nil, T23), X20), countstack(X20, T17)), SCOPE: 4, CLAUSE: 6\n\nT23 is ground\nX20 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: countstack(T28, T17)\n\nT28 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: countstack(T15, T2), SCOPE: 1, CLAUSE: 2\n\nT15 is ground\nX9 is free\nX26 is free\nX27 is free\ncountstack(T15, T2) !=? countstack(empty, X9)\npop(T15, nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: ','(pop(T34, X47), ','(head(X47, X48), ','(tail(X47, X49), ','(popped(T34, X50), countstack(push(X48, push(X49, X50)), T36)))))\n\nT34 is ground\nX9 is free\nX26 is free\nX27 is free\nX47 is free\nX48 is free\nX49 is free\nX50 is free\ncountstack(T34, T2) !=? countstack(empty, X9)\npop(T34, nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: ','(pop(T34, X47), ','(head(X47, X48), ','(tail(X47, X49), ','(popped(T34, X50), countstack(push(X48, push(X49, X50)), T36))))), SCOPE: 5, CLAUSE: 3 | ','(pop(T34, X47), ','(head(X47, X48), ','(tail(X47, X49), ','(popped(T34, X50), countstack(push(X48, push(X49, X50)), T36))))), SCOPE: 5, CLAUSE: 4\n\nT34 is ground\nX9 is free\nX26 is free\nX27 is free\nX47 is free\nX48 is free\nX49 is free\nX50 is free\ncountstack(T34, T2) !=? countstack(empty, X9)\npop(T34, nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: ','(pop(T34, X47), ','(head(X47, X48), ','(tail(X47, X49), ','(popped(T34, X50), countstack(push(X48, push(X49, X50)), T36))))), SCOPE: 5, CLAUSE: 4\n\nT34 is ground\nX9 is free\nX26 is free\nX27 is free\nX47 is free\nX48 is free\nX49 is free\nX50 is free\ncountstack(T34, T2) !=? countstack(empty, X9)\npop(T34, nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: ','(head(T41, X48), ','(tail(T41, X49), ','(popped(push(T41, T42), X50), countstack(push(X48, push(X49, X50)), T36))))\n\nT41 is ground\nT42 is ground\nX26 is free\nX27 is free\nX48 is free\nX49 is free\nX50 is free\npop(push(T41, T42), nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: ','(head(T41, X48), ','(tail(T41, X49), ','(popped(push(T41, T42), X50), countstack(push(X48, push(X49, X50)), T36)))), SCOPE: 6, CLAUSE: 7 | ','(head(T41, X48), ','(tail(T41, X49), ','(popped(push(T41, T42), X50), countstack(push(X48, push(X49, X50)), T36)))), SCOPE: 6, CLAUSE: 8\n\nT41 is ground\nT42 is ground\nX26 is free\nX27 is free\nX48 is free\nX49 is free\nX50 is free\npop(push(T41, T42), nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: ','(head(T41, X48), ','(tail(T41, X49), ','(popped(push(T41, T42), X50), countstack(push(X48, push(X49, X50)), T36)))), SCOPE: 6, CLAUSE: 8\n\nT41 is ground\nT42 is ground\nX26 is free\nX27 is free\nX48 is free\nX49 is free\nX50 is free\npop(push(T41, T42), nil) !=? pop(push(X26, X27), X26)", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: ','(tail(cons(T47, T48), X49), ','(popped(push(cons(T47, T48), T42), X50), countstack(push(T47, push(X49, X50)), T36)))\n\nT42 is ground\nT47 is ground\nT48 is ground\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: ','(tail(cons(T47, T48), X49), ','(popped(push(cons(T47, T48), T42), X50), countstack(push(T47, push(X49, X50)), T36))), SCOPE: 7, CLAUSE: 9 | ','(tail(cons(T47, T48), X49), ','(popped(push(cons(T47, T48), T42), X50), countstack(push(T47, push(X49, X50)), T36))), SCOPE: 7, CLAUSE: 10\n\nT42 is ground\nT47 is ground\nT48 is ground\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: ','(tail(cons(T47, T48), X49), ','(popped(push(cons(T47, T48), T42), X50), countstack(push(T47, push(X49, X50)), T36))), SCOPE: 7, CLAUSE: 10\n\nT42 is ground\nT47 is ground\nT48 is ground\nX49 is free\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: ','(popped(push(cons(T53, T54), T42), X50), countstack(push(T53, push(T54, X50)), T36))\n\nT42 is ground\nT53 is ground\nT54 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: ','(popped(push(cons(T53, T54), T42), X50), countstack(push(T53, push(T54, X50)), T36)), SCOPE: 8, CLAUSE: 5 | ','(popped(push(cons(T53, T54), T42), X50), countstack(push(T53, push(T54, X50)), T36)), SCOPE: 8, CLAUSE: 6\n\nT42 is ground\nT53 is ground\nT54 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: ','(popped(push(cons(T53, T54), T42), X50), countstack(push(T53, push(T54, X50)), T36)), SCOPE: 8, CLAUSE: 6\n\nT42 is ground\nT53 is ground\nT54 is ground\nX50 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: countstack(push(T61, push(T62, T63)), T36)\n\nT61 is ground\nT62 is ground\nT63 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 71 [arrowhead = none ];
71 -> 3;

72 [label="EVAL with clause\ncountstack(empty, X9) :- ','(!_1, eq(X9, 0)).\nand substitutionT1 -> empty,\nT2 -> T6,\nX9 -> T6,\nT5 -> T6", fontsize=14, style = filled, fillcolor = lightblue];
3 -> 72 [arrowhead = none ];
72 -> 6;

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

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

75 [label="ONLY EVAL with clause\ncountstack(X18, X19) :- ','(pop(X18, nil), ','(!_1, ','(popped(X18, X20), countstack(X20, X19)))).\nand substitutionT1 -> T15,\nX18 -> T15,\nT2 -> T17,\nX19 -> T17,\nT16 -> T17", fontsize=14, style = filled, fillcolor = lightblue];
8 -> 75 [arrowhead = none ];
75 -> 28;

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

77 [label="EVAL with clause\neq(X12, X12).\nand substitutionT6 -> 0,\nX12 -> 0,\nT9 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
21 -> 77 [arrowhead = none ];
77 -> 24;

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

79 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
24 -> 79 [arrowhead = none ];
79 -> 26;

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

81 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (countstack(T15, T2), countstack(empty, X9))", fontsize=14, style = filled, fillcolor = lightgreen];
29 -> 81 [arrowhead = none ];
81 -> 30;

82 [label="EVAL with clause\npop(push(X26, X27), X26).\nand substitutionX26 -> nil,\nX27 -> T23,\nT15 -> push(nil, T23),\nT22 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 82 [arrowhead = none ];
82 -> 31;

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

84 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
31 -> 84 [arrowhead = none ];
84 -> 33;

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

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

87 [label="BACKTRACK\nfor clause: popped(empty, empty)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
35 -> 87 [arrowhead = none ];
87 -> 36;

88 [label="ONLY EVAL with clause\npopped(push(X34, X35), X35).\nand substitutionX34 -> nil,\nT23 -> T28,\nX35 -> T28,\nX20 -> T28", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 88 [arrowhead = none ];
88 -> 37;

89 [label="INSTANCE with matching:\nT1 -> T28\nT2 -> T17", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 89 [arrowhead = none , style=dashed];
89 -> 2[style=dashed];

90 [label="EVAL with clause\ncountstack(X45, s(X46)) :- ','(pop(X45, X47), ','(head(X47, X48), ','(tail(X47, X49), ','(popped(X45, X50), countstack(push(X48, push(X49, X50)), X46))))).\nand substitutionT15 -> T34,\nX45 -> T34,\nX46 -> T36,\nT2 -> s(T36),\nT35 -> T36", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 90 [arrowhead = none ];
90 -> 43;

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

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

93 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (countstack(T34, T2), countstack(empty, X9))", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 93 [arrowhead = none ];
93 -> 48;

94 [label="EVAL with clause\npop(push(X58, X59), X58).\nand substitutionX58 -> T41,\nX59 -> T42,\nT34 -> push(T41, T42),\nX47 -> T41", fontsize=14, style = filled, fillcolor = lightblue];
48 -> 94 [arrowhead = none ];
94 -> 51;

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

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

97 [label="BACKTRACK\nfor clause: head(nil, X4)\nwith clash: (pop(push(T41, T42), nil), pop(push(X26, X27), X26))", fontsize=14, style = filled, fillcolor = lightgreen];
53 -> 97 [arrowhead = none ];
97 -> 56;

98 [label="EVAL with clause\nhead(cons(X67, X68), X67).\nand substitutionX67 -> T47,\nX68 -> T48,\nT41 -> cons(T47, T48),\nX48 -> T47", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 98 [arrowhead = none ];
98 -> 59;

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

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

101 [label="BACKTRACK\nfor clause: tail(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 101 [arrowhead = none ];
101 -> 62;

102 [label="ONLY EVAL with clause\ntail(cons(X75, X76), X76).\nand substitutionT47 -> T53,\nX75 -> T53,\nT48 -> T54,\nX76 -> T54,\nX49 -> T54", fontsize=14, style = filled, fillcolor = lightblue];
62 -> 102 [arrowhead = none ];
102 -> 66;

103 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
66 -> 103 [arrowhead = none ];
103 -> 67;

104 [label="BACKTRACK\nfor clause: popped(empty, empty)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
67 -> 104 [arrowhead = none ];
104 -> 68;

105 [label="ONLY EVAL with clause\npopped(push(X83, X84), X84).\nand substitutionT53 -> T61,\nT54 -> T62,\nX83 -> cons(T61, T62),\nT42 -> T63,\nX84 -> T63,\nX50 -> T63", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 105 [arrowhead = none ];
105 -> 70;

106 [label="INSTANCE with matching:\nT1 -> push(T61, push(T62, T63))\nT2 -> T36", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 106 [arrowhead = none , style=dashed];
106 -> 2[style=dashed];

}

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(empty) → f2_out1(0)
f2_in(push(nil, z0)) → U1(f2_in(z0), push(nil, z0))
f2_in(push(cons(z0, z1), z2)) → U2(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U1(f2_out1(z0), push(nil, z1)) → f2_out1(z0)
U2(f2_out1(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))

Tuples:

F2_IN(push(nil, z0)) → c1(U1'(f2_in(z0), push(nil, z0)), F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(U2'(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F2_IN(push(z0, push(z1, z2))))

S tuples:

F2_IN(push(nil, z0)) → c1(U1'(f2_in(z0), push(nil, z0)), F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(U2'(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F2_IN(push(z0, push(z1, z2))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2

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

Removed 2 trailing tuple parts

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(empty) → f2_out1(0)
f2_in(push(nil, z0)) → U1(f2_in(z0), push(nil, z0))
f2_in(push(cons(z0, z1), z2)) → U2(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U1(f2_out1(z0), push(nil, z1)) → f2_out1(z0)
U2(f2_out1(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))

Tuples:

F2_IN(push(nil, z0)) → c1(F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(F2_IN(push(z0, push(z1, z2))))

S tuples:

F2_IN(push(nil, z0)) → c1(F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(F2_IN(push(z0, push(z1, z2))))

K tuples:none
Defined Rule Symbols:

f2_in, U1, U2

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2

(5) 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(push(nil, z0)) → c1(F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(F2_IN(push(z0, push(z1, z2))))

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

F2_IN(push(nil, z0)) → c1(F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(F2_IN(push(z0, push(z1, z2))))

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

POL(F2_IN(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(cons(x₁, x₂)) = [3] + x₁ + x₂   
POL(nil) = 0   
POL(push(x₁, x₂)) = [1] + x₁ + x₂   

(6) Obligation:

Complexity Dependency Tuples Problem
Rules:

f2_in(empty) → f2_out1(0)
f2_in(push(nil, z0)) → U1(f2_in(z0), push(nil, z0))
f2_in(push(cons(z0, z1), z2)) → U2(f2_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U1(f2_out1(z0), push(nil, z1)) → f2_out1(z0)
U2(f2_out1(z0), push(cons(z1, z2), z3)) → f2_out1(s(z0))

Tuples:

F2_IN(push(nil, z0)) → c1(F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(F2_IN(push(z0, push(z1, z2))))

S tuples:none
K tuples:

F2_IN(push(nil, z0)) → c1(F2_IN(z0))
F2_IN(push(cons(z0, z1), z2)) → c2(F2_IN(push(z0, push(z1, z2))))

Defined Rule Symbols:

f2_in, U1, U2

Defined Pair Symbols:

F2_IN

Compound Symbols:

c1, c2

(7) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(8) BOUNDS(O(1), O(1))

(9) 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: countstack(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: countstack(T1, T2), SCOPE: 1, CLAUSE: 0 | countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
5 [label="5: ','(!_1, eq(T5, 0)) | countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
7 [label="7: countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX8 is free\ncountstack(T1, T2) !=? countstack(empty, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: eq(T5, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: eq(T5, 0), SCOPE: 2, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(pop(T11, nil), ','(!_1, ','(popped(T11, X16), countstack(X16, T13)))) | countstack(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX8 is free\nX16 is free\ncountstack(T11, T2) !=? countstack(empty, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(pop(T11, nil), ','(!_1, ','(popped(T11, X16), countstack(X16, T13)))), SCOPE: 3, CLAUSE: 3 | ','(pop(T11, nil), ','(!_1, ','(popped(T11, X16), countstack(X16, T13)))), SCOPE: 3, CLAUSE: 4 | ?_3 | countstack(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX8 is free\nX16 is free\ncountstack(T11, T2) !=? countstack(empty, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(pop(T11, nil), ','(!_1, ','(popped(T11, X16), countstack(X16, T13)))), SCOPE: 3, CLAUSE: 4 | ?_3 | countstack(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX8 is free\nX16 is free\ncountstack(T11, T2) !=? countstack(empty, X8)", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(!_1, ','(popped(push(nil, T19), X16), countstack(X16, T13))) | ?_3 | countstack(push(nil, T19), T2), SCOPE: 1, CLAUSE: 2\n\nT19 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ?_3 | countstack(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX8 is free\nX22 is free\nX23 is free\ncountstack(T11, T2) !=? countstack(empty, X8)\npop(T11, nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(popped(push(nil, T19), X16), countstack(X16, T13))\n\nT19 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(popped(push(nil, T19), X16), countstack(X16, T13)), SCOPE: 4, CLAUSE: 5 | ','(popped(push(nil, T19), X16), countstack(X16, T13)), SCOPE: 4, CLAUSE: 6\n\nT19 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: ','(popped(push(nil, T19), X16), countstack(X16, T13)), SCOPE: 4, CLAUSE: 6\n\nT19 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: countstack(T24, T13)\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: countstack(T11, T2), SCOPE: 1, CLAUSE: 2\n\nT11 is ground\nX8 is free\nX22 is free\nX23 is free\ncountstack(T11, T2) !=? countstack(empty, X8)\npop(T11, nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: ','(pop(T30, X43), ','(head(X43, X44), ','(tail(X43, X45), ','(popped(T30, X46), countstack(push(X44, push(X45, X46)), T32)))))\n\nT30 is ground\nX8 is free\nX22 is free\nX23 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\ncountstack(T30, T2) !=? countstack(empty, X8)\npop(T30, nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: ','(pop(T30, X43), ','(head(X43, X44), ','(tail(X43, X45), ','(popped(T30, X46), countstack(push(X44, push(X45, X46)), T32))))), SCOPE: 5, CLAUSE: 3 | ','(pop(T30, X43), ','(head(X43, X44), ','(tail(X43, X45), ','(popped(T30, X46), countstack(push(X44, push(X45, X46)), T32))))), SCOPE: 5, CLAUSE: 4\n\nT30 is ground\nX8 is free\nX22 is free\nX23 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\ncountstack(T30, T2) !=? countstack(empty, X8)\npop(T30, nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: ','(pop(T30, X43), ','(head(X43, X44), ','(tail(X43, X45), ','(popped(T30, X46), countstack(push(X44, push(X45, X46)), T32))))), SCOPE: 5, CLAUSE: 4\n\nT30 is ground\nX8 is free\nX22 is free\nX23 is free\nX43 is free\nX44 is free\nX45 is free\nX46 is free\ncountstack(T30, T2) !=? countstack(empty, X8)\npop(T30, nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: ','(head(T37, X44), ','(tail(T37, X45), ','(popped(push(T37, T38), X46), countstack(push(X44, push(X45, X46)), T32))))\n\nT37 is ground\nT38 is ground\nX22 is free\nX23 is free\nX44 is free\nX45 is free\nX46 is free\npop(push(T37, T38), nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: ','(head(T37, X44), ','(tail(T37, X45), ','(popped(push(T37, T38), X46), countstack(push(X44, push(X45, X46)), T32)))), SCOPE: 6, CLAUSE: 7 | ','(head(T37, X44), ','(tail(T37, X45), ','(popped(push(T37, T38), X46), countstack(push(X44, push(X45, X46)), T32)))), SCOPE: 6, CLAUSE: 8\n\nT37 is ground\nT38 is ground\nX22 is free\nX23 is free\nX44 is free\nX45 is free\nX46 is free\npop(push(T37, T38), nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(head(T37, X44), ','(tail(T37, X45), ','(popped(push(T37, T38), X46), countstack(push(X44, push(X45, X46)), T32)))), SCOPE: 6, CLAUSE: 8\n\nT37 is ground\nT38 is ground\nX22 is free\nX23 is free\nX44 is free\nX45 is free\nX46 is free\npop(push(T37, T38), nil) !=? pop(push(X22, X23), X22)", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: ','(tail(cons(T43, T44), X45), ','(popped(push(cons(T43, T44), T38), X46), countstack(push(T43, push(X45, X46)), T32)))\n\nT38 is ground\nT43 is ground\nT44 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: ','(tail(cons(T43, T44), X45), ','(popped(push(cons(T43, T44), T38), X46), countstack(push(T43, push(X45, X46)), T32))), SCOPE: 7, CLAUSE: 9 | ','(tail(cons(T43, T44), X45), ','(popped(push(cons(T43, T44), T38), X46), countstack(push(T43, push(X45, X46)), T32))), SCOPE: 7, CLAUSE: 10\n\nT38 is ground\nT43 is ground\nT44 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(tail(cons(T43, T44), X45), ','(popped(push(cons(T43, T44), T38), X46), countstack(push(T43, push(X45, X46)), T32))), SCOPE: 7, CLAUSE: 10\n\nT38 is ground\nT43 is ground\nT44 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(popped(push(cons(T49, T50), T38), X46), countstack(push(T49, push(T50, X46)), T32))\n\nT38 is ground\nT49 is ground\nT50 is ground\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: ','(popped(push(cons(T49, T50), T38), X46), countstack(push(T49, push(T50, X46)), T32)), SCOPE: 8, CLAUSE: 5 | ','(popped(push(cons(T49, T50), T38), X46), countstack(push(T49, push(T50, X46)), T32)), SCOPE: 8, CLAUSE: 6\n\nT38 is ground\nT49 is ground\nT50 is ground\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: ','(popped(push(cons(T49, T50), T38), X46), countstack(push(T49, push(T50, X46)), T32)), SCOPE: 8, CLAUSE: 6\n\nT38 is ground\nT49 is ground\nT50 is ground\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: countstack(push(T57, push(T58, T59)), T32)\n\nT57 is ground\nT58 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 70 [arrowhead = none ];
70 -> 4;

71 [label="EVAL with clause\ncountstack(empty, X8) :- ','(!_1, eq(X8, 0)).\nand substitutionT1 -> empty,\nT2 -> T5,\nX8 -> T5,\nT4 -> T5", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 71 [arrowhead = none ];
71 -> 5;

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

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

74 [label="ONLY EVAL with clause\ncountstack(X14, X15) :- ','(pop(X14, nil), ','(!_1, ','(popped(X14, X16), countstack(X16, X15)))).\nand substitutionT1 -> T11,\nX14 -> T11,\nT2 -> T13,\nX15 -> T13,\nT12 -> T13", fontsize=14, style = filled, fillcolor = lightblue];
7 -> 74 [arrowhead = none ];
74 -> 15;

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

76 [label="EVAL with clause\neq(X11, X11).\nand substitutionT5 -> 0,\nX11 -> 0,\nT8 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
11 -> 76 [arrowhead = none ];
76 -> 12;

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

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

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

80 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (countstack(T11, T2), countstack(empty, X8))", fontsize=14, style = filled, fillcolor = lightgreen];
16 -> 80 [arrowhead = none ];
80 -> 17;

81 [label="EVAL with clause\npop(push(X22, X23), X22).\nand substitutionX22 -> nil,\nX23 -> T19,\nT11 -> push(nil, T19),\nT18 -> nil", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 81 [arrowhead = none ];
81 -> 18;

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

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

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

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

86 [label="BACKTRACK\nfor clause: popped(empty, empty)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 86 [arrowhead = none ];
86 -> 23;

87 [label="ONLY EVAL with clause\npopped(push(X30, X31), X31).\nand substitutionX30 -> nil,\nT19 -> T24,\nX31 -> T24,\nX16 -> T24", fontsize=14, style = filled, fillcolor = lightblue];
23 -> 87 [arrowhead = none ];
87 -> 27;

88 [label="INSTANCE with matching:\nT1 -> T24\nT2 -> T13", fontsize=14, style = filled, fillcolor = lightgrey];
27 -> 88 [arrowhead = none , style=dashed];
88 -> 1[style=dashed];

89 [label="EVAL with clause\ncountstack(X41, s(X42)) :- ','(pop(X41, X43), ','(head(X43, X44), ','(tail(X43, X45), ','(popped(X41, X46), countstack(push(X44, push(X45, X46)), X42))))).\nand substitutionT11 -> T30,\nX41 -> T30,\nX42 -> T32,\nT2 -> s(T32),\nT31 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 89 [arrowhead = none ];
89 -> 39;

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

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

92 [label="BACKTRACK\nfor clause: pop(empty, X1)\nwith clash: (countstack(T30, T2), countstack(empty, X8))", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 92 [arrowhead = none ];
92 -> 42;

93 [label="EVAL with clause\npop(push(X54, X55), X54).\nand substitutionX54 -> T37,\nX55 -> T38,\nT30 -> push(T37, T38),\nX43 -> T37", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 93 [arrowhead = none ];
93 -> 46;

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

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

96 [label="BACKTRACK\nfor clause: head(nil, X4)\nwith clash: (pop(push(T37, T38), nil), pop(push(X22, X23), X22))", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 96 [arrowhead = none ];
96 -> 50;

97 [label="EVAL with clause\nhead(cons(X63, X64), X63).\nand substitutionX63 -> T43,\nX64 -> T44,\nT37 -> cons(T43, T44),\nX44 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 97 [arrowhead = none ];
97 -> 54;

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

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

100 [label="BACKTRACK\nfor clause: tail(nil, nil)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
57 -> 100 [arrowhead = none ];
100 -> 58;

101 [label="ONLY EVAL with clause\ntail(cons(X71, X72), X72).\nand substitutionT43 -> T49,\nX71 -> T49,\nT44 -> T50,\nX72 -> T50,\nX45 -> T50", fontsize=14, style = filled, fillcolor = lightblue];
58 -> 101 [arrowhead = none ];
101 -> 63;

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

103 [label="BACKTRACK\nfor clause: popped(empty, empty)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
64 -> 103 [arrowhead = none ];
103 -> 65;

104 [label="ONLY EVAL with clause\npopped(push(X79, X80), X80).\nand substitutionT49 -> T57,\nT50 -> T58,\nX79 -> cons(T57, T58),\nT38 -> T59,\nX80 -> T59,\nX46 -> T59", fontsize=14, style = filled, fillcolor = lightblue];
65 -> 104 [arrowhead = none ];
104 -> 69;

105 [label="INSTANCE with matching:\nT1 -> push(T57, push(T58, T59))\nT2 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
69 -> 105 [arrowhead = none , style=dashed];
105 -> 1[style=dashed];

}

(10) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(empty) → f1_out1(0)
f1_in(push(nil, z0)) → U1(f1_in(z0), push(nil, z0))
f1_in(push(cons(z0, z1), z2)) → U2(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U1(f1_out1(z0), push(nil, z1)) → f1_out1(z0)
U2(f1_out1(z0), push(cons(z1, z2), z3)) → f1_out1(s(z0))

Tuples:

F1_IN(push(nil, z0)) → c1(U1'(f1_in(z0), push(nil, z0)), F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(U2'(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F1_IN(push(z0, push(z1, z2))))

S tuples:

F1_IN(push(nil, z0)) → c1(U1'(f1_in(z0), push(nil, z0)), F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(U2'(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2)), F1_IN(push(z0, push(z1, z2))))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2

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

Removed 2 trailing tuple parts

(12) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(empty) → f1_out1(0)
f1_in(push(nil, z0)) → U1(f1_in(z0), push(nil, z0))
f1_in(push(cons(z0, z1), z2)) → U2(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U1(f1_out1(z0), push(nil, z1)) → f1_out1(z0)
U2(f1_out1(z0), push(cons(z1, z2), z3)) → f1_out1(s(z0))

Tuples:

F1_IN(push(nil, z0)) → c1(F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(F1_IN(push(z0, push(z1, z2))))

S tuples:

F1_IN(push(nil, z0)) → c1(F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(F1_IN(push(z0, push(z1, z2))))

K tuples:none
Defined Rule Symbols:

f1_in, U1, U2

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2

(13) 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(push(nil, z0)) → c1(F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(F1_IN(push(z0, push(z1, z2))))

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

F1_IN(push(nil, z0)) → c1(F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(F1_IN(push(z0, push(z1, z2))))

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

POL(F1_IN(x₁)) = x₁   
POL(c1(x₁)) = x₁   
POL(c2(x₁)) = x₁   
POL(cons(x₁, x₂)) = [3] + x₁ + x₂   
POL(nil) = 0   
POL(push(x₁, x₂)) = [1] + x₁ + x₂   

(14) Obligation:

Complexity Dependency Tuples Problem
Rules:

f1_in(empty) → f1_out1(0)
f1_in(push(nil, z0)) → U1(f1_in(z0), push(nil, z0))
f1_in(push(cons(z0, z1), z2)) → U2(f1_in(push(z0, push(z1, z2))), push(cons(z0, z1), z2))
U1(f1_out1(z0), push(nil, z1)) → f1_out1(z0)
U2(f1_out1(z0), push(cons(z1, z2), z3)) → f1_out1(s(z0))

Tuples:

F1_IN(push(nil, z0)) → c1(F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(F1_IN(push(z0, push(z1, z2))))

S tuples:none
K tuples:

F1_IN(push(nil, z0)) → c1(F1_IN(z0))
F1_IN(push(cons(z0, z1), z2)) → c2(F1_IN(push(z0, push(z1, z2))))

Defined Rule Symbols:

f1_in, U1, U2

Defined Pair Symbols:

F1_IN

Compound Symbols:

c1, c2