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

(0) Obligation:

Clauses:

rev([], []).
rev(.(X, Xs), Ys) :- ','(rev(Xs, Zs), app(Zs, .(X, []), Ys)).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Query: rev(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: rev(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: rev(T1, T2), SCOPE: 1, CLAUSE: 0 | rev(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: true | rev([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: rev(T1, T2), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nrev(T1, T2) !=? rev([], [])", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="17: rev([], T2), SCOPE: 1, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(rev(T7, X10), app(X10, .(T6, []), T9))\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="26: ','(rev(T7, X10), app(X10, .(T6, []), T9)), SCOPE: 2, CLAUSE: 0 | ','(rev(T7, X10), app(X10, .(T6, []), T9)), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(rev(T7, X10), app(X10, .(T6, []), T9)), SCOPE: 2, CLAUSE: 0\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: ','(rev(T7, X10), app(X10, .(T6, []), T9)), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nT7 is ground\nX10 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: app([], .(T6, []), T9)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: app([], .(T6, []), T9), SCOPE: 3, CLAUSE: 2 | app([], .(T6, []), T9), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: app([], .(T6, []), T9), SCOPE: 3, CLAUSE: 2\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: app([], .(T6, []), T9), SCOPE: 3, CLAUSE: 3\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="B: ','(','(rev(T22, X34), app(X34, .(T21, []), X35)), app(X35, .(T6, []), T9))\n\nT6 is ground\nT21 is ground\nT22 is ground\nX35 is free\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="C: rev(T22, X34)\n\nT22 is ground\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="G: ','(app(T23, .(T21, []), X35), app(X35, .(T6, []), T9))\n\nT6 is ground\nT21 is ground\nT23 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: rev(T22, X34), SCOPE: 4, CLAUSE: 0 | rev(T22, X34), SCOPE: 4, CLAUSE: 1\n\nT22 is ground\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: rev(T22, X34), SCOPE: 4, CLAUSE: 0\n\nT22 is ground\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: rev(T22, X34), SCOPE: 4, CLAUSE: 1\n\nT22 is ground\nX34 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="D: ','(rev(T29, X48), app(X48, .(T28, []), X49))\n\nT28 is ground\nT29 is ground\nX49 is free\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: rev(T29, X48)\n\nT29 is ground\nX48 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="E: app(T30, .(T28, []), X49)\n\nT28 is ground\nT30 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: app(T30, .(T28, []), X49), SCOPE: 5, CLAUSE: 2 | app(T30, .(T28, []), X49), SCOPE: 5, CLAUSE: 3\n\nT28 is ground\nT30 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: app(T30, .(T28, []), X49), SCOPE: 5, CLAUSE: 2\n\nT28 is ground\nT30 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: app(T30, .(T28, []), X49), SCOPE: 5, CLAUSE: 3\n\nT28 is ground\nT30 is ground\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="103: app(T45, .(T46, []), X71)\n\nT45 is ground\nT46 is ground\nX71 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: app(T23, .(T21, []), X35)\n\nT21 is ground\nT23 is ground\nX35 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="F: app(T51, .(T6, []), T9)\n\nT6 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: app(T51, .(T6, []), T9), SCOPE: 6, CLAUSE: 2 | app(T51, .(T6, []), T9), SCOPE: 6, CLAUSE: 3\n\nT6 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: app(T51, .(T6, []), T9), SCOPE: 6, CLAUSE: 2\n\nT6 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: app(T51, .(T6, []), T9), SCOPE: 6, CLAUSE: 3\n\nT6 is ground\nT51 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: app(T70, .(T71, []), T73)\n\nT70 is ground\nT71 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 132 [arrowhead = none ];
132 -> 4;

133 [label="EVAL with clause\nrev([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 133 [arrowhead = none ];
133 -> 11;

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

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

136 [label="EVAL with clause\nrev(.(X7, X8), X9) :- ','(rev(X8, X10), app(X10, .(X7, []), X9)).\nand substitutionX7 -> T6,\nX8 -> T7,\nT1 -> .(T6, T7),\nT2 -> T9,\nX9 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 136 [arrowhead = none ];
136 -> 22;

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

138 [label="BACKTRACK\nfor clause: rev(.(X, Xs), Ys) :- ','(rev(Xs, Zs), app(Zs, .(X, []), Ys))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
17 -> 138 [arrowhead = none ];
138 -> 19;

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

140 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
26 -> 140 [arrowhead = none ];
140 -> 28;

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

142 [label="EVAL with clause\nrev([], []).\nand substitutionT7 -> [],\nX10 -> []", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 142 [arrowhead = none ];
142 -> 32;

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

144 [label="EVAL with clause\nrev(.(X31, X32), X33) :- ','(rev(X32, X34), app(X34, .(X31, []), X33)).\nand substitutionX31 -> T21,\nX32 -> T22,\nT7 -> .(T21, T22),\nX10 -> X35,\nX33 -> X35", fontsize=14, style = filled, fillcolor = lightblue];
30 -> 144 [arrowhead = none ];
144 -> 58;

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

146 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
32 -> 146 [arrowhead = none ];
146 -> 36;

147 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 147 [arrowhead = none ];
147 -> 38;

148 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
36 -> 148 [arrowhead = none ];
148 -> 40;

149 [label="EVAL with clause\napp([], X17, X17).\nand substitutionT6 -> T16,\nX17 -> .(T16, []),\nT9 -> .(T16, [])", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 149 [arrowhead = none ];
149 -> 44;

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

151 [label="BACKTRACK\nfor clause: app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
40 -> 151 [arrowhead = none ];
151 -> 50;

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

153 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
58 -> 153 [arrowhead = none ];
153 -> 64;

154 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT23 is ground\nreplacements:X34 -> T23", fontsize=14, style = filled, fillcolor = violet];
58 -> 154 [arrowhead = none ];
154 -> 65;

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

156 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
65 -> 156 [arrowhead = none ];
156 -> 113;

157 [label="SPLIT 2\nnew knowledge:\nT23 is ground\nT21 is ground\nT51 is ground\nreplacements:X35 -> T51", fontsize=14, style = filled, fillcolor = violet];
65 -> 157 [arrowhead = none ];
157 -> 114;

158 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 158 [arrowhead = none ];
158 -> 68;

159 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
66 -> 159 [arrowhead = none ];
159 -> 69;

160 [label="EVAL with clause\nrev([], []).\nand substitutionT22 -> [],\nX34 -> []", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 160 [arrowhead = none ];
160 -> 71;

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

162 [label="EVAL with clause\nrev(.(X45, X46), X47) :- ','(rev(X46, X48), app(X48, .(X45, []), X47)).\nand substitutionX45 -> T28,\nX46 -> T29,\nT22 -> .(T28, T29),\nX34 -> X49,\nX47 -> X49", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 162 [arrowhead = none ];
162 -> 80;

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

164 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
71 -> 164 [arrowhead = none ];
164 -> 75;

165 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
80 -> 165 [arrowhead = none ];
165 -> 89;

166 [label="SPLIT 2\nnew knowledge:\nT29 is ground\nT30 is ground\nreplacements:X48 -> T30", fontsize=14, style = filled, fillcolor = violet];
80 -> 166 [arrowhead = none ];
166 -> 91;

167 [label="INSTANCE with matching:\nT22 -> T29\nX34 -> X48", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 167 [arrowhead = none , style=dashed];
167 -> 64[style=dashed];

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

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

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

171 [label="EVAL with clause\napp([], X56, X56).\nand substitutionT30 -> [],\nT28 -> T37,\nX56 -> .(T37, []),\nX49 -> .(T37, [])", fontsize=14, style = filled, fillcolor = lightblue];
93 -> 171 [arrowhead = none ];
171 -> 97;

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

173 [label="EVAL with clause\napp(.(X67, X68), X69, .(X67, X70)) :- app(X68, X69, X70).\nand substitutionX67 -> T44,\nX68 -> T45,\nT30 -> .(T44, T45),\nT28 -> T46,\nX69 -> .(T46, []),\nX70 -> X71,\nX49 -> .(T44, X71)", fontsize=14, style = filled, fillcolor = lightblue];
94 -> 173 [arrowhead = none ];
173 -> 103;

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

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

176 [label="INSTANCE with matching:\nT30 -> T45\nT28 -> T46\nX49 -> X71", fontsize=14, style = filled, fillcolor = lightgrey];
103 -> 176 [arrowhead = none , style=dashed];
176 -> 91[style=dashed];

177 [label="INSTANCE with matching:\nT30 -> T23\nT28 -> T21\nX49 -> X35", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 177 [arrowhead = none , style=dashed];
177 -> 91[style=dashed];

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

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

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

181 [label="EVAL with clause\napp([], X84, X84).\nand substitutionT51 -> [],\nT6 -> T60,\nX84 -> .(T60, []),\nT9 -> .(T60, [])", fontsize=14, style = filled, fillcolor = lightblue];
121 -> 181 [arrowhead = none ];
181 -> 125;

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

183 [label="EVAL with clause\napp(.(X93, X94), X95, .(X93, X96)) :- app(X94, X95, X96).\nand substitutionX93 -> T69,\nX94 -> T70,\nT51 -> .(T69, T70),\nT6 -> T71,\nX95 -> .(T71, []),\nX96 -> T73,\nT9 -> .(T69, T73),\nT72 -> T73", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 183 [arrowhead = none ];
183 -> 130;

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

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

186 [label="INSTANCE with matching:\nT51 -> T70\nT6 -> T71\nT9 -> T73", fontsize=14, style = filled, fillcolor = lightgrey];
130 -> 186 [arrowhead = none , style=dashed];
186 -> 114[style=dashed];

}

(2) Obligation:

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

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T16, []), .(T16, [])) → revA_out_ga(.(T16, []), .(T16, []))
revA_in_ga(.(T6, .(T21, T22)), T9) → U1_ga(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
pB_in_gagaga(T22, T23, T21, X35, T6, T9) → U5_gagaga(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
revC_in_ga([], []) → revC_out_ga([], [])
revC_in_ga(.(T28, T29), X49) → U2_ga(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
pD_in_gaga(T29, T30, T28, X49) → U9_gaga(T29, T30, T28, X49, revC_in_ga(T29, T30))
U9_gaga(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_gaga(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
appE_in_gga([], T37, .(T37, [])) → appE_out_gga([], T37, .(T37, []))
appE_in_gga(.(T44, T45), T46, .(T44, X71)) → U3_gga(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
U3_gga(T44, T45, T46, X71, appE_out_gga(T45, T46, X71)) → appE_out_gga(.(T44, T45), T46, .(T44, X71))
U10_gaga(T29, T30, T28, X49, appE_out_gga(T30, T28, X49)) → pD_out_gaga(T29, T30, T28, X49)
U2_ga(T28, T29, X49, pD_out_gaga(T29, X48, T28, X49)) → revC_out_ga(.(T28, T29), X49)
U5_gagaga(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_gagaga(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
pG_in_ggaga(T23, T21, T51, T6, T9) → U7_ggaga(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
U7_ggaga(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_ggaga(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
appF_in_gga([], T60, .(T60, [])) → appF_out_gga([], T60, .(T60, []))
appF_in_gga(.(T69, T70), T71, .(T69, T73)) → U4_gga(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
U4_gga(T69, T70, T71, T73, appF_out_gga(T70, T71, T73)) → appF_out_gga(.(T69, T70), T71, .(T69, T73))
U8_ggaga(T23, T21, T51, T6, T9, appF_out_gga(T51, T6, T9)) → pG_out_ggaga(T23, T21, T51, T6, T9)
U6_gagaga(T22, T23, T21, X35, T6, T9, pG_out_ggaga(T23, T21, X35, T6, T9)) → pB_out_gagaga(T22, T23, T21, X35, T6, T9)
U1_ga(T6, T21, T22, T9, pB_out_gagaga(T22, X34, T21, X35, T6, T9)) → revA_out_ga(.(T6, .(T21, T22)), T9)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2)  =  revA_in_ga(x1)
[]  =  []
revA_out_ga(x1, x2)  =  revA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
revC_in_ga(x1, x2)  =  revC_in_ga(x1)
revC_out_ga(x1, x2)  =  revC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
appF_in_gga(x1, x2, x3)  =  appF_in_gga(x1, x2)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)

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

REVA_IN_GA(.(T6, .(T21, T22)), T9) → U1_GA(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
REVA_IN_GA(.(T6, .(T21, T22)), T9) → PB_IN_GAGAGA(T22, X34, T21, X35, T6, T9)
PB_IN_GAGAGA(T22, T23, T21, X35, T6, T9) → U5_GAGAGA(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
PB_IN_GAGAGA(T22, T23, T21, X35, T6, T9) → REVC_IN_GA(T22, T23)
REVC_IN_GA(.(T28, T29), X49) → U2_GA(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
REVC_IN_GA(.(T28, T29), X49) → PD_IN_GAGA(T29, X48, T28, X49)
PD_IN_GAGA(T29, T30, T28, X49) → U9_GAGA(T29, T30, T28, X49, revC_in_ga(T29, T30))
PD_IN_GAGA(T29, T30, T28, X49) → REVC_IN_GA(T29, T30)
U9_GAGA(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_GAGA(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
U9_GAGA(T29, T30, T28, X49, revC_out_ga(T29, T30)) → APPE_IN_GGA(T30, T28, X49)
APPE_IN_GGA(.(T44, T45), T46, .(T44, X71)) → U3_GGA(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
APPE_IN_GGA(.(T44, T45), T46, .(T44, X71)) → APPE_IN_GGA(T45, T46, X71)
U5_GAGAGA(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_GAGAGA(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
U5_GAGAGA(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → PG_IN_GGAGA(T23, T21, X35, T6, T9)
PG_IN_GGAGA(T23, T21, T51, T6, T9) → U7_GGAGA(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
PG_IN_GGAGA(T23, T21, T51, T6, T9) → APPE_IN_GGA(T23, T21, T51)
U7_GGAGA(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_GGAGA(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
U7_GGAGA(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → APPF_IN_GGA(T51, T6, T9)
APPF_IN_GGA(.(T69, T70), T71, .(T69, T73)) → U4_GGA(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
APPF_IN_GGA(.(T69, T70), T71, .(T69, T73)) → APPF_IN_GGA(T70, T71, T73)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T16, []), .(T16, [])) → revA_out_ga(.(T16, []), .(T16, []))
revA_in_ga(.(T6, .(T21, T22)), T9) → U1_ga(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
pB_in_gagaga(T22, T23, T21, X35, T6, T9) → U5_gagaga(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
revC_in_ga([], []) → revC_out_ga([], [])
revC_in_ga(.(T28, T29), X49) → U2_ga(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
pD_in_gaga(T29, T30, T28, X49) → U9_gaga(T29, T30, T28, X49, revC_in_ga(T29, T30))
U9_gaga(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_gaga(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
appE_in_gga([], T37, .(T37, [])) → appE_out_gga([], T37, .(T37, []))
appE_in_gga(.(T44, T45), T46, .(T44, X71)) → U3_gga(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
U3_gga(T44, T45, T46, X71, appE_out_gga(T45, T46, X71)) → appE_out_gga(.(T44, T45), T46, .(T44, X71))
U10_gaga(T29, T30, T28, X49, appE_out_gga(T30, T28, X49)) → pD_out_gaga(T29, T30, T28, X49)
U2_ga(T28, T29, X49, pD_out_gaga(T29, X48, T28, X49)) → revC_out_ga(.(T28, T29), X49)
U5_gagaga(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_gagaga(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
pG_in_ggaga(T23, T21, T51, T6, T9) → U7_ggaga(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
U7_ggaga(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_ggaga(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
appF_in_gga([], T60, .(T60, [])) → appF_out_gga([], T60, .(T60, []))
appF_in_gga(.(T69, T70), T71, .(T69, T73)) → U4_gga(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
U4_gga(T69, T70, T71, T73, appF_out_gga(T70, T71, T73)) → appF_out_gga(.(T69, T70), T71, .(T69, T73))
U8_ggaga(T23, T21, T51, T6, T9, appF_out_gga(T51, T6, T9)) → pG_out_ggaga(T23, T21, T51, T6, T9)
U6_gagaga(T22, T23, T21, X35, T6, T9, pG_out_ggaga(T23, T21, X35, T6, T9)) → pB_out_gagaga(T22, T23, T21, X35, T6, T9)
U1_ga(T6, T21, T22, T9, pB_out_gagaga(T22, X34, T21, X35, T6, T9)) → revA_out_ga(.(T6, .(T21, T22)), T9)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2)  =  revA_in_ga(x1)
[]  =  []
revA_out_ga(x1, x2)  =  revA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
revC_in_ga(x1, x2)  =  revC_in_ga(x1)
revC_out_ga(x1, x2)  =  revC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
appF_in_gga(x1, x2, x3)  =  appF_in_gga(x1, x2)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
REVA_IN_GA(x1, x2)  =  REVA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
PB_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAGAGA(x1, x3, x5)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)
REVC_IN_GA(x1, x2)  =  REVC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
PD_IN_GAGA(x1, x2, x3, x4)  =  PD_IN_GAGA(x1, x3)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x2, x3, x5)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAGAGA(x1, x2, x3, x5, x7)
PG_IN_GGAGA(x1, x2, x3, x4, x5)  =  PG_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6)  =  U7_GGAGA(x1, x2, x4, x6)
U8_GGAGA(x1, x2, x3, x4, x5, x6)  =  U8_GGAGA(x1, x2, x3, x4, x6)
APPF_IN_GGA(x1, x2, x3)  =  APPF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(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:

REVA_IN_GA(.(T6, .(T21, T22)), T9) → U1_GA(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
REVA_IN_GA(.(T6, .(T21, T22)), T9) → PB_IN_GAGAGA(T22, X34, T21, X35, T6, T9)
PB_IN_GAGAGA(T22, T23, T21, X35, T6, T9) → U5_GAGAGA(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
PB_IN_GAGAGA(T22, T23, T21, X35, T6, T9) → REVC_IN_GA(T22, T23)
REVC_IN_GA(.(T28, T29), X49) → U2_GA(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
REVC_IN_GA(.(T28, T29), X49) → PD_IN_GAGA(T29, X48, T28, X49)
PD_IN_GAGA(T29, T30, T28, X49) → U9_GAGA(T29, T30, T28, X49, revC_in_ga(T29, T30))
PD_IN_GAGA(T29, T30, T28, X49) → REVC_IN_GA(T29, T30)
U9_GAGA(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_GAGA(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
U9_GAGA(T29, T30, T28, X49, revC_out_ga(T29, T30)) → APPE_IN_GGA(T30, T28, X49)
APPE_IN_GGA(.(T44, T45), T46, .(T44, X71)) → U3_GGA(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
APPE_IN_GGA(.(T44, T45), T46, .(T44, X71)) → APPE_IN_GGA(T45, T46, X71)
U5_GAGAGA(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_GAGAGA(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
U5_GAGAGA(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → PG_IN_GGAGA(T23, T21, X35, T6, T9)
PG_IN_GGAGA(T23, T21, T51, T6, T9) → U7_GGAGA(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
PG_IN_GGAGA(T23, T21, T51, T6, T9) → APPE_IN_GGA(T23, T21, T51)
U7_GGAGA(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_GGAGA(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
U7_GGAGA(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → APPF_IN_GGA(T51, T6, T9)
APPF_IN_GGA(.(T69, T70), T71, .(T69, T73)) → U4_GGA(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
APPF_IN_GGA(.(T69, T70), T71, .(T69, T73)) → APPF_IN_GGA(T70, T71, T73)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T16, []), .(T16, [])) → revA_out_ga(.(T16, []), .(T16, []))
revA_in_ga(.(T6, .(T21, T22)), T9) → U1_ga(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
pB_in_gagaga(T22, T23, T21, X35, T6, T9) → U5_gagaga(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
revC_in_ga([], []) → revC_out_ga([], [])
revC_in_ga(.(T28, T29), X49) → U2_ga(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
pD_in_gaga(T29, T30, T28, X49) → U9_gaga(T29, T30, T28, X49, revC_in_ga(T29, T30))
U9_gaga(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_gaga(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
appE_in_gga([], T37, .(T37, [])) → appE_out_gga([], T37, .(T37, []))
appE_in_gga(.(T44, T45), T46, .(T44, X71)) → U3_gga(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
U3_gga(T44, T45, T46, X71, appE_out_gga(T45, T46, X71)) → appE_out_gga(.(T44, T45), T46, .(T44, X71))
U10_gaga(T29, T30, T28, X49, appE_out_gga(T30, T28, X49)) → pD_out_gaga(T29, T30, T28, X49)
U2_ga(T28, T29, X49, pD_out_gaga(T29, X48, T28, X49)) → revC_out_ga(.(T28, T29), X49)
U5_gagaga(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_gagaga(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
pG_in_ggaga(T23, T21, T51, T6, T9) → U7_ggaga(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
U7_ggaga(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_ggaga(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
appF_in_gga([], T60, .(T60, [])) → appF_out_gga([], T60, .(T60, []))
appF_in_gga(.(T69, T70), T71, .(T69, T73)) → U4_gga(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
U4_gga(T69, T70, T71, T73, appF_out_gga(T70, T71, T73)) → appF_out_gga(.(T69, T70), T71, .(T69, T73))
U8_ggaga(T23, T21, T51, T6, T9, appF_out_gga(T51, T6, T9)) → pG_out_ggaga(T23, T21, T51, T6, T9)
U6_gagaga(T22, T23, T21, X35, T6, T9, pG_out_ggaga(T23, T21, X35, T6, T9)) → pB_out_gagaga(T22, T23, T21, X35, T6, T9)
U1_ga(T6, T21, T22, T9, pB_out_gagaga(T22, X34, T21, X35, T6, T9)) → revA_out_ga(.(T6, .(T21, T22)), T9)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2)  =  revA_in_ga(x1)
[]  =  []
revA_out_ga(x1, x2)  =  revA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
revC_in_ga(x1, x2)  =  revC_in_ga(x1)
revC_out_ga(x1, x2)  =  revC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
appF_in_gga(x1, x2, x3)  =  appF_in_gga(x1, x2)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
REVA_IN_GA(x1, x2)  =  REVA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
PB_IN_GAGAGA(x1, x2, x3, x4, x5, x6)  =  PB_IN_GAGAGA(x1, x3, x5)
U5_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U5_GAGAGA(x1, x3, x5, x7)
REVC_IN_GA(x1, x2)  =  REVC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x2, x4)
PD_IN_GAGA(x1, x2, x3, x4)  =  PD_IN_GAGA(x1, x3)
U9_GAGA(x1, x2, x3, x4, x5)  =  U9_GAGA(x1, x3, x5)
U10_GAGA(x1, x2, x3, x4, x5)  =  U10_GAGA(x1, x2, x3, x5)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5)  =  U3_GGA(x1, x2, x3, x5)
U6_GAGAGA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAGAGA(x1, x2, x3, x5, x7)
PG_IN_GGAGA(x1, x2, x3, x4, x5)  =  PG_IN_GGAGA(x1, x2, x4)
U7_GGAGA(x1, x2, x3, x4, x5, x6)  =  U7_GGAGA(x1, x2, x4, x6)
U8_GGAGA(x1, x2, x3, x4, x5, x6)  =  U8_GGAGA(x1, x2, x3, x4, x6)
APPF_IN_GGA(x1, x2, x3)  =  APPF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5)  =  U4_GGA(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 3 SCCs with 16 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APPF_IN_GGA(.(T69, T70), T71, .(T69, T73)) → APPF_IN_GGA(T70, T71, T73)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T16, []), .(T16, [])) → revA_out_ga(.(T16, []), .(T16, []))
revA_in_ga(.(T6, .(T21, T22)), T9) → U1_ga(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
pB_in_gagaga(T22, T23, T21, X35, T6, T9) → U5_gagaga(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
revC_in_ga([], []) → revC_out_ga([], [])
revC_in_ga(.(T28, T29), X49) → U2_ga(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
pD_in_gaga(T29, T30, T28, X49) → U9_gaga(T29, T30, T28, X49, revC_in_ga(T29, T30))
U9_gaga(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_gaga(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
appE_in_gga([], T37, .(T37, [])) → appE_out_gga([], T37, .(T37, []))
appE_in_gga(.(T44, T45), T46, .(T44, X71)) → U3_gga(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
U3_gga(T44, T45, T46, X71, appE_out_gga(T45, T46, X71)) → appE_out_gga(.(T44, T45), T46, .(T44, X71))
U10_gaga(T29, T30, T28, X49, appE_out_gga(T30, T28, X49)) → pD_out_gaga(T29, T30, T28, X49)
U2_ga(T28, T29, X49, pD_out_gaga(T29, X48, T28, X49)) → revC_out_ga(.(T28, T29), X49)
U5_gagaga(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_gagaga(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
pG_in_ggaga(T23, T21, T51, T6, T9) → U7_ggaga(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
U7_ggaga(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_ggaga(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
appF_in_gga([], T60, .(T60, [])) → appF_out_gga([], T60, .(T60, []))
appF_in_gga(.(T69, T70), T71, .(T69, T73)) → U4_gga(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
U4_gga(T69, T70, T71, T73, appF_out_gga(T70, T71, T73)) → appF_out_gga(.(T69, T70), T71, .(T69, T73))
U8_ggaga(T23, T21, T51, T6, T9, appF_out_gga(T51, T6, T9)) → pG_out_ggaga(T23, T21, T51, T6, T9)
U6_gagaga(T22, T23, T21, X35, T6, T9, pG_out_ggaga(T23, T21, X35, T6, T9)) → pB_out_gagaga(T22, T23, T21, X35, T6, T9)
U1_ga(T6, T21, T22, T9, pB_out_gagaga(T22, X34, T21, X35, T6, T9)) → revA_out_ga(.(T6, .(T21, T22)), T9)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2)  =  revA_in_ga(x1)
[]  =  []
revA_out_ga(x1, x2)  =  revA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
revC_in_ga(x1, x2)  =  revC_in_ga(x1)
revC_out_ga(x1, x2)  =  revC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
appF_in_gga(x1, x2, x3)  =  appF_in_gga(x1, x2)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
APPF_IN_GGA(x1, x2, x3)  =  APPF_IN_GGA(x1, 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:

APPF_IN_GGA(.(T69, T70), T71, .(T69, T73)) → APPF_IN_GGA(T70, T71, T73)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APPF_IN_GGA(x1, x2, x3)  =  APPF_IN_GGA(x1, 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:

APPF_IN_GGA(.(T69, T70), T71) → APPF_IN_GGA(T70, T71)

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:

• APPF_IN_GGA(.(T69, T70), T71) → APPF_IN_GGA(T70, T71)
  The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

APPE_IN_GGA(.(T44, T45), T46, .(T44, X71)) → APPE_IN_GGA(T45, T46, X71)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T16, []), .(T16, [])) → revA_out_ga(.(T16, []), .(T16, []))
revA_in_ga(.(T6, .(T21, T22)), T9) → U1_ga(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
pB_in_gagaga(T22, T23, T21, X35, T6, T9) → U5_gagaga(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
revC_in_ga([], []) → revC_out_ga([], [])
revC_in_ga(.(T28, T29), X49) → U2_ga(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
pD_in_gaga(T29, T30, T28, X49) → U9_gaga(T29, T30, T28, X49, revC_in_ga(T29, T30))
U9_gaga(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_gaga(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
appE_in_gga([], T37, .(T37, [])) → appE_out_gga([], T37, .(T37, []))
appE_in_gga(.(T44, T45), T46, .(T44, X71)) → U3_gga(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
U3_gga(T44, T45, T46, X71, appE_out_gga(T45, T46, X71)) → appE_out_gga(.(T44, T45), T46, .(T44, X71))
U10_gaga(T29, T30, T28, X49, appE_out_gga(T30, T28, X49)) → pD_out_gaga(T29, T30, T28, X49)
U2_ga(T28, T29, X49, pD_out_gaga(T29, X48, T28, X49)) → revC_out_ga(.(T28, T29), X49)
U5_gagaga(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_gagaga(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
pG_in_ggaga(T23, T21, T51, T6, T9) → U7_ggaga(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
U7_ggaga(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_ggaga(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
appF_in_gga([], T60, .(T60, [])) → appF_out_gga([], T60, .(T60, []))
appF_in_gga(.(T69, T70), T71, .(T69, T73)) → U4_gga(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
U4_gga(T69, T70, T71, T73, appF_out_gga(T70, T71, T73)) → appF_out_gga(.(T69, T70), T71, .(T69, T73))
U8_ggaga(T23, T21, T51, T6, T9, appF_out_gga(T51, T6, T9)) → pG_out_ggaga(T23, T21, T51, T6, T9)
U6_gagaga(T22, T23, T21, X35, T6, T9, pG_out_ggaga(T23, T21, X35, T6, T9)) → pB_out_gagaga(T22, T23, T21, X35, T6, T9)
U1_ga(T6, T21, T22, T9, pB_out_gagaga(T22, X34, T21, X35, T6, T9)) → revA_out_ga(.(T6, .(T21, T22)), T9)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2)  =  revA_in_ga(x1)
[]  =  []
revA_out_ga(x1, x2)  =  revA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
revC_in_ga(x1, x2)  =  revC_in_ga(x1)
revC_out_ga(x1, x2)  =  revC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
appF_in_gga(x1, x2, x3)  =  appF_in_gga(x1, x2)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
APPE_IN_GGA(x1, x2, x3)  =  APPE_IN_GGA(x1, x2)

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:

APPE_IN_GGA(.(T44, T45), T46, .(T44, X71)) → APPE_IN_GGA(T45, T46, X71)

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

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:

APPE_IN_GGA(.(T44, T45), T46) → APPE_IN_GGA(T45, T46)

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:

• APPE_IN_GGA(.(T44, T45), T46) → APPE_IN_GGA(T45, T46)
  The graph contains the following edges 1 > 1, 2 >= 2

(20) YES

(21) Obligation:

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

REVC_IN_GA(.(T28, T29), X49) → PD_IN_GAGA(T29, X48, T28, X49)
PD_IN_GAGA(T29, T30, T28, X49) → REVC_IN_GA(T29, T30)

The TRS R consists of the following rules:

revA_in_ga([], []) → revA_out_ga([], [])
revA_in_ga(.(T16, []), .(T16, [])) → revA_out_ga(.(T16, []), .(T16, []))
revA_in_ga(.(T6, .(T21, T22)), T9) → U1_ga(T6, T21, T22, T9, pB_in_gagaga(T22, X34, T21, X35, T6, T9))
pB_in_gagaga(T22, T23, T21, X35, T6, T9) → U5_gagaga(T22, T23, T21, X35, T6, T9, revC_in_ga(T22, T23))
revC_in_ga([], []) → revC_out_ga([], [])
revC_in_ga(.(T28, T29), X49) → U2_ga(T28, T29, X49, pD_in_gaga(T29, X48, T28, X49))
pD_in_gaga(T29, T30, T28, X49) → U9_gaga(T29, T30, T28, X49, revC_in_ga(T29, T30))
U9_gaga(T29, T30, T28, X49, revC_out_ga(T29, T30)) → U10_gaga(T29, T30, T28, X49, appE_in_gga(T30, T28, X49))
appE_in_gga([], T37, .(T37, [])) → appE_out_gga([], T37, .(T37, []))
appE_in_gga(.(T44, T45), T46, .(T44, X71)) → U3_gga(T44, T45, T46, X71, appE_in_gga(T45, T46, X71))
U3_gga(T44, T45, T46, X71, appE_out_gga(T45, T46, X71)) → appE_out_gga(.(T44, T45), T46, .(T44, X71))
U10_gaga(T29, T30, T28, X49, appE_out_gga(T30, T28, X49)) → pD_out_gaga(T29, T30, T28, X49)
U2_ga(T28, T29, X49, pD_out_gaga(T29, X48, T28, X49)) → revC_out_ga(.(T28, T29), X49)
U5_gagaga(T22, T23, T21, X35, T6, T9, revC_out_ga(T22, T23)) → U6_gagaga(T22, T23, T21, X35, T6, T9, pG_in_ggaga(T23, T21, X35, T6, T9))
pG_in_ggaga(T23, T21, T51, T6, T9) → U7_ggaga(T23, T21, T51, T6, T9, appE_in_gga(T23, T21, T51))
U7_ggaga(T23, T21, T51, T6, T9, appE_out_gga(T23, T21, T51)) → U8_ggaga(T23, T21, T51, T6, T9, appF_in_gga(T51, T6, T9))
appF_in_gga([], T60, .(T60, [])) → appF_out_gga([], T60, .(T60, []))
appF_in_gga(.(T69, T70), T71, .(T69, T73)) → U4_gga(T69, T70, T71, T73, appF_in_gga(T70, T71, T73))
U4_gga(T69, T70, T71, T73, appF_out_gga(T70, T71, T73)) → appF_out_gga(.(T69, T70), T71, .(T69, T73))
U8_ggaga(T23, T21, T51, T6, T9, appF_out_gga(T51, T6, T9)) → pG_out_ggaga(T23, T21, T51, T6, T9)
U6_gagaga(T22, T23, T21, X35, T6, T9, pG_out_ggaga(T23, T21, X35, T6, T9)) → pB_out_gagaga(T22, T23, T21, X35, T6, T9)
U1_ga(T6, T21, T22, T9, pB_out_gagaga(T22, X34, T21, X35, T6, T9)) → revA_out_ga(.(T6, .(T21, T22)), T9)

The argument filtering Pi contains the following mapping:
revA_in_ga(x1, x2)  =  revA_in_ga(x1)
[]  =  []
revA_out_ga(x1, x2)  =  revA_out_ga(x1, x2)
.(x1, x2)  =  .(x1, x2)
U1_ga(x1, x2, x3, x4, x5)  =  U1_ga(x1, x2, x3, x5)
pB_in_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_in_gagaga(x1, x3, x5)
U5_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U5_gagaga(x1, x3, x5, x7)
revC_in_ga(x1, x2)  =  revC_in_ga(x1)
revC_out_ga(x1, x2)  =  revC_out_ga(x1, x2)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x2, x4)
pD_in_gaga(x1, x2, x3, x4)  =  pD_in_gaga(x1, x3)
U9_gaga(x1, x2, x3, x4, x5)  =  U9_gaga(x1, x3, x5)
U10_gaga(x1, x2, x3, x4, x5)  =  U10_gaga(x1, x2, x3, x5)
appE_in_gga(x1, x2, x3)  =  appE_in_gga(x1, x2)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
U3_gga(x1, x2, x3, x4, x5)  =  U3_gga(x1, x2, x3, x5)
pD_out_gaga(x1, x2, x3, x4)  =  pD_out_gaga(x1, x2, x3, x4)
U6_gagaga(x1, x2, x3, x4, x5, x6, x7)  =  U6_gagaga(x1, x2, x3, x5, x7)
pG_in_ggaga(x1, x2, x3, x4, x5)  =  pG_in_ggaga(x1, x2, x4)
U7_ggaga(x1, x2, x3, x4, x5, x6)  =  U7_ggaga(x1, x2, x4, x6)
U8_ggaga(x1, x2, x3, x4, x5, x6)  =  U8_ggaga(x1, x2, x3, x4, x6)
appF_in_gga(x1, x2, x3)  =  appF_in_gga(x1, x2)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
pG_out_ggaga(x1, x2, x3, x4, x5)  =  pG_out_ggaga(x1, x2, x3, x4, x5)
pB_out_gagaga(x1, x2, x3, x4, x5, x6)  =  pB_out_gagaga(x1, x2, x3, x4, x5, x6)
REVC_IN_GA(x1, x2)  =  REVC_IN_GA(x1)
PD_IN_GAGA(x1, x2, x3, x4)  =  PD_IN_GAGA(x1, x3)

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:

REVC_IN_GA(.(T28, T29), X49) → PD_IN_GAGA(T29, X48, T28, X49)
PD_IN_GAGA(T29, T30, T28, X49) → REVC_IN_GA(T29, T30)

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

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:

REVC_IN_GA(.(T28, T29)) → PD_IN_GAGA(T29, T28)
PD_IN_GAGA(T29, T28) → REVC_IN_GA(T29)

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:

• PD_IN_GAGA(T29, T28) → REVC_IN_GA(T29)
  The graph contains the following edges 1 >= 1

• REVC_IN_GA(.(T28, T29)) → PD_IN_GAGA(T29, T28)
  The graph contains the following edges 1 > 1, 1 > 2

(27) YES