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

(0) Obligation:

Clauses:

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

Query: goal(g)

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: goal(T1)\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
4 [label="4: goal(T1), SCOPE: 1, CLAUSE: 4\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(s2l(T3, X3), list(X3))\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(s2l(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 2 | ','(s2l(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(s2l(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 2\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(s2l(T3, X3), list(X3)), SCOPE: 2, CLAUSE: 3\n\nT3 is ground\nX3 is free", fontsize=16, style=filled, fillcolor=lightyellow];
17 [label="B: ','(s2l(T8, X28), list(.(X27, X28)))\n\nT8 is ground\nX27 is free\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="19: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
25 [label="C: s2l(T8, X28)\n\nT8 is ground\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
26 [label="E: list(.(X27, T10))\n\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
30 [label="30: s2l(T8, X28), SCOPE: 3, CLAUSE: 2 | s2l(T8, X28), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
33 [label="33: s2l(T8, X28), SCOPE: 3, CLAUSE: 2\n\nT8 is ground\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
34 [label="34: s2l(T8, X28), SCOPE: 3, CLAUSE: 3\n\nT8 is ground\nX28 is free", fontsize=16, style=filled, fillcolor=lightyellow];
42 [label="42: s2l(T16, X63)\n\nT16 is ground\nX63 is free", fontsize=16, style=filled, fillcolor=lightyellow];
43 [label="43: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
48 [label="48: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
49 [label="49: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
53 [label="53: list(.(X27, T10)), SCOPE: 4, CLAUSE: 0 | list(.(X27, T10)), SCOPE: 4, CLAUSE: 1\n\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
54 [label="54: list(.(X27, T10)), SCOPE: 4, CLAUSE: 1\n\nX27 is free", fontsize=16, style=filled, fillcolor=lightyellow];
63 [label="D: list(T22)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: list(T22), SCOPE: 5, CLAUSE: 0 | list(T22), SCOPE: 5, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
68 [label="68: list(T22), SCOPE: 5, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
69 [label="69: list(T22), SCOPE: 5, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
74 [label="74: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
75 [label="75: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
78 [label="78: list(T29)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
79 [label="79: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
82 [label="82: list([])\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
83 [label="83: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
87 [label="87: list([]), SCOPE: 6, CLAUSE: 0 | list([]), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
88 [label="88: list([]), SCOPE: 6, CLAUSE: 0\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
90 [label="90: list([]), SCOPE: 6, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
92 [label="92: 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];
1 -> 96 [arrowhead = none ];
96 -> 4;

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

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

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

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

101 [label="EVAL with clause\ns2l(s(X24), .(X25, X26)) :- s2l(X24, X26).\nand substitutionX24 -> T8,\nT3 -> s(T8),\nX25 -> X27,\nX26 -> X28,\nX3 -> .(X27, X28)", 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 -> 19;

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

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

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

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

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

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

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(X59), .(X60, X61)) :- s2l(X59, X61).\nand substitutionX59 -> T16,\nT8 -> s(T16),\nX60 -> X62,\nX61 -> X63,\nX28 -> .(X62, X63)", fontsize=14, style = filled, fillcolor = lightblue];
33 -> 111 [arrowhead = none ];
111 -> 42;

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

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

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

115 [label="INSTANCE with matching:\nT8 -> T16\nX28 -> X63", fontsize=14, style = filled, fillcolor = lightgrey];
42 -> 115 [arrowhead = none , style=dashed];
115 -> 25[style=dashed];

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

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

118 [label="ONLY EVAL with clause\nlist(.(X75, X76)) :- list(X76).\nand substitutionX27 -> X77,\nX75 -> X77,\nT10 -> T22,\nX76 -> T22,\nT21 -> T22", fontsize=14, style = filled, fillcolor = lightblue];
54 -> 118 [arrowhead = none ];
118 -> 63;

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

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

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

122 [label="EVAL with clause\nlist([]).\nand substitutionT22 -> []", fontsize=14, style = filled, fillcolor = lightblue];
68 -> 122 [arrowhead = none ];
122 -> 72;

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

124 [label="EVAL with clause\nlist(.(X82, X83)) :- list(X83).\nand substitutionX82 -> T27,\nX83 -> T29,\nT22 -> .(T27, T29),\nT28 -> T29", fontsize=14, style = filled, fillcolor = lightblue];
69 -> 124 [arrowhead = none ];
124 -> 78;

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

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

127 [label="INSTANCE with matching:\nT22 -> T29", fontsize=14, style = filled, fillcolor = lightgrey];
78 -> 127 [arrowhead = none , style=dashed];
127 -> 63[style=dashed];

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

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

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

131 [label="ONLY EVAL with clause\nlist([]).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
88 -> 131 [arrowhead = none ];
131 -> 92;

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

133 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
92 -> 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_gaa(T8, X28, X27))
pB_in_gaa(T8, T10, X27) → U5_gaa(T8, T10, X27, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X62, X63)) → U2_ga(T16, X62, X63, s2lC_in_ga(T16, X63))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X62, X63, s2lC_out_ga(T16, X63)) → s2lC_out_ga(s(T16), .(X62, X63))
U5_gaa(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_gaa(T8, T10, X27, listE_in_ag(X27, T10))
listE_in_ag(X77, T22) → U4_ag(X77, T22, listD_in_g(T22))
listD_in_g([]) → listD_out_g([])
listD_in_g(.(T27, T29)) → U3_g(T27, T29, listD_in_g(T29))
U3_g(T27, T29, listD_out_g(T29)) → listD_out_g(.(T27, T29))
U4_ag(X77, T22, listD_out_g(T22)) → listE_out_ag(X77, T22)
U6_gaa(T8, T10, X27, listE_out_ag(X27, T10)) → pB_out_gaa(T8, T10, X27)
U1_g(T8, pB_out_gaa(T8, X28, X27)) → 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_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
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_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x2, x4)
listE_in_ag(x1, x2)  =  listE_in_ag(x2)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
listD_in_g(x1)  =  listD_in_g(x1)
[]  =  []
listD_out_g(x1)  =  listD_out_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
listE_out_ag(x1, x2)  =  listE_out_ag(x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(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_gaa(T8, X28, X27))
GOALA_IN_G(s(T8)) → PB_IN_GAA(T8, X28, X27)
PB_IN_GAA(T8, T10, X27) → U5_GAA(T8, T10, X27, s2lC_in_ga(T8, T10))
PB_IN_GAA(T8, T10, X27) → S2LC_IN_GA(T8, T10)
S2LC_IN_GA(s(T16), .(X62, X63)) → U2_GA(T16, X62, X63, s2lC_in_ga(T16, X63))
S2LC_IN_GA(s(T16), .(X62, X63)) → S2LC_IN_GA(T16, X63)
U5_GAA(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_GAA(T8, T10, X27, listE_in_ag(X27, T10))
U5_GAA(T8, T10, X27, s2lC_out_ga(T8, T10)) → LISTE_IN_AG(X27, T10)
LISTE_IN_AG(X77, T22) → U4_AG(X77, T22, listD_in_g(T22))
LISTE_IN_AG(X77, T22) → LISTD_IN_G(T22)
LISTD_IN_G(.(T27, T29)) → U3_G(T27, T29, listD_in_g(T29))
LISTD_IN_G(.(T27, T29)) → LISTD_IN_G(T29)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X28, X27))
pB_in_gaa(T8, T10, X27) → U5_gaa(T8, T10, X27, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X62, X63)) → U2_ga(T16, X62, X63, s2lC_in_ga(T16, X63))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X62, X63, s2lC_out_ga(T16, X63)) → s2lC_out_ga(s(T16), .(X62, X63))
U5_gaa(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_gaa(T8, T10, X27, listE_in_ag(X27, T10))
listE_in_ag(X77, T22) → U4_ag(X77, T22, listD_in_g(T22))
listD_in_g([]) → listD_out_g([])
listD_in_g(.(T27, T29)) → U3_g(T27, T29, listD_in_g(T29))
U3_g(T27, T29, listD_out_g(T29)) → listD_out_g(.(T27, T29))
U4_ag(X77, T22, listD_out_g(T22)) → listE_out_ag(X77, T22)
U6_gaa(T8, T10, X27, listE_out_ag(X27, T10)) → pB_out_gaa(T8, T10, X27)
U1_g(T8, pB_out_gaa(T8, X28, X27)) → 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_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
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_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x2, x4)
listE_in_ag(x1, x2)  =  listE_in_ag(x2)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
listD_in_g(x1)  =  listD_in_g(x1)
[]  =  []
listD_out_g(x1)  =  listD_out_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
listE_out_ag(x1, x2)  =  listE_out_ag(x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(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_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
S2LC_IN_GA(x1, x2)  =  S2LC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x2, x4)
LISTE_IN_AG(x1, x2)  =  LISTE_IN_AG(x2)
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)
LISTD_IN_G(x1)  =  LISTD_IN_G(x1)
U3_G(x1, x2, x3)  =  U3_G(x2, x3)

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_gaa(T8, X28, X27))
GOALA_IN_G(s(T8)) → PB_IN_GAA(T8, X28, X27)
PB_IN_GAA(T8, T10, X27) → U5_GAA(T8, T10, X27, s2lC_in_ga(T8, T10))
PB_IN_GAA(T8, T10, X27) → S2LC_IN_GA(T8, T10)
S2LC_IN_GA(s(T16), .(X62, X63)) → U2_GA(T16, X62, X63, s2lC_in_ga(T16, X63))
S2LC_IN_GA(s(T16), .(X62, X63)) → S2LC_IN_GA(T16, X63)
U5_GAA(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_GAA(T8, T10, X27, listE_in_ag(X27, T10))
U5_GAA(T8, T10, X27, s2lC_out_ga(T8, T10)) → LISTE_IN_AG(X27, T10)
LISTE_IN_AG(X77, T22) → U4_AG(X77, T22, listD_in_g(T22))
LISTE_IN_AG(X77, T22) → LISTD_IN_G(T22)
LISTD_IN_G(.(T27, T29)) → U3_G(T27, T29, listD_in_g(T29))
LISTD_IN_G(.(T27, T29)) → LISTD_IN_G(T29)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X28, X27))
pB_in_gaa(T8, T10, X27) → U5_gaa(T8, T10, X27, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X62, X63)) → U2_ga(T16, X62, X63, s2lC_in_ga(T16, X63))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X62, X63, s2lC_out_ga(T16, X63)) → s2lC_out_ga(s(T16), .(X62, X63))
U5_gaa(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_gaa(T8, T10, X27, listE_in_ag(X27, T10))
listE_in_ag(X77, T22) → U4_ag(X77, T22, listD_in_g(T22))
listD_in_g([]) → listD_out_g([])
listD_in_g(.(T27, T29)) → U3_g(T27, T29, listD_in_g(T29))
U3_g(T27, T29, listD_out_g(T29)) → listD_out_g(.(T27, T29))
U4_ag(X77, T22, listD_out_g(T22)) → listE_out_ag(X77, T22)
U6_gaa(T8, T10, X27, listE_out_ag(X27, T10)) → pB_out_gaa(T8, T10, X27)
U1_g(T8, pB_out_gaa(T8, X28, X27)) → 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_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
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_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x2, x4)
listE_in_ag(x1, x2)  =  listE_in_ag(x2)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
listD_in_g(x1)  =  listD_in_g(x1)
[]  =  []
listD_out_g(x1)  =  listD_out_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
listE_out_ag(x1, x2)  =  listE_out_ag(x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(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_GAA(x1, x2, x3)  =  PB_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
S2LC_IN_GA(x1, x2)  =  S2LC_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
U6_GAA(x1, x2, x3, x4)  =  U6_GAA(x1, x2, x4)
LISTE_IN_AG(x1, x2)  =  LISTE_IN_AG(x2)
U4_AG(x1, x2, x3)  =  U4_AG(x2, x3)
LISTD_IN_G(x1)  =  LISTD_IN_G(x1)
U3_G(x1, x2, x3)  =  U3_G(x2, x3)

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:

LISTD_IN_G(.(T27, T29)) → LISTD_IN_G(T29)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X28, X27))
pB_in_gaa(T8, T10, X27) → U5_gaa(T8, T10, X27, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X62, X63)) → U2_ga(T16, X62, X63, s2lC_in_ga(T16, X63))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X62, X63, s2lC_out_ga(T16, X63)) → s2lC_out_ga(s(T16), .(X62, X63))
U5_gaa(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_gaa(T8, T10, X27, listE_in_ag(X27, T10))
listE_in_ag(X77, T22) → U4_ag(X77, T22, listD_in_g(T22))
listD_in_g([]) → listD_out_g([])
listD_in_g(.(T27, T29)) → U3_g(T27, T29, listD_in_g(T29))
U3_g(T27, T29, listD_out_g(T29)) → listD_out_g(.(T27, T29))
U4_ag(X77, T22, listD_out_g(T22)) → listE_out_ag(X77, T22)
U6_gaa(T8, T10, X27, listE_out_ag(X27, T10)) → pB_out_gaa(T8, T10, X27)
U1_g(T8, pB_out_gaa(T8, X28, X27)) → 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_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
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_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x2, x4)
listE_in_ag(x1, x2)  =  listE_in_ag(x2)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
listD_in_g(x1)  =  listD_in_g(x1)
[]  =  []
listD_out_g(x1)  =  listD_out_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
listE_out_ag(x1, x2)  =  listE_out_ag(x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(x1, x2)
goalA_out_g(x1)  =  goalA_out_g(x1)
LISTD_IN_G(x1)  =  LISTD_IN_G(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:

LISTD_IN_G(.(T27, T29)) → LISTD_IN_G(T29)

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

LISTD_IN_G(.(T29)) → LISTD_IN_G(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:

• LISTD_IN_G(.(T29)) → LISTD_IN_G(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), .(X62, X63)) → S2LC_IN_GA(T16, X63)

The TRS R consists of the following rules:

goalA_in_g(s(T8)) → U1_g(T8, pB_in_gaa(T8, X28, X27))
pB_in_gaa(T8, T10, X27) → U5_gaa(T8, T10, X27, s2lC_in_ga(T8, T10))
s2lC_in_ga(s(T16), .(X62, X63)) → U2_ga(T16, X62, X63, s2lC_in_ga(T16, X63))
s2lC_in_ga(0, []) → s2lC_out_ga(0, [])
U2_ga(T16, X62, X63, s2lC_out_ga(T16, X63)) → s2lC_out_ga(s(T16), .(X62, X63))
U5_gaa(T8, T10, X27, s2lC_out_ga(T8, T10)) → U6_gaa(T8, T10, X27, listE_in_ag(X27, T10))
listE_in_ag(X77, T22) → U4_ag(X77, T22, listD_in_g(T22))
listD_in_g([]) → listD_out_g([])
listD_in_g(.(T27, T29)) → U3_g(T27, T29, listD_in_g(T29))
U3_g(T27, T29, listD_out_g(T29)) → listD_out_g(.(T27, T29))
U4_ag(X77, T22, listD_out_g(T22)) → listE_out_ag(X77, T22)
U6_gaa(T8, T10, X27, listE_out_ag(X27, T10)) → pB_out_gaa(T8, T10, X27)
U1_g(T8, pB_out_gaa(T8, X28, X27)) → 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_gaa(x1, x2, x3)  =  pB_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
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_gaa(x1, x2, x3, x4)  =  U6_gaa(x1, x2, x4)
listE_in_ag(x1, x2)  =  listE_in_ag(x2)
U4_ag(x1, x2, x3)  =  U4_ag(x2, x3)
listD_in_g(x1)  =  listD_in_g(x1)
[]  =  []
listD_out_g(x1)  =  listD_out_g(x1)
U3_g(x1, x2, x3)  =  U3_g(x2, x3)
listE_out_ag(x1, x2)  =  listE_out_ag(x2)
pB_out_gaa(x1, x2, x3)  =  pB_out_gaa(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), .(X62, X63)) → S2LC_IN_GA(T16, X63)

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