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, 0).
countstack(push(nil, T), X) :- countstack(T, X).
countstack(push(cons(U, V), T), s(X)) :- countstack(push(U, push(V, T)), X).

Query: countstack(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: countstack(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
5 [label="5: 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];
11 [label="11: true | countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: countstack(T1, T2), SCOPE: 1, CLAUSE: 1 | countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\ncountstack(T1, T2) !=? countstack(empty, 0)", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: countstack(empty, T2), SCOPE: 1, CLAUSE: 1 | countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: countstack(empty, T2), SCOPE: 1, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="23: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: countstack(T5, T7) | countstack(push(nil, T5), T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: countstack(T1, T2), SCOPE: 1, CLAUSE: 2\n\nT1 is ground\nX9 is free\nX10 is free\ncountstack(T1, T2) !=? countstack(empty, 0)\ncountstack(T1, T2) !=? countstack(push(nil, X9), X10)", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: countstack(T5, T7), SCOPE: 2, CLAUSE: 0 | countstack(T5, T7), SCOPE: 2, CLAUSE: 1 | countstack(T5, T7), SCOPE: 2, CLAUSE: 2 | ?_2 | countstack(push(nil, T5), T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: countstack(T5, T7), SCOPE: 2, CLAUSE: 0\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: countstack(T5, T7), SCOPE: 2, CLAUSE: 1 | countstack(T5, T7), SCOPE: 2, CLAUSE: 2 | ?_2 | countstack(push(nil, T5), T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: countstack(T5, T7), SCOPE: 2, CLAUSE: 1\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: countstack(T5, T7), SCOPE: 2, CLAUSE: 2 | ?_2 | countstack(push(nil, T5), T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: countstack(T16, T18)\n\nT16 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: countstack(T5, T7), SCOPE: 2, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: ?_2 | countstack(push(nil, T5), T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: countstack(push(T35, push(T36, T37)), T39)\n\nT35 is ground\nT36 is ground\nT37 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
61 [label="61: countstack(push(nil, T5), T2), SCOPE: 1, CLAUSE: 2\n\nT5 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: countstack(push(T44, push(T45, T46)), T48)\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 0 | countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 1 | countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 2\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 1 | countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 2\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 1\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: countstack(push(T44, push(T45, T46)), T48), SCOPE: 3, CLAUSE: 2\n\nT44 is ground\nT45 is ground\nT46 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: countstack(push(T61, T62), T64)\n\nT61 is ground\nT62 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: countstack(push(T75, push(T76, push(T77, T78))), T80)\n\nT75 is ground\nT76 is ground\nT77 is ground\nT78 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 82 [arrowhead = none ];
82 -> 5;

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

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

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

86 [label="EVAL with clause\ncountstack(push(nil, X9), X10) :- countstack(X9, X10).\nand substitutionX9 -> T5,\nT1 -> push(nil, T5),\nT2 -> T7,\nX10 -> T7,\nT6 -> T7", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 86 [arrowhead = none ];
86 -> 27;

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

88 [label="BACKTRACK\nfor clause: countstack(push(nil, T), X) :- countstack(T, X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 88 [arrowhead = none ];
88 -> 19;

89 [label="BACKTRACK\nfor clause: countstack(push(cons(U, V), T), s(X)) :- countstack(push(U, push(V, T)), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
19 -> 89 [arrowhead = none ];
89 -> 23;

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

91 [label="EVAL with clause\ncountstack(push(cons(X49, X50), X51), s(X52)) :- countstack(push(X49, push(X50, X51)), X52).\nand substitutionX49 -> T44,\nX50 -> T45,\nX51 -> T46,\nT1 -> push(cons(T44, T45), T46),\nX52 -> T48,\nT2 -> s(T48),\nT47 -> T48", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 91 [arrowhead = none ];
91 -> 65;

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

93 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
30 -> 93 [arrowhead = none ];
93 -> 33;

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

95 [label="EVAL with clause\ncountstack(empty, 0).\nand substitutionT5 -> empty,\nT7 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 95 [arrowhead = none ];
95 -> 37;

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

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

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

99 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
37 -> 99 [arrowhead = none ];
99 -> 41;

100 [label="EVAL with clause\ncountstack(push(nil, X19), X20) :- countstack(X19, X20).\nand substitutionX19 -> T16,\nT5 -> push(nil, T16),\nT7 -> T18,\nX20 -> T18,\nT17 -> T18", fontsize=14, style = filled, fillcolor = lightblue];
43 -> 100 [arrowhead = none ];
100 -> 47;

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

102 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 102 [arrowhead = none ];
102 -> 53;

103 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
45 -> 103 [arrowhead = none ];
103 -> 55;

104 [label="INSTANCE with matching:\nT1 -> T16\nT2 -> T18", fontsize=14, style = filled, fillcolor = lightgrey];
47 -> 104 [arrowhead = none , style=dashed];
104 -> 1[style=dashed];

105 [label="EVAL with clause\ncountstack(push(cons(X37, X38), X39), s(X40)) :- countstack(push(X37, push(X38, X39)), X40).\nand substitutionX37 -> T35,\nX38 -> T36,\nX39 -> T37,\nT5 -> push(cons(T35, T36), T37),\nX40 -> T39,\nT7 -> s(T39),\nT38 -> T39", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 105 [arrowhead = none ];
105 -> 57;

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

107 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
55 -> 107 [arrowhead = none ];
107 -> 61;

108 [label="INSTANCE with matching:\nT1 -> push(T35, push(T36, T37))\nT2 -> T39", fontsize=14, style = filled, fillcolor = lightgrey];
57 -> 108 [arrowhead = none , style=dashed];
108 -> 1[style=dashed];

109 [label="BACKTRACK\nfor clause: countstack(push(cons(U, V), T), s(X)) :- countstack(push(U, push(V, T)), X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
61 -> 109 [arrowhead = none ];
109 -> 62;

110 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
65 -> 110 [arrowhead = none ];
110 -> 69;

111 [label="BACKTRACK\nfor clause: countstack(empty, 0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 111 [arrowhead = none ];
111 -> 71;

112 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
71 -> 112 [arrowhead = none ];
112 -> 73;

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

114 [label="EVAL with clause\ncountstack(push(nil, X61), X62) :- countstack(X61, X62).\nand substitutionT44 -> nil,\nT45 -> T61,\nT46 -> T62,\nX61 -> push(T61, T62),\nT48 -> T64,\nX62 -> T64,\nT63 -> T64", fontsize=14, style = filled, fillcolor = lightblue];
73 -> 114 [arrowhead = none ];
114 -> 77;

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

116 [label="EVAL with clause\ncountstack(push(cons(X71, X72), X73), s(X74)) :- countstack(push(X71, push(X72, X73)), X74).\nand substitutionX71 -> T75,\nX72 -> T76,\nT44 -> cons(T75, T76),\nT45 -> T77,\nT46 -> T78,\nX73 -> push(T77, T78),\nX74 -> T80,\nT48 -> s(T80),\nT79 -> T80", fontsize=14, style = filled, fillcolor = lightblue];
75 -> 116 [arrowhead = none ];
116 -> 80;

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

118 [label="INSTANCE with matching:\nT1 -> push(T61, T62)\nT2 -> T64", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 118 [arrowhead = none , style=dashed];
118 -> 1[style=dashed];

119 [label="INSTANCE with matching:\nT1 -> push(T75, push(T76, push(T77, T78)))\nT2 -> T80", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 119 [arrowhead = none , style=dashed];
119 -> 1[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, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)

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)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x2, x4)
U4_ga(x1, x2, x3, x4, x5, x6)  =  U4_ga(x1, x2, x3, x4, x6)
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, push(nil, T16)), T18) → U1_GA(T16, T18, countstackA_in_ga(T16, T18))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_GA(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → U3_GA(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_GA(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)

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)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x2, x4)
U4_ga(x1, x2, x3, x4, x5, x6)  =  U4_ga(x1, x2, x3, x4, x6)
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)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5, x6)  =  U4_GA(x1, x2, x3, x4, x6)

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, push(nil, T16)), T18) → U1_GA(T16, T18, countstackA_in_ga(T16, T18))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_GA(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → U3_GA(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_GA(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)

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)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x2, x4)
U4_ga(x1, x2, x3, x4, x5, x6)  =  U4_ga(x1, x2, x3, x4, x6)
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)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4, x5, x6)  =  U4_GA(x1, x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Obligation:

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

COUNTSTACKA_IN_GA(push(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)

The TRS R consists of the following rules:

countstackA_in_ga(empty, 0) → countstackA_out_ga(empty, 0)
countstackA_in_ga(push(nil, empty), 0) → countstackA_out_ga(push(nil, empty), 0)
countstackA_in_ga(push(nil, push(nil, T16)), T18) → U1_ga(T16, T18, countstackA_in_ga(T16, T18))
countstackA_in_ga(push(nil, push(cons(T35, T36), T37)), s(T39)) → U2_ga(T35, T36, T37, T39, countstackA_in_ga(push(T35, push(T36, T37)), T39))
countstackA_in_ga(push(cons(nil, T61), T62), s(T64)) → U3_ga(T61, T62, T64, countstackA_in_ga(push(T61, T62), T64))
countstackA_in_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → U4_ga(T75, T76, T77, T78, T80, countstackA_in_ga(push(T75, push(T76, push(T77, T78))), T80))
U4_ga(T75, T76, T77, T78, T80, countstackA_out_ga(push(T75, push(T76, push(T77, T78))), T80)) → countstackA_out_ga(push(cons(cons(T75, T76), T77), T78), s(s(T80)))
U3_ga(T61, T62, T64, countstackA_out_ga(push(T61, T62), T64)) → countstackA_out_ga(push(cons(nil, T61), T62), s(T64))
U2_ga(T35, T36, T37, T39, countstackA_out_ga(push(T35, push(T36, T37)), T39)) → countstackA_out_ga(push(nil, push(cons(T35, T36), T37)), s(T39))
U1_ga(T16, T18, countstackA_out_ga(T16, T18)) → countstackA_out_ga(push(nil, push(nil, T16)), T18)

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)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x2, x4)
U4_ga(x1, x2, x3, x4, x5, x6)  =  U4_ga(x1, x2, x3, x4, x6)
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(nil, push(cons(T35, T36), T37)), s(T39)) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)), T39)
COUNTSTACKA_IN_GA(push(nil, push(nil, T16)), T18) → COUNTSTACKA_IN_GA(T16, T18)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62), s(T64)) → COUNTSTACKA_IN_GA(push(T61, T62), T64)
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78), s(s(T80))) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))), T80)

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(nil, push(cons(T35, T36), T37))) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16))) → COUNTSTACKA_IN_GA(T16)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62)) → COUNTSTACKA_IN_GA(push(T61, T62))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78)) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))))

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(nil, push(cons(T35, T36), T37))) → COUNTSTACKA_IN_GA(push(T35, push(T36, T37)))
COUNTSTACKA_IN_GA(push(nil, push(nil, T16))) → COUNTSTACKA_IN_GA(T16)
COUNTSTACKA_IN_GA(push(cons(nil, T61), T62)) → COUNTSTACKA_IN_GA(push(T61, T62))
COUNTSTACKA_IN_GA(push(cons(cons(T75, T76), T77), T78)) → COUNTSTACKA_IN_GA(push(T75, push(T76, push(T77, T78))))

No rules are removed from R.

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(COUNTSTACKA_IN_GA(x₁)) = 2·x₁   
POL(cons(x₁, x₂)) = x₁ + x₂   
POL(nil) = 0   
POL(push(x₁, x₂)) = 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