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

(0) Obligation:

Clauses:

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

Query: reverse(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: reverse(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: reverse(T1, T2), SCOPE: 1, CLAUSE: 2 | reverse(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: ','(reverse(T7, X7), app(X7, .(T6, []), T9)) | reverse(.(T6, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: reverse(T1, T2), SCOPE: 1, CLAUSE: 3\n\nT1 is ground\nX4 is free\nX5 is free\nX6 is free\nreverse(T1, T2) !=? reverse(.(X4, X5), X6)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(reverse(T7, X7), app(X7, .(T6, []), T9)), SCOPE: 2, CLAUSE: 2 | ','(reverse(T7, X7), app(X7, .(T6, []), T9)), SCOPE: 2, CLAUSE: 3 | ?_2 | reverse(.(T6, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(reverse(T7, X7), app(X7, .(T6, []), T9)), SCOPE: 2, CLAUSE: 2\n\nT6 is ground\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(reverse(T7, X7), app(X7, .(T6, []), T9)), SCOPE: 2, CLAUSE: 3 | ?_2 | reverse(.(T6, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
23 [label="B: ','(','(reverse(T19, X29), app(X29, .(T18, []), X30)), app(X30, .(T6, []), T9))\n\nT6 is ground\nT18 is ground\nT19 is ground\nX30 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="24: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="C: reverse(T19, X29)\n\nT19 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="G: ','(app(T22, .(T18, []), X30), app(X30, .(T6, []), T9))\n\nT6 is ground\nT18 is ground\nT22 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: reverse(T19, X29), SCOPE: 3, CLAUSE: 2 | reverse(T19, X29), SCOPE: 3, CLAUSE: 3\n\nT19 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: reverse(T19, X29), SCOPE: 3, CLAUSE: 2\n\nT19 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: reverse(T19, X29), SCOPE: 3, CLAUSE: 3\n\nT19 is ground\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="D: ','(reverse(T34, X62), app(X62, .(T33, []), X63))\n\nT33 is ground\nT34 is ground\nX63 is free\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: reverse(T34, X62)\n\nT34 is ground\nX62 is free", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="E: app(T37, .(T33, []), X63)\n\nT33 is ground\nT37 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: app(T37, .(T33, []), X63), SCOPE: 4, CLAUSE: 0 | app(T37, .(T33, []), X63), SCOPE: 4, CLAUSE: 1\n\nT33 is ground\nT37 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: app(T37, .(T33, []), X63), SCOPE: 4, CLAUSE: 0\n\nT33 is ground\nT37 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
55 [label="55: app(T37, .(T33, []), X63), SCOPE: 4, CLAUSE: 1\n\nT33 is ground\nT37 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: app(T56, .(T57, []), X103)\n\nT56 is ground\nT57 is ground\nX103 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
64 [label="64: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: app(T22, .(T18, []), X30)\n\nT18 is ground\nT22 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="F: app(T67, .(T6, []), T9)\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: app(T67, .(T6, []), T9), SCOPE: 5, CLAUSE: 0 | app(T67, .(T6, []), T9), SCOPE: 5, CLAUSE: 1\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: app(T67, .(T6, []), T9), SCOPE: 5, CLAUSE: 0\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: app(T67, .(T6, []), T9), SCOPE: 5, CLAUSE: 1\n\nT6 is ground\nT67 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
89 [label="89: app(T92, .(T93, []), T95)\n\nT92 is ground\nT93 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
100 [label="100: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: ','(reverse(T7, X7), app(X7, .(T6, []), T9)), SCOPE: 2, CLAUSE: 3\n\nT6 is ground\nT7 is ground\nX7 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: ?_2 | reverse(.(T6, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: app([], .(T6, []), T9)\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: app([], .(T6, []), T9), SCOPE: 6, CLAUSE: 0 | app([], .(T6, []), T9), SCOPE: 6, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: app([], .(T6, []), T9), SCOPE: 6, CLAUSE: 1\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: reverse(.(T6, T7), T2), SCOPE: 1, CLAUSE: 3\n\nT6 is ground\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 133 [arrowhead = none ];
133 -> 6;

134 [label="EVAL with clause\nreverse(.(X4, X5), X6) :- ','(reverse(X5, X7), app(X7, .(X4, []), X6)).\nand substitutionX4 -> T6,\nX5 -> T7,\nT1 -> .(T6, T7),\nT2 -> T9,\nX6 -> T9,\nT8 -> T9", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 134 [arrowhead = none ];
134 -> 12;

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

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

137 [label="EVAL with clause\nreverse([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 137 [arrowhead = none ];
137 -> 128;

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

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

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

141 [label="EVAL with clause\nreverse(.(X26, X27), X28) :- ','(reverse(X27, X29), app(X29, .(X26, []), X28)).\nand substitutionX26 -> T18,\nX27 -> T19,\nT7 -> .(T18, T19),\nX7 -> X30,\nX28 -> X30", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 141 [arrowhead = none ];
141 -> 23;

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

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

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

145 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
23 -> 145 [arrowhead = none ];
145 -> 29;

146 [label="SPLIT 2\nnew knowledge:\nT19 is ground\nT22 is ground\nreplacements:X29 -> T22", fontsize=14, style = filled, fillcolor = violet];
23 -> 146 [arrowhead = none ];
146 -> 30;

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

148 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
30 -> 148 [arrowhead = none ];
148 -> 77;

149 [label="SPLIT 2\nnew knowledge:\nT22 is ground\nT18 is ground\nT67 is ground\nreplacements:X30 -> T67", fontsize=14, style = filled, fillcolor = violet];
30 -> 149 [arrowhead = none ];
149 -> 79;

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

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

152 [label="EVAL with clause\nreverse(.(X59, X60), X61) :- ','(reverse(X60, X62), app(X62, .(X59, []), X61)).\nand substitutionX59 -> T33,\nX60 -> T34,\nT19 -> .(T33, T34),\nX29 -> X63,\nX61 -> X63", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 152 [arrowhead = none ];
152 -> 40;

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

154 [label="EVAL with clause\nreverse([], []).\nand substitutionT19 -> [],\nX29 -> []", fontsize=14, style = filled, fillcolor = lightblue];
38 -> 154 [arrowhead = none ];
154 -> 69;

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

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

157 [label="SPLIT 2\nnew knowledge:\nT34 is ground\nT37 is ground\nreplacements:X62 -> T37", fontsize=14, style = filled, fillcolor = violet];
40 -> 157 [arrowhead = none ];
157 -> 45;

158 [label="INSTANCE with matching:\nT19 -> T34\nX29 -> X62", fontsize=14, style = filled, fillcolor = lightgrey];
44 -> 158 [arrowhead = none , style=dashed];
158 -> 29[style=dashed];

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

160 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
50 -> 160 [arrowhead = none ];
160 -> 54;

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

162 [label="EVAL with clause\napp(.(X99, X100), X101, .(X99, X102)) :- app(X100, X101, X102).\nand substitutionX99 -> T55,\nX100 -> T56,\nT37 -> .(T55, T56),\nT33 -> T57,\nX101 -> .(T57, []),\nX102 -> X103,\nX63 -> .(T55, X103)", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 162 [arrowhead = none ];
162 -> 58;

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

164 [label="EVAL with clause\napp([], X111, X111).\nand substitutionT37 -> [],\nT33 -> T63,\nX111 -> .(T63, []),\nX63 -> .(T63, [])", fontsize=14, style = filled, fillcolor = lightblue];
55 -> 164 [arrowhead = none ];
164 -> 62;

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

166 [label="INSTANCE with matching:\nT37 -> T56\nT33 -> T57\nX63 -> X103", fontsize=14, style = filled, fillcolor = lightgrey];
58 -> 166 [arrowhead = none , style=dashed];
166 -> 45[style=dashed];

167 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
62 -> 167 [arrowhead = none ];
167 -> 64;

168 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
69 -> 168 [arrowhead = none ];
168 -> 74;

169 [label="INSTANCE with matching:\nT37 -> T22\nT33 -> T18\nX63 -> X30", fontsize=14, style = filled, fillcolor = lightgrey];
77 -> 169 [arrowhead = none , style=dashed];
169 -> 45[style=dashed];

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

171 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
82 -> 171 [arrowhead = none ];
171 -> 84;

172 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
82 -> 172 [arrowhead = none ];
172 -> 85;

173 [label="EVAL with clause\napp(.(X142, X143), X144, .(X142, X145)) :- app(X143, X144, X145).\nand substitutionX142 -> T91,\nX143 -> T92,\nT67 -> .(T91, T92),\nT6 -> T93,\nX144 -> .(T93, []),\nX145 -> T95,\nT9 -> .(T91, T95),\nT94 -> T95", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 173 [arrowhead = none ];
173 -> 89;

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

175 [label="EVAL with clause\napp([], X152, X152).\nand substitutionT67 -> [],\nT6 -> T102,\nX152 -> .(T102, []),\nT9 -> .(T102, [])", fontsize=14, style = filled, fillcolor = lightblue];
85 -> 175 [arrowhead = none ];
175 -> 99;

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

177 [label="INSTANCE with matching:\nT67 -> T92\nT6 -> T93\nT9 -> T95", fontsize=14, style = filled, fillcolor = lightgrey];
89 -> 177 [arrowhead = none , style=dashed];
177 -> 79[style=dashed];

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

179 [label="EVAL with clause\nreverse([], []).\nand substitutionT7 -> [],\nX7 -> []", fontsize=14, style = filled, fillcolor = lightblue];
104 -> 179 [arrowhead = none ];
179 -> 109;

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

181 [label="FAILURE", fontsize=14, style = filled, fillcolor = lightgreen];
105 -> 181 [arrowhead = none ];
181 -> 123;

182 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
109 -> 182 [arrowhead = none ];
182 -> 113;

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

184 [label="EVAL with clause\napp([], X163, X163).\nand substitutionT6 -> T105,\nX163 -> .(T105, []),\nT9 -> .(T105, [])", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 184 [arrowhead = none ];
184 -> 118;

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

186 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
118 -> 186 [arrowhead = none ];
186 -> 121;

187 [label="BACKTRACK\nfor clause: reverse([], [])because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
123 -> 187 [arrowhead = none ];
187 -> 127;

188 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
128 -> 188 [arrowhead = none ];
188 -> 132;

}

(2) Obligation:

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

reverseA_in_ga(.(T6, .(T18, T19)), T9) → U1_ga(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
pB_in_gagaga(T19, T22, T18, X30, T6, T9) → U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
reverseC_in_ga(.(T33, T34), X63) → U2_ga(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
pD_in_gaga(T34, T37, T33, X63) → U9_gaga(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
reverseC_in_ga([], []) → reverseC_out_ga([], [])
U9_gaga(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_gaga(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
appE_in_gga(.(T55, T56), T57, .(T55, X103)) → U3_gga(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
appE_in_gga([], T63, .(T63, [])) → appE_out_gga([], T63, .(T63, []))
U3_gga(T55, T56, T57, X103, appE_out_gga(T56, T57, X103)) → appE_out_gga(.(T55, T56), T57, .(T55, X103))
U10_gaga(T34, T37, T33, X63, appE_out_gga(T37, T33, X63)) → pD_out_gaga(T34, T37, T33, X63)
U2_ga(T33, T34, X63, pD_out_gaga(T34, X62, T33, X63)) → reverseC_out_ga(.(T33, T34), X63)
U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_gagaga(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
pG_in_ggaga(T22, T18, T67, T6, T9) → U7_ggaga(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
U7_ggaga(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_ggaga(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
appF_in_gga(.(T91, T92), T93, .(T91, T95)) → U4_gga(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
appF_in_gga([], T102, .(T102, [])) → appF_out_gga([], T102, .(T102, []))
U4_gga(T91, T92, T93, T95, appF_out_gga(T92, T93, T95)) → appF_out_gga(.(T91, T92), T93, .(T91, T95))
U8_ggaga(T22, T18, T67, T6, T9, appF_out_gga(T67, T6, T9)) → pG_out_ggaga(T22, T18, T67, T6, T9)
U6_gagaga(T19, T22, T18, X30, T6, T9, pG_out_ggaga(T22, T18, X30, T6, T9)) → pB_out_gagaga(T19, T22, T18, X30, T6, T9)
U1_ga(T6, T18, T19, T9, pB_out_gagaga(T19, X29, T18, X30, T6, T9)) → reverseA_out_ga(.(T6, .(T18, T19)), T9)
reverseA_in_ga(.(T105, []), .(T105, [])) → reverseA_out_ga(.(T105, []), .(T105, []))
reverseA_in_ga([], []) → reverseA_out_ga([], [])

The argument filtering Pi contains the following mapping:
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
.(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)
reverseC_in_ga(x1, x2)  =  reverseC_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)
[]  =  []
reverseC_out_ga(x1, x2)  =  reverseC_out_ga(x1, x2)
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)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
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)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
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)
reverseA_out_ga(x1, x2)  =  reverseA_out_ga(x1, 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:

REVERSEA_IN_GA(.(T6, .(T18, T19)), T9) → U1_GA(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
REVERSEA_IN_GA(.(T6, .(T18, T19)), T9) → PB_IN_GAGAGA(T19, X29, T18, X30, T6, T9)
PB_IN_GAGAGA(T19, T22, T18, X30, T6, T9) → U5_GAGAGA(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
PB_IN_GAGAGA(T19, T22, T18, X30, T6, T9) → REVERSEC_IN_GA(T19, T22)
REVERSEC_IN_GA(.(T33, T34), X63) → U2_GA(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
REVERSEC_IN_GA(.(T33, T34), X63) → PD_IN_GAGA(T34, X62, T33, X63)
PD_IN_GAGA(T34, T37, T33, X63) → U9_GAGA(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
PD_IN_GAGA(T34, T37, T33, X63) → REVERSEC_IN_GA(T34, T37)
U9_GAGA(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_GAGA(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
U9_GAGA(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → APPE_IN_GGA(T37, T33, X63)
APPE_IN_GGA(.(T55, T56), T57, .(T55, X103)) → U3_GGA(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
APPE_IN_GGA(.(T55, T56), T57, .(T55, X103)) → APPE_IN_GGA(T56, T57, X103)
U5_GAGAGA(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_GAGAGA(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
U5_GAGAGA(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → PG_IN_GGAGA(T22, T18, X30, T6, T9)
PG_IN_GGAGA(T22, T18, T67, T6, T9) → U7_GGAGA(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
PG_IN_GGAGA(T22, T18, T67, T6, T9) → APPE_IN_GGA(T22, T18, T67)
U7_GGAGA(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_GGAGA(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
U7_GGAGA(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → APPF_IN_GGA(T67, T6, T9)
APPF_IN_GGA(.(T91, T92), T93, .(T91, T95)) → U4_GGA(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
APPF_IN_GGA(.(T91, T92), T93, .(T91, T95)) → APPF_IN_GGA(T92, T93, T95)

The TRS R consists of the following rules:

reverseA_in_ga(.(T6, .(T18, T19)), T9) → U1_ga(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
pB_in_gagaga(T19, T22, T18, X30, T6, T9) → U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
reverseC_in_ga(.(T33, T34), X63) → U2_ga(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
pD_in_gaga(T34, T37, T33, X63) → U9_gaga(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
reverseC_in_ga([], []) → reverseC_out_ga([], [])
U9_gaga(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_gaga(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
appE_in_gga(.(T55, T56), T57, .(T55, X103)) → U3_gga(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
appE_in_gga([], T63, .(T63, [])) → appE_out_gga([], T63, .(T63, []))
U3_gga(T55, T56, T57, X103, appE_out_gga(T56, T57, X103)) → appE_out_gga(.(T55, T56), T57, .(T55, X103))
U10_gaga(T34, T37, T33, X63, appE_out_gga(T37, T33, X63)) → pD_out_gaga(T34, T37, T33, X63)
U2_ga(T33, T34, X63, pD_out_gaga(T34, X62, T33, X63)) → reverseC_out_ga(.(T33, T34), X63)
U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_gagaga(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
pG_in_ggaga(T22, T18, T67, T6, T9) → U7_ggaga(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
U7_ggaga(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_ggaga(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
appF_in_gga(.(T91, T92), T93, .(T91, T95)) → U4_gga(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
appF_in_gga([], T102, .(T102, [])) → appF_out_gga([], T102, .(T102, []))
U4_gga(T91, T92, T93, T95, appF_out_gga(T92, T93, T95)) → appF_out_gga(.(T91, T92), T93, .(T91, T95))
U8_ggaga(T22, T18, T67, T6, T9, appF_out_gga(T67, T6, T9)) → pG_out_ggaga(T22, T18, T67, T6, T9)
U6_gagaga(T19, T22, T18, X30, T6, T9, pG_out_ggaga(T22, T18, X30, T6, T9)) → pB_out_gagaga(T19, T22, T18, X30, T6, T9)
U1_ga(T6, T18, T19, T9, pB_out_gagaga(T19, X29, T18, X30, T6, T9)) → reverseA_out_ga(.(T6, .(T18, T19)), T9)
reverseA_in_ga(.(T105, []), .(T105, [])) → reverseA_out_ga(.(T105, []), .(T105, []))
reverseA_in_ga([], []) → reverseA_out_ga([], [])

The argument filtering Pi contains the following mapping:
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
.(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)
reverseC_in_ga(x1, x2)  =  reverseC_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)
[]  =  []
reverseC_out_ga(x1, x2)  =  reverseC_out_ga(x1, x2)
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)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
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)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
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)
reverseA_out_ga(x1, x2)  =  reverseA_out_ga(x1, x2)
REVERSEA_IN_GA(x1, x2)  =  REVERSEA_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)
REVERSEC_IN_GA(x1, x2)  =  REVERSEC_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:

REVERSEA_IN_GA(.(T6, .(T18, T19)), T9) → U1_GA(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
REVERSEA_IN_GA(.(T6, .(T18, T19)), T9) → PB_IN_GAGAGA(T19, X29, T18, X30, T6, T9)
PB_IN_GAGAGA(T19, T22, T18, X30, T6, T9) → U5_GAGAGA(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
PB_IN_GAGAGA(T19, T22, T18, X30, T6, T9) → REVERSEC_IN_GA(T19, T22)
REVERSEC_IN_GA(.(T33, T34), X63) → U2_GA(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
REVERSEC_IN_GA(.(T33, T34), X63) → PD_IN_GAGA(T34, X62, T33, X63)
PD_IN_GAGA(T34, T37, T33, X63) → U9_GAGA(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
PD_IN_GAGA(T34, T37, T33, X63) → REVERSEC_IN_GA(T34, T37)
U9_GAGA(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_GAGA(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
U9_GAGA(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → APPE_IN_GGA(T37, T33, X63)
APPE_IN_GGA(.(T55, T56), T57, .(T55, X103)) → U3_GGA(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
APPE_IN_GGA(.(T55, T56), T57, .(T55, X103)) → APPE_IN_GGA(T56, T57, X103)
U5_GAGAGA(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_GAGAGA(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
U5_GAGAGA(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → PG_IN_GGAGA(T22, T18, X30, T6, T9)
PG_IN_GGAGA(T22, T18, T67, T6, T9) → U7_GGAGA(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
PG_IN_GGAGA(T22, T18, T67, T6, T9) → APPE_IN_GGA(T22, T18, T67)
U7_GGAGA(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_GGAGA(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
U7_GGAGA(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → APPF_IN_GGA(T67, T6, T9)
APPF_IN_GGA(.(T91, T92), T93, .(T91, T95)) → U4_GGA(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
APPF_IN_GGA(.(T91, T92), T93, .(T91, T95)) → APPF_IN_GGA(T92, T93, T95)

The TRS R consists of the following rules:

reverseA_in_ga(.(T6, .(T18, T19)), T9) → U1_ga(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
pB_in_gagaga(T19, T22, T18, X30, T6, T9) → U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
reverseC_in_ga(.(T33, T34), X63) → U2_ga(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
pD_in_gaga(T34, T37, T33, X63) → U9_gaga(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
reverseC_in_ga([], []) → reverseC_out_ga([], [])
U9_gaga(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_gaga(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
appE_in_gga(.(T55, T56), T57, .(T55, X103)) → U3_gga(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
appE_in_gga([], T63, .(T63, [])) → appE_out_gga([], T63, .(T63, []))
U3_gga(T55, T56, T57, X103, appE_out_gga(T56, T57, X103)) → appE_out_gga(.(T55, T56), T57, .(T55, X103))
U10_gaga(T34, T37, T33, X63, appE_out_gga(T37, T33, X63)) → pD_out_gaga(T34, T37, T33, X63)
U2_ga(T33, T34, X63, pD_out_gaga(T34, X62, T33, X63)) → reverseC_out_ga(.(T33, T34), X63)
U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_gagaga(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
pG_in_ggaga(T22, T18, T67, T6, T9) → U7_ggaga(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
U7_ggaga(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_ggaga(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
appF_in_gga(.(T91, T92), T93, .(T91, T95)) → U4_gga(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
appF_in_gga([], T102, .(T102, [])) → appF_out_gga([], T102, .(T102, []))
U4_gga(T91, T92, T93, T95, appF_out_gga(T92, T93, T95)) → appF_out_gga(.(T91, T92), T93, .(T91, T95))
U8_ggaga(T22, T18, T67, T6, T9, appF_out_gga(T67, T6, T9)) → pG_out_ggaga(T22, T18, T67, T6, T9)
U6_gagaga(T19, T22, T18, X30, T6, T9, pG_out_ggaga(T22, T18, X30, T6, T9)) → pB_out_gagaga(T19, T22, T18, X30, T6, T9)
U1_ga(T6, T18, T19, T9, pB_out_gagaga(T19, X29, T18, X30, T6, T9)) → reverseA_out_ga(.(T6, .(T18, T19)), T9)
reverseA_in_ga(.(T105, []), .(T105, [])) → reverseA_out_ga(.(T105, []), .(T105, []))
reverseA_in_ga([], []) → reverseA_out_ga([], [])

The argument filtering Pi contains the following mapping:
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
.(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)
reverseC_in_ga(x1, x2)  =  reverseC_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)
[]  =  []
reverseC_out_ga(x1, x2)  =  reverseC_out_ga(x1, x2)
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)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
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)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
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)
reverseA_out_ga(x1, x2)  =  reverseA_out_ga(x1, x2)
REVERSEA_IN_GA(x1, x2)  =  REVERSEA_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)
REVERSEC_IN_GA(x1, x2)  =  REVERSEC_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(.(T91, T92), T93, .(T91, T95)) → APPF_IN_GGA(T92, T93, T95)

The TRS R consists of the following rules:

reverseA_in_ga(.(T6, .(T18, T19)), T9) → U1_ga(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
pB_in_gagaga(T19, T22, T18, X30, T6, T9) → U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
reverseC_in_ga(.(T33, T34), X63) → U2_ga(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
pD_in_gaga(T34, T37, T33, X63) → U9_gaga(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
reverseC_in_ga([], []) → reverseC_out_ga([], [])
U9_gaga(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_gaga(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
appE_in_gga(.(T55, T56), T57, .(T55, X103)) → U3_gga(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
appE_in_gga([], T63, .(T63, [])) → appE_out_gga([], T63, .(T63, []))
U3_gga(T55, T56, T57, X103, appE_out_gga(T56, T57, X103)) → appE_out_gga(.(T55, T56), T57, .(T55, X103))
U10_gaga(T34, T37, T33, X63, appE_out_gga(T37, T33, X63)) → pD_out_gaga(T34, T37, T33, X63)
U2_ga(T33, T34, X63, pD_out_gaga(T34, X62, T33, X63)) → reverseC_out_ga(.(T33, T34), X63)
U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_gagaga(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
pG_in_ggaga(T22, T18, T67, T6, T9) → U7_ggaga(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
U7_ggaga(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_ggaga(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
appF_in_gga(.(T91, T92), T93, .(T91, T95)) → U4_gga(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
appF_in_gga([], T102, .(T102, [])) → appF_out_gga([], T102, .(T102, []))
U4_gga(T91, T92, T93, T95, appF_out_gga(T92, T93, T95)) → appF_out_gga(.(T91, T92), T93, .(T91, T95))
U8_ggaga(T22, T18, T67, T6, T9, appF_out_gga(T67, T6, T9)) → pG_out_ggaga(T22, T18, T67, T6, T9)
U6_gagaga(T19, T22, T18, X30, T6, T9, pG_out_ggaga(T22, T18, X30, T6, T9)) → pB_out_gagaga(T19, T22, T18, X30, T6, T9)
U1_ga(T6, T18, T19, T9, pB_out_gagaga(T19, X29, T18, X30, T6, T9)) → reverseA_out_ga(.(T6, .(T18, T19)), T9)
reverseA_in_ga(.(T105, []), .(T105, [])) → reverseA_out_ga(.(T105, []), .(T105, []))
reverseA_in_ga([], []) → reverseA_out_ga([], [])

The argument filtering Pi contains the following mapping:
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
.(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)
reverseC_in_ga(x1, x2)  =  reverseC_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)
[]  =  []
reverseC_out_ga(x1, x2)  =  reverseC_out_ga(x1, x2)
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)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
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)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
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)
reverseA_out_ga(x1, x2)  =  reverseA_out_ga(x1, x2)
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(.(T91, T92), T93, .(T91, T95)) → APPF_IN_GGA(T92, T93, T95)

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(.(T91, T92), T93) → APPF_IN_GGA(T92, T93)

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(.(T91, T92), T93) → APPF_IN_GGA(T92, T93)
  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(.(T55, T56), T57, .(T55, X103)) → APPE_IN_GGA(T56, T57, X103)

The TRS R consists of the following rules:

reverseA_in_ga(.(T6, .(T18, T19)), T9) → U1_ga(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
pB_in_gagaga(T19, T22, T18, X30, T6, T9) → U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
reverseC_in_ga(.(T33, T34), X63) → U2_ga(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
pD_in_gaga(T34, T37, T33, X63) → U9_gaga(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
reverseC_in_ga([], []) → reverseC_out_ga([], [])
U9_gaga(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_gaga(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
appE_in_gga(.(T55, T56), T57, .(T55, X103)) → U3_gga(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
appE_in_gga([], T63, .(T63, [])) → appE_out_gga([], T63, .(T63, []))
U3_gga(T55, T56, T57, X103, appE_out_gga(T56, T57, X103)) → appE_out_gga(.(T55, T56), T57, .(T55, X103))
U10_gaga(T34, T37, T33, X63, appE_out_gga(T37, T33, X63)) → pD_out_gaga(T34, T37, T33, X63)
U2_ga(T33, T34, X63, pD_out_gaga(T34, X62, T33, X63)) → reverseC_out_ga(.(T33, T34), X63)
U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_gagaga(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
pG_in_ggaga(T22, T18, T67, T6, T9) → U7_ggaga(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
U7_ggaga(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_ggaga(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
appF_in_gga(.(T91, T92), T93, .(T91, T95)) → U4_gga(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
appF_in_gga([], T102, .(T102, [])) → appF_out_gga([], T102, .(T102, []))
U4_gga(T91, T92, T93, T95, appF_out_gga(T92, T93, T95)) → appF_out_gga(.(T91, T92), T93, .(T91, T95))
U8_ggaga(T22, T18, T67, T6, T9, appF_out_gga(T67, T6, T9)) → pG_out_ggaga(T22, T18, T67, T6, T9)
U6_gagaga(T19, T22, T18, X30, T6, T9, pG_out_ggaga(T22, T18, X30, T6, T9)) → pB_out_gagaga(T19, T22, T18, X30, T6, T9)
U1_ga(T6, T18, T19, T9, pB_out_gagaga(T19, X29, T18, X30, T6, T9)) → reverseA_out_ga(.(T6, .(T18, T19)), T9)
reverseA_in_ga(.(T105, []), .(T105, [])) → reverseA_out_ga(.(T105, []), .(T105, []))
reverseA_in_ga([], []) → reverseA_out_ga([], [])

The argument filtering Pi contains the following mapping:
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
.(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)
reverseC_in_ga(x1, x2)  =  reverseC_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)
[]  =  []
reverseC_out_ga(x1, x2)  =  reverseC_out_ga(x1, x2)
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)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
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)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
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)
reverseA_out_ga(x1, x2)  =  reverseA_out_ga(x1, x2)
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(.(T55, T56), T57, .(T55, X103)) → APPE_IN_GGA(T56, T57, X103)

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(.(T55, T56), T57) → APPE_IN_GGA(T56, T57)

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(.(T55, T56), T57) → APPE_IN_GGA(T56, T57)
  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:

REVERSEC_IN_GA(.(T33, T34), X63) → PD_IN_GAGA(T34, X62, T33, X63)
PD_IN_GAGA(T34, T37, T33, X63) → REVERSEC_IN_GA(T34, T37)

The TRS R consists of the following rules:

reverseA_in_ga(.(T6, .(T18, T19)), T9) → U1_ga(T6, T18, T19, T9, pB_in_gagaga(T19, X29, T18, X30, T6, T9))
pB_in_gagaga(T19, T22, T18, X30, T6, T9) → U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_in_ga(T19, T22))
reverseC_in_ga(.(T33, T34), X63) → U2_ga(T33, T34, X63, pD_in_gaga(T34, X62, T33, X63))
pD_in_gaga(T34, T37, T33, X63) → U9_gaga(T34, T37, T33, X63, reverseC_in_ga(T34, T37))
reverseC_in_ga([], []) → reverseC_out_ga([], [])
U9_gaga(T34, T37, T33, X63, reverseC_out_ga(T34, T37)) → U10_gaga(T34, T37, T33, X63, appE_in_gga(T37, T33, X63))
appE_in_gga(.(T55, T56), T57, .(T55, X103)) → U3_gga(T55, T56, T57, X103, appE_in_gga(T56, T57, X103))
appE_in_gga([], T63, .(T63, [])) → appE_out_gga([], T63, .(T63, []))
U3_gga(T55, T56, T57, X103, appE_out_gga(T56, T57, X103)) → appE_out_gga(.(T55, T56), T57, .(T55, X103))
U10_gaga(T34, T37, T33, X63, appE_out_gga(T37, T33, X63)) → pD_out_gaga(T34, T37, T33, X63)
U2_ga(T33, T34, X63, pD_out_gaga(T34, X62, T33, X63)) → reverseC_out_ga(.(T33, T34), X63)
U5_gagaga(T19, T22, T18, X30, T6, T9, reverseC_out_ga(T19, T22)) → U6_gagaga(T19, T22, T18, X30, T6, T9, pG_in_ggaga(T22, T18, X30, T6, T9))
pG_in_ggaga(T22, T18, T67, T6, T9) → U7_ggaga(T22, T18, T67, T6, T9, appE_in_gga(T22, T18, T67))
U7_ggaga(T22, T18, T67, T6, T9, appE_out_gga(T22, T18, T67)) → U8_ggaga(T22, T18, T67, T6, T9, appF_in_gga(T67, T6, T9))
appF_in_gga(.(T91, T92), T93, .(T91, T95)) → U4_gga(T91, T92, T93, T95, appF_in_gga(T92, T93, T95))
appF_in_gga([], T102, .(T102, [])) → appF_out_gga([], T102, .(T102, []))
U4_gga(T91, T92, T93, T95, appF_out_gga(T92, T93, T95)) → appF_out_gga(.(T91, T92), T93, .(T91, T95))
U8_ggaga(T22, T18, T67, T6, T9, appF_out_gga(T67, T6, T9)) → pG_out_ggaga(T22, T18, T67, T6, T9)
U6_gagaga(T19, T22, T18, X30, T6, T9, pG_out_ggaga(T22, T18, X30, T6, T9)) → pB_out_gagaga(T19, T22, T18, X30, T6, T9)
U1_ga(T6, T18, T19, T9, pB_out_gagaga(T19, X29, T18, X30, T6, T9)) → reverseA_out_ga(.(T6, .(T18, T19)), T9)
reverseA_in_ga(.(T105, []), .(T105, [])) → reverseA_out_ga(.(T105, []), .(T105, []))
reverseA_in_ga([], []) → reverseA_out_ga([], [])

The argument filtering Pi contains the following mapping:
reverseA_in_ga(x1, x2)  =  reverseA_in_ga(x1)
.(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)
reverseC_in_ga(x1, x2)  =  reverseC_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)
[]  =  []
reverseC_out_ga(x1, x2)  =  reverseC_out_ga(x1, x2)
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)
appE_out_gga(x1, x2, x3)  =  appE_out_gga(x1, x2, x3)
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)
U4_gga(x1, x2, x3, x4, x5)  =  U4_gga(x1, x2, x3, x5)
appF_out_gga(x1, x2, x3)  =  appF_out_gga(x1, x2, x3)
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)
reverseA_out_ga(x1, x2)  =  reverseA_out_ga(x1, x2)
REVERSEC_IN_GA(x1, x2)  =  REVERSEC_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:

REVERSEC_IN_GA(.(T33, T34), X63) → PD_IN_GAGA(T34, X62, T33, X63)
PD_IN_GAGA(T34, T37, T33, X63) → REVERSEC_IN_GA(T34, T37)

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

REVERSEC_IN_GA(.(T33, T34)) → PD_IN_GAGA(T34, T33)
PD_IN_GAGA(T34, T33) → REVERSEC_IN_GA(T34)

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(T34, T33) → REVERSEC_IN_GA(T34)
  The graph contains the following edges 1 >= 1

• REVERSEC_IN_GA(.(T33, T34)) → PD_IN_GAGA(T34, T33)
  The graph contains the following edges 1 > 1, 1 > 2

(27) YES