Left Termination proof of /tmp/tmpw76AoC/perm.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 (⇒, 148 ms)

↳2 PiTRS

↳3 DependencyPairsProof (⇔, 77 ms)

↳4 PiDP

↳5 DependencyGraphProof (⇔, 12 ms)

↳6 AND

    ↳7 PiDP

        ↳8 UsableRulesProof (⇔, 0 ms)

        ↳9 PiDP

        ↳10 PiDPToQDPProof (⇒, 11 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 (⇔, 13 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 (⇔, 0 ms)

        ↳37 QDP

        ↳38 Instantiation (⇔, 0 ms)

        ↳39 QDP

        ↳40 QDPOrderProof (⇔, 154 ms)

        ↳41 QDP

        ↳42 DependencyGraphProof (⇔, 0 ms)

        ↳43 TRUE

(0) Obligation:

Clauses:

append(nil, XS, XS).
append(cons(X, XS1), XS2, cons(X, YS)) :- append(XS1, XS2, YS).
split(XS, nil, XS).
split(cons(X, XS), cons(X, YS1), YS2) :- split(XS, YS1, YS2).
perm(nil, nil).
perm(XS, cons(Y, YS)) :- ','(split(XS, YS1, cons(Y, YS2)), ','(append(YS1, YS2, ZS), perm(ZS, YS))).

Query: perm(g,a)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: perm(T1, T2)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: 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: true | perm(nil, T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: perm(T1, T2), SCOPE: 1, CLAUSE: 5\n\nT1 is ground\nperm(T1, T2) !=? perm(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
16 [label="16: perm(nil, T2), SCOPE: 1, CLAUSE: 5\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
18 [label="18: ','(split(nil, X7, cons(T7, X8)), ','(append(X7, X8, X9), perm(X9, T8)))\n\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
20 [label="20: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="22: ','(split(nil, X7, cons(T7, X8)), ','(append(X7, X8, X9), perm(X9, T8))), SCOPE: 2, CLAUSE: 2 | ','(split(nil, X7, cons(T7, X8)), ','(append(X7, X8, X9), perm(X9, T8))), SCOPE: 2, CLAUSE: 3\n\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="25: ','(split(nil, X7, cons(T7, X8)), ','(append(X7, X8, X9), perm(X9, T8))), SCOPE: 2, CLAUSE: 3\n\nX7 is free\nX8 is free\nX9 is free", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
29 [label="29: ','(split(T12, X21, cons(T15, X22)), ','(append(X21, X22, X23), perm(X23, T16)))\n\nT12 is ground\nX21 is free\nX22 is free\nX23 is free\nperm(T12, T2) !=? perm(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: ','(split(T12, X21, cons(T15, X22)), ','(append(X21, X22, X23), perm(X23, T16))), SCOPE: 3, CLAUSE: 2 | ','(split(T12, X21, cons(T15, X22)), ','(append(X21, X22, X23), perm(X23, T16))), SCOPE: 3, CLAUSE: 3\n\nT12 is ground\nX21 is free\nX22 is free\nX23 is free\nperm(T12, T2) !=? perm(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
35 [label="35: ','(split(T12, X21, cons(T15, X22)), ','(append(X21, X22, X23), perm(X23, T16))), SCOPE: 3, CLAUSE: 2\n\nT12 is ground\nX21 is free\nX22 is free\nX23 is free\nperm(T12, T2) !=? perm(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
36 [label="36: ','(split(T12, X21, cons(T15, X22)), ','(append(X21, X22, X23), perm(X23, T16))), SCOPE: 3, CLAUSE: 3\n\nT12 is ground\nX21 is free\nX22 is free\nX23 is free\nperm(T12, T2) !=? perm(nil, nil)", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="B: ','(append(nil, T31, X23), perm(X23, T32))\n\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
44 [label="F: append(nil, T31, X23)\n\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: perm(T34, T32)\n\nT34 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: append(nil, T31, X23), SCOPE: 4, CLAUSE: 0 | append(nil, T31, X23), SCOPE: 4, CLAUSE: 1\n\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: append(nil, T31, X23), SCOPE: 4, CLAUSE: 0\n\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: append(nil, T31, X23), SCOPE: 4, CLAUSE: 1\n\nT31 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
59 [label="59: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
60 [label="60: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
70 [label="C: ','(split(T48, X56, cons(T50, X57)), ','(append(cons(T47, X56), X57, X23), perm(X23, T51)))\n\nT47 is ground\nT48 is ground\nX23 is free\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="D: split(T48, X56, cons(T50, X57))\n\nT48 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="H: ','(append(cons(T47, T58), T59, X23), perm(X23, T60))\n\nT47 is ground\nT58 is ground\nT59 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: split(T48, X56, cons(T50, X57)), SCOPE: 5, CLAUSE: 2 | split(T48, X56, cons(T50, X57)), SCOPE: 5, CLAUSE: 3\n\nT48 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: split(T48, X56, cons(T50, X57)), SCOPE: 5, CLAUSE: 2\n\nT48 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: split(T48, X56, cons(T50, X57)), SCOPE: 5, CLAUSE: 3\n\nT48 is ground\nX56 is free\nX57 is free", fontsize=16, style=filled, fillcolor=lightyellow];
85 [label="85: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
86 [label="86: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: split(T89, X83, cons(T91, X84))\n\nT89 is ground\nX83 is free\nX84 is free", fontsize=16, style=filled, fillcolor=lightyellow];
93 [label="93: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
97 [label="G: append(cons(T47, T58), T59, X23)\n\nT47 is ground\nT58 is ground\nT59 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
98 [label="98: perm(T98, T60)\n\nT98 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
99 [label="99: append(cons(T47, T58), T59, X23), SCOPE: 6, CLAUSE: 0 | append(cons(T47, T58), T59, X23), SCOPE: 6, CLAUSE: 1\n\nT47 is ground\nT58 is ground\nT59 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
102 [label="102: append(cons(T47, T58), T59, X23), SCOPE: 6, CLAUSE: 1\n\nT47 is ground\nT58 is ground\nT59 is ground\nX23 is free", fontsize=16, style=filled, fillcolor=lightyellow];
103 [label="E: append(T108, T109, X108)\n\nT108 is ground\nT109 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
104 [label="104: append(T108, T109, X108), SCOPE: 7, CLAUSE: 0 | append(T108, T109, X108), SCOPE: 7, CLAUSE: 1\n\nT108 is ground\nT109 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
105 [label="105: append(T108, T109, X108), SCOPE: 7, CLAUSE: 0\n\nT108 is ground\nT109 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
106 [label="106: append(T108, T109, X108), SCOPE: 7, CLAUSE: 1\n\nT108 is ground\nT109 is ground\nX108 is free", fontsize=16, style=filled, fillcolor=lightyellow];
107 [label="107: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
109 [label="109: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
113 [label="113: append(T124, T125, X130)\n\nT124 is ground\nT125 is ground\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
114 [label="114: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
115 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 115 [arrowhead = none ];
115 -> 6;

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

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

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

119 [label="EVAL with clause\nperm(X18, cons(X19, X20)) :- ','(split(X18, X21, cons(X19, X22)), ','(append(X21, X22, X23), perm(X23, X20))).\nand substitutionT1 -> T12,\nX18 -> T12,\nX19 -> T15,\nX20 -> T16,\nT2 -> cons(T15, T16),\nT13 -> T15,\nT14 -> T16", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 119 [arrowhead = none ];
119 -> 29;

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

121 [label="EVAL with clause\nperm(X4, cons(X5, X6)) :- ','(split(X4, X7, cons(X5, X8)), ','(append(X7, X8, X9), perm(X9, X6))).\nand substitutionX4 -> nil,\nX5 -> T7,\nX6 -> T8,\nT2 -> cons(T7, T8),\nT5 -> T7,\nT6 -> T8", fontsize=14, style = filled, fillcolor = lightblue];
16 -> 121 [arrowhead = none ];
121 -> 18;

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

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

124 [label="BACKTRACK\nfor clause: split(XS, nil, XS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
22 -> 124 [arrowhead = none ];
124 -> 25;

125 [label="BACKTRACK\nfor clause: split(cons(X, XS), cons(X, YS1), YS2) :- split(XS, YS1, YS2)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
25 -> 125 [arrowhead = none ];
125 -> 28;

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

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

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

129 [label="EVAL with clause\nsplit(X28, nil, X28).\nand substitutionT12 -> cons(T30, T31),\nX28 -> cons(T30, T31),\nX21 -> nil,\nT15 -> T30,\nX22 -> T31,\nT29 -> cons(T30, T31),\nT16 -> T32", fontsize=14, style = filled, fillcolor = lightblue];
35 -> 129 [arrowhead = none ];
129 -> 40;

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

131 [label="EVAL with clause\nsplit(cons(X52, X53), cons(X52, X54), X55) :- split(X53, X54, X55).\nand substitutionX52 -> T47,\nX53 -> T48,\nT12 -> cons(T47, T48),\nX54 -> X56,\nX21 -> cons(T47, X56),\nT15 -> T50,\nX22 -> X57,\nX55 -> cons(T50, X57),\nT49 -> T50,\nT16 -> T51", fontsize=14, style = filled, fillcolor = lightblue];
36 -> 131 [arrowhead = none ];
131 -> 70;

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

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

134 [label="SPLIT 2\nnew knowledge:\nT31 is ground\nT34 is ground\nreplacements:X23 -> T34", fontsize=14, style = filled, fillcolor = violet];
40 -> 134 [arrowhead = none ];
134 -> 47;

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

136 [label="INSTANCE with matching:\nT1 -> T34\nT2 -> T32", fontsize=14, style = filled, fillcolor = lightgrey];
47 -> 136 [arrowhead = none , style=dashed];
136 -> 2[style=dashed];

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

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

139 [label="ONLY EVAL with clause\nappend(nil, X35, X35).\nand substitutionT31 -> T40,\nX35 -> T40,\nX23 -> T40", fontsize=14, style = filled, fillcolor = lightblue];
53 -> 139 [arrowhead = none ];
139 -> 59;

140 [label="BACKTRACK\nfor clause: append(cons(X, XS1), XS2, cons(X, YS)) :- append(XS1, XS2, YS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
54 -> 140 [arrowhead = none ];
140 -> 63;

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

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

143 [label="SPLIT 2\nnew knowledge:\nT48 is ground\nT58 is ground\nT50 is ground\nT59 is ground\nreplacements:X56 -> T58,\nX57 -> T59,\nT51 -> T60", fontsize=14, style = filled, fillcolor = violet];
70 -> 143 [arrowhead = none ];
143 -> 75;

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

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

146 [label="SPLIT 2\nnew knowledge:\nT47 is ground\nT58 is ground\nT59 is ground\nT98 is ground\nreplacements:X23 -> T98", fontsize=14, style = filled, fillcolor = violet];
75 -> 146 [arrowhead = none ];
146 -> 98;

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

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

149 [label="EVAL with clause\nsplit(X66, nil, X66).\nand substitutionT48 -> cons(T80, T81),\nX66 -> cons(T80, T81),\nX56 -> nil,\nT50 -> T80,\nX57 -> T81,\nT79 -> cons(T80, T81)", fontsize=14, style = filled, fillcolor = lightblue];
83 -> 149 [arrowhead = none ];
149 -> 85;

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

151 [label="EVAL with clause\nsplit(cons(X79, X80), cons(X79, X81), X82) :- split(X80, X81, X82).\nand substitutionX79 -> T88,\nX80 -> T89,\nT48 -> cons(T88, T89),\nX81 -> X83,\nX56 -> cons(T88, X83),\nT50 -> T91,\nX57 -> X84,\nX82 -> cons(T91, X84),\nT90 -> T91", fontsize=14, style = filled, fillcolor = lightblue];
84 -> 151 [arrowhead = none ];
151 -> 92;

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

153 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
85 -> 153 [arrowhead = none ];
153 -> 87;

154 [label="INSTANCE with matching:\nT48 -> T89\nX56 -> X83\nT50 -> T91\nX57 -> X84", fontsize=14, style = filled, fillcolor = lightgrey];
92 -> 154 [arrowhead = none , style=dashed];
154 -> 74[style=dashed];

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

156 [label="INSTANCE with matching:\nT1 -> T98\nT2 -> T60", fontsize=14, style = filled, fillcolor = lightgrey];
98 -> 156 [arrowhead = none , style=dashed];
156 -> 2[style=dashed];

157 [label="BACKTRACK\nfor clause: append(nil, XS, XS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
99 -> 157 [arrowhead = none ];
157 -> 102;

158 [label="ONLY EVAL with clause\nappend(cons(X104, X105), X106, cons(X104, X107)) :- append(X105, X106, X107).\nand substitutionT47 -> T107,\nX104 -> T107,\nT58 -> T108,\nX105 -> T108,\nT59 -> T109,\nX106 -> T109,\nX107 -> X108,\nX23 -> cons(T107, X108)", fontsize=14, style = filled, fillcolor = lightblue];
102 -> 158 [arrowhead = none ];
158 -> 103;

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

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

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

162 [label="EVAL with clause\nappend(nil, X115, X115).\nand substitutionT108 -> nil,\nT109 -> T116,\nX115 -> T116,\nX108 -> T116", fontsize=14, style = filled, fillcolor = lightblue];
105 -> 162 [arrowhead = none ];
162 -> 107;

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

164 [label="EVAL with clause\nappend(cons(X126, X127), X128, cons(X126, X129)) :- append(X127, X128, X129).\nand substitutionX126 -> T123,\nX127 -> T124,\nT108 -> cons(T123, T124),\nT109 -> T125,\nX128 -> T125,\nX129 -> X130,\nX108 -> cons(T123, X130)", fontsize=14, style = filled, fillcolor = lightblue];
106 -> 164 [arrowhead = none ];
164 -> 113;

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

166 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
107 -> 166 [arrowhead = none ];
166 -> 109;

167 [label="INSTANCE with matching:\nT108 -> T124\nT109 -> T125\nX108 -> X130", fontsize=14, style = filled, fillcolor = lightgrey];
113 -> 167 [arrowhead = none , style=dashed];
167 -> 103[style=dashed];

}

(2) Obligation:

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

permA_in_ga(nil, nil) → permA_out_ga(nil, nil)
permA_in_ga(cons(T30, T31), cons(T30, T32)) → U1_ga(T30, T31, T32, pB_in_gaa(T31, X23, T32))
pB_in_gaa(T31, T34, T32) → U6_gaa(T31, T34, T32, appendF_in_ga(T31, T34))
appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
U6_gaa(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_gaa(T31, T34, T32, permA_in_ga(T34, T32))
permA_in_ga(cons(T47, T48), cons(T50, T51)) → U2_ga(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
pC_in_gaaagaa(T48, T58, T50, T59, T47, X23, T60) → U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
pH_in_gggaa(T47, T58, T59, T98, T60) → U10_gggaa(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U10_gggaa(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_gggaa(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U11_gggaa(T47, T58, T59, T98, T60, permA_out_ga(T98, T60)) → pH_out_gggaa(T47, T58, T59, T98, T60)
U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_out_gggaa(T47, T58, T59, X23, T60)) → pC_out_gaaagaa(T48, T58, T50, T59, T47, X23, T60)
U2_ga(T47, T48, T50, T51, pC_out_gaaagaa(T48, X56, T50, X57, T47, X23, T51)) → permA_out_ga(cons(T47, T48), cons(T50, T51))
U7_gaa(T31, T34, T32, permA_out_ga(T34, T32)) → pB_out_gaa(T31, T34, T32)
U1_ga(T30, T31, T32, pB_out_gaa(T31, X23, T32)) → permA_out_ga(cons(T30, T31), cons(T30, T32))

(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(cons(T30, T31), cons(T30, T32)) → U1_GA(T30, T31, T32, pB_in_gaa(T31, X23, T32))
PERMA_IN_GA(cons(T30, T31), cons(T30, T32)) → PB_IN_GAA(T31, X23, T32)
PB_IN_GAA(T31, T34, T32) → U6_GAA(T31, T34, T32, appendF_in_ga(T31, T34))
PB_IN_GAA(T31, T34, T32) → APPENDF_IN_GA(T31, T34)
U6_GAA(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_GAA(T31, T34, T32, permA_in_ga(T34, T32))
U6_GAA(T31, T34, T32, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34, T32)
PERMA_IN_GA(cons(T47, T48), cons(T50, T51)) → U2_GA(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
PERMA_IN_GA(cons(T47, T48), cons(T50, T51)) → PC_IN_GAAAGAA(T48, X56, T50, X57, T47, X23, T51)
PC_IN_GAAAGAA(T48, T58, T50, T59, T47, X23, T60) → U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
PC_IN_GAAAGAA(T48, T58, T50, T59, T47, X23, T60) → SPLITD_IN_GAAA(T48, T58, T50, T59)
SPLITD_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → U3_GAAA(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
SPLITD_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITD_IN_GAAA(T89, X83, T91, X84)
U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59, X23, T60)
PH_IN_GGGAA(T47, T58, T59, T98, T60) → U10_GGGAA(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
PH_IN_GGGAA(T47, T58, T59, T98, T60) → APPENDG_IN_GGGA(T47, T58, T59, T98)
APPENDG_IN_GGGA(T107, T108, T109, cons(T107, X108)) → U5_GGGA(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
APPENDG_IN_GGGA(T107, T108, T109, cons(T107, X108)) → APPENDE_IN_GGA(T108, T109, X108)
APPENDE_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → U4_GGA(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
APPENDE_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDE_IN_GGA(T124, T125, X130)
U10_GGGAA(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_GGGAA(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U10_GGGAA(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98, T60)

The TRS R consists of the following rules:

permA_in_ga(nil, nil) → permA_out_ga(nil, nil)
permA_in_ga(cons(T30, T31), cons(T30, T32)) → U1_ga(T30, T31, T32, pB_in_gaa(T31, X23, T32))
pB_in_gaa(T31, T34, T32) → U6_gaa(T31, T34, T32, appendF_in_ga(T31, T34))
appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
U6_gaa(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_gaa(T31, T34, T32, permA_in_ga(T34, T32))
permA_in_ga(cons(T47, T48), cons(T50, T51)) → U2_ga(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
pC_in_gaaagaa(T48, T58, T50, T59, T47, X23, T60) → U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
pH_in_gggaa(T47, T58, T59, T98, T60) → U10_gggaa(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U10_gggaa(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_gggaa(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U11_gggaa(T47, T58, T59, T98, T60, permA_out_ga(T98, T60)) → pH_out_gggaa(T47, T58, T59, T98, T60)
U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_out_gggaa(T47, T58, T59, X23, T60)) → pC_out_gaaagaa(T48, T58, T50, T59, T47, X23, T60)
U2_ga(T47, T48, T50, T51, pC_out_gaaagaa(T48, X56, T50, X57, T47, X23, T51)) → permA_out_ga(cons(T47, T48), cons(T50, T51))
U7_gaa(T31, T34, T32, permA_out_ga(T34, T32)) → pB_out_gaa(T31, T34, T32)
U1_ga(T30, T31, T32, pB_out_gaa(T31, X23, T32)) → permA_out_ga(cons(T30, T31), cons(T30, T32))

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2) = permA_in_ga(x1)
nil = nil
permA_out_ga(x1, x2) = permA_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x1, x2, x4)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4) = U6_gaa(x1, x4)
appendF_in_ga(x1, x2) = appendF_in_ga(x1)
appendF_out_ga(x1, x2) = appendF_out_ga(x1, x2)
U7_gaa(x1, x2, x3, x4) = U7_gaa(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x5)
pC_in_gaaagaa(x1, x2, x3, x4, x5, x6, x7) = pC_in_gaaagaa(x1, x5)
U8_gaaagaa(x1, x2, x3, x4, x5, x6, x7, x8) = U8_gaaagaa(x1, x5, x8)
splitD_in_gaaa(x1, x2, x3, x4) = splitD_in_gaaa(x1)
splitD_out_gaaa(x1, x2, x3, x4) = splitD_out_gaaa(x1, x2, x3, x4)
U3_gaaa(x1, x2, x3, x4, x5, x6) = U3_gaaa(x1, x2, x6)
U9_gaaagaa(x1, x2, x3, x4, x5, x6, x7, x8) = U9_gaaagaa(x1, x2, x3, x4, x5, x8)
pH_in_gggaa(x1, x2, x3, x4, x5) = pH_in_gggaa(x1, x2, x3)
U10_gggaa(x1, x2, x3, x4, x5, x6) = U10_gggaa(x1, x2, x3, x6)
appendG_in_ggga(x1, x2, x3, x4) = appendG_in_ggga(x1, x2, x3)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
appendG_out_ggga(x1, x2, x3, x4) = appendG_out_ggga(x1, x2, x3, x4)
U11_gggaa(x1, x2, x3, x4, x5, x6) = U11_gggaa(x1, x2, x3, x4, x6)
pH_out_gggaa(x1, x2, x3, x4, x5) = pH_out_gggaa(x1, x2, x3, x4, x5)
pC_out_gaaagaa(x1, x2, x3, x4, x5, x6, x7) = pC_out_gaaagaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
PERMA_IN_GA(x1, x2) = PERMA_IN_GA(x1)
U1_GA(x1, x2, x3, x4) = U1_GA(x1, x2, x4)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4) = U6_GAA(x1, x4)
APPENDF_IN_GA(x1, x2) = APPENDF_IN_GA(x1)
U7_GAA(x1, x2, x3, x4) = U7_GAA(x1, x2, x4)
U2_GA(x1, x2, x3, x4, x5) = U2_GA(x1, x2, x5)
PC_IN_GAAAGAA(x1, x2, x3, x4, x5, x6, x7) = PC_IN_GAAAGAA(x1, x5)
U8_GAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GAAAGAA(x1, x5, x8)
SPLITD_IN_GAAA(x1, x2, x3, x4) = SPLITD_IN_GAAA(x1)
U3_GAAA(x1, x2, x3, x4, x5, x6) = U3_GAAA(x1, x2, x6)
U9_GAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U9_GAAAGAA(x1, x2, x3, x4, x5, x8)
PH_IN_GGGAA(x1, x2, x3, x4, x5) = PH_IN_GGGAA(x1, x2, x3)
U10_GGGAA(x1, x2, x3, x4, x5, x6) = U10_GGGAA(x1, x2, x3, x6)
APPENDG_IN_GGGA(x1, x2, x3, x4) = APPENDG_IN_GGGA(x1, x2, x3)
U5_GGGA(x1, x2, x3, x4, x5) = U5_GGGA(x1, x2, x3, x5)
APPENDE_IN_GGA(x1, x2, x3) = APPENDE_IN_GGA(x1, x2)
U4_GGA(x1, x2, x3, x4, x5) = U4_GGA(x1, x2, x3, x5)
U11_GGGAA(x1, x2, x3, x4, x5, x6) = U11_GGGAA(x1, x2, x3, x4, x6)

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(cons(T30, T31), cons(T30, T32)) → U1_GA(T30, T31, T32, pB_in_gaa(T31, X23, T32))
PERMA_IN_GA(cons(T30, T31), cons(T30, T32)) → PB_IN_GAA(T31, X23, T32)
PB_IN_GAA(T31, T34, T32) → U6_GAA(T31, T34, T32, appendF_in_ga(T31, T34))
PB_IN_GAA(T31, T34, T32) → APPENDF_IN_GA(T31, T34)
U6_GAA(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_GAA(T31, T34, T32, permA_in_ga(T34, T32))
U6_GAA(T31, T34, T32, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34, T32)
PERMA_IN_GA(cons(T47, T48), cons(T50, T51)) → U2_GA(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
PERMA_IN_GA(cons(T47, T48), cons(T50, T51)) → PC_IN_GAAAGAA(T48, X56, T50, X57, T47, X23, T51)
PC_IN_GAAAGAA(T48, T58, T50, T59, T47, X23, T60) → U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
PC_IN_GAAAGAA(T48, T58, T50, T59, T47, X23, T60) → SPLITD_IN_GAAA(T48, T58, T50, T59)
SPLITD_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → U3_GAAA(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
SPLITD_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITD_IN_GAAA(T89, X83, T91, X84)
U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59, X23, T60)
PH_IN_GGGAA(T47, T58, T59, T98, T60) → U10_GGGAA(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
PH_IN_GGGAA(T47, T58, T59, T98, T60) → APPENDG_IN_GGGA(T47, T58, T59, T98)
APPENDG_IN_GGGA(T107, T108, T109, cons(T107, X108)) → U5_GGGA(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
APPENDG_IN_GGGA(T107, T108, T109, cons(T107, X108)) → APPENDE_IN_GGA(T108, T109, X108)
APPENDE_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → U4_GGA(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
APPENDE_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDE_IN_GGA(T124, T125, X130)
U10_GGGAA(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_GGGAA(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U10_GGGAA(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98, T60)

The TRS R consists of the following rules:

permA_in_ga(nil, nil) → permA_out_ga(nil, nil)
permA_in_ga(cons(T30, T31), cons(T30, T32)) → U1_ga(T30, T31, T32, pB_in_gaa(T31, X23, T32))
pB_in_gaa(T31, T34, T32) → U6_gaa(T31, T34, T32, appendF_in_ga(T31, T34))
appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
U6_gaa(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_gaa(T31, T34, T32, permA_in_ga(T34, T32))
permA_in_ga(cons(T47, T48), cons(T50, T51)) → U2_ga(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
pC_in_gaaagaa(T48, T58, T50, T59, T47, X23, T60) → U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
pH_in_gggaa(T47, T58, T59, T98, T60) → U10_gggaa(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U10_gggaa(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_gggaa(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U11_gggaa(T47, T58, T59, T98, T60, permA_out_ga(T98, T60)) → pH_out_gggaa(T47, T58, T59, T98, T60)
U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_out_gggaa(T47, T58, T59, X23, T60)) → pC_out_gaaagaa(T48, T58, T50, T59, T47, X23, T60)
U2_ga(T47, T48, T50, T51, pC_out_gaaagaa(T48, X56, T50, X57, T47, X23, T51)) → permA_out_ga(cons(T47, T48), cons(T50, T51))
U7_gaa(T31, T34, T32, permA_out_ga(T34, T32)) → pB_out_gaa(T31, T34, T32)
U1_ga(T30, T31, T32, pB_out_gaa(T31, X23, T32)) → permA_out_ga(cons(T30, T31), cons(T30, T32))

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

APPENDE_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDE_IN_GGA(T124, T125, X130)

The TRS R consists of the following rules:

permA_in_ga(nil, nil) → permA_out_ga(nil, nil)
permA_in_ga(cons(T30, T31), cons(T30, T32)) → U1_ga(T30, T31, T32, pB_in_gaa(T31, X23, T32))
pB_in_gaa(T31, T34, T32) → U6_gaa(T31, T34, T32, appendF_in_ga(T31, T34))
appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
U6_gaa(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_gaa(T31, T34, T32, permA_in_ga(T34, T32))
permA_in_ga(cons(T47, T48), cons(T50, T51)) → U2_ga(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
pC_in_gaaagaa(T48, T58, T50, T59, T47, X23, T60) → U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
pH_in_gggaa(T47, T58, T59, T98, T60) → U10_gggaa(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U10_gggaa(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_gggaa(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U11_gggaa(T47, T58, T59, T98, T60, permA_out_ga(T98, T60)) → pH_out_gggaa(T47, T58, T59, T98, T60)
U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_out_gggaa(T47, T58, T59, X23, T60)) → pC_out_gaaagaa(T48, T58, T50, T59, T47, X23, T60)
U2_ga(T47, T48, T50, T51, pC_out_gaaagaa(T48, X56, T50, X57, T47, X23, T51)) → permA_out_ga(cons(T47, T48), cons(T50, T51))
U7_gaa(T31, T34, T32, permA_out_ga(T34, T32)) → pB_out_gaa(T31, T34, T32)
U1_ga(T30, T31, T32, pB_out_gaa(T31, X23, T32)) → permA_out_ga(cons(T30, T31), cons(T30, T32))

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

APPENDE_IN_GGA(cons(T123, T124), T125, cons(T123, X130)) → APPENDE_IN_GGA(T124, T125, X130)

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

APPENDE_IN_GGA(cons(T123, T124), T125) → APPENDE_IN_GGA(T124, T125)

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:

APPENDE_IN_GGA(cons(T123, T124), T125) → APPENDE_IN_GGA(T124, T125)
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:

SPLITD_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITD_IN_GAAA(T89, X83, T91, X84)

The TRS R consists of the following rules:

permA_in_ga(nil, nil) → permA_out_ga(nil, nil)
permA_in_ga(cons(T30, T31), cons(T30, T32)) → U1_ga(T30, T31, T32, pB_in_gaa(T31, X23, T32))
pB_in_gaa(T31, T34, T32) → U6_gaa(T31, T34, T32, appendF_in_ga(T31, T34))
appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
U6_gaa(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_gaa(T31, T34, T32, permA_in_ga(T34, T32))
permA_in_ga(cons(T47, T48), cons(T50, T51)) → U2_ga(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
pC_in_gaaagaa(T48, T58, T50, T59, T47, X23, T60) → U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
pH_in_gggaa(T47, T58, T59, T98, T60) → U10_gggaa(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U10_gggaa(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_gggaa(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U11_gggaa(T47, T58, T59, T98, T60, permA_out_ga(T98, T60)) → pH_out_gggaa(T47, T58, T59, T98, T60)
U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_out_gggaa(T47, T58, T59, X23, T60)) → pC_out_gaaagaa(T48, T58, T50, T59, T47, X23, T60)
U2_ga(T47, T48, T50, T51, pC_out_gaaagaa(T48, X56, T50, X57, T47, X23, T51)) → permA_out_ga(cons(T47, T48), cons(T50, T51))
U7_gaa(T31, T34, T32, permA_out_ga(T34, T32)) → pB_out_gaa(T31, T34, T32)
U1_ga(T30, T31, T32, pB_out_gaa(T31, X23, T32)) → permA_out_ga(cons(T30, T31), cons(T30, T32))

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

SPLITD_IN_GAAA(cons(T88, T89), cons(T88, X83), T91, X84) → SPLITD_IN_GAAA(T89, X83, T91, X84)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

SPLITD_IN_GAAA(cons(T88, T89)) → SPLITD_IN_GAAA(T89)

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:

SPLITD_IN_GAAA(cons(T88, T89)) → SPLITD_IN_GAAA(T89)
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(cons(T30, T31), cons(T30, T32)) → PB_IN_GAA(T31, X23, T32)
PB_IN_GAA(T31, T34, T32) → U6_GAA(T31, T34, T32, appendF_in_ga(T31, T34))
U6_GAA(T31, T34, T32, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34, T32)
PERMA_IN_GA(cons(T47, T48), cons(T50, T51)) → PC_IN_GAAAGAA(T48, X56, T50, X57, T47, X23, T51)
PC_IN_GAAAGAA(T48, T58, T50, T59, T47, X23, T60) → U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59, X23, T60)
PH_IN_GGGAA(T47, T58, T59, T98, T60) → U10_GGGAA(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
U10_GGGAA(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98, T60)

The TRS R consists of the following rules:

permA_in_ga(nil, nil) → permA_out_ga(nil, nil)
permA_in_ga(cons(T30, T31), cons(T30, T32)) → U1_ga(T30, T31, T32, pB_in_gaa(T31, X23, T32))
pB_in_gaa(T31, T34, T32) → U6_gaa(T31, T34, T32, appendF_in_ga(T31, T34))
appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
U6_gaa(T31, T34, T32, appendF_out_ga(T31, T34)) → U7_gaa(T31, T34, T32, permA_in_ga(T34, T32))
permA_in_ga(cons(T47, T48), cons(T50, T51)) → U2_ga(T47, T48, T50, T51, pC_in_gaaagaa(T48, X56, T50, X57, T47, X23, T51))
pC_in_gaaagaa(T48, T58, T50, T59, T47, X23, T60) → U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U8_gaaagaa(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_in_gggaa(T47, T58, T59, X23, T60))
pH_in_gggaa(T47, T58, T59, T98, T60) → U10_gggaa(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U10_gggaa(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → U11_gggaa(T47, T58, T59, T98, T60, permA_in_ga(T98, T60))
U11_gggaa(T47, T58, T59, T98, T60, permA_out_ga(T98, T60)) → pH_out_gggaa(T47, T58, T59, T98, T60)
U9_gaaagaa(T48, T58, T50, T59, T47, X23, T60, pH_out_gggaa(T47, T58, T59, X23, T60)) → pC_out_gaaagaa(T48, T58, T50, T59, T47, X23, T60)
U2_ga(T47, T48, T50, T51, pC_out_gaaagaa(T48, X56, T50, X57, T47, X23, T51)) → permA_out_ga(cons(T47, T48), cons(T50, T51))
U7_gaa(T31, T34, T32, permA_out_ga(T34, T32)) → pB_out_gaa(T31, T34, T32)
U1_ga(T30, T31, T32, pB_out_gaa(T31, X23, T32)) → permA_out_ga(cons(T30, T31), cons(T30, T32))

The argument filtering Pi contains the following mapping:
permA_in_ga(x1, x2) = permA_in_ga(x1)
nil = nil
permA_out_ga(x1, x2) = permA_out_ga(x1, x2)
cons(x1, x2) = cons(x1, x2)
U1_ga(x1, x2, x3, x4) = U1_ga(x1, x2, x4)
pB_in_gaa(x1, x2, x3) = pB_in_gaa(x1)
U6_gaa(x1, x2, x3, x4) = U6_gaa(x1, x4)
appendF_in_ga(x1, x2) = appendF_in_ga(x1)
appendF_out_ga(x1, x2) = appendF_out_ga(x1, x2)
U7_gaa(x1, x2, x3, x4) = U7_gaa(x1, x2, x4)
U2_ga(x1, x2, x3, x4, x5) = U2_ga(x1, x2, x5)
pC_in_gaaagaa(x1, x2, x3, x4, x5, x6, x7) = pC_in_gaaagaa(x1, x5)
U8_gaaagaa(x1, x2, x3, x4, x5, x6, x7, x8) = U8_gaaagaa(x1, x5, x8)
splitD_in_gaaa(x1, x2, x3, x4) = splitD_in_gaaa(x1)
splitD_out_gaaa(x1, x2, x3, x4) = splitD_out_gaaa(x1, x2, x3, x4)
U3_gaaa(x1, x2, x3, x4, x5, x6) = U3_gaaa(x1, x2, x6)
U9_gaaagaa(x1, x2, x3, x4, x5, x6, x7, x8) = U9_gaaagaa(x1, x2, x3, x4, x5, x8)
pH_in_gggaa(x1, x2, x3, x4, x5) = pH_in_gggaa(x1, x2, x3)
U10_gggaa(x1, x2, x3, x4, x5, x6) = U10_gggaa(x1, x2, x3, x6)
appendG_in_ggga(x1, x2, x3, x4) = appendG_in_ggga(x1, x2, x3)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
appendG_out_ggga(x1, x2, x3, x4) = appendG_out_ggga(x1, x2, x3, x4)
U11_gggaa(x1, x2, x3, x4, x5, x6) = U11_gggaa(x1, x2, x3, x4, x6)
pH_out_gggaa(x1, x2, x3, x4, x5) = pH_out_gggaa(x1, x2, x3, x4, x5)
pC_out_gaaagaa(x1, x2, x3, x4, x5, x6, x7) = pC_out_gaaagaa(x1, x2, x3, x4, x5, x6, x7)
pB_out_gaa(x1, x2, x3) = pB_out_gaa(x1, x2, x3)
PERMA_IN_GA(x1, x2) = PERMA_IN_GA(x1)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4) = U6_GAA(x1, x4)
PC_IN_GAAAGAA(x1, x2, x3, x4, x5, x6, x7) = PC_IN_GAAAGAA(x1, x5)
U8_GAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GAAAGAA(x1, x5, x8)
PH_IN_GGGAA(x1, x2, x3, x4, x5) = PH_IN_GGGAA(x1, x2, x3)
U10_GGGAA(x1, x2, x3, x4, x5, x6) = U10_GGGAA(x1, x2, x3, x6)

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(cons(T30, T31), cons(T30, T32)) → PB_IN_GAA(T31, X23, T32)
PB_IN_GAA(T31, T34, T32) → U6_GAA(T31, T34, T32, appendF_in_ga(T31, T34))
U6_GAA(T31, T34, T32, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34, T32)
PERMA_IN_GA(cons(T47, T48), cons(T50, T51)) → PC_IN_GAAAGAA(T48, X56, T50, X57, T47, X23, T51)
PC_IN_GAAAGAA(T48, T58, T50, T59, T47, X23, T60) → U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_in_gaaa(T48, T58, T50, T59))
U8_GAAAGAA(T48, T58, T50, T59, T47, X23, T60, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59, X23, T60)
PH_IN_GGGAA(T47, T58, T59, T98, T60) → U10_GGGAA(T47, T58, T59, T98, T60, appendG_in_ggga(T47, T58, T59, T98))
U10_GGGAA(T47, T58, T59, T98, T60, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98, T60)

The TRS R consists of the following rules:

appendF_in_ga(T40, T40) → appendF_out_ga(T40, T40)
splitD_in_gaaa(cons(T80, T81), nil, T80, T81) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89), cons(T88, X83), T91, X84) → U3_gaaa(T88, T89, X83, T91, X84, splitD_in_gaaa(T89, X83, T91, X84))
appendG_in_ggga(T107, T108, T109, cons(T107, X108)) → U5_ggga(T107, T108, T109, X108, appendE_in_gga(T108, T109, X108))
U3_gaaa(T88, T89, X83, T91, X84, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U5_ggga(T107, T108, T109, X108, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
appendE_in_gga(nil, T116, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125, cons(T123, X130)) → U4_gga(T123, T124, T125, X130, appendE_in_gga(T124, T125, X130))
U4_gga(T123, T124, T125, X130, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))

The argument filtering Pi contains the following mapping:
nil = nil
cons(x1, x2) = cons(x1, x2)
appendF_in_ga(x1, x2) = appendF_in_ga(x1)
appendF_out_ga(x1, x2) = appendF_out_ga(x1, x2)
splitD_in_gaaa(x1, x2, x3, x4) = splitD_in_gaaa(x1)
splitD_out_gaaa(x1, x2, x3, x4) = splitD_out_gaaa(x1, x2, x3, x4)
U3_gaaa(x1, x2, x3, x4, x5, x6) = U3_gaaa(x1, x2, x6)
appendG_in_ggga(x1, x2, x3, x4) = appendG_in_ggga(x1, x2, x3)
U5_ggga(x1, x2, x3, x4, x5) = U5_ggga(x1, x2, x3, x5)
appendE_in_gga(x1, x2, x3) = appendE_in_gga(x1, x2)
appendE_out_gga(x1, x2, x3) = appendE_out_gga(x1, x2, x3)
U4_gga(x1, x2, x3, x4, x5) = U4_gga(x1, x2, x3, x5)
appendG_out_ggga(x1, x2, x3, x4) = appendG_out_ggga(x1, x2, x3, x4)
PERMA_IN_GA(x1, x2) = PERMA_IN_GA(x1)
PB_IN_GAA(x1, x2, x3) = PB_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4) = U6_GAA(x1, x4)
PC_IN_GAAAGAA(x1, x2, x3, x4, x5, x6, x7) = PC_IN_GAAAGAA(x1, x5)
U8_GAAAGAA(x1, x2, x3, x4, x5, x6, x7, x8) = U8_GAAAGAA(x1, x5, x8)
PH_IN_GGGAA(x1, x2, x3, x4, x5) = PH_IN_GGGAA(x1, x2, x3)
U10_GGGAA(x1, x2, x3, x4, x5, x6) = U10_GGGAA(x1, x2, x3, 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:

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_in_ga(T31))
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, appendG_in_ggga(T47, T58, T59))
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)

The TRS R consists of the following rules:

appendF_in_ga(T40) → appendF_out_ga(T40, T40)
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
appendG_in_ggga(T107, T108, T109) → U5_ggga(T107, T108, T109, appendE_in_gga(T108, T109))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))

The set Q consists of the following terms:

appendF_in_ga(x0)
splitD_in_gaaa(x0)
appendG_in_ggga(x0, x1, x2)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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 PB_IN_GAA(T31) → U6_GAA(T31, appendF_in_ga(T31)) at position [1] we obtained the following new rules [LPAR04]:

PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))

(27) Obligation:

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

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, appendG_in_ggga(T47, T58, T59))
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))

The TRS R consists of the following rules:

appendF_in_ga(T40) → appendF_out_ga(T40, T40)
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
appendG_in_ggga(T107, T108, T109) → U5_ggga(T107, T108, T109, appendE_in_gga(T108, T109))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))

The set Q consists of the following terms:

appendF_in_ga(x0)
splitD_in_gaaa(x0)
appendG_in_ggga(x0, x1, x2)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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(cons(T30, T31)) → PB_IN_GAA(T31)
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, appendG_in_ggga(T47, T58, T59))
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))

The TRS R consists of the following rules:

appendG_in_ggga(T107, T108, T109) → U5_ggga(T107, T108, T109, appendE_in_gga(T108, T109))
appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

appendF_in_ga(x0)
splitD_in_gaaa(x0)
appendG_in_ggga(x0, x1, x2)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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].

appendF_in_ga(x0)

(31) Obligation:

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

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, appendG_in_ggga(T47, T58, T59))
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))

The TRS R consists of the following rules:

appendG_in_ggga(T107, T108, T109) → U5_ggga(T107, T108, T109, appendE_in_gga(T108, T109))
appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

splitD_in_gaaa(x0)
appendG_in_ggga(x0, x1, x2)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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 PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, appendG_in_ggga(T47, T58, T59)) at position [3] we obtained the following new rules [LPAR04]:

PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, U5_ggga(T47, T58, T59, appendE_in_gga(T58, T59)))

(33) Obligation:

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

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, U5_ggga(T47, T58, T59, appendE_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendG_in_ggga(T107, T108, T109) → U5_ggga(T107, T108, T109, appendE_in_gga(T108, T109))
appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

splitD_in_gaaa(x0)
appendG_in_ggga(x0, x1, x2)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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(cons(T30, T31)) → PB_IN_GAA(T31)
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, U5_ggga(T47, T58, T59, appendE_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

splitD_in_gaaa(x0)
appendG_in_ggga(x0, x1, x2)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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].

appendG_in_ggga(x0, x1, x2)

(37) Obligation:

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

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, U5_ggga(T47, T58, T59, appendE_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

splitD_in_gaaa(x0)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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 U6_GAA(T31, appendF_out_ga(T31, T34)) → PERMA_IN_GA(T34) we obtained the following new rules [LPAR04]:

U6_GAA(z0, appendF_out_ga(z0, z0)) → PERMA_IN_GA(z0)

(39) Obligation:

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

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, U5_ggga(T47, T58, T59, appendE_in_gga(T58, T59)))
U6_GAA(z0, appendF_out_ga(z0, z0)) → PERMA_IN_GA(z0)

The TRS R consists of the following rules:

appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

splitD_in_gaaa(x0)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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.

PC_IN_GAAAGAA(T48, T47) → U8_GAAAGAA(T48, T47, splitD_in_gaaa(T48))
U6_GAA(z0, appendF_out_ga(z0, z0)) → PERMA_IN_GA(z0)

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

POL(PB_IN_GAA(x₁)) = 1 + x₁
POL(PC_IN_GAAAGAA(x₁, x₂)) = 1 + x₁
POL(PERMA_IN_GA(x₁)) = x₁
POL(PH_IN_GGGAA(x₁, x₂, x₃)) = x₂ + x₃
POL(U10_GGGAA(x₁, x₂, x₃, x₄)) = x₄
POL(U3_gaaa(x₁, x₂, x₃)) = 1 + x₃
POL(U4_gga(x₁, x₂, x₃, x₄)) = 1 + x₄
POL(U5_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(U6_GAA(x₁, x₂)) = x₂
POL(U8_GAAAGAA(x₁, x₂, x₃)) = x₃
POL(appendE_in_gga(x₁, x₂)) = x₁ + x₂
POL(appendE_out_gga(x₁, x₂, x₃)) = 1 + x₃
POL(appendF_out_ga(x₁, x₂)) = 1 + x₁
POL(appendG_out_ggga(x₁, x₂, x₃, x₄)) = x₄
POL(cons(x₁, x₂)) = 1 + x₂
POL(nil) = 1
POL(splitD_in_gaaa(x₁)) = x₁
POL(splitD_out_gaaa(x₁, x₂, x₃, x₄)) = x₂ + x₄

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

splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

(41) Obligation:

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

PERMA_IN_GA(cons(T30, T31)) → PB_IN_GAA(T31)
PERMA_IN_GA(cons(T47, T48)) → PC_IN_GAAAGAA(T48, T47)
U8_GAAAGAA(T48, T47, splitD_out_gaaa(T48, T58, T50, T59)) → PH_IN_GGGAA(T47, T58, T59)
U10_GGGAA(T47, T58, T59, appendG_out_ggga(T47, T58, T59, T98)) → PERMA_IN_GA(T98)
PB_IN_GAA(T31) → U6_GAA(T31, appendF_out_ga(T31, T31))
PH_IN_GGGAA(T47, T58, T59) → U10_GGGAA(T47, T58, T59, U5_ggga(T47, T58, T59, appendE_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendE_in_gga(nil, T116) → appendE_out_gga(nil, T116, T116)
appendE_in_gga(cons(T123, T124), T125) → U4_gga(T123, T124, T125, appendE_in_gga(T124, T125))
U5_ggga(T107, T108, T109, appendE_out_gga(T108, T109, X108)) → appendG_out_ggga(T107, T108, T109, cons(T107, X108))
U4_gga(T123, T124, T125, appendE_out_gga(T124, T125, X130)) → appendE_out_gga(cons(T123, T124), T125, cons(T123, X130))
splitD_in_gaaa(cons(T80, T81)) → splitD_out_gaaa(cons(T80, T81), nil, T80, T81)
splitD_in_gaaa(cons(T88, T89)) → U3_gaaa(T88, T89, splitD_in_gaaa(T89))
U3_gaaa(T88, T89, splitD_out_gaaa(T89, X83, T91, X84)) → splitD_out_gaaa(cons(T88, T89), cons(T88, X83), T91, X84)

The set Q consists of the following terms:

splitD_in_gaaa(x0)
U3_gaaa(x0, x1, x2)
U5_ggga(x0, x1, x2, x3)
appendE_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