Left Termination proof of /tmp/tmpmsJew1/hanoiapp.suc.pl

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

0 Prolog

↳1 PrologToPiTRSViaGraphTransformerProof (⇒, 252 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 274 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 14 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 (⇔, 9 ms)

        ↳23 PiDP

        ↳24 PiDPToQDPProof (⇒, 4 ms)

        ↳25 QDP

        ↳26 QDPSizeChangeProof (⇔, 0 ms)

        ↳27 YES

(0) Obligation:

Clauses:

shanoi(s(0), A, B, C, .(mv(A, C), [])).
shanoi(s(s(X)), A, B, C, M) :- ','(eq(N1, s(X)), ','(shanoi(N1, A, C, B, M1), ','(shanoi(N1, B, A, C, M2), ','(append(M1, .(mv(A, C), []), T), append(T, M2, M))))).
append([], L, L).
append(.(H, L), L1, .(H, R)) :- append(L, L1, R).
eq(X, X).

Query: shanoi(g,g,g,g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: shanoi(T1, T2, T3, T4, T5)\n\nT1 is ground\nT2 is ground\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: shanoi(T1, T2, T3, T4, T5), SCOPE: 1, CLAUSE: 0 | shanoi(T1, T2, T3, T4, T5), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nT3 is ground\nT4 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: true | shanoi(s(0), T9, T10, T11, T5), SCOPE: 1, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
12 [label="12: shanoi(T1, T2, T3, T4, T5), SCOPE: 1, CLAUSE: 1\n\nT1 is ground\nT2 is ground\nT3 is ground\nT4 is ground\nX4 is free\nX5 is free\nX6 is free\nshanoi(T1, T2, T3, T4, T5) !=? shanoi(s(0), X4, X5, X6, .(mv(X4, X6), []))", fontsize=16, style=filled, fillcolor=lightyellow];
14 [label="14: shanoi(s(0), T9, T10, T11, T5), SCOPE: 1, CLAUSE: 1\n\nT9 is ground\nT10 is ground\nT11 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(eq(X22, s(T17)), ','(shanoi(X22, T18, T20, T19, X23), ','(shanoi(X22, T19, T18, T20, X24), ','(append(X23, .(mv(T18, T20), []), X25), append(X25, X24, T22)))))\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground\nX22 is free\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
27 [label="27: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: ','(eq(X22, s(T17)), ','(shanoi(X22, T18, T20, T19, X23), ','(shanoi(X22, T19, T18, T20, X24), ','(append(X23, .(mv(T18, T20), []), X25), append(X25, X24, T22))))), SCOPE: 2, CLAUSE: 4\n\nT17 is ground\nT18 is ground\nT19 is ground\nT20 is ground\nX22 is free\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="B: ','(shanoi(s(T31), T18, T20, T19, X23), ','(shanoi(s(T31), T19, T18, T20, X24), ','(append(X23, .(mv(T18, T20), []), X25), append(X25, X24, T22))))\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nX23 is free\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="C: shanoi(s(T31), T18, T20, T19, X23)\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="G: ','(shanoi(s(T31), T19, T18, T20, X24), ','(append(T38, .(mv(T18, T20), []), X25), append(X25, X24, T22)))\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nT38 is ground\nX24 is free\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
39 [label="39: shanoi(s(T31), T18, T20, T19, X23), SCOPE: 3, CLAUSE: 0 | shanoi(s(T31), T18, T20, T19, X23), SCOPE: 3, CLAUSE: 1\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: shanoi(s(T31), T18, T20, T19, X23), SCOPE: 3, CLAUSE: 0\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="44: shanoi(s(T31), T18, T20, T19, X23), SCOPE: 3, CLAUSE: 1\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
51 [label="51: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
52 [label="52: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="58: ','(eq(X86, s(T68)), ','(shanoi(X86, T69, T71, T70, X87), ','(shanoi(X86, T70, T69, T71, X88), ','(append(X87, .(mv(T69, T71), []), X89), append(X89, X88, X90)))))\n\nT68 is ground\nT69 is ground\nT70 is ground\nT71 is ground\nX90 is free\nX86 is free\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: ','(eq(X86, s(T68)), ','(shanoi(X86, T69, T71, T70, X87), ','(shanoi(X86, T70, T69, T71, X88), ','(append(X87, .(mv(T69, T71), []), X89), append(X89, X88, X90))))), SCOPE: 4, CLAUSE: 4\n\nT68 is ground\nT69 is ground\nT70 is ground\nT71 is ground\nX90 is free\nX86 is free\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="D: ','(shanoi(s(T88), T69, T71, T70, X87), ','(shanoi(s(T88), T70, T69, T71, X88), ','(append(X87, .(mv(T69, T71), []), X89), append(X89, X88, X90))))\n\nT69 is ground\nT70 is ground\nT71 is ground\nT88 is ground\nX90 is free\nX87 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="70: shanoi(s(T88), T69, T71, T70, X87)\n\nT69 is ground\nT70 is ground\nT71 is ground\nT88 is ground\nX87 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="I: ','(shanoi(s(T88), T70, T69, T71, X88), ','(append(T95, .(mv(T69, T71), []), X89), append(X89, X88, X90)))\n\nT69 is ground\nT70 is ground\nT71 is ground\nT88 is ground\nT95 is ground\nX90 is free\nX88 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: shanoi(s(T88), T70, T69, T71, X88)\n\nT69 is ground\nT70 is ground\nT71 is ground\nT88 is ground\nX88 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="J: ','(append(T95, .(mv(T69, T71), []), X89), append(X89, T108, X90))\n\nT69 is ground\nT71 is ground\nT95 is ground\nT108 is ground\nX90 is free\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: append(T95, .(mv(T69, T71), []), X89)\n\nT69 is ground\nT71 is ground\nT95 is ground\nX89 is free", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="E: append(T119, T108, X90)\n\nT108 is ground\nT119 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: append(T119, T108, X90), SCOPE: 5, CLAUSE: 2 | append(T119, T108, X90), SCOPE: 5, CLAUSE: 3\n\nT108 is ground\nT119 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
91 [label="91: append(T119, T108, X90), SCOPE: 5, CLAUSE: 2\n\nT108 is ground\nT119 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: append(T119, T108, X90), SCOPE: 5, CLAUSE: 3\n\nT108 is ground\nT119 is ground\nX90 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
94 [label="94: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
95 [label="95: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: append(T138, T139, X161)\n\nT138 is ground\nT139 is ground\nX161 is free", fontsize=16, style=filled, fillcolor=lightyellow];
101 [label="101: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: shanoi(s(T31), T19, T18, T20, X24)\n\nT18 is ground\nT19 is ground\nT20 is ground\nT31 is ground\nX24 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="H: ','(append(T38, .(mv(T18, T20), []), X25), append(X25, T148, T22))\n\nT18 is ground\nT20 is ground\nT38 is ground\nT148 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
116 [label="116: append(T38, .(mv(T18, T20), []), X25)\n\nT18 is ground\nT20 is ground\nT38 is ground\nX25 is free", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="F: append(T159, T148, T22)\n\nT148 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="126: append(T159, T148, T22), SCOPE: 6, CLAUSE: 2 | append(T159, T148, T22), SCOPE: 6, CLAUSE: 3\n\nT148 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: append(T159, T148, T22), SCOPE: 6, CLAUSE: 2\n\nT148 is ground\nT159 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: append(T159, T148, T22), SCOPE: 6, CLAUSE: 3\n\nT148 is ground\nT159 is ground", 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];
136 [label="136: append(T180, T181, T183)\n\nT180 is ground\nT181 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 138 [arrowhead = none ];
138 -> 6;

139 [label="EVAL with clause\nshanoi(s(0), X4, X5, X6, .(mv(X4, X6), [])).\nand substitutionT1 -> s(0),\nT2 -> T9,\nX4 -> T9,\nT3 -> T10,\nX5 -> T10,\nT4 -> T11,\nX6 -> T11,\nT5 -> .(mv(T9, T11), [])", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 139 [arrowhead = none ];
139 -> 10;

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

141 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
10 -> 141 [arrowhead = none ];
141 -> 14;

142 [label="EVAL with clause\nshanoi(s(s(X17)), X18, X19, X20, X21) :- ','(eq(X22, s(X17)), ','(shanoi(X22, X18, X20, X19, X23), ','(shanoi(X22, X19, X18, X20, X24), ','(append(X23, .(mv(X18, X20), []), X25), append(X25, X24, X21))))).\nand substitutionX17 -> T17,\nT1 -> s(s(T17)),\nT2 -> T18,\nX18 -> T18,\nT3 -> T19,\nX19 -> T19,\nT4 -> T20,\nX20 -> T20,\nT5 -> T22,\nX21 -> T22,\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
12 -> 142 [arrowhead = none ];
142 -> 25;

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

144 [label="BACKTRACK\nfor clause: shanoi(s(s(X)), A, B, C, M) :- ','(eq(N1, s(X)), ','(shanoi(N1, A, C, B, M1), ','(shanoi(N1, B, A, C, M2), ','(append(M1, .(mv(A, C), []), T), append(T, M2, M)))))because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
14 -> 144 [arrowhead = none ];
144 -> 18;

145 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
25 -> 145 [arrowhead = none ];
145 -> 28;

146 [label="ONLY EVAL with clause\neq(X36, X36).\nand substitutionX22 -> s(T31),\nX36 -> s(T31),\nT17 -> T31,\nX37 -> s(T31)", fontsize=14, style = filled, fillcolor = lightblue];
28 -> 146 [arrowhead = none ];
146 -> 30;

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

148 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT18 is ground\nT20 is ground\nT19 is ground\nT38 is ground\nreplacements:X23 -> T38", fontsize=14, style = filled, fillcolor = violet];
30 -> 148 [arrowhead = none ];
148 -> 35;

149 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
34 -> 149 [arrowhead = none ];
149 -> 39;

150 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
35 -> 150 [arrowhead = none ];
150 -> 110;

151 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT19 is ground\nT18 is ground\nT20 is ground\nT148 is ground\nreplacements:X24 -> T148", fontsize=14, style = filled, fillcolor = violet];
35 -> 151 [arrowhead = none ];
151 -> 111;

152 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
39 -> 152 [arrowhead = none ];
152 -> 42;

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

154 [label="EVAL with clause\nshanoi(s(0), X62, X63, X64, .(mv(X62, X64), [])).\nand substitutionT31 -> 0,\nT18 -> T57,\nX62 -> T57,\nT20 -> T58,\nX63 -> T58,\nT19 -> T59,\nX64 -> T59,\nX23 -> .(mv(T57, T59), [])", fontsize=14, style = filled, fillcolor = lightblue];
42 -> 154 [arrowhead = none ];
154 -> 49;

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

156 [label="EVAL with clause\nshanoi(s(s(X81)), X82, X83, X84, X85) :- ','(eq(X86, s(X81)), ','(shanoi(X86, X82, X84, X83, X87), ','(shanoi(X86, X83, X82, X84, X88), ','(append(X87, .(mv(X82, X84), []), X89), append(X89, X88, X85))))).\nand substitutionX81 -> T68,\nT31 -> s(T68),\nT18 -> T69,\nX82 -> T69,\nT20 -> T70,\nX83 -> T70,\nT19 -> T71,\nX84 -> T71,\nX23 -> X90,\nX85 -> X90", fontsize=14, style = filled, fillcolor = lightblue];
44 -> 156 [arrowhead = none ];
156 -> 58;

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

158 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
49 -> 158 [arrowhead = none ];
158 -> 52;

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

160 [label="ONLY EVAL with clause\neq(X110, X110).\nand substitutionX86 -> s(T88),\nX110 -> s(T88),\nT68 -> T88,\nX111 -> s(T88)", fontsize=14, style = filled, fillcolor = lightblue];
63 -> 160 [arrowhead = none ];
160 -> 65;

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

162 [label="SPLIT 2\nnew knowledge:\nT88 is ground\nT69 is ground\nT71 is ground\nT70 is ground\nT95 is ground\nreplacements:X87 -> T95", fontsize=14, style = filled, fillcolor = violet];
65 -> 162 [arrowhead = none ];
162 -> 71;

163 [label="INSTANCE with matching:\nT31 -> T88\nT18 -> T69\nT20 -> T71\nT19 -> T70\nX23 -> X87", fontsize=14, style = filled, fillcolor = lightgrey];
70 -> 163 [arrowhead = none , style=dashed];
163 -> 34[style=dashed];

164 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
71 -> 164 [arrowhead = none ];
164 -> 76;

165 [label="SPLIT 2\nnew knowledge:\nT88 is ground\nT70 is ground\nT69 is ground\nT71 is ground\nT108 is ground\nreplacements:X88 -> T108", fontsize=14, style = filled, fillcolor = violet];
71 -> 165 [arrowhead = none ];
165 -> 77;

166 [label="INSTANCE with matching:\nT31 -> T88\nT18 -> T70\nT20 -> T69\nT19 -> T71\nX23 -> X88", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 166 [arrowhead = none , style=dashed];
166 -> 34[style=dashed];

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

168 [label="SPLIT 2\nnew knowledge:\nT95 is ground\nT69 is ground\nT71 is ground\nT119 is ground\nreplacements:X89 -> T119", fontsize=14, style = filled, fillcolor = violet];
77 -> 168 [arrowhead = none ];
168 -> 81;

169 [label="INSTANCE with matching:\nT119 -> T95\nT108 -> .(mv(T69, T71), [])\nX90 -> X89", fontsize=14, style = filled, fillcolor = lightgrey];
80 -> 169 [arrowhead = none , style=dashed];
169 -> 81[style=dashed];

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

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

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

173 [label="EVAL with clause\nappend([], X146, X146).\nand substitutionT119 -> [],\nT108 -> T130,\nX146 -> T130,\nX90 -> T130", fontsize=14, style = filled, fillcolor = lightblue];
91 -> 173 [arrowhead = none ];
173 -> 93;

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

175 [label="EVAL with clause\nappend(.(X157, X158), X159, .(X157, X160)) :- append(X158, X159, X160).\nand substitutionX157 -> T137,\nX158 -> T138,\nT119 -> .(T137, T138),\nT108 -> T139,\nX159 -> T139,\nX160 -> X161,\nX90 -> .(T137, X161)", fontsize=14, style = filled, fillcolor = lightblue];
92 -> 175 [arrowhead = none ];
175 -> 98;

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

177 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
93 -> 177 [arrowhead = none ];
177 -> 95;

178 [label="INSTANCE with matching:\nT119 -> T138\nT108 -> T139\nX90 -> X161", fontsize=14, style = filled, fillcolor = lightgrey];
98 -> 178 [arrowhead = none , style=dashed];
178 -> 81[style=dashed];

179 [label="INSTANCE with matching:\nT18 -> T19\nT20 -> T18\nT19 -> T20\nX23 -> X24", fontsize=14, style = filled, fillcolor = lightgrey];
110 -> 179 [arrowhead = none , style=dashed];
179 -> 34[style=dashed];

180 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
111 -> 180 [arrowhead = none ];
180 -> 116;

181 [label="SPLIT 2\nnew knowledge:\nT38 is ground\nT18 is ground\nT20 is ground\nT159 is ground\nreplacements:X25 -> T159", fontsize=14, style = filled, fillcolor = violet];
111 -> 181 [arrowhead = none ];
181 -> 117;

182 [label="INSTANCE with matching:\nT159 -> T38\nT148 -> .(mv(T18, T20), [])\nT22 -> X25", fontsize=14, style = filled, fillcolor = lightgrey];
116 -> 182 [arrowhead = none , style=dashed];
182 -> 117[style=dashed];

183 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
117 -> 183 [arrowhead = none ];
183 -> 126;

184 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 184 [arrowhead = none ];
184 -> 127;

185 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
126 -> 185 [arrowhead = none ];
185 -> 128;

186 [label="EVAL with clause\nappend([], X186, X186).\nand substitutionT159 -> [],\nT148 -> T170,\nX186 -> T170,\nT22 -> T170", fontsize=14, style = filled, fillcolor = lightblue];
127 -> 186 [arrowhead = none ];
186 -> 129;

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

188 [label="EVAL with clause\nappend(.(X195, X196), X197, .(X195, X198)) :- append(X196, X197, X198).\nand substitutionX195 -> T179,\nX196 -> T180,\nT159 -> .(T179, T180),\nT148 -> T181,\nX197 -> T181,\nX198 -> T183,\nT22 -> .(T179, T183),\nT182 -> T183", fontsize=14, style = filled, fillcolor = lightblue];
128 -> 188 [arrowhead = none ];
188 -> 136;

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

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

191 [label="INSTANCE with matching:\nT159 -> T180\nT148 -> T181\nT22 -> T183", fontsize=14, style = filled, fillcolor = lightgrey];
136 -> 191 [arrowhead = none , style=dashed];
191 -> 117[style=dashed];

}

(2) Obligation:

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

shanoiA_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoiA_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoiA_in_gggga(s(s(T31)), T18, T19, T20, T22) → U1_gggga(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
pB_in_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22) → U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
pG_in_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22) → U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
pH_in_gggaga(T38, T18, T20, T159, T148, T22) → U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
appendF_in_gga([], T170, T170) → appendF_out_gga([], T170, T170)
appendF_in_gga(.(T179, T180), T181, .(T179, T183)) → U4_gga(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
U4_gga(T179, T180, T181, T183, appendF_out_gga(T180, T181, T183)) → appendF_out_gga(.(T179, T180), T181, .(T179, T183))
U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T159, T148, T22)) → pH_out_gggaga(T38, T18, T20, T159, T148, T22)
U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_out_gggaga(T38, T18, T20, X25, T148, T22)) → pG_out_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22)
U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_out_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22)) → pB_out_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22)
U1_gggga(T31, T18, T19, T20, T22, pB_out_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22)) → shanoiA_out_gggga(s(s(T31)), T18, T19, T20, T22)

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

SHANOIA_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U1_GGGGA(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
SHANOIA_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → PB_IN_GGGGAAAA(T31, T18, T20, T19, X23, X24, X25, T22)
PB_IN_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22) → U5_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
PB_IN_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22) → SHANOIC_IN_GGGGA(T31, T18, T20, T19, T38)
SHANOIC_IN_GGGGA(s(T88), T69, T70, T71, X90) → U2_GGGGA(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
SHANOIC_IN_GGGGA(s(T88), T69, T70, T71, X90) → PD_IN_GGGGAAAA(T88, T69, T71, T70, X87, X88, X89, X90)
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → SHANOIC_IN_GGGGA(T88, T69, T71, T70, T95)
U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → PI_IN_GGGGAGAA(T88, T70, T69, T71, X88, T95, X89, X90)
PI_IN_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90) → U11_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
PI_IN_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90) → SHANOIC_IN_GGGGA(T88, T70, T69, T71, T108)
U11_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
U11_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → PJ_IN_GGGAGA(T95, T69, T71, X89, T108, X90)
PJ_IN_GGGAGA(T95, T69, T71, T119, T108, X90) → U13_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
PJ_IN_GGGAGA(T95, T69, T71, T119, T108, X90) → APPENDE_IN_GGA(T95, .(mv(T69, T71), []), T119)
APPENDE_IN_GGA(.(T137, T138), T139, .(T137, X161)) → U3_GGA(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
APPENDE_IN_GGA(.(T137, T138), T139, .(T137, X161)) → APPENDE_IN_GGA(T138, T139, X161)
U13_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U13_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → APPENDE_IN_GGA(T119, T108, X90)
U5_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
U5_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → PG_IN_GGGGAGAA(T31, T19, T18, T20, X24, T38, X25, T22)
PG_IN_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22) → U7_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
PG_IN_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22) → SHANOIC_IN_GGGGA(T31, T19, T18, T20, T148)
U7_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
U7_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → PH_IN_GGGAGA(T38, T18, T20, X25, T148, T22)
PH_IN_GGGAGA(T38, T18, T20, T159, T148, T22) → U15_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
PH_IN_GGGAGA(T38, T18, T20, T159, T148, T22) → APPENDF_IN_GGA(T38, .(mv(T18, T20), []), T159)
APPENDF_IN_GGA(.(T179, T180), T181, .(T179, T183)) → U4_GGA(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
APPENDF_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPENDF_IN_GGA(T180, T181, T183)
U15_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U15_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → APPENDF_IN_GGA(T159, T148, T22)

The TRS R consists of the following rules:

shanoiA_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoiA_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoiA_in_gggga(s(s(T31)), T18, T19, T20, T22) → U1_gggga(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
pB_in_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22) → U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
pG_in_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22) → U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
pH_in_gggaga(T38, T18, T20, T159, T148, T22) → U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
appendF_in_gga([], T170, T170) → appendF_out_gga([], T170, T170)
appendF_in_gga(.(T179, T180), T181, .(T179, T183)) → U4_gga(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
U4_gga(T179, T180, T181, T183, appendF_out_gga(T180, T181, T183)) → appendF_out_gga(.(T179, T180), T181, .(T179, T183))
U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T159, T148, T22)) → pH_out_gggaga(T38, T18, T20, T159, T148, T22)
U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_out_gggaga(T38, T18, T20, X25, T148, T22)) → pG_out_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22)
U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_out_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22)) → pB_out_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22)
U1_gggga(T31, T18, T19, T20, T22, pB_out_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22)) → shanoiA_out_gggga(s(s(T31)), T18, T19, T20, T22)

The argument filtering Pi contains the following mapping:
shanoiA_in_gggga(x1, x2, x3, x4, x5) = shanoiA_in_gggga(x1, x2, x3, x4)
s(x1) = s(x1)
0 = 0
shanoiA_out_gggga(x1, x2, x3, x4, x5) = shanoiA_out_gggga(x1, x2, x3, x4, x5)
U1_gggga(x1, x2, x3, x4, x5, x6) = U1_gggga(x1, x2, x3, x4, x6)
pB_in_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_in_ggggaaaa(x1, x2, x3, x4)
U5_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U5_ggggaaaa(x1, x2, x3, x4, x9)
shanoiC_in_gggga(x1, x2, x3, x4, x5) = shanoiC_in_gggga(x1, x2, x3, x4)
shanoiC_out_gggga(x1, x2, x3, x4, x5) = shanoiC_out_gggga(x1, x2, x3, x4, x5)
U2_gggga(x1, x2, x3, x4, x5, x6) = U2_gggga(x1, x2, x3, x4, x6)
pD_in_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pD_in_ggggaaaa(x1, x2, x3, x4)
U9_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U9_ggggaaaa(x1, x2, x3, x4, x9)
U10_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U10_ggggaaaa(x1, x2, x3, x4, x5, x9)
pI_in_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pI_in_ggggagaa(x1, x2, x3, x4, x6)
U11_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U11_ggggagaa(x1, x2, x3, x4, x6, x9)
U12_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U12_ggggagaa(x1, x2, x3, x4, x5, x6, x9)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6) = pJ_in_gggaga(x1, x2, x3, x5)
U13_gggaga(x1, x2, x3, x4, x5, x6, x7) = U13_gggaga(x1, x2, x3, x5, x7)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
[] = []
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U14_gggaga(x1, x2, x3, x4, x5, x6, x7) = U14_gggaga(x1, x2, x3, x4, x5, x7)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6) = pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pI_out_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8)
pD_out_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pD_out_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
U6_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U6_ggggaaaa(x1, x2, x3, x4, x5, x9)
pG_in_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pG_in_ggggagaa(x1, x2, x3, x4, x6)
U7_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_ggggagaa(x1, x2, x3, x4, x6, x9)
U8_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_ggggagaa(x1, x2, x3, x4, x5, x6, x9)
pH_in_gggaga(x1, x2, x3, x4, x5, x6) = pH_in_gggaga(x1, x2, x3, x5)
U15_gggaga(x1, x2, x3, x4, x5, x6, x7) = U15_gggaga(x1, x2, x3, x5, x7)
appendF_in_gga(x1, x2, x3) = appendF_in_gga(x1, x2)
appendF_out_gga(x1, x2, x3) = appendF_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
U16_gggaga(x1, x2, x3, x4, x5, x6, x7) = U16_gggaga(x1, x2, x3, x4, x5, x7)
pH_out_gggaga(x1, x2, x3, x4, x5, x6) = pH_out_gggaga(x1, x2, x3, x4, x5, x6)
pG_out_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pG_out_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8)
pB_out_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pB_out_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
SHANOIA_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOIA_IN_GGGGA(x1, x2, x3, x4)
U1_GGGGA(x1, x2, x3, x4, x5, x6) = U1_GGGGA(x1, x2, x3, x4, x6)
PB_IN_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = PB_IN_GGGGAAAA(x1, x2, x3, x4)
U5_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U5_GGGGAAAA(x1, x2, x3, x4, x9)
SHANOIC_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOIC_IN_GGGGA(x1, x2, x3, x4)
U2_GGGGA(x1, x2, x3, x4, x5, x6) = U2_GGGGA(x1, x2, x3, x4, x6)
PD_IN_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = PD_IN_GGGGAAAA(x1, x2, x3, x4)
U9_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U9_GGGGAAAA(x1, x2, x3, x4, x9)
U10_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U10_GGGGAAAA(x1, x2, x3, x4, x5, x9)
PI_IN_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PI_IN_GGGGAGAA(x1, x2, x3, x4, x6)
U11_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U11_GGGGAGAA(x1, x2, x3, x4, x6, x9)
U12_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U12_GGGGAGAA(x1, x2, x3, x4, x5, x6, x9)
PJ_IN_GGGAGA(x1, x2, x3, x4, x5, x6) = PJ_IN_GGGAGA(x1, x2, x3, x5)
U13_GGGAGA(x1, x2, x3, x4, x5, x6, x7) = U13_GGGAGA(x1, x2, x3, x5, x7)
APPENDE_IN_GGA(x1, x2, x3) = APPENDE_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4, x5) = U3_GGA(x1, x2, x3, x5)
U14_GGGAGA(x1, x2, x3, x4, x5, x6, x7) = U14_GGGAGA(x1, x2, x3, x4, x5, x7)
U6_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U6_GGGGAAAA(x1, x2, x3, x4, x5, x9)
PG_IN_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PG_IN_GGGGAGAA(x1, x2, x3, x4, x6)
U7_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U7_GGGGAGAA(x1, x2, x3, x4, x6, x9)
U8_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U8_GGGGAGAA(x1, x2, x3, x4, x5, x6, x9)
PH_IN_GGGAGA(x1, x2, x3, x4, x5, x6) = PH_IN_GGGAGA(x1, x2, x3, x5)
U15_GGGAGA(x1, x2, x3, x4, x5, x6, x7) = U15_GGGAGA(x1, x2, x3, x5, x7)
APPENDF_IN_GGA(x1, x2, x3) = APPENDF_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5) = U4_GGA(x1, x2, x3, x5)
U16_GGGAGA(x1, x2, x3, x4, x5, x6, x7) = U16_GGGAGA(x1, x2, x3, x4, x5, x7)

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

(4) Obligation:

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

SHANOIA_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → U1_GGGGA(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
SHANOIA_IN_GGGGA(s(s(T31)), T18, T19, T20, T22) → PB_IN_GGGGAAAA(T31, T18, T20, T19, X23, X24, X25, T22)
PB_IN_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22) → U5_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
PB_IN_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22) → SHANOIC_IN_GGGGA(T31, T18, T20, T19, T38)
SHANOIC_IN_GGGGA(s(T88), T69, T70, T71, X90) → U2_GGGGA(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
SHANOIC_IN_GGGGA(s(T88), T69, T70, T71, X90) → PD_IN_GGGGAAAA(T88, T69, T71, T70, X87, X88, X89, X90)
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → SHANOIC_IN_GGGGA(T88, T69, T71, T70, T95)
U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → PI_IN_GGGGAGAA(T88, T70, T69, T71, X88, T95, X89, X90)
PI_IN_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90) → U11_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
PI_IN_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90) → SHANOIC_IN_GGGGA(T88, T70, T69, T71, T108)
U11_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
U11_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → PJ_IN_GGGAGA(T95, T69, T71, X89, T108, X90)
PJ_IN_GGGAGA(T95, T69, T71, T119, T108, X90) → U13_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
PJ_IN_GGGAGA(T95, T69, T71, T119, T108, X90) → APPENDE_IN_GGA(T95, .(mv(T69, T71), []), T119)
APPENDE_IN_GGA(.(T137, T138), T139, .(T137, X161)) → U3_GGA(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
APPENDE_IN_GGA(.(T137, T138), T139, .(T137, X161)) → APPENDE_IN_GGA(T138, T139, X161)
U13_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U13_GGGAGA(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → APPENDE_IN_GGA(T119, T108, X90)
U5_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
U5_GGGGAAAA(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → PG_IN_GGGGAGAA(T31, T19, T18, T20, X24, T38, X25, T22)
PG_IN_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22) → U7_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
PG_IN_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22) → SHANOIC_IN_GGGGA(T31, T19, T18, T20, T148)
U7_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
U7_GGGGAGAA(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → PH_IN_GGGAGA(T38, T18, T20, X25, T148, T22)
PH_IN_GGGAGA(T38, T18, T20, T159, T148, T22) → U15_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
PH_IN_GGGAGA(T38, T18, T20, T159, T148, T22) → APPENDF_IN_GGA(T38, .(mv(T18, T20), []), T159)
APPENDF_IN_GGA(.(T179, T180), T181, .(T179, T183)) → U4_GGA(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
APPENDF_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPENDF_IN_GGA(T180, T181, T183)
U15_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U15_GGGAGA(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → APPENDF_IN_GGA(T159, T148, T22)

The TRS R consists of the following rules:

shanoiA_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoiA_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoiA_in_gggga(s(s(T31)), T18, T19, T20, T22) → U1_gggga(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
pB_in_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22) → U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
pG_in_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22) → U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
pH_in_gggaga(T38, T18, T20, T159, T148, T22) → U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
appendF_in_gga([], T170, T170) → appendF_out_gga([], T170, T170)
appendF_in_gga(.(T179, T180), T181, .(T179, T183)) → U4_gga(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
U4_gga(T179, T180, T181, T183, appendF_out_gga(T180, T181, T183)) → appendF_out_gga(.(T179, T180), T181, .(T179, T183))
U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T159, T148, T22)) → pH_out_gggaga(T38, T18, T20, T159, T148, T22)
U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_out_gggaga(T38, T18, T20, X25, T148, T22)) → pG_out_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22)
U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_out_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22)) → pB_out_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22)
U1_gggga(T31, T18, T19, T20, T22, pB_out_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22)) → shanoiA_out_gggga(s(s(T31)), T18, T19, T20, T22)

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APPENDF_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPENDF_IN_GGA(T180, T181, T183)

The TRS R consists of the following rules:

shanoiA_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoiA_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoiA_in_gggga(s(s(T31)), T18, T19, T20, T22) → U1_gggga(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
pB_in_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22) → U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
pG_in_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22) → U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
pH_in_gggaga(T38, T18, T20, T159, T148, T22) → U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
appendF_in_gga([], T170, T170) → appendF_out_gga([], T170, T170)
appendF_in_gga(.(T179, T180), T181, .(T179, T183)) → U4_gga(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
U4_gga(T179, T180, T181, T183, appendF_out_gga(T180, T181, T183)) → appendF_out_gga(.(T179, T180), T181, .(T179, T183))
U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T159, T148, T22)) → pH_out_gggaga(T38, T18, T20, T159, T148, T22)
U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_out_gggaga(T38, T18, T20, X25, T148, T22)) → pG_out_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22)
U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_out_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22)) → pB_out_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22)
U1_gggga(T31, T18, T19, T20, T22, pB_out_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22)) → shanoiA_out_gggga(s(s(T31)), T18, T19, T20, T22)

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

APPENDF_IN_GGA(.(T179, T180), T181, .(T179, T183)) → APPENDF_IN_GGA(T180, T181, T183)

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

APPENDF_IN_GGA(.(T179, T180), T181) → APPENDF_IN_GGA(T180, T181)

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:

APPENDF_IN_GGA(.(T179, T180), T181) → APPENDF_IN_GGA(T180, T181)
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:

APPENDE_IN_GGA(.(T137, T138), T139, .(T137, X161)) → APPENDE_IN_GGA(T138, T139, X161)

The TRS R consists of the following rules:

shanoiA_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoiA_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoiA_in_gggga(s(s(T31)), T18, T19, T20, T22) → U1_gggga(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
pB_in_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22) → U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
pG_in_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22) → U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
pH_in_gggaga(T38, T18, T20, T159, T148, T22) → U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
appendF_in_gga([], T170, T170) → appendF_out_gga([], T170, T170)
appendF_in_gga(.(T179, T180), T181, .(T179, T183)) → U4_gga(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
U4_gga(T179, T180, T181, T183, appendF_out_gga(T180, T181, T183)) → appendF_out_gga(.(T179, T180), T181, .(T179, T183))
U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T159, T148, T22)) → pH_out_gggaga(T38, T18, T20, T159, T148, T22)
U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_out_gggaga(T38, T18, T20, X25, T148, T22)) → pG_out_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22)
U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_out_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22)) → pB_out_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22)
U1_gggga(T31, T18, T19, T20, T22, pB_out_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22)) → shanoiA_out_gggga(s(s(T31)), T18, T19, T20, T22)

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

APPENDE_IN_GGA(.(T137, T138), T139, .(T137, X161)) → APPENDE_IN_GGA(T138, T139, X161)

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

APPENDE_IN_GGA(.(T137, T138), T139) → APPENDE_IN_GGA(T138, T139)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

APPENDE_IN_GGA(.(T137, T138), T139) → APPENDE_IN_GGA(T138, T139)
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:

SHANOIC_IN_GGGGA(s(T88), T69, T70, T71, X90) → PD_IN_GGGGAAAA(T88, T69, T71, T70, X87, X88, X89, X90)
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → PI_IN_GGGGAGAA(T88, T70, T69, T71, X88, T95, X89, X90)
PI_IN_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90) → SHANOIC_IN_GGGGA(T88, T70, T69, T71, T108)
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → SHANOIC_IN_GGGGA(T88, T69, T71, T70, T95)

The TRS R consists of the following rules:

shanoiA_in_gggga(s(0), T9, T10, T11, .(mv(T9, T11), [])) → shanoiA_out_gggga(s(0), T9, T10, T11, .(mv(T9, T11), []))
shanoiA_in_gggga(s(s(T31)), T18, T19, T20, T22) → U1_gggga(T31, T18, T19, T20, T22, pB_in_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22))
pB_in_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22) → U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_in_gggga(T31, T18, T20, T19, T38))
shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
U5_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, shanoiC_out_gggga(T31, T18, T20, T19, T38)) → U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_in_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22))
pG_in_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22) → U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_in_gggga(T31, T19, T18, T20, T148))
U7_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, shanoiC_out_gggga(T31, T19, T18, T20, T148)) → U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_in_gggaga(T38, T18, T20, X25, T148, T22))
pH_in_gggaga(T38, T18, T20, T159, T148, T22) → U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T38, .(mv(T18, T20), []), T159))
appendF_in_gga([], T170, T170) → appendF_out_gga([], T170, T170)
appendF_in_gga(.(T179, T180), T181, .(T179, T183)) → U4_gga(T179, T180, T181, T183, appendF_in_gga(T180, T181, T183))
U4_gga(T179, T180, T181, T183, appendF_out_gga(T180, T181, T183)) → appendF_out_gga(.(T179, T180), T181, .(T179, T183))
U15_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T38, .(mv(T18, T20), []), T159)) → U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_in_gga(T159, T148, T22))
U16_gggaga(T38, T18, T20, T159, T148, T22, appendF_out_gga(T159, T148, T22)) → pH_out_gggaga(T38, T18, T20, T159, T148, T22)
U8_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22, pH_out_gggaga(T38, T18, T20, X25, T148, T22)) → pG_out_ggggagaa(T31, T19, T18, T20, T148, T38, X25, T22)
U6_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22, pG_out_ggggagaa(T31, T19, T18, T20, X24, T38, X25, T22)) → pB_out_ggggaaaa(T31, T18, T20, T19, T38, X24, X25, T22)
U1_gggga(T31, T18, T19, T20, T22, pB_out_ggggaaaa(T31, T18, T20, T19, X23, X24, X25, T22)) → shanoiA_out_gggga(s(s(T31)), T18, T19, T20, T22)

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

SHANOIC_IN_GGGGA(s(T88), T69, T70, T71, X90) → PD_IN_GGGGAAAA(T88, T69, T71, T70, X87, X88, X89, X90)
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → PI_IN_GGGGAGAA(T88, T70, T69, T71, X88, T95, X89, X90)
PI_IN_GGGGAGAA(T88, T70, T69, T71, T108, T95, X89, X90) → SHANOIC_IN_GGGGA(T88, T70, T69, T71, T108)
PD_IN_GGGGAAAA(T88, T69, T71, T70, T95, X88, X89, X90) → SHANOIC_IN_GGGGA(T88, T69, T71, T70, T95)

The TRS R consists of the following rules:

shanoiC_in_gggga(0, T57, T58, T59, .(mv(T57, T59), [])) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71, X90) → U2_gggga(T88, T69, T70, T71, X90, pD_in_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90))
U2_gggga(T88, T69, T70, T71, X90, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
pD_in_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90) → U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_in_gggga(T88, T69, T71, T70, T95))
U9_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_in_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90))
U10_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
pI_in_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90) → U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_in_gggga(T88, T70, T69, T71, T108))
U11_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_in_gggaga(T95, T69, T71, X89, T108, X90))
U12_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
pJ_in_gggaga(T95, T69, T71, T119, T108, X90) → U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T95, .(mv(T69, T71), []), T119))
U13_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_in_gga(T119, T108, X90))
appendE_in_gga([], T130, T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139, .(T137, X161)) → U3_gga(T137, T138, T139, X161, appendE_in_gga(T138, T139, X161))
U14_gggaga(T95, T69, T71, T119, T108, X90, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U3_gga(T137, T138, T139, X161, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))

The argument filtering Pi contains the following mapping:
s(x1) = s(x1)
0 = 0
shanoiC_in_gggga(x1, x2, x3, x4, x5) = shanoiC_in_gggga(x1, x2, x3, x4)
shanoiC_out_gggga(x1, x2, x3, x4, x5) = shanoiC_out_gggga(x1, x2, x3, x4, x5)
U2_gggga(x1, x2, x3, x4, x5, x6) = U2_gggga(x1, x2, x3, x4, x6)
pD_in_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pD_in_ggggaaaa(x1, x2, x3, x4)
U9_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U9_ggggaaaa(x1, x2, x3, x4, x9)
U10_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U10_ggggaaaa(x1, x2, x3, x4, x5, x9)
pI_in_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pI_in_ggggagaa(x1, x2, x3, x4, x6)
U11_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U11_ggggagaa(x1, x2, x3, x4, x6, x9)
U12_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U12_ggggagaa(x1, x2, x3, x4, x5, x6, x9)
pJ_in_gggaga(x1, x2, x3, x4, x5, x6) = pJ_in_gggaga(x1, x2, x3, x5)
U13_gggaga(x1, x2, x3, x4, x5, x6, x7) = U13_gggaga(x1, x2, x3, x5, x7)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
[] = []
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
.(x1, x2) = .(x1, x2)
U3_gga(x1, x2, x3, x4, x5) = U3_gga(x1, x2, x3, x5)
mv(x1, x2) = mv(x1, x2)
U14_gggaga(x1, x2, x3, x4, x5, x6, x7) = U14_gggaga(x1, x2, x3, x4, x5, x7)
pJ_out_gggaga(x1, x2, x3, x4, x5, x6) = pJ_out_gggaga(x1, x2, x3, x4, x5, x6)
pI_out_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8) = pI_out_ggggagaa(x1, x2, x3, x4, x5, x6, x7, x8)
pD_out_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8) = pD_out_ggggaaaa(x1, x2, x3, x4, x5, x6, x7, x8)
SHANOIC_IN_GGGGA(x1, x2, x3, x4, x5) = SHANOIC_IN_GGGGA(x1, x2, x3, x4)
PD_IN_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8) = PD_IN_GGGGAAAA(x1, x2, x3, x4)
U9_GGGGAAAA(x1, x2, x3, x4, x5, x6, x7, x8, x9) = U9_GGGGAAAA(x1, x2, x3, x4, x9)
PI_IN_GGGGAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = PI_IN_GGGGAGAA(x1, x2, x3, x4, x6)

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:

SHANOIC_IN_GGGGA(s(T88), T69, T70, T71) → PD_IN_GGGGAAAA(T88, T69, T71, T70)
PD_IN_GGGGAAAA(T88, T69, T71, T70) → U9_GGGGAAAA(T88, T69, T71, T70, shanoiC_in_gggga(T88, T69, T71, T70))
U9_GGGGAAAA(T88, T69, T71, T70, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → PI_IN_GGGGAGAA(T88, T70, T69, T71, T95)
PI_IN_GGGGAGAA(T88, T70, T69, T71, T95) → SHANOIC_IN_GGGGA(T88, T70, T69, T71)
PD_IN_GGGGAAAA(T88, T69, T71, T70) → SHANOIC_IN_GGGGA(T88, T69, T71, T70)

The TRS R consists of the following rules:

shanoiC_in_gggga(0, T57, T58, T59) → shanoiC_out_gggga(0, T57, T58, T59, .(mv(T57, T59), []))
shanoiC_in_gggga(s(T88), T69, T70, T71) → U2_gggga(T88, T69, T70, T71, pD_in_ggggaaaa(T88, T69, T71, T70))
U2_gggga(T88, T69, T70, T71, pD_out_ggggaaaa(T88, T69, T71, T70, X87, X88, X89, X90)) → shanoiC_out_gggga(s(T88), T69, T70, T71, X90)
pD_in_ggggaaaa(T88, T69, T71, T70) → U9_ggggaaaa(T88, T69, T71, T70, shanoiC_in_gggga(T88, T69, T71, T70))
U9_ggggaaaa(T88, T69, T71, T70, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → U10_ggggaaaa(T88, T69, T71, T70, T95, pI_in_ggggagaa(T88, T70, T69, T71, T95))
U10_ggggaaaa(T88, T69, T71, T70, T95, pI_out_ggggagaa(T88, T70, T69, T71, X88, T95, X89, X90)) → pD_out_ggggaaaa(T88, T69, T71, T70, T95, X88, X89, X90)
pI_in_ggggagaa(T88, T70, T69, T71, T95) → U11_ggggagaa(T88, T70, T69, T71, T95, shanoiC_in_gggga(T88, T70, T69, T71))
U11_ggggagaa(T88, T70, T69, T71, T95, shanoiC_out_gggga(T88, T70, T69, T71, T108)) → U12_ggggagaa(T88, T70, T69, T71, T108, T95, pJ_in_gggaga(T95, T69, T71, T108))
U12_ggggagaa(T88, T70, T69, T71, T108, T95, pJ_out_gggaga(T95, T69, T71, X89, T108, X90)) → pI_out_ggggagaa(T88, T70, T69, T71, T108, T95, X89, X90)
pJ_in_gggaga(T95, T69, T71, T108) → U13_gggaga(T95, T69, T71, T108, appendE_in_gga(T95, .(mv(T69, T71), [])))
U13_gggaga(T95, T69, T71, T108, appendE_out_gga(T95, .(mv(T69, T71), []), T119)) → U14_gggaga(T95, T69, T71, T119, T108, appendE_in_gga(T119, T108))
appendE_in_gga([], T130) → appendE_out_gga([], T130, T130)
appendE_in_gga(.(T137, T138), T139) → U3_gga(T137, T138, T139, appendE_in_gga(T138, T139))
U14_gggaga(T95, T69, T71, T119, T108, appendE_out_gga(T119, T108, X90)) → pJ_out_gggaga(T95, T69, T71, T119, T108, X90)
U3_gga(T137, T138, T139, appendE_out_gga(T138, T139, X161)) → appendE_out_gga(.(T137, T138), T139, .(T137, X161))

The set Q consists of the following terms:

shanoiC_in_gggga(x0, x1, x2, x3)
U2_gggga(x0, x1, x2, x3, x4)
pD_in_ggggaaaa(x0, x1, x2, x3)
U9_ggggaaaa(x0, x1, x2, x3, x4)
U10_ggggaaaa(x0, x1, x2, x3, x4, x5)
pI_in_ggggagaa(x0, x1, x2, x3, x4)
U11_ggggagaa(x0, x1, x2, x3, x4, x5)
U12_ggggagaa(x0, x1, x2, x3, x4, x5, x6)
pJ_in_gggaga(x0, x1, x2, x3)
U13_gggaga(x0, x1, x2, x3, x4)
appendE_in_gga(x0, x1)
U14_gggaga(x0, x1, x2, x3, x4, x5)
U3_gga(x0, x1, x2, x3)

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_GGGGAAAA(T88, T69, T71, T70) → SHANOIC_IN_GGGGA(T88, T69, T71, T70)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
PD_IN_GGGGAAAA(T88, T69, T71, T70) → U9_GGGGAAAA(T88, T69, T71, T70, shanoiC_in_gggga(T88, T69, T71, T70))
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
PI_IN_GGGGAGAA(T88, T70, T69, T71, T95) → SHANOIC_IN_GGGGA(T88, T70, T69, T71)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3, 4 >= 4
U9_GGGGAAAA(T88, T69, T71, T70, shanoiC_out_gggga(T88, T69, T71, T70, T95)) → PI_IN_GGGGAGAA(T88, T70, T69, T71, T95)
The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2, 5 > 2, 2 >= 3, 5 > 3, 3 >= 4, 5 > 4, 5 > 5
SHANOIC_IN_GGGGA(s(T88), T69, T70, T71) → PD_IN_GGGGAAAA(T88, T69, T71, T70)
The graph contains the following edges 1 > 1, 2 >= 2, 4 >= 3, 3 >= 4

(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) QDPSizeChangeProof (EQUIVALENT transformation)

(27) YES