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

(0) Obligation:

Clauses:

goal(A, B, C) :- ','(s2l(A, D), applast(D, B, C)).
applast(L, X, Last) :- ','(append(L, .(X, []), LX), last(Last, LX)).
last(X, .(X, [])).
last(X, .(H, T)) :- last(X, T).
append([], L, L).
append(.(H, L1), L2, .(H, L3)) :- append(L1, L2, L3).
s2l(s(X), .(Y, Xs)) :- s2l(X, Xs).
s2l(0, []).

Query: goal(g,a,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
3 [label="A: goal(T1, T2, T3)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: goal(T1, T2, T3), SCOPE: 1, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(s2l(T7, X7), applast(X7, T10, T11))\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(s2l(T7, X7), applast(X7, T10, T11)), SCOPE: 2, CLAUSE: 6 | ','(s2l(T7, X7), applast(X7, T10, T11)), SCOPE: 2, CLAUSE: 7\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(s2l(T7, X7), applast(X7, T10, T11)), SCOPE: 2, CLAUSE: 6\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: ','(s2l(T7, X7), applast(X7, T10, T11)), SCOPE: 2, CLAUSE: 7\n\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="B: ','(s2l(T16, X32), applast(.(X31, X32), T10, T11))\n\nT16 is ground\nX31 is free\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="D: s2l(T16, X32)\n\nT16 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="G: applast(.(X31, T18), T10, T11)\n\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: s2l(T16, X32), SCOPE: 3, CLAUSE: 6 | s2l(T16, X32), SCOPE: 3, CLAUSE: 7\n\nT16 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: s2l(T16, X32), SCOPE: 3, CLAUSE: 6\n\nT16 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: s2l(T16, X32), SCOPE: 3, CLAUSE: 7\n\nT16 is ground\nX32 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: s2l(T24, X67)\n\nT24 is ground\nX67 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: applast(.(X31, T18), T10, T11), SCOPE: 4, CLAUSE: 1\n\nX31 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="H: ','(append(.(X93, T41), .(T42, []), X92), last(T43, X92))\n\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="I: append(.(X93, T41), .(T42, []), X92)\n\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="F: last(T46, T45)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: append(.(X93, T41), .(T42, []), X92), SCOPE: 5, CLAUSE: 4 | append(.(X93, T41), .(T42, []), X92), SCOPE: 5, CLAUSE: 5\n\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: append(.(X93, T41), .(T42, []), X92), SCOPE: 5, CLAUSE: 5\n\nX93 is free\nX92 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="E: append(T57, .(T58, []), X118)\n\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: append(T57, .(T58, []), X118), SCOPE: 6, CLAUSE: 4 | append(T57, .(T58, []), X118), SCOPE: 6, CLAUSE: 5\n\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: append(T57, .(T58, []), X118), SCOPE: 6, CLAUSE: 4\n\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: append(T57, .(T58, []), X118), SCOPE: 6, CLAUSE: 5\n\nX118 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: append(T75, .(T76, []), X140)\n\nX140 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: last(T46, T45), SCOPE: 7, CLAUSE: 2 | last(T46, T45), SCOPE: 7, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: last(T46, T45), SCOPE: 7, CLAUSE: 2\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: last(T46, T45), SCOPE: 7, CLAUSE: 3\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: last(T95, T96)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: applast([], T10, T11)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: applast([], T10, T11), SCOPE: 8, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="C: ','(append([], .(T111, []), X177), last(T112, X177))\n\nX177 is free", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="J: append([], .(T111, []), X177)\n\nX177 is free", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: last(T116, T115)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: append([], .(T111, []), X177), SCOPE: 9, CLAUSE: 4 | append([], .(T111, []), X177), SCOPE: 9, CLAUSE: 5\n\nX177 is free", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: append([], .(T111, []), X177), SCOPE: 9, CLAUSE: 4\n\nX177 is free", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: append([], .(T111, []), X177), SCOPE: 9, CLAUSE: 5\n\nX177 is free", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
3 -> 140 [arrowhead = none ];
140 -> 4;

141 [label="ONLY EVAL with clause\ngoal(X4, X5, X6) :- ','(s2l(X4, X7), applast(X7, X5, X6)).\nand substitutionT1 -> T7,\nX4 -> T7,\nT2 -> T10,\nX5 -> T10,\nT3 -> T11,\nX6 -> T11,\nT8 -> T10,\nT9 -> T11", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 141 [arrowhead = none ];
141 -> 8;

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

143 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 143 [arrowhead = none ];
143 -> 16;

144 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 144 [arrowhead = none ];
144 -> 17;

145 [label="EVAL with clause\ns2l(s(X28), .(X29, X30)) :- s2l(X28, X30).\nand substitutionX28 -> T16,\nT7 -> s(T16),\nX29 -> X31,\nX30 -> X32,\nX7 -> .(X31, X32)", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 145 [arrowhead = none ];
145 -> 18;

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

147 [label="EVAL with clause\ns2l(0, []).\nand substitutionT7 -> 0,\nX7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
17 -> 147 [arrowhead = none ];
147 -> 128;

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

149 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
18 -> 149 [arrowhead = none ];
149 -> 20;

150 [label="SPLIT 2\nnew knowledge:\nT16 is ground\nreplacements:X32 -> T18", fontsize=14, style = filled, fillcolor = violet];
18 -> 150 [arrowhead = none ];
150 -> 22;

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

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

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

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

155 [label="EVAL with clause\ns2l(s(X63), .(X64, X65)) :- s2l(X63, X65).\nand substitutionX63 -> T24,\nT16 -> s(T24),\nX64 -> X66,\nX65 -> X67,\nX32 -> .(X66, X67)", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 155 [arrowhead = none ];
155 -> 37;

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

157 [label="EVAL with clause\ns2l(0, []).\nand substitutionT16 -> 0,\nX32 -> []", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 157 [arrowhead = none ];
157 -> 42;

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

159 [label="INSTANCE with matching:\nT16 -> T24\nX32 -> X67", fontsize=14, style = filled, fillcolor = lightgrey];
37 -> 159 [arrowhead = none , style=dashed];
159 -> 20[style=dashed];

160 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
42 -> 160 [arrowhead = none ];
160 -> 44;

161 [label="ONLY EVAL with clause\napplast(X89, X90, X91) :- ','(append(X89, .(X90, []), X92), last(X91, X92)).\nand substitutionX31 -> X93,\nT18 -> T41,\nX89 -> .(X93, T41),\nT10 -> T42,\nX90 -> T42,\nT11 -> T43,\nX91 -> T43,\nT38 -> T41,\nT39 -> T42,\nT40 -> T43", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 161 [arrowhead = none ];
161 -> 59;

162 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
59 -> 162 [arrowhead = none ];
162 -> 62;

163 [label="SPLIT 2\nreplacements:X93 -> T44,\nX92 -> T45,\nT43 -> T46", fontsize=14, style = filled, fillcolor = violet];
59 -> 163 [arrowhead = none ];
163 -> 63;

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

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

166 [label="BACKTRACK\nfor clause: append([], L, L)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
77 -> 166 [arrowhead = none ];
166 -> 79;

167 [label="ONLY EVAL with clause\nappend(.(X113, X114), X115, .(X113, X116)) :- append(X114, X115, X116).\nand substitutionX93 -> X117,\nX113 -> X117,\nT41 -> T57,\nX114 -> T57,\nT42 -> T58,\nX115 -> .(T58, []),\nX116 -> X118,\nX92 -> .(X117, X118),\nT55 -> T57,\nT56 -> T58", fontsize=14, style = filled, fillcolor = lightblue];
79 -> 167 [arrowhead = none ];
167 -> 87;

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

169 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 169 [arrowhead = none ];
169 -> 104;

170 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
90 -> 170 [arrowhead = none ];
170 -> 105;

171 [label="EVAL with clause\nappend([], X125, X125).\nand substitutionT57 -> [],\nT58 -> T65,\nX125 -> .(T65, []),\nX118 -> .(T65, [])", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 171 [arrowhead = none ];
171 -> 106;

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

173 [label="EVAL with clause\nappend(.(X136, X137), X138, .(X136, X139)) :- append(X137, X138, X139).\nand substitutionX136 -> T72,\nX137 -> T75,\nT57 -> .(T72, T75),\nT58 -> T76,\nX138 -> .(T76, []),\nX139 -> X140,\nX118 -> .(T72, X140),\nT73 -> T75,\nT74 -> T76", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 173 [arrowhead = none ];
173 -> 115;

174 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 174 [arrowhead = none ];
174 -> 116;

175 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
106 -> 175 [arrowhead = none ];
175 -> 108;

176 [label="INSTANCE with matching:\nT57 -> T75\nT58 -> T76\nX118 -> X140", fontsize=14, style = filled, fillcolor = lightgrey];
115 -> 176 [arrowhead = none , style=dashed];
176 -> 87[style=dashed];

177 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 177 [arrowhead = none ];
177 -> 121;

178 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
120 -> 178 [arrowhead = none ];
178 -> 122;

179 [label="EVAL with clause\nlast(X149, .(X149, [])).\nand substitutionT46 -> T85,\nX149 -> T85,\nT45 -> .(T85, [])", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 179 [arrowhead = none ];
179 -> 123;

180 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 180 [arrowhead = none ];
180 -> 124;

181 [label="EVAL with clause\nlast(X156, .(X157, X158)) :- last(X156, X158).\nand substitutionT46 -> T95,\nX156 -> T95,\nX157 -> T93,\nX158 -> T96,\nT45 -> .(T93, T96),\nT92 -> T95,\nT94 -> T96", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 181 [arrowhead = none ];
181 -> 126;

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

183 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 183 [arrowhead = none ];
183 -> 125;

184 [label="INSTANCE with matching:\nT46 -> T95\nT45 -> T96", fontsize=14, style = filled, fillcolor = lightgrey];
126 -> 184 [arrowhead = none , style=dashed];
184 -> 63[style=dashed];

185 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
128 -> 185 [arrowhead = none ];
185 -> 130;

186 [label="ONLY EVAL with clause\napplast(X174, X175, X176) :- ','(append(X174, .(X175, []), X177), last(X176, X177)).\nand substitutionX174 -> [],\nT10 -> T111,\nX175 -> T111,\nT11 -> T112,\nX176 -> T112,\nT109 -> T111,\nT110 -> T112", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 186 [arrowhead = none ];
186 -> 131;

187 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
131 -> 187 [arrowhead = none ];
187 -> 132;

188 [label="SPLIT 2\nreplacements:X177 -> T115,\nT112 -> T116", fontsize=14, style = filled, fillcolor = violet];
131 -> 188 [arrowhead = none ];
188 -> 133;

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

190 [label="INSTANCE with matching:\nT46 -> T116\nT45 -> T115", fontsize=14, style = filled, fillcolor = lightgrey];
133 -> 190 [arrowhead = none , style=dashed];
190 -> 63[style=dashed];

191 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
134 -> 191 [arrowhead = none ];
191 -> 135;

192 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
134 -> 192 [arrowhead = none ];
192 -> 136;

193 [label="ONLY EVAL with clause\nappend([], X185, X185).\nand substitutionT111 -> T122,\nX185 -> .(T122, []),\nX177 -> .(T122, [])", fontsize=14, style = filled, fillcolor = lightblue];
135 -> 193 [arrowhead = none ];
193 -> 137;

194 [label="BACKTRACK\nfor clause: append(.(H, L1), L2, .(H, L3)) :- append(L1, L2, L3)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
136 -> 194 [arrowhead = none ];
194 -> 139;

195 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
137 -> 195 [arrowhead = none ];
195 -> 138;

}

(2) Obligation:

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

goalA_in_gaa(s(T16), T10, T11) → U1_gaa(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
pB_in_gaaaa(T16, T18, X31, T10, T11) → U8_gaaaa(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
s2lD_in_ga(s(T24), .(X66, X67)) → U3_ga(T24, X66, X67, s2lD_in_ga(T24, X67))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
U3_ga(T24, X66, X67, s2lD_out_ga(T24, X67)) → s2lD_out_ga(s(T24), .(X66, X67))
U8_gaaaa(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_gaaaa(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
applastG_in_agaa(X93, T41, T42, T43) → U6_agaa(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
pH_in_agaaa(T44, T41, T42, T45, T46) → U10_agaaa(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
appendI_in_agaa(X117, T57, T58, .(X117, X118)) → U7_agaa(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
appendE_in_gaa([], T65, .(T65, [])) → appendE_out_gaa([], T65, .(T65, []))
appendE_in_gaa(.(T72, T75), T76, .(T72, X140)) → U4_gaa(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
U4_gaa(T72, T75, T76, X140, appendE_out_gaa(T75, T76, X140)) → appendE_out_gaa(.(T72, T75), T76, .(T72, X140))
U7_agaa(X117, T57, T58, X118, appendE_out_gaa(T57, T58, X118)) → appendI_out_agaa(X117, T57, T58, .(X117, X118))
U10_agaaa(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_agaaa(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
lastF_in_ag(T85, .(T85, [])) → lastF_out_ag(T85, .(T85, []))
lastF_in_ag(T95, .(T93, T96)) → U5_ag(T95, T93, T96, lastF_in_ag(T95, T96))
U5_ag(T95, T93, T96, lastF_out_ag(T95, T96)) → lastF_out_ag(T95, .(T93, T96))
U11_agaaa(T44, T41, T42, T45, T46, lastF_out_ag(T46, T45)) → pH_out_agaaa(T44, T41, T42, T45, T46)
U6_agaa(X93, T41, T42, T43, pH_out_agaaa(X93, T41, T42, X92, T43)) → applastG_out_agaa(X93, T41, T42, T43)
U9_gaaaa(T16, T18, X31, T10, T11, applastG_out_agaa(X31, T18, T10, T11)) → pB_out_gaaaa(T16, T18, X31, T10, T11)
U1_gaa(T16, T10, T11, pB_out_gaaaa(T16, X32, X31, T10, T11)) → goalA_out_gaa(s(T16), T10, T11)
goalA_in_gaa(0, T111, T112) → U2_gaa(T111, T112, pC_in_aaa(T111, X177, T112))
pC_in_aaa(T111, T115, T116) → U12_aaa(T111, T115, T116, appendJ_in_aa(T111, T115))
appendJ_in_aa(T122, .(T122, [])) → appendJ_out_aa(T122, .(T122, []))
U12_aaa(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_aaa(T111, T115, T116, lastF_in_ag(T116, T115))
U13_aaa(T111, T115, T116, lastF_out_ag(T116, T115)) → pC_out_aaa(T111, T115, T116)
U2_gaa(T111, T112, pC_out_aaa(T111, X177, T112)) → goalA_out_gaa(0, T111, T112)

The argument filtering Pi contains the following mapping:
goalA_in_gaa(x1, x2, x3)  =  goalA_in_gaa(x1)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
0  =  0
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U9_gaaaa(x1, x2, x3, x4, x5, x6)  =  U9_gaaaa(x1, x2, x6)
applastG_in_agaa(x1, x2, x3, x4)  =  applastG_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
pH_in_agaaa(x1, x2, x3, x4, x5)  =  pH_in_agaaa(x2)
U10_agaaa(x1, x2, x3, x4, x5, x6)  =  U10_agaaa(x2, x6)
appendI_in_agaa(x1, x2, x3, x4)  =  appendI_in_agaa(x2)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1, x3)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x2, x5)
appendI_out_agaa(x1, x2, x3, x4)  =  appendI_out_agaa(x2, x4)
U11_agaaa(x1, x2, x3, x4, x5, x6)  =  U11_agaaa(x2, x4, x6)
lastF_in_ag(x1, x2)  =  lastF_in_ag(x2)
lastF_out_ag(x1, x2)  =  lastF_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
pH_out_agaaa(x1, x2, x3, x4, x5)  =  pH_out_agaaa(x2, x4)
applastG_out_agaa(x1, x2, x3, x4)  =  applastG_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_gaa(x1, x2, x3)  =  goalA_out_gaa(x1)
U2_gaa(x1, x2, x3)  =  U2_gaa(x3)
pC_in_aaa(x1, x2, x3)  =  pC_in_aaa
U12_aaa(x1, x2, x3, x4)  =  U12_aaa(x4)
appendJ_in_aa(x1, x2)  =  appendJ_in_aa
appendJ_out_aa(x1, x2)  =  appendJ_out_aa(x2)
U13_aaa(x1, x2, x3, x4)  =  U13_aaa(x2, x4)
pC_out_aaa(x1, x2, x3)  =  pC_out_aaa(x2)

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

GOALA_IN_GAA(s(T16), T10, T11) → U1_GAA(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
GOALA_IN_GAA(s(T16), T10, T11) → PB_IN_GAAAA(T16, X32, X31, T10, T11)
PB_IN_GAAAA(T16, T18, X31, T10, T11) → U8_GAAAA(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
PB_IN_GAAAA(T16, T18, X31, T10, T11) → S2LD_IN_GA(T16, T18)
S2LD_IN_GA(s(T24), .(X66, X67)) → U3_GA(T24, X66, X67, s2lD_in_ga(T24, X67))
S2LD_IN_GA(s(T24), .(X66, X67)) → S2LD_IN_GA(T24, X67)
U8_GAAAA(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_GAAAA(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
U8_GAAAA(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → APPLASTG_IN_AGAA(X31, T18, T10, T11)
APPLASTG_IN_AGAA(X93, T41, T42, T43) → U6_AGAA(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
APPLASTG_IN_AGAA(X93, T41, T42, T43) → PH_IN_AGAAA(X93, T41, T42, X92, T43)
PH_IN_AGAAA(T44, T41, T42, T45, T46) → U10_AGAAA(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
PH_IN_AGAAA(T44, T41, T42, T45, T46) → APPENDI_IN_AGAA(T44, T41, T42, T45)
APPENDI_IN_AGAA(X117, T57, T58, .(X117, X118)) → U7_AGAA(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
APPENDI_IN_AGAA(X117, T57, T58, .(X117, X118)) → APPENDE_IN_GAA(T57, T58, X118)
APPENDE_IN_GAA(.(T72, T75), T76, .(T72, X140)) → U4_GAA(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
APPENDE_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDE_IN_GAA(T75, T76, X140)
U10_AGAAA(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_AGAAA(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
U10_AGAAA(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → LASTF_IN_AG(T46, T45)
LASTF_IN_AG(T95, .(T93, T96)) → U5_AG(T95, T93, T96, lastF_in_ag(T95, T96))
LASTF_IN_AG(T95, .(T93, T96)) → LASTF_IN_AG(T95, T96)
GOALA_IN_GAA(0, T111, T112) → U2_GAA(T111, T112, pC_in_aaa(T111, X177, T112))
GOALA_IN_GAA(0, T111, T112) → PC_IN_AAA(T111, X177, T112)
PC_IN_AAA(T111, T115, T116) → U12_AAA(T111, T115, T116, appendJ_in_aa(T111, T115))
PC_IN_AAA(T111, T115, T116) → APPENDJ_IN_AA(T111, T115)
U12_AAA(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_AAA(T111, T115, T116, lastF_in_ag(T116, T115))
U12_AAA(T111, T115, T116, appendJ_out_aa(T111, T115)) → LASTF_IN_AG(T116, T115)

The TRS R consists of the following rules:

goalA_in_gaa(s(T16), T10, T11) → U1_gaa(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
pB_in_gaaaa(T16, T18, X31, T10, T11) → U8_gaaaa(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
s2lD_in_ga(s(T24), .(X66, X67)) → U3_ga(T24, X66, X67, s2lD_in_ga(T24, X67))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
U3_ga(T24, X66, X67, s2lD_out_ga(T24, X67)) → s2lD_out_ga(s(T24), .(X66, X67))
U8_gaaaa(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_gaaaa(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
applastG_in_agaa(X93, T41, T42, T43) → U6_agaa(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
pH_in_agaaa(T44, T41, T42, T45, T46) → U10_agaaa(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
appendI_in_agaa(X117, T57, T58, .(X117, X118)) → U7_agaa(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
appendE_in_gaa([], T65, .(T65, [])) → appendE_out_gaa([], T65, .(T65, []))
appendE_in_gaa(.(T72, T75), T76, .(T72, X140)) → U4_gaa(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
U4_gaa(T72, T75, T76, X140, appendE_out_gaa(T75, T76, X140)) → appendE_out_gaa(.(T72, T75), T76, .(T72, X140))
U7_agaa(X117, T57, T58, X118, appendE_out_gaa(T57, T58, X118)) → appendI_out_agaa(X117, T57, T58, .(X117, X118))
U10_agaaa(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_agaaa(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
lastF_in_ag(T85, .(T85, [])) → lastF_out_ag(T85, .(T85, []))
lastF_in_ag(T95, .(T93, T96)) → U5_ag(T95, T93, T96, lastF_in_ag(T95, T96))
U5_ag(T95, T93, T96, lastF_out_ag(T95, T96)) → lastF_out_ag(T95, .(T93, T96))
U11_agaaa(T44, T41, T42, T45, T46, lastF_out_ag(T46, T45)) → pH_out_agaaa(T44, T41, T42, T45, T46)
U6_agaa(X93, T41, T42, T43, pH_out_agaaa(X93, T41, T42, X92, T43)) → applastG_out_agaa(X93, T41, T42, T43)
U9_gaaaa(T16, T18, X31, T10, T11, applastG_out_agaa(X31, T18, T10, T11)) → pB_out_gaaaa(T16, T18, X31, T10, T11)
U1_gaa(T16, T10, T11, pB_out_gaaaa(T16, X32, X31, T10, T11)) → goalA_out_gaa(s(T16), T10, T11)
goalA_in_gaa(0, T111, T112) → U2_gaa(T111, T112, pC_in_aaa(T111, X177, T112))
pC_in_aaa(T111, T115, T116) → U12_aaa(T111, T115, T116, appendJ_in_aa(T111, T115))
appendJ_in_aa(T122, .(T122, [])) → appendJ_out_aa(T122, .(T122, []))
U12_aaa(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_aaa(T111, T115, T116, lastF_in_ag(T116, T115))
U13_aaa(T111, T115, T116, lastF_out_ag(T116, T115)) → pC_out_aaa(T111, T115, T116)
U2_gaa(T111, T112, pC_out_aaa(T111, X177, T112)) → goalA_out_gaa(0, T111, T112)

The argument filtering Pi contains the following mapping:
goalA_in_gaa(x1, x2, x3)  =  goalA_in_gaa(x1)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
0  =  0
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U9_gaaaa(x1, x2, x3, x4, x5, x6)  =  U9_gaaaa(x1, x2, x6)
applastG_in_agaa(x1, x2, x3, x4)  =  applastG_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
pH_in_agaaa(x1, x2, x3, x4, x5)  =  pH_in_agaaa(x2)
U10_agaaa(x1, x2, x3, x4, x5, x6)  =  U10_agaaa(x2, x6)
appendI_in_agaa(x1, x2, x3, x4)  =  appendI_in_agaa(x2)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1, x3)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x2, x5)
appendI_out_agaa(x1, x2, x3, x4)  =  appendI_out_agaa(x2, x4)
U11_agaaa(x1, x2, x3, x4, x5, x6)  =  U11_agaaa(x2, x4, x6)
lastF_in_ag(x1, x2)  =  lastF_in_ag(x2)
lastF_out_ag(x1, x2)  =  lastF_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
pH_out_agaaa(x1, x2, x3, x4, x5)  =  pH_out_agaaa(x2, x4)
applastG_out_agaa(x1, x2, x3, x4)  =  applastG_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_gaa(x1, x2, x3)  =  goalA_out_gaa(x1)
U2_gaa(x1, x2, x3)  =  U2_gaa(x3)
pC_in_aaa(x1, x2, x3)  =  pC_in_aaa
U12_aaa(x1, x2, x3, x4)  =  U12_aaa(x4)
appendJ_in_aa(x1, x2)  =  appendJ_in_aa
appendJ_out_aa(x1, x2)  =  appendJ_out_aa(x2)
U13_aaa(x1, x2, x3, x4)  =  U13_aaa(x2, x4)
pC_out_aaa(x1, x2, x3)  =  pC_out_aaa(x2)
GOALA_IN_GAA(x1, x2, x3)  =  GOALA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
PB_IN_GAAAA(x1, x2, x3, x4, x5)  =  PB_IN_GAAAA(x1)
U8_GAAAA(x1, x2, x3, x4, x5, x6)  =  U8_GAAAA(x1, x6)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U9_GAAAA(x1, x2, x3, x4, x5, x6)  =  U9_GAAAA(x1, x2, x6)
APPLASTG_IN_AGAA(x1, x2, x3, x4)  =  APPLASTG_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
PH_IN_AGAAA(x1, x2, x3, x4, x5)  =  PH_IN_AGAAA(x2)
U10_AGAAA(x1, x2, x3, x4, x5, x6)  =  U10_AGAAA(x2, x6)
APPENDI_IN_AGAA(x1, x2, x3, x4)  =  APPENDI_IN_AGAA(x2)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x5)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x2, x5)
U11_AGAAA(x1, x2, x3, x4, x5, x6)  =  U11_AGAAA(x2, x4, x6)
LASTF_IN_AG(x1, x2)  =  LASTF_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U2_GAA(x1, x2, x3)  =  U2_GAA(x3)
PC_IN_AAA(x1, x2, x3)  =  PC_IN_AAA
U12_AAA(x1, x2, x3, x4)  =  U12_AAA(x4)
APPENDJ_IN_AA(x1, x2)  =  APPENDJ_IN_AA
U13_AAA(x1, x2, x3, x4)  =  U13_AAA(x2, x4)

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

(4) Obligation:

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

GOALA_IN_GAA(s(T16), T10, T11) → U1_GAA(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
GOALA_IN_GAA(s(T16), T10, T11) → PB_IN_GAAAA(T16, X32, X31, T10, T11)
PB_IN_GAAAA(T16, T18, X31, T10, T11) → U8_GAAAA(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
PB_IN_GAAAA(T16, T18, X31, T10, T11) → S2LD_IN_GA(T16, T18)
S2LD_IN_GA(s(T24), .(X66, X67)) → U3_GA(T24, X66, X67, s2lD_in_ga(T24, X67))
S2LD_IN_GA(s(T24), .(X66, X67)) → S2LD_IN_GA(T24, X67)
U8_GAAAA(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_GAAAA(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
U8_GAAAA(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → APPLASTG_IN_AGAA(X31, T18, T10, T11)
APPLASTG_IN_AGAA(X93, T41, T42, T43) → U6_AGAA(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
APPLASTG_IN_AGAA(X93, T41, T42, T43) → PH_IN_AGAAA(X93, T41, T42, X92, T43)
PH_IN_AGAAA(T44, T41, T42, T45, T46) → U10_AGAAA(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
PH_IN_AGAAA(T44, T41, T42, T45, T46) → APPENDI_IN_AGAA(T44, T41, T42, T45)
APPENDI_IN_AGAA(X117, T57, T58, .(X117, X118)) → U7_AGAA(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
APPENDI_IN_AGAA(X117, T57, T58, .(X117, X118)) → APPENDE_IN_GAA(T57, T58, X118)
APPENDE_IN_GAA(.(T72, T75), T76, .(T72, X140)) → U4_GAA(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
APPENDE_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDE_IN_GAA(T75, T76, X140)
U10_AGAAA(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_AGAAA(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
U10_AGAAA(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → LASTF_IN_AG(T46, T45)
LASTF_IN_AG(T95, .(T93, T96)) → U5_AG(T95, T93, T96, lastF_in_ag(T95, T96))
LASTF_IN_AG(T95, .(T93, T96)) → LASTF_IN_AG(T95, T96)
GOALA_IN_GAA(0, T111, T112) → U2_GAA(T111, T112, pC_in_aaa(T111, X177, T112))
GOALA_IN_GAA(0, T111, T112) → PC_IN_AAA(T111, X177, T112)
PC_IN_AAA(T111, T115, T116) → U12_AAA(T111, T115, T116, appendJ_in_aa(T111, T115))
PC_IN_AAA(T111, T115, T116) → APPENDJ_IN_AA(T111, T115)
U12_AAA(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_AAA(T111, T115, T116, lastF_in_ag(T116, T115))
U12_AAA(T111, T115, T116, appendJ_out_aa(T111, T115)) → LASTF_IN_AG(T116, T115)

The TRS R consists of the following rules:

goalA_in_gaa(s(T16), T10, T11) → U1_gaa(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
pB_in_gaaaa(T16, T18, X31, T10, T11) → U8_gaaaa(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
s2lD_in_ga(s(T24), .(X66, X67)) → U3_ga(T24, X66, X67, s2lD_in_ga(T24, X67))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
U3_ga(T24, X66, X67, s2lD_out_ga(T24, X67)) → s2lD_out_ga(s(T24), .(X66, X67))
U8_gaaaa(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_gaaaa(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
applastG_in_agaa(X93, T41, T42, T43) → U6_agaa(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
pH_in_agaaa(T44, T41, T42, T45, T46) → U10_agaaa(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
appendI_in_agaa(X117, T57, T58, .(X117, X118)) → U7_agaa(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
appendE_in_gaa([], T65, .(T65, [])) → appendE_out_gaa([], T65, .(T65, []))
appendE_in_gaa(.(T72, T75), T76, .(T72, X140)) → U4_gaa(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
U4_gaa(T72, T75, T76, X140, appendE_out_gaa(T75, T76, X140)) → appendE_out_gaa(.(T72, T75), T76, .(T72, X140))
U7_agaa(X117, T57, T58, X118, appendE_out_gaa(T57, T58, X118)) → appendI_out_agaa(X117, T57, T58, .(X117, X118))
U10_agaaa(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_agaaa(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
lastF_in_ag(T85, .(T85, [])) → lastF_out_ag(T85, .(T85, []))
lastF_in_ag(T95, .(T93, T96)) → U5_ag(T95, T93, T96, lastF_in_ag(T95, T96))
U5_ag(T95, T93, T96, lastF_out_ag(T95, T96)) → lastF_out_ag(T95, .(T93, T96))
U11_agaaa(T44, T41, T42, T45, T46, lastF_out_ag(T46, T45)) → pH_out_agaaa(T44, T41, T42, T45, T46)
U6_agaa(X93, T41, T42, T43, pH_out_agaaa(X93, T41, T42, X92, T43)) → applastG_out_agaa(X93, T41, T42, T43)
U9_gaaaa(T16, T18, X31, T10, T11, applastG_out_agaa(X31, T18, T10, T11)) → pB_out_gaaaa(T16, T18, X31, T10, T11)
U1_gaa(T16, T10, T11, pB_out_gaaaa(T16, X32, X31, T10, T11)) → goalA_out_gaa(s(T16), T10, T11)
goalA_in_gaa(0, T111, T112) → U2_gaa(T111, T112, pC_in_aaa(T111, X177, T112))
pC_in_aaa(T111, T115, T116) → U12_aaa(T111, T115, T116, appendJ_in_aa(T111, T115))
appendJ_in_aa(T122, .(T122, [])) → appendJ_out_aa(T122, .(T122, []))
U12_aaa(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_aaa(T111, T115, T116, lastF_in_ag(T116, T115))
U13_aaa(T111, T115, T116, lastF_out_ag(T116, T115)) → pC_out_aaa(T111, T115, T116)
U2_gaa(T111, T112, pC_out_aaa(T111, X177, T112)) → goalA_out_gaa(0, T111, T112)

The argument filtering Pi contains the following mapping:
goalA_in_gaa(x1, x2, x3)  =  goalA_in_gaa(x1)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
0  =  0
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U9_gaaaa(x1, x2, x3, x4, x5, x6)  =  U9_gaaaa(x1, x2, x6)
applastG_in_agaa(x1, x2, x3, x4)  =  applastG_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
pH_in_agaaa(x1, x2, x3, x4, x5)  =  pH_in_agaaa(x2)
U10_agaaa(x1, x2, x3, x4, x5, x6)  =  U10_agaaa(x2, x6)
appendI_in_agaa(x1, x2, x3, x4)  =  appendI_in_agaa(x2)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1, x3)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x2, x5)
appendI_out_agaa(x1, x2, x3, x4)  =  appendI_out_agaa(x2, x4)
U11_agaaa(x1, x2, x3, x4, x5, x6)  =  U11_agaaa(x2, x4, x6)
lastF_in_ag(x1, x2)  =  lastF_in_ag(x2)
lastF_out_ag(x1, x2)  =  lastF_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
pH_out_agaaa(x1, x2, x3, x4, x5)  =  pH_out_agaaa(x2, x4)
applastG_out_agaa(x1, x2, x3, x4)  =  applastG_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_gaa(x1, x2, x3)  =  goalA_out_gaa(x1)
U2_gaa(x1, x2, x3)  =  U2_gaa(x3)
pC_in_aaa(x1, x2, x3)  =  pC_in_aaa
U12_aaa(x1, x2, x3, x4)  =  U12_aaa(x4)
appendJ_in_aa(x1, x2)  =  appendJ_in_aa
appendJ_out_aa(x1, x2)  =  appendJ_out_aa(x2)
U13_aaa(x1, x2, x3, x4)  =  U13_aaa(x2, x4)
pC_out_aaa(x1, x2, x3)  =  pC_out_aaa(x2)
GOALA_IN_GAA(x1, x2, x3)  =  GOALA_IN_GAA(x1)
U1_GAA(x1, x2, x3, x4)  =  U1_GAA(x1, x4)
PB_IN_GAAAA(x1, x2, x3, x4, x5)  =  PB_IN_GAAAA(x1)
U8_GAAAA(x1, x2, x3, x4, x5, x6)  =  U8_GAAAA(x1, x6)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U9_GAAAA(x1, x2, x3, x4, x5, x6)  =  U9_GAAAA(x1, x2, x6)
APPLASTG_IN_AGAA(x1, x2, x3, x4)  =  APPLASTG_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
PH_IN_AGAAA(x1, x2, x3, x4, x5)  =  PH_IN_AGAAA(x2)
U10_AGAAA(x1, x2, x3, x4, x5, x6)  =  U10_AGAAA(x2, x6)
APPENDI_IN_AGAA(x1, x2, x3, x4)  =  APPENDI_IN_AGAA(x2)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x5)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)
U4_GAA(x1, x2, x3, x4, x5)  =  U4_GAA(x2, x5)
U11_AGAAA(x1, x2, x3, x4, x5, x6)  =  U11_AGAAA(x2, x4, x6)
LASTF_IN_AG(x1, x2)  =  LASTF_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U2_GAA(x1, x2, x3)  =  U2_GAA(x3)
PC_IN_AAA(x1, x2, x3)  =  PC_IN_AAA
U12_AAA(x1, x2, x3, x4)  =  U12_AAA(x4)
APPENDJ_IN_AA(x1, x2)  =  APPENDJ_IN_AA
U13_AAA(x1, x2, x3, x4)  =  U13_AAA(x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 23 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

LASTF_IN_AG(T95, .(T93, T96)) → LASTF_IN_AG(T95, T96)

The TRS R consists of the following rules:

goalA_in_gaa(s(T16), T10, T11) → U1_gaa(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
pB_in_gaaaa(T16, T18, X31, T10, T11) → U8_gaaaa(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
s2lD_in_ga(s(T24), .(X66, X67)) → U3_ga(T24, X66, X67, s2lD_in_ga(T24, X67))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
U3_ga(T24, X66, X67, s2lD_out_ga(T24, X67)) → s2lD_out_ga(s(T24), .(X66, X67))
U8_gaaaa(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_gaaaa(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
applastG_in_agaa(X93, T41, T42, T43) → U6_agaa(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
pH_in_agaaa(T44, T41, T42, T45, T46) → U10_agaaa(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
appendI_in_agaa(X117, T57, T58, .(X117, X118)) → U7_agaa(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
appendE_in_gaa([], T65, .(T65, [])) → appendE_out_gaa([], T65, .(T65, []))
appendE_in_gaa(.(T72, T75), T76, .(T72, X140)) → U4_gaa(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
U4_gaa(T72, T75, T76, X140, appendE_out_gaa(T75, T76, X140)) → appendE_out_gaa(.(T72, T75), T76, .(T72, X140))
U7_agaa(X117, T57, T58, X118, appendE_out_gaa(T57, T58, X118)) → appendI_out_agaa(X117, T57, T58, .(X117, X118))
U10_agaaa(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_agaaa(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
lastF_in_ag(T85, .(T85, [])) → lastF_out_ag(T85, .(T85, []))
lastF_in_ag(T95, .(T93, T96)) → U5_ag(T95, T93, T96, lastF_in_ag(T95, T96))
U5_ag(T95, T93, T96, lastF_out_ag(T95, T96)) → lastF_out_ag(T95, .(T93, T96))
U11_agaaa(T44, T41, T42, T45, T46, lastF_out_ag(T46, T45)) → pH_out_agaaa(T44, T41, T42, T45, T46)
U6_agaa(X93, T41, T42, T43, pH_out_agaaa(X93, T41, T42, X92, T43)) → applastG_out_agaa(X93, T41, T42, T43)
U9_gaaaa(T16, T18, X31, T10, T11, applastG_out_agaa(X31, T18, T10, T11)) → pB_out_gaaaa(T16, T18, X31, T10, T11)
U1_gaa(T16, T10, T11, pB_out_gaaaa(T16, X32, X31, T10, T11)) → goalA_out_gaa(s(T16), T10, T11)
goalA_in_gaa(0, T111, T112) → U2_gaa(T111, T112, pC_in_aaa(T111, X177, T112))
pC_in_aaa(T111, T115, T116) → U12_aaa(T111, T115, T116, appendJ_in_aa(T111, T115))
appendJ_in_aa(T122, .(T122, [])) → appendJ_out_aa(T122, .(T122, []))
U12_aaa(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_aaa(T111, T115, T116, lastF_in_ag(T116, T115))
U13_aaa(T111, T115, T116, lastF_out_ag(T116, T115)) → pC_out_aaa(T111, T115, T116)
U2_gaa(T111, T112, pC_out_aaa(T111, X177, T112)) → goalA_out_gaa(0, T111, T112)

The argument filtering Pi contains the following mapping:
goalA_in_gaa(x1, x2, x3)  =  goalA_in_gaa(x1)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
0  =  0
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U9_gaaaa(x1, x2, x3, x4, x5, x6)  =  U9_gaaaa(x1, x2, x6)
applastG_in_agaa(x1, x2, x3, x4)  =  applastG_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
pH_in_agaaa(x1, x2, x3, x4, x5)  =  pH_in_agaaa(x2)
U10_agaaa(x1, x2, x3, x4, x5, x6)  =  U10_agaaa(x2, x6)
appendI_in_agaa(x1, x2, x3, x4)  =  appendI_in_agaa(x2)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1, x3)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x2, x5)
appendI_out_agaa(x1, x2, x3, x4)  =  appendI_out_agaa(x2, x4)
U11_agaaa(x1, x2, x3, x4, x5, x6)  =  U11_agaaa(x2, x4, x6)
lastF_in_ag(x1, x2)  =  lastF_in_ag(x2)
lastF_out_ag(x1, x2)  =  lastF_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
pH_out_agaaa(x1, x2, x3, x4, x5)  =  pH_out_agaaa(x2, x4)
applastG_out_agaa(x1, x2, x3, x4)  =  applastG_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_gaa(x1, x2, x3)  =  goalA_out_gaa(x1)
U2_gaa(x1, x2, x3)  =  U2_gaa(x3)
pC_in_aaa(x1, x2, x3)  =  pC_in_aaa
U12_aaa(x1, x2, x3, x4)  =  U12_aaa(x4)
appendJ_in_aa(x1, x2)  =  appendJ_in_aa
appendJ_out_aa(x1, x2)  =  appendJ_out_aa(x2)
U13_aaa(x1, x2, x3, x4)  =  U13_aaa(x2, x4)
pC_out_aaa(x1, x2, x3)  =  pC_out_aaa(x2)
LASTF_IN_AG(x1, x2)  =  LASTF_IN_AG(x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LASTF_IN_AG(T95, .(T93, T96)) → LASTF_IN_AG(T95, T96)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
LASTF_IN_AG(x1, x2)  =  LASTF_IN_AG(x2)

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

LASTF_IN_AG(.(T96)) → LASTF_IN_AG(T96)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• LASTF_IN_AG(.(T96)) → LASTF_IN_AG(T96)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

APPENDE_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDE_IN_GAA(T75, T76, X140)

The TRS R consists of the following rules:

goalA_in_gaa(s(T16), T10, T11) → U1_gaa(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
pB_in_gaaaa(T16, T18, X31, T10, T11) → U8_gaaaa(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
s2lD_in_ga(s(T24), .(X66, X67)) → U3_ga(T24, X66, X67, s2lD_in_ga(T24, X67))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
U3_ga(T24, X66, X67, s2lD_out_ga(T24, X67)) → s2lD_out_ga(s(T24), .(X66, X67))
U8_gaaaa(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_gaaaa(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
applastG_in_agaa(X93, T41, T42, T43) → U6_agaa(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
pH_in_agaaa(T44, T41, T42, T45, T46) → U10_agaaa(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
appendI_in_agaa(X117, T57, T58, .(X117, X118)) → U7_agaa(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
appendE_in_gaa([], T65, .(T65, [])) → appendE_out_gaa([], T65, .(T65, []))
appendE_in_gaa(.(T72, T75), T76, .(T72, X140)) → U4_gaa(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
U4_gaa(T72, T75, T76, X140, appendE_out_gaa(T75, T76, X140)) → appendE_out_gaa(.(T72, T75), T76, .(T72, X140))
U7_agaa(X117, T57, T58, X118, appendE_out_gaa(T57, T58, X118)) → appendI_out_agaa(X117, T57, T58, .(X117, X118))
U10_agaaa(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_agaaa(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
lastF_in_ag(T85, .(T85, [])) → lastF_out_ag(T85, .(T85, []))
lastF_in_ag(T95, .(T93, T96)) → U5_ag(T95, T93, T96, lastF_in_ag(T95, T96))
U5_ag(T95, T93, T96, lastF_out_ag(T95, T96)) → lastF_out_ag(T95, .(T93, T96))
U11_agaaa(T44, T41, T42, T45, T46, lastF_out_ag(T46, T45)) → pH_out_agaaa(T44, T41, T42, T45, T46)
U6_agaa(X93, T41, T42, T43, pH_out_agaaa(X93, T41, T42, X92, T43)) → applastG_out_agaa(X93, T41, T42, T43)
U9_gaaaa(T16, T18, X31, T10, T11, applastG_out_agaa(X31, T18, T10, T11)) → pB_out_gaaaa(T16, T18, X31, T10, T11)
U1_gaa(T16, T10, T11, pB_out_gaaaa(T16, X32, X31, T10, T11)) → goalA_out_gaa(s(T16), T10, T11)
goalA_in_gaa(0, T111, T112) → U2_gaa(T111, T112, pC_in_aaa(T111, X177, T112))
pC_in_aaa(T111, T115, T116) → U12_aaa(T111, T115, T116, appendJ_in_aa(T111, T115))
appendJ_in_aa(T122, .(T122, [])) → appendJ_out_aa(T122, .(T122, []))
U12_aaa(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_aaa(T111, T115, T116, lastF_in_ag(T116, T115))
U13_aaa(T111, T115, T116, lastF_out_ag(T116, T115)) → pC_out_aaa(T111, T115, T116)
U2_gaa(T111, T112, pC_out_aaa(T111, X177, T112)) → goalA_out_gaa(0, T111, T112)

The argument filtering Pi contains the following mapping:
goalA_in_gaa(x1, x2, x3)  =  goalA_in_gaa(x1)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
0  =  0
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U9_gaaaa(x1, x2, x3, x4, x5, x6)  =  U9_gaaaa(x1, x2, x6)
applastG_in_agaa(x1, x2, x3, x4)  =  applastG_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
pH_in_agaaa(x1, x2, x3, x4, x5)  =  pH_in_agaaa(x2)
U10_agaaa(x1, x2, x3, x4, x5, x6)  =  U10_agaaa(x2, x6)
appendI_in_agaa(x1, x2, x3, x4)  =  appendI_in_agaa(x2)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1, x3)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x2, x5)
appendI_out_agaa(x1, x2, x3, x4)  =  appendI_out_agaa(x2, x4)
U11_agaaa(x1, x2, x3, x4, x5, x6)  =  U11_agaaa(x2, x4, x6)
lastF_in_ag(x1, x2)  =  lastF_in_ag(x2)
lastF_out_ag(x1, x2)  =  lastF_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
pH_out_agaaa(x1, x2, x3, x4, x5)  =  pH_out_agaaa(x2, x4)
applastG_out_agaa(x1, x2, x3, x4)  =  applastG_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_gaa(x1, x2, x3)  =  goalA_out_gaa(x1)
U2_gaa(x1, x2, x3)  =  U2_gaa(x3)
pC_in_aaa(x1, x2, x3)  =  pC_in_aaa
U12_aaa(x1, x2, x3, x4)  =  U12_aaa(x4)
appendJ_in_aa(x1, x2)  =  appendJ_in_aa
appendJ_out_aa(x1, x2)  =  appendJ_out_aa(x2)
U13_aaa(x1, x2, x3, x4)  =  U13_aaa(x2, x4)
pC_out_aaa(x1, x2, x3)  =  pC_out_aaa(x2)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

APPENDE_IN_GAA(.(T72, T75), T76, .(T72, X140)) → APPENDE_IN_GAA(T75, T76, X140)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
APPENDE_IN_GAA(x1, x2, x3)  =  APPENDE_IN_GAA(x1)

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

APPENDE_IN_GAA(.(T75)) → APPENDE_IN_GAA(T75)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• APPENDE_IN_GAA(.(T75)) → APPENDE_IN_GAA(T75)
  The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

S2LD_IN_GA(s(T24), .(X66, X67)) → S2LD_IN_GA(T24, X67)

The TRS R consists of the following rules:

goalA_in_gaa(s(T16), T10, T11) → U1_gaa(T16, T10, T11, pB_in_gaaaa(T16, X32, X31, T10, T11))
pB_in_gaaaa(T16, T18, X31, T10, T11) → U8_gaaaa(T16, T18, X31, T10, T11, s2lD_in_ga(T16, T18))
s2lD_in_ga(s(T24), .(X66, X67)) → U3_ga(T24, X66, X67, s2lD_in_ga(T24, X67))
s2lD_in_ga(0, []) → s2lD_out_ga(0, [])
U3_ga(T24, X66, X67, s2lD_out_ga(T24, X67)) → s2lD_out_ga(s(T24), .(X66, X67))
U8_gaaaa(T16, T18, X31, T10, T11, s2lD_out_ga(T16, T18)) → U9_gaaaa(T16, T18, X31, T10, T11, applastG_in_agaa(X31, T18, T10, T11))
applastG_in_agaa(X93, T41, T42, T43) → U6_agaa(X93, T41, T42, T43, pH_in_agaaa(X93, T41, T42, X92, T43))
pH_in_agaaa(T44, T41, T42, T45, T46) → U10_agaaa(T44, T41, T42, T45, T46, appendI_in_agaa(T44, T41, T42, T45))
appendI_in_agaa(X117, T57, T58, .(X117, X118)) → U7_agaa(X117, T57, T58, X118, appendE_in_gaa(T57, T58, X118))
appendE_in_gaa([], T65, .(T65, [])) → appendE_out_gaa([], T65, .(T65, []))
appendE_in_gaa(.(T72, T75), T76, .(T72, X140)) → U4_gaa(T72, T75, T76, X140, appendE_in_gaa(T75, T76, X140))
U4_gaa(T72, T75, T76, X140, appendE_out_gaa(T75, T76, X140)) → appendE_out_gaa(.(T72, T75), T76, .(T72, X140))
U7_agaa(X117, T57, T58, X118, appendE_out_gaa(T57, T58, X118)) → appendI_out_agaa(X117, T57, T58, .(X117, X118))
U10_agaaa(T44, T41, T42, T45, T46, appendI_out_agaa(T44, T41, T42, T45)) → U11_agaaa(T44, T41, T42, T45, T46, lastF_in_ag(T46, T45))
lastF_in_ag(T85, .(T85, [])) → lastF_out_ag(T85, .(T85, []))
lastF_in_ag(T95, .(T93, T96)) → U5_ag(T95, T93, T96, lastF_in_ag(T95, T96))
U5_ag(T95, T93, T96, lastF_out_ag(T95, T96)) → lastF_out_ag(T95, .(T93, T96))
U11_agaaa(T44, T41, T42, T45, T46, lastF_out_ag(T46, T45)) → pH_out_agaaa(T44, T41, T42, T45, T46)
U6_agaa(X93, T41, T42, T43, pH_out_agaaa(X93, T41, T42, X92, T43)) → applastG_out_agaa(X93, T41, T42, T43)
U9_gaaaa(T16, T18, X31, T10, T11, applastG_out_agaa(X31, T18, T10, T11)) → pB_out_gaaaa(T16, T18, X31, T10, T11)
U1_gaa(T16, T10, T11, pB_out_gaaaa(T16, X32, X31, T10, T11)) → goalA_out_gaa(s(T16), T10, T11)
goalA_in_gaa(0, T111, T112) → U2_gaa(T111, T112, pC_in_aaa(T111, X177, T112))
pC_in_aaa(T111, T115, T116) → U12_aaa(T111, T115, T116, appendJ_in_aa(T111, T115))
appendJ_in_aa(T122, .(T122, [])) → appendJ_out_aa(T122, .(T122, []))
U12_aaa(T111, T115, T116, appendJ_out_aa(T111, T115)) → U13_aaa(T111, T115, T116, lastF_in_ag(T116, T115))
U13_aaa(T111, T115, T116, lastF_out_ag(T116, T115)) → pC_out_aaa(T111, T115, T116)
U2_gaa(T111, T112, pC_out_aaa(T111, X177, T112)) → goalA_out_gaa(0, T111, T112)

The argument filtering Pi contains the following mapping:
goalA_in_gaa(x1, x2, x3)  =  goalA_in_gaa(x1)
s(x1)  =  s(x1)
U1_gaa(x1, x2, x3, x4)  =  U1_gaa(x1, x4)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U8_gaaaa(x1, x2, x3, x4, x5, x6)  =  U8_gaaaa(x1, x6)
s2lD_in_ga(x1, x2)  =  s2lD_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
0  =  0
s2lD_out_ga(x1, x2)  =  s2lD_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U9_gaaaa(x1, x2, x3, x4, x5, x6)  =  U9_gaaaa(x1, x2, x6)
applastG_in_agaa(x1, x2, x3, x4)  =  applastG_in_agaa(x2)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
pH_in_agaaa(x1, x2, x3, x4, x5)  =  pH_in_agaaa(x2)
U10_agaaa(x1, x2, x3, x4, x5, x6)  =  U10_agaaa(x2, x6)
appendI_in_agaa(x1, x2, x3, x4)  =  appendI_in_agaa(x2)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x5)
appendE_in_gaa(x1, x2, x3)  =  appendE_in_gaa(x1)
[]  =  []
appendE_out_gaa(x1, x2, x3)  =  appendE_out_gaa(x1, x3)
U4_gaa(x1, x2, x3, x4, x5)  =  U4_gaa(x2, x5)
appendI_out_agaa(x1, x2, x3, x4)  =  appendI_out_agaa(x2, x4)
U11_agaaa(x1, x2, x3, x4, x5, x6)  =  U11_agaaa(x2, x4, x6)
lastF_in_ag(x1, x2)  =  lastF_in_ag(x2)
lastF_out_ag(x1, x2)  =  lastF_out_ag(x2)
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
pH_out_agaaa(x1, x2, x3, x4, x5)  =  pH_out_agaaa(x2, x4)
applastG_out_agaa(x1, x2, x3, x4)  =  applastG_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_gaa(x1, x2, x3)  =  goalA_out_gaa(x1)
U2_gaa(x1, x2, x3)  =  U2_gaa(x3)
pC_in_aaa(x1, x2, x3)  =  pC_in_aaa
U12_aaa(x1, x2, x3, x4)  =  U12_aaa(x4)
appendJ_in_aa(x1, x2)  =  appendJ_in_aa
appendJ_out_aa(x1, x2)  =  appendJ_out_aa(x2)
U13_aaa(x1, x2, x3, x4)  =  U13_aaa(x2, x4)
pC_out_aaa(x1, x2, x3)  =  pC_out_aaa(x2)
S2LD_IN_GA(x1, x2)  =  S2LD_IN_GA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

S2LD_IN_GA(s(T24), .(X66, X67)) → S2LD_IN_GA(T24, X67)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

S2LD_IN_GA(s(T24)) → S2LD_IN_GA(T24)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

• S2LD_IN_GA(s(T24)) → S2LD_IN_GA(T24)
  The graph contains the following edges 1 > 1

(27) YES