Left Termination of the query pattern
countstack(g,a)
w.r.t. the given Prolog program could successfully be proven:

(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) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: countstack(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: 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];
7 [label="7: ','(!_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];
14 [label="14: 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];
15 [label="15: eq(T5, 0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: eq(T5, 0), SCOPE: 2, CLAUSE: 11\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(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];
33 [label="33: ','(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];
36 [label="36: ','(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];
42 [label="42: ','(!_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];
45 [label="45: ?_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];
48 [label="48: ','(popped(push(nil, T19), X16), countstack(X16, T13))\n\nT19 is ground\nX16 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: ','(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];
51 [label="51: ','(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];
54 [label="54: countstack(T24, T13)\n\nT24 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: 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];
60 [label="60: ','(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];
61 [label="61: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(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];
67 [label="67: ','(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];
72 [label="72: ','(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];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: ','(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];
79 [label="79: ','(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];
84 [label="84: ','(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];
85 [label="85: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: ','(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];
89 [label="89: ','(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];
95 [label="95: ','(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];
98 [label="98: ','(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];
99 [label="99: ','(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];
101 [label="101: countstack(push(T57, push(T58, T59)), T32)\n\nT57 is ground\nT58 is ground\nT59 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 102 [arrowhead = none ];
102 -> 6;

103 [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];
6 -> 103 [arrowhead = none ];
103 -> 7;

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

105 [label="CUT", fontsize=14, style = filled, fillcolor = lightgreen];
7 -> 105 [arrowhead = none ];
105 -> 15;

106 [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];
14 -> 106 [arrowhead = none ];
106 -> 28;

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

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

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

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

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

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

113 [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];
36 -> 113 [arrowhead = none ];
113 -> 42;

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

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

116 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
45 -> 116 [arrowhead = none ];
116 -> 57;

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

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

119 [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];
51 -> 119 [arrowhead = none ];
119 -> 54;

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

121 [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];
57 -> 121 [arrowhead = none ];
121 -> 60;

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

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

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

125 [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];
67 -> 125 [arrowhead = none ];
125 -> 72;

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

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

128 [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];
75 -> 128 [arrowhead = none ];
128 -> 79;

129 [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];
79 -> 129 [arrowhead = none ];
129 -> 84;

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

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

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

133 [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];
89 -> 133 [arrowhead = none ];
133 -> 95;

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

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

136 [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];
99 -> 136 [arrowhead = none ];
136 -> 101;

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

}

(2) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T24), T13) → U1_ga(T24, T13, countstackA_in_ga(T24, T13))
countstackA_in_ga(push(cons(T57, T58), T59), s(T32)) → U2_ga(T57, T58, T59, T32, countstackA_in_ga(push(T57, push(T58, T59)), T32))
U2_ga(T57, T58, T59, T32, countstackA_out_ga(push(T57, push(T58, T59)), T32)) → countstackA_out_ga(push(cons(T57, T58), T59), s(T32))
U1_ga(T24, T13, countstackA_out_ga(T24, T13)) → countstackA_out_ga(push(nil, T24), T13)

The argument filtering Pi contains the following mapping:
countstackA_in_ga(x1, x2)  =  countstackA_in_ga(x1)
empty  =  empty
countstackA_out_ga(x1, x2)  =  countstackA_out_ga(x1, x2)
push(x1, x2)  =  push(x1, x2)
nil  =  nil
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
cons(x1, x2)  =  cons(x1, x2)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
s(x1)  =  s(x1)

(3) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

COUNTSTACKA_IN_GA(push(nil, T24), T13) → U1_GA(T24, T13, countstackA_in_ga(T24, T13))
COUNTSTACKA_IN_GA(push(nil, T24), T13) → COUNTSTACKA_IN_GA(T24, T13)
COUNTSTACKA_IN_GA(push(cons(T57, T58), T59), s(T32)) → U2_GA(T57, T58, T59, T32, countstackA_in_ga(push(T57, push(T58, T59)), T32))
COUNTSTACKA_IN_GA(push(cons(T57, T58), T59), s(T32)) → COUNTSTACKA_IN_GA(push(T57, push(T58, T59)), T32)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T24), T13) → U1_ga(T24, T13, countstackA_in_ga(T24, T13))
countstackA_in_ga(push(cons(T57, T58), T59), s(T32)) → U2_ga(T57, T58, T59, T32, countstackA_in_ga(push(T57, push(T58, T59)), T32))
U2_ga(T57, T58, T59, T32, countstackA_out_ga(push(T57, push(T58, T59)), T32)) → countstackA_out_ga(push(cons(T57, T58), T59), s(T32))
U1_ga(T24, T13, countstackA_out_ga(T24, T13)) → countstackA_out_ga(push(nil, T24), T13)

The argument filtering Pi contains the following mapping:
countstackA_in_ga(x1, x2)  =  countstackA_in_ga(x1)
empty  =  empty
countstackA_out_ga(x1, x2)  =  countstackA_out_ga(x1, x2)
push(x1, x2)  =  push(x1, x2)
nil  =  nil
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
cons(x1, x2)  =  cons(x1, x2)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
s(x1)  =  s(x1)
COUNTSTACKA_IN_GA(x1, x2)  =  COUNTSTACKA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(4) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

COUNTSTACKA_IN_GA(push(nil, T24), T13) → U1_GA(T24, T13, countstackA_in_ga(T24, T13))
COUNTSTACKA_IN_GA(push(nil, T24), T13) → COUNTSTACKA_IN_GA(T24, T13)
COUNTSTACKA_IN_GA(push(cons(T57, T58), T59), s(T32)) → U2_GA(T57, T58, T59, T32, countstackA_in_ga(push(T57, push(T58, T59)), T32))
COUNTSTACKA_IN_GA(push(cons(T57, T58), T59), s(T32)) → COUNTSTACKA_IN_GA(push(T57, push(T58, T59)), T32)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T24), T13) → U1_ga(T24, T13, countstackA_in_ga(T24, T13))
countstackA_in_ga(push(cons(T57, T58), T59), s(T32)) → U2_ga(T57, T58, T59, T32, countstackA_in_ga(push(T57, push(T58, T59)), T32))
U2_ga(T57, T58, T59, T32, countstackA_out_ga(push(T57, push(T58, T59)), T32)) → countstackA_out_ga(push(cons(T57, T58), T59), s(T32))
U1_ga(T24, T13, countstackA_out_ga(T24, T13)) → countstackA_out_ga(push(nil, T24), T13)

The argument filtering Pi contains the following mapping:
countstackA_in_ga(x1, x2)  =  countstackA_in_ga(x1)
empty  =  empty
countstackA_out_ga(x1, x2)  =  countstackA_out_ga(x1, x2)
push(x1, x2)  =  push(x1, x2)
nil  =  nil
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
cons(x1, x2)  =  cons(x1, x2)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
s(x1)  =  s(x1)
COUNTSTACKA_IN_GA(x1, x2)  =  COUNTSTACKA_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)

We have to consider all (P,R,Pi)-chains

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 2 less nodes.

(6) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

COUNTSTACKA_IN_GA(push(cons(T57, T58), T59), s(T32)) → COUNTSTACKA_IN_GA(push(T57, push(T58, T59)), T32)
COUNTSTACKA_IN_GA(push(nil, T24), T13) → COUNTSTACKA_IN_GA(T24, T13)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, T24), T13) → U1_ga(T24, T13, countstackA_in_ga(T24, T13))
countstackA_in_ga(push(cons(T57, T58), T59), s(T32)) → U2_ga(T57, T58, T59, T32, countstackA_in_ga(push(T57, push(T58, T59)), T32))
U2_ga(T57, T58, T59, T32, countstackA_out_ga(push(T57, push(T58, T59)), T32)) → countstackA_out_ga(push(cons(T57, T58), T59), s(T32))
U1_ga(T24, T13, countstackA_out_ga(T24, T13)) → countstackA_out_ga(push(nil, T24), T13)

The argument filtering Pi contains the following mapping:
countstackA_in_ga(x1, x2)  =  countstackA_in_ga(x1)
empty  =  empty
countstackA_out_ga(x1, x2)  =  countstackA_out_ga(x1, x2)
push(x1, x2)  =  push(x1, x2)
nil  =  nil
U1_ga(x1, x2, x3)  =  U1_ga(x1, x3)
cons(x1, x2)  =  cons(x1, x2)
U2_ga(x1, x2, x3, x4, x5)  =  U2_ga(x1, x2, x3, x5)
s(x1)  =  s(x1)
COUNTSTACKA_IN_GA(x1, x2)  =  COUNTSTACKA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(7) UsableRulesProof (EQUIVALENT transformation)

For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.

(8) Obligation:

Pi DP problem:
The TRS P consists of the following rules:

COUNTSTACKA_IN_GA(push(cons(T57, T58), T59), s(T32)) → COUNTSTACKA_IN_GA(push(T57, push(T58, T59)), T32)
COUNTSTACKA_IN_GA(push(nil, T24), T13) → COUNTSTACKA_IN_GA(T24, T13)

R is empty.
The argument filtering Pi contains the following mapping:
push(x1, x2)  =  push(x1, x2)
nil  =  nil
cons(x1, x2)  =  cons(x1, x2)
s(x1)  =  s(x1)
COUNTSTACKA_IN_GA(x1, x2)  =  COUNTSTACKA_IN_GA(x1)

We have to consider all (P,R,Pi)-chains

(9) PiDPToQDPProof (SOUND transformation)

Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.

(10) Obligation:

Q DP problem:
The TRS P consists of the following rules:

COUNTSTACKA_IN_GA(push(cons(T57, T58), T59)) → COUNTSTACKA_IN_GA(push(T57, push(T58, T59)))
COUNTSTACKA_IN_GA(push(nil, T24)) → COUNTSTACKA_IN_GA(T24)

R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(11) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

COUNTSTACKA_IN_GA(push(cons(T57, T58), T59)) → COUNTSTACKA_IN_GA(push(T57, push(T58, T59)))
COUNTSTACKA_IN_GA(push(nil, T24)) → COUNTSTACKA_IN_GA(T24)

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(COUNTSTACKA_IN_GA(x₁)) = 2·x₁   
POL(cons(x₁, x₂)) = 2 + 2·x₁ + 2·x₂   
POL(nil) = 0   
POL(push(x₁, x₂)) = 1 + 2·x₁ + x₂   

(12) Obligation:

Q DP problem:
P is empty.
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.

(13) PisEmptyProof (EQUIVALENT transformation)

The TRS P is empty. Hence, there is no (P,Q,R) chain.

(14) YES