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

(0) Obligation:

Clauses:

append([], XS, XS).
append(.(X, XS), YS, .(X, ZS)) :- append(XS, YS, ZS).
s2l(s(X), .(Y, Xs)) :- s2l(X, Xs).
s2l(0, []).
goal(X) :- ','(s2l(X, XS), append(XS, YS, ZS)).

Query: goal(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
2 [label="A: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: goal(T1), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(s2l(T3, X3), append(X3, X4, X5))\n\nT3 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
10 [label="10: ','(s2l(T3, X3), append(X3, X4, X5)), SCOPE: 2, CLAUSE: 2 | ','(s2l(T3, X3), append(X3, X4, X5)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(s2l(T3, X3), append(X3, X4, X5)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(s2l(T3, X3), append(X3, X4, X5)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="B: ','(s2l(T8, X30), append(.(X29, X30), X4, X5))\n\nT8 is ground\nX4 is free\nX5 is free\nX29 is free\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
21 [label="21: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="C: s2l(T8, X30)\n\nT8 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="E: append(.(X29, T10), X4, X5)\n\nX4 is free\nX5 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: s2l(T8, X30), SCOPE: 3, CLAUSE: 2 | s2l(T8, X30), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: s2l(T8, X30), SCOPE: 3, CLAUSE: 2\n\nT8 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: s2l(T8, X30), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX30 is free", fontsize=16, style=filled, fillcolor=lightyellow];
38 [label="38: s2l(T16, X65)\n\nT16 is ground\nX65 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
41 [label="41: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
45 [label="45: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: append(.(X29, T10), X4, X5), SCOPE: 4, CLAUSE: 0 | append(.(X29, T10), X4, X5), SCOPE: 4, CLAUSE: 1\n\nX4 is free\nX5 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
50 [label="50: append(.(X29, T10), X4, X5), SCOPE: 4, CLAUSE: 1\n\nX4 is free\nX5 is free\nX29 is free", fontsize=16, style=filled, fillcolor=lightyellow];
58 [label="D: append(T22, X97, X98)\n\nX97 is free\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="63: append(T22, X97, X98), SCOPE: 5, CLAUSE: 0 | append(T22, X97, X98), SCOPE: 5, CLAUSE: 1\n\nX97 is free\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
66 [label="66: append(T22, X97, X98), SCOPE: 5, CLAUSE: 0\n\nX97 is free\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
67 [label="67: append(T22, X97, X98), SCOPE: 5, CLAUSE: 1\n\nX97 is free\nX98 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
73 [label="73: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
76 [label="76: append(T29, X129, X130)\n\nX129 is free\nX130 is free", fontsize=16, style=filled, fillcolor=lightyellow];
77 [label="77: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
81 [label="81: append([], X4, X5)\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
84 [label="84: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: append([], X4, X5), SCOPE: 6, CLAUSE: 0 | append([], X4, X5), SCOPE: 6, CLAUSE: 1\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: append([], X4, X5), SCOPE: 6, CLAUSE: 0\n\nX4 is free\nX5 is free", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: append([], X4, X5), SCOPE: 6, CLAUSE: 1\n\nX4 is free\nX5 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];
96 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
2 -> 96 [arrowhead = none ];
96 -> 6;

97 [label="ONLY EVAL with clause\ngoal(X2) :- ','(s2l(X2, X3), append(X3, X4, X5)).\nand substitutionT1 -> T3,\nX2 -> T3", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 97 [arrowhead = none ];
97 -> 8;

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

99 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 99 [arrowhead = none ];
99 -> 13;

100 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
10 -> 100 [arrowhead = none ];
100 -> 15;

101 [label="EVAL with clause\ns2l(s(X26), .(X27, X28)) :- s2l(X26, X28).\nand substitutionX26 -> T8,\nT3 -> s(T8),\nX27 -> X29,\nX28 -> X30,\nX3 -> .(X29, X30)", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 101 [arrowhead = none ];
101 -> 17;

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

103 [label="EVAL with clause\ns2l(0, []).\nand substitutionT3 -> 0,\nX3 -> []", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 103 [arrowhead = none ];
103 -> 81;

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

105 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
17 -> 105 [arrowhead = none ];
105 -> 24;

106 [label="SPLIT 2\nnew knowledge:\nT8 is ground\nreplacements:X30 -> T10", fontsize=14, style = filled, fillcolor = violet];
17 -> 106 [arrowhead = none ];
106 -> 26;

107 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
24 -> 107 [arrowhead = none ];
107 -> 30;

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

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

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

111 [label="EVAL with clause\ns2l(s(X61), .(X62, X63)) :- s2l(X61, X63).\nand substitutionX61 -> T16,\nT8 -> s(T16),\nX62 -> X64,\nX63 -> X65,\nX30 -> .(X64, X65)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 111 [arrowhead = none ];
111 -> 38;

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

113 [label="EVAL with clause\ns2l(0, []).\nand substitutionT8 -> 0,\nX30 -> []", fontsize=14, style = filled, fillcolor = lightblue];
34 -> 113 [arrowhead = none ];
113 -> 41;

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

115 [label="INSTANCE with matching:\nT8 -> T16\nX30 -> X65", fontsize=14, style = filled, fillcolor = lightgrey];
38 -> 115 [arrowhead = none , style=dashed];
115 -> 24[style=dashed];

116 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
41 -> 116 [arrowhead = none ];
116 -> 45;

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

118 [label="ONLY EVAL with clause\nappend(.(X92, X93), X94, .(X92, X95)) :- append(X93, X94, X95).\nand substitutionX29 -> X96,\nX92 -> X96,\nT10 -> T22,\nX93 -> T22,\nX4 -> X97,\nX94 -> X97,\nX95 -> X98,\nX5 -> .(X96, X98),\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
50 -> 118 [arrowhead = none ];
118 -> 58;

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

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

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

122 [label="EVAL with clause\nappend([], X111, X111).\nand substitutionT22 -> [],\nX97 -> X112,\nX111 -> X112,\nX98 -> X112", fontsize=14, style = filled, fillcolor = lightblue];
66 -> 122 [arrowhead = none ];
122 -> 71;

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

124 [label="EVAL with clause\nappend(.(X125, X126), X127, .(X125, X128)) :- append(X126, X127, X128).\nand substitutionX125 -> T27,\nX126 -> T29,\nT22 -> .(T27, T29),\nX97 -> X129,\nX127 -> X129,\nX128 -> X130,\nX98 -> .(T27, X130),\nT28 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
67 -> 124 [arrowhead = none ];
124 -> 76;

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

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

127 [label="INSTANCE with matching:\nT22 -> T29\nX97 -> X129\nX98 -> X130", fontsize=14, style = filled, fillcolor = lightgrey];
76 -> 127 [arrowhead = none , style=dashed];
127 -> 58[style=dashed];

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

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

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

131 [label="ONLY EVAL with clause\nappend([], X145, X145).\nand substitutionX4 -> X146,\nX145 -> X146,\nX5 -> X146", fontsize=14, style = filled, fillcolor = lightblue];
90 -> 131 [arrowhead = none ];
131 -> 93;

132 [label="BACKTRACK\nfor clause: append(.(X, XS), YS, .(X, ZS)) :- append(XS, YS, ZS)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 132 [arrowhead = none ];
132 -> 95;

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

}

(2) Obligation:

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

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
pB_in_gaaaa(T8, T10, X29, X4, X5) → U5_gaaaa(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X64, X65)) → U2_ga(T16, X64, X65, s2lC_in_ga(T16, X65))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X64, X65, s2lC_out_ga(T16, X65)) → s2lC_out_ga(s(T16), .(X64, X65))
U5_gaaaa(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_gaaaa(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
appendE_in_agaa(X96, T22, X97, .(X96, X98)) → U4_agaa(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
appendD_in_gaa([], X112, X112) → appendD_out_gaa([], X112, X112)
appendD_in_gaa(.(T27, T29), X129, .(T27, X130)) → U3_gaa(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
U3_gaa(T27, T29, X129, X130, appendD_out_gaa(T29, X129, X130)) → appendD_out_gaa(.(T27, T29), X129, .(T27, X130))
U4_agaa(X96, T22, X97, X98, appendD_out_gaa(T22, X97, X98)) → appendE_out_agaa(X96, T22, X97, .(X96, X98))
U6_gaaaa(T8, T10, X29, X4, X5, appendE_out_agaa(X29, T10, X4, X5)) → pB_out_gaaaa(T8, T10, X29, X4, X5)
U1_g(T8, pB_out_gaaaa(T8, X30, X29, X4, X5)) → goalA_out_g(s(T8))
goalA_in_g(0) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U5_gaaaa(x1, x2, x3, x4, x5, x6)  =  U5_gaaaa(x1, x6)
s2lC_in_ga(x1, x2)  =  s2lC_in_ga(x1)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x4)
0  =  0
s2lC_out_ga(x1, x2)  =  s2lC_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U6_gaaaa(x1, x2, x3, x4, x5, x6)  =  U6_gaaaa(x1, x2, x6)
appendE_in_agaa(x1, x2, x3, x4)  =  appendE_in_agaa(x2)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
appendD_in_gaa(x1, x2, x3)  =  appendD_in_gaa(x1)
[]  =  []
appendD_out_gaa(x1, x2, x3)  =  appendD_out_gaa(x1)
U3_gaa(x1, x2, x3, x4, x5)  =  U3_gaa(x2, x5)
appendE_out_agaa(x1, x2, x3, x4)  =  appendE_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)

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

GOALA_IN_G(s(T8)) → U1_G(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
GOALA_IN_G(s(T8)) → PB_IN_GAAAA(T8, X30, X29, X4, X5)
PB_IN_GAAAA(T8, T10, X29, X4, X5) → U5_GAAAA(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
PB_IN_GAAAA(T8, T10, X29, X4, X5) → S2LC_IN_GA(T8, T10)
S2LC_IN_GA(s(T16), .(X64, X65)) → U2_GA(T16, X64, X65, s2lC_in_ga(T16, X65))
S2LC_IN_GA(s(T16), .(X64, X65)) → S2LC_IN_GA(T16, X65)
U5_GAAAA(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_GAAAA(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
U5_GAAAA(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → APPENDE_IN_AGAA(X29, T10, X4, X5)
APPENDE_IN_AGAA(X96, T22, X97, .(X96, X98)) → U4_AGAA(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
APPENDE_IN_AGAA(X96, T22, X97, .(X96, X98)) → APPENDD_IN_GAA(T22, X97, X98)
APPENDD_IN_GAA(.(T27, T29), X129, .(T27, X130)) → U3_GAA(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
APPENDD_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDD_IN_GAA(T29, X129, X130)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
pB_in_gaaaa(T8, T10, X29, X4, X5) → U5_gaaaa(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X64, X65)) → U2_ga(T16, X64, X65, s2lC_in_ga(T16, X65))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X64, X65, s2lC_out_ga(T16, X65)) → s2lC_out_ga(s(T16), .(X64, X65))
U5_gaaaa(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_gaaaa(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
appendE_in_agaa(X96, T22, X97, .(X96, X98)) → U4_agaa(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
appendD_in_gaa([], X112, X112) → appendD_out_gaa([], X112, X112)
appendD_in_gaa(.(T27, T29), X129, .(T27, X130)) → U3_gaa(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
U3_gaa(T27, T29, X129, X130, appendD_out_gaa(T29, X129, X130)) → appendD_out_gaa(.(T27, T29), X129, .(T27, X130))
U4_agaa(X96, T22, X97, X98, appendD_out_gaa(T22, X97, X98)) → appendE_out_agaa(X96, T22, X97, .(X96, X98))
U6_gaaaa(T8, T10, X29, X4, X5, appendE_out_agaa(X29, T10, X4, X5)) → pB_out_gaaaa(T8, T10, X29, X4, X5)
U1_g(T8, pB_out_gaaaa(T8, X30, X29, X4, X5)) → goalA_out_g(s(T8))
goalA_in_g(0) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U5_gaaaa(x1, x2, x3, x4, x5, x6)  =  U5_gaaaa(x1, x6)
s2lC_in_ga(x1, x2)  =  s2lC_in_ga(x1)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x4)
0  =  0
s2lC_out_ga(x1, x2)  =  s2lC_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U6_gaaaa(x1, x2, x3, x4, x5, x6)  =  U6_gaaaa(x1, x2, x6)
appendE_in_agaa(x1, x2, x3, x4)  =  appendE_in_agaa(x2)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
appendD_in_gaa(x1, x2, x3)  =  appendD_in_gaa(x1)
[]  =  []
appendD_out_gaa(x1, x2, x3)  =  appendD_out_gaa(x1)
U3_gaa(x1, x2, x3, x4, x5)  =  U3_gaa(x2, x5)
appendE_out_agaa(x1, x2, x3, x4)  =  appendE_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
PB_IN_GAAAA(x1, x2, x3, x4, x5)  =  PB_IN_GAAAA(x1)
U5_GAAAA(x1, x2, x3, x4, x5, x6)  =  U5_GAAAA(x1, x6)
S2LC_IN_GA(x1, x2)  =  S2LC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U6_GAAAA(x1, x2, x3, x4, x5, x6)  =  U6_GAAAA(x1, x2, x6)
APPENDE_IN_AGAA(x1, x2, x3, x4)  =  APPENDE_IN_AGAA(x2)
U4_AGAA(x1, x2, x3, x4, x5)  =  U4_AGAA(x2, x5)
APPENDD_IN_GAA(x1, x2, x3)  =  APPENDD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4, x5)  =  U3_GAA(x2, x5)

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

(4) Obligation:

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

GOALA_IN_G(s(T8)) → U1_G(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
GOALA_IN_G(s(T8)) → PB_IN_GAAAA(T8, X30, X29, X4, X5)
PB_IN_GAAAA(T8, T10, X29, X4, X5) → U5_GAAAA(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
PB_IN_GAAAA(T8, T10, X29, X4, X5) → S2LC_IN_GA(T8, T10)
S2LC_IN_GA(s(T16), .(X64, X65)) → U2_GA(T16, X64, X65, s2lC_in_ga(T16, X65))
S2LC_IN_GA(s(T16), .(X64, X65)) → S2LC_IN_GA(T16, X65)
U5_GAAAA(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_GAAAA(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
U5_GAAAA(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → APPENDE_IN_AGAA(X29, T10, X4, X5)
APPENDE_IN_AGAA(X96, T22, X97, .(X96, X98)) → U4_AGAA(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
APPENDE_IN_AGAA(X96, T22, X97, .(X96, X98)) → APPENDD_IN_GAA(T22, X97, X98)
APPENDD_IN_GAA(.(T27, T29), X129, .(T27, X130)) → U3_GAA(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
APPENDD_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDD_IN_GAA(T29, X129, X130)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
pB_in_gaaaa(T8, T10, X29, X4, X5) → U5_gaaaa(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X64, X65)) → U2_ga(T16, X64, X65, s2lC_in_ga(T16, X65))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X64, X65, s2lC_out_ga(T16, X65)) → s2lC_out_ga(s(T16), .(X64, X65))
U5_gaaaa(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_gaaaa(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
appendE_in_agaa(X96, T22, X97, .(X96, X98)) → U4_agaa(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
appendD_in_gaa([], X112, X112) → appendD_out_gaa([], X112, X112)
appendD_in_gaa(.(T27, T29), X129, .(T27, X130)) → U3_gaa(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
U3_gaa(T27, T29, X129, X130, appendD_out_gaa(T29, X129, X130)) → appendD_out_gaa(.(T27, T29), X129, .(T27, X130))
U4_agaa(X96, T22, X97, X98, appendD_out_gaa(T22, X97, X98)) → appendE_out_agaa(X96, T22, X97, .(X96, X98))
U6_gaaaa(T8, T10, X29, X4, X5, appendE_out_agaa(X29, T10, X4, X5)) → pB_out_gaaaa(T8, T10, X29, X4, X5)
U1_g(T8, pB_out_gaaaa(T8, X30, X29, X4, X5)) → goalA_out_g(s(T8))
goalA_in_g(0) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U5_gaaaa(x1, x2, x3, x4, x5, x6)  =  U5_gaaaa(x1, x6)
s2lC_in_ga(x1, x2)  =  s2lC_in_ga(x1)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x4)
0  =  0
s2lC_out_ga(x1, x2)  =  s2lC_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U6_gaaaa(x1, x2, x3, x4, x5, x6)  =  U6_gaaaa(x1, x2, x6)
appendE_in_agaa(x1, x2, x3, x4)  =  appendE_in_agaa(x2)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
appendD_in_gaa(x1, x2, x3)  =  appendD_in_gaa(x1)
[]  =  []
appendD_out_gaa(x1, x2, x3)  =  appendD_out_gaa(x1)
U3_gaa(x1, x2, x3, x4, x5)  =  U3_gaa(x2, x5)
appendE_out_agaa(x1, x2, x3, x4)  =  appendE_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
GOALA_IN_G(x1)  =  GOALA_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
PB_IN_GAAAA(x1, x2, x3, x4, x5)  =  PB_IN_GAAAA(x1)
U5_GAAAA(x1, x2, x3, x4, x5, x6)  =  U5_GAAAA(x1, x6)
S2LC_IN_GA(x1, x2)  =  S2LC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U6_GAAAA(x1, x2, x3, x4, x5, x6)  =  U6_GAAAA(x1, x2, x6)
APPENDE_IN_AGAA(x1, x2, x3, x4)  =  APPENDE_IN_AGAA(x2)
U4_AGAA(x1, x2, x3, x4, x5)  =  U4_AGAA(x2, x5)
APPENDD_IN_GAA(x1, x2, x3)  =  APPENDD_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4, x5)  =  U3_GAA(x2, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 10 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APPENDD_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDD_IN_GAA(T29, X129, X130)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
pB_in_gaaaa(T8, T10, X29, X4, X5) → U5_gaaaa(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X64, X65)) → U2_ga(T16, X64, X65, s2lC_in_ga(T16, X65))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X64, X65, s2lC_out_ga(T16, X65)) → s2lC_out_ga(s(T16), .(X64, X65))
U5_gaaaa(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_gaaaa(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
appendE_in_agaa(X96, T22, X97, .(X96, X98)) → U4_agaa(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
appendD_in_gaa([], X112, X112) → appendD_out_gaa([], X112, X112)
appendD_in_gaa(.(T27, T29), X129, .(T27, X130)) → U3_gaa(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
U3_gaa(T27, T29, X129, X130, appendD_out_gaa(T29, X129, X130)) → appendD_out_gaa(.(T27, T29), X129, .(T27, X130))
U4_agaa(X96, T22, X97, X98, appendD_out_gaa(T22, X97, X98)) → appendE_out_agaa(X96, T22, X97, .(X96, X98))
U6_gaaaa(T8, T10, X29, X4, X5, appendE_out_agaa(X29, T10, X4, X5)) → pB_out_gaaaa(T8, T10, X29, X4, X5)
U1_g(T8, pB_out_gaaaa(T8, X30, X29, X4, X5)) → goalA_out_g(s(T8))
goalA_in_g(0) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U5_gaaaa(x1, x2, x3, x4, x5, x6)  =  U5_gaaaa(x1, x6)
s2lC_in_ga(x1, x2)  =  s2lC_in_ga(x1)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x4)
0  =  0
s2lC_out_ga(x1, x2)  =  s2lC_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U6_gaaaa(x1, x2, x3, x4, x5, x6)  =  U6_gaaaa(x1, x2, x6)
appendE_in_agaa(x1, x2, x3, x4)  =  appendE_in_agaa(x2)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
appendD_in_gaa(x1, x2, x3)  =  appendD_in_gaa(x1)
[]  =  []
appendD_out_gaa(x1, x2, x3)  =  appendD_out_gaa(x1)
U3_gaa(x1, x2, x3, x4, x5)  =  U3_gaa(x2, x5)
appendE_out_agaa(x1, x2, x3, x4)  =  appendE_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
APPENDD_IN_GAA(x1, x2, x3)  =  APPENDD_IN_GAA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APPENDD_IN_GAA(.(T27, T29), X129, .(T27, X130)) → APPENDD_IN_GAA(T29, X129, X130)

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

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:

APPENDD_IN_GAA(.(T29)) → APPENDD_IN_GAA(T29)

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:

• APPENDD_IN_GAA(.(T29)) → APPENDD_IN_GAA(T29)
  The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

S2LC_IN_GA(s(T16), .(X64, X65)) → S2LC_IN_GA(T16, X65)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaaaa(T8, X30, X29, X4, X5))
pB_in_gaaaa(T8, T10, X29, X4, X5) → U5_gaaaa(T8, T10, X29, X4, X5, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X64, X65)) → U2_ga(T16, X64, X65, s2lC_in_ga(T16, X65))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X64, X65, s2lC_out_ga(T16, X65)) → s2lC_out_ga(s(T16), .(X64, X65))
U5_gaaaa(T8, T10, X29, X4, X5, s2lC_out_ga(T8, T10)) → U6_gaaaa(T8, T10, X29, X4, X5, appendE_in_agaa(X29, T10, X4, X5))
appendE_in_agaa(X96, T22, X97, .(X96, X98)) → U4_agaa(X96, T22, X97, X98, appendD_in_gaa(T22, X97, X98))
appendD_in_gaa([], X112, X112) → appendD_out_gaa([], X112, X112)
appendD_in_gaa(.(T27, T29), X129, .(T27, X130)) → U3_gaa(T27, T29, X129, X130, appendD_in_gaa(T29, X129, X130))
U3_gaa(T27, T29, X129, X130, appendD_out_gaa(T29, X129, X130)) → appendD_out_gaa(.(T27, T29), X129, .(T27, X130))
U4_agaa(X96, T22, X97, X98, appendD_out_gaa(T22, X97, X98)) → appendE_out_agaa(X96, T22, X97, .(X96, X98))
U6_gaaaa(T8, T10, X29, X4, X5, appendE_out_agaa(X29, T10, X4, X5)) → pB_out_gaaaa(T8, T10, X29, X4, X5)
U1_g(T8, pB_out_gaaaa(T8, X30, X29, X4, X5)) → goalA_out_g(s(T8))
goalA_in_g(0) → goalA_out_g(0)

The argument filtering Pi contains the following mapping:
goalA_in_g(x1)  =  goalA_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
pB_in_gaaaa(x1, x2, x3, x4, x5)  =  pB_in_gaaaa(x1)
U5_gaaaa(x1, x2, x3, x4, x5, x6)  =  U5_gaaaa(x1, x6)
s2lC_in_ga(x1, x2)  =  s2lC_in_ga(x1)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x1, x4)
0  =  0
s2lC_out_ga(x1, x2)  =  s2lC_out_ga(x1, x2)
.(x1, x2)  =  .(x2)
U6_gaaaa(x1, x2, x3, x4, x5, x6)  =  U6_gaaaa(x1, x2, x6)
appendE_in_agaa(x1, x2, x3, x4)  =  appendE_in_agaa(x2)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
appendD_in_gaa(x1, x2, x3)  =  appendD_in_gaa(x1)
[]  =  []
appendD_out_gaa(x1, x2, x3)  =  appendD_out_gaa(x1)
U3_gaa(x1, x2, x3, x4, x5)  =  U3_gaa(x2, x5)
appendE_out_agaa(x1, x2, x3, x4)  =  appendE_out_agaa(x2)
pB_out_gaaaa(x1, x2, x3, x4, x5)  =  pB_out_gaaaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
S2LC_IN_GA(x1, x2)  =  S2LC_IN_GA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

S2LC_IN_GA(s(T16), .(X64, X65)) → S2LC_IN_GA(T16, X65)

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

S2LC_IN_GA(s(T16)) → S2LC_IN_GA(T16)

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:

• S2LC_IN_GA(s(T16)) → S2LC_IN_GA(T16)
  The graph contains the following edges 1 > 1

(20) YES