Left Termination proof of /tmp/tmp3XT3Ca/permutation.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 158 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 79 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 7 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 0 ms)

        ↳11 QDP

        ↳12 QDPSizeChangeProof (⇔, 0 ms)

        ↳13 YES

    ↳14 PiDP

        ↳15 UsableRulesProof (⇔, 0 ms)

        ↳16 PiDP

        ↳17 PiDPToQDPProof (⇒, 0 ms)

        ↳18 QDP

        ↳19 QDPSizeChangeProof (⇔, 0 ms)

        ↳20 YES

    ↳21 PiDP

        ↳22 UsableRulesProof (⇔, 0 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 0 ms)

        ↳25 QDP

        ↳26 Rewriting (⇔, 0 ms)

        ↳27 QDP

        ↳28 UsableRulesProof (⇔, 0 ms)

        ↳29 QDP

        ↳30 QReductionProof (⇔, 0 ms)

        ↳31 QDP

        ↳32 Rewriting (⇔, 0 ms)

        ↳33 QDP

        ↳34 UsableRulesProof (⇔, 0 ms)

        ↳35 QDP

        ↳36 QReductionProof (⇔, 11 ms)

        ↳37 QDP

        ↳38 Instantiation (⇔, 0 ms)

        ↳39 QDP

        ↳40 QDPOrderProof (⇔, 127 ms)

        ↳41 QDP

        ↳42 DependencyGraphProof (⇔, 0 ms)

        ↳43 TRUE

(0) Obligation:

Clauses:

app1(.(X0, X), Y, .(X0, Z)) :- app1(X, Y, Z).
app1([], Y, Y).
app2(.(X0, X), Y, .(X0, Z)) :- app2(X, Y, Z).
app2([], Y, Y).
perm(X, .(X0, Y)) :- ','(app1(X1, .(X0, X2), X), ','(app2(X1, X2, Z), perm(Z, Y))).
perm([], []).

Query: perm(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: perm(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: perm(T1, T2), SCOPE: 1, CLAUSE: 4 | perm(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(app1(X9, .(T9, X10), T6), ','(app2(X9, X10, X11), perm(X11, T10))) | perm(T6, T2), SCOPE: 1, CLAUSE: 5\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: perm(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nX6 is free\nX7 is free\nX8 is free\nperm(T1, T2) !=? perm(X6, .(X7, X8))", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: ','(app1(X9, .(T9, X10), T6), ','(app2(X9, X10, X11), perm(X11, T10))), SCOPE: 2, CLAUSE: 0 | ','(app1(X9, .(T9, X10), T6), ','(app2(X9, X10, X11), perm(X11, T10))), SCOPE: 2, CLAUSE: 1 | ?_2 | perm(T6, T2), SCOPE: 1, CLAUSE: 5\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: ','(app1(X9, .(T9, X10), T6), ','(app2(X9, X10, X11), perm(X11, T10))), SCOPE: 2, CLAUSE: 0\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: ','(app1(X9, .(T9, X10), T6), ','(app2(X9, X10, X11), perm(X11, T10))), SCOPE: 2, CLAUSE: 1 | ?_2 | perm(T6, T2), SCOPE: 1, CLAUSE: 5\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="B: ','(app1(X45, .(T26, X46), T25), ','(app2(.(T24, X45), X46, X11), perm(X11, T27)))\n\nT24 is ground\nT25 is ground\nX11 is free\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="D: app1(X45, .(T26, X46), T25)\n\nT25 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="H: ','(app2(.(T24, T31), T32, X11), perm(X11, T33))\n\nT24 is ground\nT31 is ground\nT32 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: app1(X45, .(T26, X46), T25), SCOPE: 3, CLAUSE: 0 | app1(X45, .(T26, X46), T25), SCOPE: 3, CLAUSE: 1\n\nT25 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
56 [label="56: app1(X45, .(T26, X46), T25), SCOPE: 3, CLAUSE: 0\n\nT25 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
57 [label="57: app1(X45, .(T26, X46), T25), SCOPE: 3, CLAUSE: 1\n\nT25 is ground\nX45 is free\nX46 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: app1(X94, .(T52, X95), T51)\n\nT51 is ground\nX94 is free\nX95 is free", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="F: app2(.(T24, T31), T32, X11)\n\nT24 is ground\nT31 is ground\nT32 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: perm(T65, T33)\n\nT65 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: app2(.(T24, T31), T32, X11), SCOPE: 4, CLAUSE: 2 | app2(.(T24, T31), T32, X11), SCOPE: 4, CLAUSE: 3\n\nT24 is ground\nT31 is ground\nT32 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: app2(.(T24, T31), T32, X11), SCOPE: 4, CLAUSE: 2\n\nT24 is ground\nT31 is ground\nT32 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="97: app2(.(T24, T31), T32, X11), SCOPE: 4, CLAUSE: 3\n\nT24 is ground\nT31 is ground\nT32 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="E: app2(T88, T89, X153)\n\nT88 is ground\nT89 is ground\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: app2(T88, T89, X153), SCOPE: 5, CLAUSE: 2 | app2(T88, T89, X153), SCOPE: 5, CLAUSE: 3\n\nT88 is ground\nT89 is ground\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: app2(T88, T89, X153), SCOPE: 5, CLAUSE: 2\n\nT88 is ground\nT89 is ground\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: app2(T88, T89, X153), SCOPE: 5, CLAUSE: 3\n\nT88 is ground\nT89 is ground\nX153 is free", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: app2(T106, T107, X183)\n\nT106 is ground\nT107 is ground\nX183 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="115: ','(app1(X9, .(T9, X10), T6), ','(app2(X9, X10, X11), perm(X11, T10))), SCOPE: 2, CLAUSE: 1\n\nT6 is ground\nX9 is free\nX10 is free\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: ?_2 | perm(T6, T2), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="C: ','(app2([], T126, X11), perm(X11, T127))\n\nT126 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="G: app2([], T126, X11)\n\nT126 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: perm(T128, T127)\n\nT128 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: app2([], T126, X11), SCOPE: 6, CLAUSE: 2 | app2([], T126, X11), SCOPE: 6, CLAUSE: 3\n\nT126 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: app2([], T126, X11), SCOPE: 6, CLAUSE: 3\n\nT126 is ground\nX11 is free", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: perm(T6, T2), SCOPE: 1, CLAUSE: 5\n\nT6 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: \n\n", 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\nperm(X6, .(X7, X8)) :- ','(app1(X9, .(X7, X10), X6), ','(app2(X9, X10, X11), perm(X11, X8))).\nand substitutionT1 -> T6,\nX6 -> T6,\nX7 -> T9,\nX8 -> T10,\nT2 -> .(T9, T10),\nT7 -> T9,\nT8 -> T10", fontsize=14, style = filled, fillcolor = lightblue];
4 -> 133 [arrowhead = none ];
133 -> 10;

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

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

136 [label="EVAL with clause\nperm([], []).\nand substitutionT1 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 136 [arrowhead = none ];
136 -> 129;

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

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

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

140 [label="EVAL with clause\napp1(.(X40, X41), X42, .(X40, X43)) :- app1(X41, X42, X43).\nand substitutionX40 -> T24,\nX41 -> X45,\nX9 -> .(T24, X45),\nT9 -> T26,\nX10 -> X46,\nX42 -> .(T26, X46),\nX44 -> T24,\nX43 -> T25,\nT6 -> .(T24, T25),\nT23 -> T26,\nT10 -> T27", fontsize=14, style = filled, fillcolor = lightblue];
19 -> 140 [arrowhead = none ];
140 -> 34;

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

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

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

144 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
34 -> 144 [arrowhead = none ];
144 -> 38;

145 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT26 is ground\nT32 is ground\nT25 is ground\nreplacements:X45 -> T31,\nX46 -> T32,\nT27 -> T33", fontsize=14, style = filled, fillcolor = violet];
34 -> 145 [arrowhead = none ];
145 -> 39;

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

147 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
39 -> 147 [arrowhead = none ];
147 -> 87;

148 [label="SPLIT 2\nnew knowledge:\nT24 is ground\nT31 is ground\nT32 is ground\nT65 is ground\nreplacements:X11 -> T65", fontsize=14, style = filled, fillcolor = violet];
39 -> 148 [arrowhead = none ];
148 -> 88;

149 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
41 -> 149 [arrowhead = none ];
149 -> 56;

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

151 [label="EVAL with clause\napp1(.(X89, X90), X91, .(X89, X92)) :- app1(X90, X91, X92).\nand substitutionX89 -> T50,\nX90 -> X94,\nX45 -> .(T50, X94),\nT26 -> T52,\nX46 -> X95,\nX91 -> .(T52, X95),\nX93 -> T50,\nX92 -> T51,\nT25 -> .(T50, T51),\nT49 -> T52", fontsize=14, style = filled, fillcolor = lightblue];
56 -> 151 [arrowhead = none ];
151 -> 72;

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

153 [label="EVAL with clause\napp1([], X107, X107).\nand substitutionX45 -> [],\nT26 -> T60,\nX46 -> T61,\nX107 -> .(T60, T61),\nX108 -> T61,\nT25 -> .(T60, T61)", fontsize=14, style = filled, fillcolor = lightblue];
57 -> 153 [arrowhead = none ];
153 -> 76;

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

155 [label="INSTANCE with matching:\nX45 -> X94\nT26 -> T52\nX46 -> X95\nT25 -> T51", fontsize=14, style = filled, fillcolor = lightgrey];
72 -> 155 [arrowhead = none , style=dashed];
155 -> 38[style=dashed];

156 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
76 -> 156 [arrowhead = none ];
156 -> 78;

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

158 [label="INSTANCE with matching:\nT1 -> T65\nT2 -> T33", fontsize=14, style = filled, fillcolor = lightgrey];
88 -> 158 [arrowhead = none , style=dashed];
158 -> 1[style=dashed];

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

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

161 [label="ONLY EVAL with clause\napp2(.(X149, X150), X151, .(X149, X152)) :- app2(X150, X151, X152).\nand substitutionT24 -> T87,\nX149 -> T87,\nT31 -> T88,\nX150 -> T88,\nT32 -> T89,\nX151 -> T89,\nX152 -> X153,\nX11 -> .(T87, X153)", fontsize=14, style = filled, fillcolor = lightblue];
95 -> 161 [arrowhead = none ];
161 -> 105;

162 [label="BACKTRACK\nfor clause: app2([], Y, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
97 -> 162 [arrowhead = none ];
162 -> 114;

163 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
105 -> 163 [arrowhead = none ];
163 -> 106;

164 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 164 [arrowhead = none ];
164 -> 107;

165 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
106 -> 165 [arrowhead = none ];
165 -> 108;

166 [label="EVAL with clause\napp2(.(X179, X180), X181, .(X179, X182)) :- app2(X180, X181, X182).\nand substitutionX179 -> T105,\nX180 -> T106,\nT88 -> .(T105, T106),\nT89 -> T107,\nX181 -> T107,\nX182 -> X183,\nX153 -> .(T105, X183)", fontsize=14, style = filled, fillcolor = lightblue];
107 -> 166 [arrowhead = none ];
166 -> 109;

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

168 [label="EVAL with clause\napp2([], X191, X191).\nand substitutionT88 -> [],\nT89 -> T113,\nX191 -> T113,\nX153 -> T113", fontsize=14, style = filled, fillcolor = lightblue];
108 -> 168 [arrowhead = none ];
168 -> 111;

169 [label="EVAL-BACKTRACK", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 169 [arrowhead = none ];
169 -> 112;

170 [label="INSTANCE with matching:\nT88 -> T106\nT89 -> T107\nX153 -> X183", fontsize=14, style = filled, fillcolor = lightgrey];
109 -> 170 [arrowhead = none , style=dashed];
170 -> 105[style=dashed];

171 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
111 -> 171 [arrowhead = none ];
171 -> 113;

172 [label="EVAL with clause\napp1([], X207, X207).\nand substitutionX9 -> [],\nT9 -> T125,\nX10 -> T126,\nX207 -> .(T125, T126),\nX208 -> T126,\nT6 -> .(T125, T126),\nT10 -> T127", fontsize=14, style = filled, fillcolor = lightblue];
115 -> 172 [arrowhead = none ];
172 -> 117;

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

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

175 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
117 -> 175 [arrowhead = none ];
175 -> 119;

176 [label="SPLIT 2\nnew knowledge:\nT126 is ground\nT128 is ground\nreplacements:X11 -> T128", fontsize=14, style = filled, fillcolor = violet];
117 -> 176 [arrowhead = none ];
176 -> 120;

177 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
119 -> 177 [arrowhead = none ];
177 -> 121;

178 [label="INSTANCE with matching:\nT1 -> T128\nT2 -> T127", fontsize=14, style = filled, fillcolor = lightgrey];
120 -> 178 [arrowhead = none , style=dashed];
178 -> 1[style=dashed];

179 [label="BACKTRACK\nfor clause: app2(.(X0, X), Y, .(X0, Z)) :- app2(X, Y, Z)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 179 [arrowhead = none ];
179 -> 122;

180 [label="ONLY EVAL with clause\napp2([], X223, X223).\nand substitutionT126 -> T131,\nX223 -> T131,\nX11 -> T131", fontsize=14, style = filled, fillcolor = lightblue];
122 -> 180 [arrowhead = none ];
180 -> 123;

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

182 [label="EVAL with clause\nperm([], []).\nand substitutionT6 -> [],\nT2 -> []", fontsize=14, style = filled, fillcolor = lightblue];
125 -> 182 [arrowhead = none ];
182 -> 126;

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

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

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

}

(2) Obligation:

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

permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X11, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U8_gggaa(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X11, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app2G_in_ga(T126, T128))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X11, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_out_gggaa(T24, T31, T32, X11, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X11, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X45, T26, X46, T25, T24, X11, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))

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

PERMA_IN_GA(.(T24, T25), .(T26, T27)) → U1_GA(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X45, T26, X46, T25, T24, X11, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X11, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X11, T33) → APP1D_IN_AAAG(T31, T26, T32, T25)
APP1D_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → U3_AAAG(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
APP1D_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1D_IN_AAAG(X94, T52, X95, T51)
U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X11, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
PH_IN_GGGAA(T24, T31, T32, T65, T33) → APP2F_IN_GGGA(T24, T31, T32, T65)
APP2F_IN_GGGA(T87, T88, T89, .(T87, X153)) → U5_GGGA(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
APP2F_IN_GGGA(T87, T88, T89, .(T87, X153)) → APP2E_IN_GGA(T88, T89, X153)
APP2E_IN_GGA(.(T105, T106), T107, .(T105, X183)) → U4_GGA(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
APP2E_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2E_IN_GGA(T106, T107, X183)
U8_GGGAA(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_GGGAA(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
U8_GGGAA(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → U2_GA(T125, T126, T127, pC_in_gaa(T126, X11, T127))
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X11, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app2G_in_ga(T126, T128))
PC_IN_GAA(T126, T128, T127) → APP2G_IN_GA(T126, T128)
U10_GAA(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_GAA(T126, T128, T127, permA_in_ga(T128, T127))
U10_GAA(T126, T128, T127, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)

The TRS R consists of the following rules:

permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X11, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U8_gggaa(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X11, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app2G_in_ga(T126, T128))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X11, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_out_gggaa(T24, T31, T32, X11, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X11, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X45, T26, X46, T25, T24, X11, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2) = permA_in_ga(x1)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x5)
pB_in_aaaggaa(x1, x2, x3, x4, x5, x6, x7) = pB_in_aaaggaa(x4, x5)
U6_aaaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U6_aaaggaa(x4, x5, x8)
app1D_in_aaag(x1, x2, x3, x4) = app1D_in_aaag(x4)
U3_aaag(x1, x2, x3, x4, x5, x6) = U3_aaag(x1, x5, x6)
app1D_out_aaag(x1, x2, x3, x4) = app1D_out_aaag(x1, x2, x3, x4)
U7_aaaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U7_aaaggaa(x1, x2, x3, x4, x5, x8)
pH_in_gggaa(x1, x2, x3, x4, x5) = pH_in_gggaa(x1, x2, x3)
U8_gggaa(x1, x2, x3, x4, x5, x6) = U8_gggaa(x1, x2, x3, x6)
app2F_in_ggga(x1, x2, x3, x4) = app2F_in_ggga(x1, x2, x3)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
app2E_in_gga(x1, x2, x3) = app2E_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
[] = []
app2E_out_gga(x1, x2, x3) = app2E_out_gga(x1, x2, x3)
app2F_out_ggga(x1, x2, x3, x4) = app2F_out_ggga(x1, x2, x3, x4)
U9_gggaa(x1, x2, x3, x4, x5, x6) = U9_gggaa(x1, x2, x3, x4, x6)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
app2G_in_ga(x1, x2) = app2G_in_ga(x1)
app2G_out_ga(x1, x2) = app2G_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
permA_out_ga(x1, x2) = permA_out_ga(x1, x2)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pH_out_gggaa(x1, x2, x3, x4, x5) = pH_out_gggaa(x1, x2, x3, x4, x5)
pB_out_aaaggaa(x1, x2, x3, x4, x5, x6, x7) = pB_out_aaaggaa(x1, x2, x3, x4, x5, x6, x7)
PERMA_IN_GA(x1, x2) = PERMA_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5) = U1_GA(x1, x2, x5)
PB_IN_AAAGGAA(x1, x2, x3, x4, x5, x6, x7) = PB_IN_AAAGGAA(x4, x5)
U6_AAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U6_AAAGGAA(x4, x5, x8)
APP1D_IN_AAAG(x1, x2, x3, x4) = APP1D_IN_AAAG(x4)
U3_AAAG(x1, x2, x3, x4, x5, x6) = U3_AAAG(x1, x5, x6)
U7_AAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U7_AAAGGAA(x1, x2, x3, x4, x5, x8)
PH_IN_GGGAA(x1, x2, x3, x4, x5) = PH_IN_GGGAA(x1, x2, x3)
U8_GGGAA(x1, x2, x3, x4, x5, x6) = U8_GGGAA(x1, x2, x3, x6)
APP2F_IN_GGGA(x1, x2, x3, x4) = APP2F_IN_GGGA(x1, x2, x3)
U5_GGGA(x1, x2, x3, x4, x5) = U5_GGGA(x1, x2, x3, x5)
APP2E_IN_GGA(x1, x2, x3) = APP2E_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5) = U4_GGA(x1, x2, x3, x5)
U9_GGGAA(x1, x2, x3, x4, x5, x6) = U9_GGGAA(x1, x2, x3, x4, x6)
U2_GA(x1, x2, x3, x4) = U2_GA(x1, x2, x4)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)
APP2G_IN_GA(x1, x2) = APP2G_IN_GA(x1)
U11_GAA(x1, x2, x3, x4) = U11_GAA(x1, x2, x4)

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

(4) Obligation:

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

PERMA_IN_GA(.(T24, T25), .(T26, T27)) → U1_GA(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X45, T26, X46, T25, T24, X11, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X11, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X11, T33) → APP1D_IN_AAAG(T31, T26, T32, T25)
APP1D_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → U3_AAAG(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
APP1D_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1D_IN_AAAG(X94, T52, X95, T51)
U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X11, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
PH_IN_GGGAA(T24, T31, T32, T65, T33) → APP2F_IN_GGGA(T24, T31, T32, T65)
APP2F_IN_GGGA(T87, T88, T89, .(T87, X153)) → U5_GGGA(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
APP2F_IN_GGGA(T87, T88, T89, .(T87, X153)) → APP2E_IN_GGA(T88, T89, X153)
APP2E_IN_GGA(.(T105, T106), T107, .(T105, X183)) → U4_GGA(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
APP2E_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2E_IN_GGA(T106, T107, X183)
U8_GGGAA(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_GGGAA(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
U8_GGGAA(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → U2_GA(T125, T126, T127, pC_in_gaa(T126, X11, T127))
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X11, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app2G_in_ga(T126, T128))
PC_IN_GAA(T126, T128, T127) → APP2G_IN_GA(T126, T128)
U10_GAA(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_GAA(T126, T128, T127, permA_in_ga(T128, T127))
U10_GAA(T126, T128, T127, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)

The TRS R consists of the following rules:

permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X11, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U8_gggaa(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X11, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app2G_in_ga(T126, T128))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X11, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_out_gggaa(T24, T31, T32, X11, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X11, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X45, T26, X46, T25, T24, X11, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APP2E_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2E_IN_GGA(T106, T107, X183)

The TRS R consists of the following rules:

permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X11, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U8_gggaa(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X11, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app2G_in_ga(T126, T128))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X11, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_out_gggaa(T24, T31, T32, X11, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X11, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X45, T26, X46, T25, T24, X11, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))

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

APP2E_IN_GGA(.(T105, T106), T107, .(T105, X183)) → APP2E_IN_GGA(T106, T107, X183)

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

APP2E_IN_GGA(.(T105, T106), T107) → APP2E_IN_GGA(T106, T107)

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:

APP2E_IN_GGA(.(T105, T106), T107) → APP2E_IN_GGA(T106, T107)
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:

APP1D_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1D_IN_AAAG(X94, T52, X95, T51)

The TRS R consists of the following rules:

permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X11, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U8_gggaa(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X11, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app2G_in_ga(T126, T128))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X11, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_out_gggaa(T24, T31, T32, X11, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X11, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X45, T26, X46, T25, T24, X11, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))

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

APP1D_IN_AAAG(.(T50, X94), T52, X95, .(T50, T51)) → APP1D_IN_AAAG(X94, T52, X95, T51)

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

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:

APP1D_IN_AAAG(.(T50, T51)) → APP1D_IN_AAAG(T51)

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:

APP1D_IN_AAAG(.(T50, T51)) → APP1D_IN_AAAG(T51)
The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X45, T26, X46, T25, T24, X11, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X11, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X11, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
U8_GGGAA(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X11, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app2G_in_ga(T126, T128))
U10_GAA(T126, T128, T127, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)

The TRS R consists of the following rules:

permA_in_ga(.(T24, T25), .(T26, T27)) → U1_ga(T24, T25, T26, T27, pB_in_aaaggaa(X45, T26, X46, T25, T24, X11, T27))
pB_in_aaaggaa(T31, T26, T32, T25, T24, X11, T33) → U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U6_aaaggaa(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_in_gggaa(T24, T31, T32, X11, T33))
pH_in_gggaa(T24, T31, T32, T65, T33) → U8_gggaa(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U8_gggaa(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → U9_gggaa(T24, T31, T32, T65, T33, permA_in_ga(T65, T33))
permA_in_ga(.(T125, T126), .(T125, T127)) → U2_ga(T125, T126, T127, pC_in_gaa(T126, X11, T127))
pC_in_gaa(T126, T128, T127) → U10_gaa(T126, T128, T127, app2G_in_ga(T126, T128))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U10_gaa(T126, T128, T127, app2G_out_ga(T126, T128)) → U11_gaa(T126, T128, T127, permA_in_ga(T128, T127))
permA_in_ga([], []) → permA_out_ga([], [])
U11_gaa(T126, T128, T127, permA_out_ga(T128, T127)) → pC_out_gaa(T126, T128, T127)
U2_ga(T125, T126, T127, pC_out_gaa(T126, X11, T127)) → permA_out_ga(.(T125, T126), .(T125, T127))
U9_gggaa(T24, T31, T32, T65, T33, permA_out_ga(T65, T33)) → pH_out_gggaa(T24, T31, T32, T65, T33)
U7_aaaggaa(T31, T26, T32, T25, T24, X11, T33, pH_out_gggaa(T24, T31, T32, X11, T33)) → pB_out_aaaggaa(T31, T26, T32, T25, T24, X11, T33)
U1_ga(T24, T25, T26, T27, pB_out_aaaggaa(X45, T26, X46, T25, T24, X11, T27)) → permA_out_ga(.(T24, T25), .(T26, T27))

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2) = permA_in_ga(x1)
.(x1, x2) = .(x1, x2)
U1_ga(x1, x2, x3, x4, x5) = U1_ga(x1, x2, x5)
pB_in_aaaggaa(x1, x2, x3, x4, x5, x6, x7) = pB_in_aaaggaa(x4, x5)
U6_aaaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U6_aaaggaa(x4, x5, x8)
app1D_in_aaag(x1, x2, x3, x4) = app1D_in_aaag(x4)
U3_aaag(x1, x2, x3, x4, x5, x6) = U3_aaag(x1, x5, x6)
app1D_out_aaag(x1, x2, x3, x4) = app1D_out_aaag(x1, x2, x3, x4)
U7_aaaggaa(x1, x2, x3, x4, x5, x6, x7, x8) = U7_aaaggaa(x1, x2, x3, x4, x5, x8)
pH_in_gggaa(x1, x2, x3, x4, x5) = pH_in_gggaa(x1, x2, x3)
U8_gggaa(x1, x2, x3, x4, x5, x6) = U8_gggaa(x1, x2, x3, x6)
app2F_in_ggga(x1, x2, x3, x4) = app2F_in_ggga(x1, x2, x3)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
app2E_in_gga(x1, x2, x3) = app2E_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
[] = []
app2E_out_gga(x1, x2, x3) = app2E_out_gga(x1, x2, x3)
app2F_out_ggga(x1, x2, x3, x4) = app2F_out_ggga(x1, x2, x3, x4)
U9_gggaa(x1, x2, x3, x4, x5, x6) = U9_gggaa(x1, x2, x3, x4, x6)
U2_ga(x1, x2, x3, x4) = U2_ga(x1, x2, x4)
pC_in_gaa(x1, x2, x3) = pC_in_gaa(x1)
U10_gaa(x1, x2, x3, x4) = U10_gaa(x1, x4)
app2G_in_ga(x1, x2) = app2G_in_ga(x1)
app2G_out_ga(x1, x2) = app2G_out_ga(x1, x2)
U11_gaa(x1, x2, x3, x4) = U11_gaa(x1, x2, x4)
permA_out_ga(x1, x2) = permA_out_ga(x1, x2)
pC_out_gaa(x1, x2, x3) = pC_out_gaa(x1, x2, x3)
pH_out_gggaa(x1, x2, x3, x4, x5) = pH_out_gggaa(x1, x2, x3, x4, x5)
pB_out_aaaggaa(x1, x2, x3, x4, x5, x6, x7) = pB_out_aaaggaa(x1, x2, x3, x4, x5, x6, x7)
PERMA_IN_GA(x1, x2) = PERMA_IN_GA(x1)
PB_IN_AAAGGAA(x1, x2, x3, x4, x5, x6, x7) = PB_IN_AAAGGAA(x4, x5)
U6_AAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U6_AAAGGAA(x4, x5, x8)
PH_IN_GGGAA(x1, x2, x3, x4, x5) = PH_IN_GGGAA(x1, x2, x3)
U8_GGGAA(x1, x2, x3, x4, x5, x6) = U8_GGGAA(x1, x2, x3, x6)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)

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:

PERMA_IN_GA(.(T24, T25), .(T26, T27)) → PB_IN_AAAGGAA(X45, T26, X46, T25, T24, X11, T27)
PB_IN_AAAGGAA(T31, T26, T32, T25, T24, X11, T33) → U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_in_aaag(T31, T26, T32, T25))
U6_AAAGGAA(T31, T26, T32, T25, T24, X11, T33, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32, X11, T33)
PH_IN_GGGAA(T24, T31, T32, T65, T33) → U8_GGGAA(T24, T31, T32, T65, T33, app2F_in_ggga(T24, T31, T32, T65))
U8_GGGAA(T24, T31, T32, T65, T33, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65, T33)
PERMA_IN_GA(.(T125, T126), .(T125, T127)) → PC_IN_GAA(T126, X11, T127)
PC_IN_GAA(T126, T128, T127) → U10_GAA(T126, T128, T127, app2G_in_ga(T126, T128))
U10_GAA(T126, T128, T127, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128, T127)

The TRS R consists of the following rules:

app1D_in_aaag(.(T50, X94), T52, X95, .(T50, T51)) → U3_aaag(T50, X94, T52, X95, T51, app1D_in_aaag(X94, T52, X95, T51))
app1D_in_aaag([], T60, T61, .(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
app2F_in_ggga(T87, T88, T89, .(T87, X153)) → U5_ggga(T87, T88, T89, X153, app2E_in_gga(T88, T89, X153))
app2G_in_ga(T131, T131) → app2G_out_ga(T131, T131)
U3_aaag(T50, X94, T52, X95, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U5_ggga(T87, T88, T89, X153, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
app2E_in_gga(.(T105, T106), T107, .(T105, X183)) → U4_gga(T105, T106, T107, X183, app2E_in_gga(T106, T107, X183))
app2E_in_gga([], T113, T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, X183, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))

The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
app1D_in_aaag(x1, x2, x3, x4) = app1D_in_aaag(x4)
U3_aaag(x1, x2, x3, x4, x5, x6) = U3_aaag(x1, x5, x6)
app1D_out_aaag(x1, x2, x3, x4) = app1D_out_aaag(x1, x2, x3, x4)
app2F_in_ggga(x1, x2, x3, x4) = app2F_in_ggga(x1, x2, x3)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
app2E_in_gga(x1, x2, x3) = app2E_in_gga(x1, x2)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
[] = []
app2E_out_gga(x1, x2, x3) = app2E_out_gga(x1, x2, x3)
app2F_out_ggga(x1, x2, x3, x4) = app2F_out_ggga(x1, x2, x3, x4)
app2G_in_ga(x1, x2) = app2G_in_ga(x1)
app2G_out_ga(x1, x2) = app2G_out_ga(x1, x2)
PERMA_IN_GA(x1, x2) = PERMA_IN_GA(x1)
PB_IN_AAAGGAA(x1, x2, x3, x4, x5, x6, x7) = PB_IN_AAAGGAA(x4, x5)
U6_AAAGGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U6_AAAGGAA(x4, x5, x8)
PH_IN_GGGAA(x1, x2, x3, x4, x5) = PH_IN_GGGAA(x1, x2, x3)
U8_GGGAA(x1, x2, x3, x4, x5, x6) = U8_GGGAA(x1, x2, x3, x6)
PC_IN_GAA(x1, x2, x3) = PC_IN_GAA(x1)
U10_GAA(x1, x2, x3, x4) = U10_GAA(x1, x4)

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:

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, app2F_in_ggga(T24, T31, T32))
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app2G_in_ga(T126))
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)

The TRS R consists of the following rules:

app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
app2F_in_ggga(T87, T88, T89) → U5_ggga(T87, T88, T89, app2E_in_gga(T88, T89))
app2G_in_ga(T131) → app2G_out_ga(T131, T131)
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))

The set Q consists of the following terms:

app1D_in_aaag(x0)
app2F_in_ggga(x0, x1, x2)
app2G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(26) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, app2F_in_ggga(T24, T31, T32)) at position [3] we obtained the following new rules [LPAR04]:

PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))

(27) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app2G_in_ga(T126))
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))

The TRS R consists of the following rules:

app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
app2F_in_ggga(T87, T88, T89) → U5_ggga(T87, T88, T89, app2E_in_gga(T88, T89))
app2G_in_ga(T131) → app2G_out_ga(T131, T131)
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))

The set Q consists of the following terms:

app1D_in_aaag(x0)
app2F_in_ggga(x0, x1, x2)
app2G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(28) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(29) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app2G_in_ga(T126))
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app2G_in_ga(T131) → app2G_out_ga(T131, T131)
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
app2F_in_ggga(x0, x1, x2)
app2G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(30) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

app2F_in_ggga(x0, x1, x2)

(31) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PC_IN_GAA(T126) → U10_GAA(T126, app2G_in_ga(T126))
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app2G_in_ga(T131) → app2G_out_ga(T131, T131)
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
app2G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(32) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PC_IN_GAA(T126) → U10_GAA(T126, app2G_in_ga(T126)) at position [1] we obtained the following new rules [LPAR04]:

PC_IN_GAA(T126) → U10_GAA(T126, app2G_out_ga(T126, T126))

(33) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app2G_out_ga(T126, T126))

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app2G_in_ga(T131) → app2G_out_ga(T131, T131)
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
app2G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(34) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(35) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app2G_out_ga(T126, T126))

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
app2G_in_ga(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(36) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

app2G_in_ga(x0)

(37) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app2G_out_ga(T126, T126))

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(38) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U10_GAA(T126, app2G_out_ga(T126, T128)) → PERMA_IN_GA(T128) we obtained the following new rules [LPAR04]:

U10_GAA(z0, app2G_out_ga(z0, z0)) → PERMA_IN_GA(z0)

(39) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app2G_out_ga(T126, T126))
U10_GAA(z0, app2G_out_ga(z0, z0)) → PERMA_IN_GA(z0)

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(40) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04,JAR06].

The following pairs can be oriented strictly and are deleted.

PB_IN_AAAGGAA(T25, T24) → U6_AAAGGAA(T25, T24, app1D_in_aaag(T25))
U10_GAA(z0, app2G_out_ga(z0, z0)) → PERMA_IN_GA(z0)

The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x₁, x₂)) = 1 + x₂
POL(PB_IN_AAAGGAA(x₁, x₂)) = 1 + x₁
POL(PC_IN_GAA(x₁)) = 1 + x₁
POL(PERMA_IN_GA(x₁)) = x₁
POL(PH_IN_GGGAA(x₁, x₂, x₃)) = x₂ + x₃
POL(U10_GAA(x₁, x₂)) = x₂
POL(U3_aaag(x₁, x₂, x₃)) = 1 + x₃
POL(U4_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U5_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(U6_AAAGGAA(x₁, x₂, x₃)) = x₃
POL(U8_GGGAA(x₁, x₂, x₃, x₄)) = x₄
POL([]) = 1
POL(app1D_in_aaag(x₁)) = x₁
POL(app1D_out_aaag(x₁, x₂, x₃, x₄)) = x₁ + x₃
POL(app2E_in_gga(x₁, x₂)) = x₁ + x₂
POL(app2E_out_gga(x₁, x₂, x₃)) = 1 + x₃
POL(app2F_out_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(app2G_out_ga(x₁, x₂)) = 1 + x₂

The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:

app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

(41) Obligation:

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

PERMA_IN_GA(.(T24, T25)) → PB_IN_AAAGGAA(T25, T24)
U6_AAAGGAA(T25, T24, app1D_out_aaag(T31, T26, T32, T25)) → PH_IN_GGGAA(T24, T31, T32)
U8_GGGAA(T24, T31, T32, app2F_out_ggga(T24, T31, T32, T65)) → PERMA_IN_GA(T65)
PERMA_IN_GA(.(T125, T126)) → PC_IN_GAA(T126)
PH_IN_GGGAA(T24, T31, T32) → U8_GGGAA(T24, T31, T32, U5_ggga(T24, T31, T32, app2E_in_gga(T31, T32)))
PC_IN_GAA(T126) → U10_GAA(T126, app2G_out_ga(T126, T126))

The TRS R consists of the following rules:

app2E_in_gga(.(T105, T106), T107) → U4_gga(T105, T106, T107, app2E_in_gga(T106, T107))
app2E_in_gga([], T113) → app2E_out_gga([], T113, T113)
U5_ggga(T87, T88, T89, app2E_out_gga(T88, T89, X153)) → app2F_out_ggga(T87, T88, T89, .(T87, X153))
U4_gga(T105, T106, T107, app2E_out_gga(T106, T107, X183)) → app2E_out_gga(.(T105, T106), T107, .(T105, X183))
app1D_in_aaag(.(T50, T51)) → U3_aaag(T50, T51, app1D_in_aaag(T51))
app1D_in_aaag(.(T60, T61)) → app1D_out_aaag([], T60, T61, .(T60, T61))
U3_aaag(T50, T51, app1D_out_aaag(X94, T52, X95, T51)) → app1D_out_aaag(.(T50, X94), T52, X95, .(T50, T51))

The set Q consists of the following terms:

app1D_in_aaag(x0)
U3_aaag(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
app2E_in_gga(x0, x1)
U4_gga(x0, x1, x2, x3)

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

(42) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 6 less nodes.

(0) Obligation:

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

(2) Obligation:

(3) DependencyPairsProof (EQUIVALENT transformation)

(4) Obligation:

(5) DependencyGraphProof (EQUIVALENT transformation)

(6) Complex Obligation (AND)

(7) Obligation:

(8) UsableRulesProof (EQUIVALENT transformation)

(9) Obligation:

(10) PiDPToQDPProof (SOUND transformation)

(11) Obligation:

(12) QDPSizeChangeProof (EQUIVALENT transformation)

(13) YES

(14) Obligation:

(15) UsableRulesProof (EQUIVALENT transformation)

(16) Obligation:

(17) PiDPToQDPProof (SOUND transformation)

(18) Obligation:

(19) QDPSizeChangeProof (EQUIVALENT transformation)

(20) YES

(21) Obligation:

(22) UsableRulesProof (EQUIVALENT transformation)

(23) Obligation:

(24) PiDPToQDPProof (SOUND transformation)

(25) Obligation:

(26) Rewriting (EQUIVALENT transformation)

(27) Obligation:

(28) UsableRulesProof (EQUIVALENT transformation)

(29) Obligation:

(30) QReductionProof (EQUIVALENT transformation)

(31) Obligation:

(32) Rewriting (EQUIVALENT transformation)

(33) Obligation:

(34) UsableRulesProof (EQUIVALENT transformation)

(35) Obligation:

(36) QReductionProof (EQUIVALENT transformation)

(37) Obligation:

(38) Instantiation (EQUIVALENT transformation)

(39) Obligation:

(40) QDPOrderProof (EQUIVALENT transformation)

(41) Obligation:

(42) DependencyGraphProof (EQUIVALENT transformation)

(43) TRUE