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

(0) Obligation:

Clauses:

even(s(s(X))) :- even(X).
even(0).
lte(s(X), s(Y)) :- lte(X, Y).
lte(0, Y).
goal :- ','(lte(X, s(s(s(s(0))))), even(X)).

Query: goal()

(1) PrologToPiTRSViaGraphTransformerProof (SOUND transformation)

Transformed Prolog program to (Pi-)TRS.

digraph dp_graph {
node [outthreshold=100, inthreshold=100];
1 [label="A: goal\n\n", fontsize=16, style=filled, fillcolor=lightyellow, color=red];
6 [label="6: goal, SCOPE: 1, CLAUSE: 4\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
8 [label="8: ','(lte(X1, s(s(s(s(0))))), even(X1))\n\nX1 is free", fontsize=16, style=filled, fillcolor=lightyellow];
11 [label="11: ','(lte(X1, s(s(s(s(0))))), even(X1)), SCOPE: 2, CLAUSE: 2 | ','(lte(X1, s(s(s(s(0))))), even(X1)), SCOPE: 2, CLAUSE: 3\n\nX1 is free", fontsize=16, style=filled, fillcolor=lightyellow];
13 [label="13: ','(lte(X1, s(s(s(s(0))))), even(X1)), SCOPE: 2, CLAUSE: 2\n\nX1 is free", fontsize=16, style=filled, fillcolor=lightyellow];
15 [label="15: ','(lte(X1, s(s(s(s(0))))), even(X1)), SCOPE: 2, CLAUSE: 3\n\nX1 is free", fontsize=16, style=filled, fillcolor=lightyellow];
19 [label="B: ','(lte(X22, s(s(s(0)))), even(s(X22)))\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
22 [label="D: lte(X22, s(s(s(0))))\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
24 [label="E: even(s(T1))\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
28 [label="28: lte(X22, s(s(s(0)))), SCOPE: 3, CLAUSE: 2 | lte(X22, s(s(s(0)))), SCOPE: 3, CLAUSE: 3\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
31 [label="31: lte(X22, s(s(s(0)))), SCOPE: 3, CLAUSE: 2\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
32 [label="32: lte(X22, s(s(s(0)))), SCOPE: 3, CLAUSE: 3\n\nX22 is free", fontsize=16, style=filled, fillcolor=lightyellow];
37 [label="37: lte(X49, s(s(0)))\n\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
40 [label="40: lte(X49, s(s(0))), SCOPE: 4, CLAUSE: 2 | lte(X49, s(s(0))), SCOPE: 4, CLAUSE: 3\n\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
46 [label="46: lte(X49, s(s(0))), SCOPE: 4, CLAUSE: 2\n\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
47 [label="47: lte(X49, s(s(0))), SCOPE: 4, CLAUSE: 3\n\nX49 is free", fontsize=16, style=filled, fillcolor=lightyellow];
62 [label="62: lte(X73, s(0))\n\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
65 [label="65: lte(X73, s(0)), SCOPE: 5, CLAUSE: 2 | lte(X73, s(0)), SCOPE: 5, CLAUSE: 3\n\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
71 [label="71: lte(X73, s(0)), SCOPE: 5, CLAUSE: 2\n\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
72 [label="72: lte(X73, s(0)), SCOPE: 5, CLAUSE: 3\n\nX73 is free", fontsize=16, style=filled, fillcolor=lightyellow];
80 [label="80: lte(X97, 0)\n\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
108 [label="108: lte(X97, 0), SCOPE: 6, CLAUSE: 2 | lte(X97, 0), SCOPE: 6, CLAUSE: 3\n\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
110 [label="110: lte(X97, 0), SCOPE: 6, CLAUSE: 3\n\nX97 is free", fontsize=16, style=filled, fillcolor=lightyellow];
111 [label="111: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
112 [label="112: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
117 [label="117: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
118 [label="118: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
119 [label="119: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
120 [label="120: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
121 [label="121: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
122 [label="122: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
123 [label="123: even(s(T1)), SCOPE: 7, CLAUSE: 0 | even(s(T1)), SCOPE: 7, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
124 [label="124: even(s(T1)), SCOPE: 7, CLAUSE: 0\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
125 [label="125: even(s(T1)), SCOPE: 7, CLAUSE: 1\n\nT1 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
126 [label="C: even(T7)\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
127 [label="127: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
128 [label="128: even(T7), SCOPE: 8, CLAUSE: 0 | even(T7), SCOPE: 8, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
129 [label="129: even(T7), SCOPE: 8, CLAUSE: 0\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
130 [label="130: even(T7), SCOPE: 8, CLAUSE: 1\n\nT7 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
131 [label="131: even(T13)\n\nT13 is ground", fontsize=16, style=filled, fillcolor=lightyellow];
132 [label="132: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
133 [label="133: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
134 [label="134: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
135 [label="135: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
136 [label="136: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
137 [label="137: even(0)\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
138 [label="138: even(0), SCOPE: 9, CLAUSE: 0 | even(0), SCOPE: 9, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
139 [label="139: even(0), SCOPE: 9, CLAUSE: 1\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
140 [label="140: true\n\n", fontsize=16, style=filled, fillcolor=lightyellow];
141 [label="141: \n\n", fontsize=16, style=filled, fillcolor=lightyellow];
142 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
1 -> 142 [arrowhead = none ];
142 -> 6;

143 [label="ONLY EVAL with clause\ngoal :- ','(lte(X1, s(s(s(s(0))))), even(X1)).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
6 -> 143 [arrowhead = none ];
143 -> 8;

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

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

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

147 [label="ONLY EVAL with clause\nlte(s(X20), s(X21)) :- lte(X20, X21).\nand substitutionX20 -> X22,\nX1 -> s(X22),\nX21 -> s(s(s(0)))", fontsize=14, style = filled, fillcolor = lightblue];
13 -> 147 [arrowhead = none ];
147 -> 19;

148 [label="ONLY EVAL with clause\nlte(0, X132).\nand substitutionX1 -> 0,\nX132 -> s(s(s(s(0))))", fontsize=14, style = filled, fillcolor = lightblue];
15 -> 148 [arrowhead = none ];
148 -> 137;

149 [label="SPLIT 1", fontsize=14, style = filled, fillcolor = violet];
19 -> 149 [arrowhead = none ];
149 -> 22;

150 [label="SPLIT 2\nnew knowledge:\nT1 is ground\nreplacements:X22 -> T1", fontsize=14, style = filled, fillcolor = violet];
19 -> 150 [arrowhead = none ];
150 -> 24;

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

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

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

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

155 [label="ONLY EVAL with clause\nlte(s(X47), s(X48)) :- lte(X47, X48).\nand substitutionX47 -> X49,\nX22 -> s(X49),\nX48 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
31 -> 155 [arrowhead = none ];
155 -> 37;

156 [label="ONLY EVAL with clause\nlte(0, X115).\nand substitutionX22 -> 0,\nX115 -> s(s(s(0)))", fontsize=14, style = filled, fillcolor = lightblue];
32 -> 156 [arrowhead = none ];
156 -> 121;

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

158 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
40 -> 158 [arrowhead = none ];
158 -> 46;

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

160 [label="ONLY EVAL with clause\nlte(s(X71), s(X72)) :- lte(X71, X72).\nand substitutionX71 -> X73,\nX49 -> s(X73),\nX72 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
46 -> 160 [arrowhead = none ];
160 -> 62;

161 [label="ONLY EVAL with clause\nlte(0, X112).\nand substitutionX49 -> 0,\nX112 -> s(s(0))", fontsize=14, style = filled, fillcolor = lightblue];
47 -> 161 [arrowhead = none ];
161 -> 119;

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

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

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

165 [label="ONLY EVAL with clause\nlte(s(X95), s(X96)) :- lte(X95, X96).\nand substitutionX95 -> X97,\nX73 -> s(X97),\nX96 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
71 -> 165 [arrowhead = none ];
165 -> 80;

166 [label="ONLY EVAL with clause\nlte(0, X109).\nand substitutionX73 -> 0,\nX109 -> s(0)", fontsize=14, style = filled, fillcolor = lightblue];
72 -> 166 [arrowhead = none ];
166 -> 117;

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

168 [label="BACKTRACK\nfor clause: lte(s(X), s(Y)) :- lte(X, Y)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
108 -> 168 [arrowhead = none ];
168 -> 110;

169 [label="ONLY EVAL with clause\nlte(0, X106).\nand substitutionX97 -> 0,\nX106 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
110 -> 169 [arrowhead = none ];
169 -> 111;

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

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

172 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
119 -> 172 [arrowhead = none ];
172 -> 120;

173 [label="SUCCESS", fontsize=14, style = filled, fillcolor = lightgreen];
121 -> 173 [arrowhead = none ];
173 -> 122;

174 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 174 [arrowhead = none ];
174 -> 124;

175 [label="PARALLEL", fontsize=14, style = filled, fillcolor = violet];
123 -> 175 [arrowhead = none ];
175 -> 125;

176 [label="EVAL with clause\neven(s(s(X121))) :- even(X121).\nand substitutionX121 -> T7,\nT1 -> s(T7)", fontsize=14, style = filled, fillcolor = lightblue];
124 -> 176 [arrowhead = none ];
176 -> 126;

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

178 [label="BACKTRACK\nfor clause: even(0)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
125 -> 178 [arrowhead = none ];
178 -> 136;

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

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

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

182 [label="EVAL with clause\neven(s(s(X127))) :- even(X127).\nand substitutionX127 -> T13,\nT7 -> s(s(T13))", fontsize=14, style = filled, fillcolor = lightblue];
129 -> 182 [arrowhead = none ];
182 -> 131;

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

184 [label="EVAL with clause\neven(0).\nand substitutionT7 -> 0", fontsize=14, style = filled, fillcolor = lightblue];
130 -> 184 [arrowhead = none ];
184 -> 133;

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

186 [label="INSTANCE with matching:\nT7 -> T13", fontsize=14, style = filled, fillcolor = lightgrey];
131 -> 186 [arrowhead = none , style=dashed];
186 -> 126[style=dashed];

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

188 [label="CASE", fontsize=14, style = filled, fillcolor = lightcyan];
137 -> 188 [arrowhead = none ];
188 -> 138;

189 [label="BACKTRACK\nfor clause: even(s(s(X))) :- even(X)because of non-unification", fontsize=14, style = filled, fillcolor = lightgreen];
138 -> 189 [arrowhead = none ];
189 -> 139;

190 [label="ONLY EVAL with clause\neven(0).\nand substitution", fontsize=14, style = filled, fillcolor = lightblue];
139 -> 190 [arrowhead = none ];
190 -> 140;

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

}

(2) Obligation:

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

goalA_in_ → U1_(pB_in_a(X22))
pB_in_a(T1) → U4_a(T1, lteD_in_a(T1))
lteD_in_a(s(s(s(0)))) → lteD_out_a(s(s(s(0))))
lteD_in_a(s(s(0))) → lteD_out_a(s(s(0)))
lteD_in_a(s(0)) → lteD_out_a(s(0))
lteD_in_a(0) → lteD_out_a(0)
U4_a(T1, lteD_out_a(T1)) → U5_a(T1, evenE_in_g(T1))
evenE_in_g(s(T7)) → U3_g(T7, evenC_in_g(T7))
evenC_in_g(s(s(T13))) → U2_g(T13, evenC_in_g(T13))
evenC_in_g(0) → evenC_out_g(0)
U2_g(T13, evenC_out_g(T13)) → evenC_out_g(s(s(T13)))
U3_g(T7, evenC_out_g(T7)) → evenE_out_g(s(T7))
U5_a(T1, evenE_out_g(T1)) → pB_out_a(T1)
U1_(pB_out_a(X22)) → goalA_out_
goalA_in_ → goalA_out_

The argument filtering Pi contains the following mapping:
goalA_in_  =  goalA_in_
U1_(x1)  =  U1_(x1)
pB_in_a(x1)  =  pB_in_a
U4_a(x1, x2)  =  U4_a(x2)
lteD_in_a(x1)  =  lteD_in_a
lteD_out_a(x1)  =  lteD_out_a(x1)
U5_a(x1, x2)  =  U5_a(x1, x2)
evenE_in_g(x1)  =  evenE_in_g(x1)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
evenC_in_g(x1)  =  evenC_in_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
0  =  0
evenC_out_g(x1)  =  evenC_out_g(x1)
evenE_out_g(x1)  =  evenE_out_g(x1)
pB_out_a(x1)  =  pB_out_a(x1)
goalA_out_  =  goalA_out_

(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_ → U1_¹(pB_in_a(X22))
GOALA_IN_ → PB_IN_A(X22)
PB_IN_A(T1) → U4_A(T1, lteD_in_a(T1))
PB_IN_A(T1) → LTED_IN_A(T1)
U4_A(T1, lteD_out_a(T1)) → U5_A(T1, evenE_in_g(T1))
U4_A(T1, lteD_out_a(T1)) → EVENE_IN_G(T1)
EVENE_IN_G(s(T7)) → U3_G(T7, evenC_in_g(T7))
EVENE_IN_G(s(T7)) → EVENC_IN_G(T7)
EVENC_IN_G(s(s(T13))) → U2_G(T13, evenC_in_g(T13))
EVENC_IN_G(s(s(T13))) → EVENC_IN_G(T13)

The TRS R consists of the following rules:

goalA_in_ → U1_(pB_in_a(X22))
pB_in_a(T1) → U4_a(T1, lteD_in_a(T1))
lteD_in_a(s(s(s(0)))) → lteD_out_a(s(s(s(0))))
lteD_in_a(s(s(0))) → lteD_out_a(s(s(0)))
lteD_in_a(s(0)) → lteD_out_a(s(0))
lteD_in_a(0) → lteD_out_a(0)
U4_a(T1, lteD_out_a(T1)) → U5_a(T1, evenE_in_g(T1))
evenE_in_g(s(T7)) → U3_g(T7, evenC_in_g(T7))
evenC_in_g(s(s(T13))) → U2_g(T13, evenC_in_g(T13))
evenC_in_g(0) → evenC_out_g(0)
U2_g(T13, evenC_out_g(T13)) → evenC_out_g(s(s(T13)))
U3_g(T7, evenC_out_g(T7)) → evenE_out_g(s(T7))
U5_a(T1, evenE_out_g(T1)) → pB_out_a(T1)
U1_(pB_out_a(X22)) → goalA_out_
goalA_in_ → goalA_out_

The argument filtering Pi contains the following mapping:
goalA_in_  =  goalA_in_
U1_(x1)  =  U1_(x1)
pB_in_a(x1)  =  pB_in_a
U4_a(x1, x2)  =  U4_a(x2)
lteD_in_a(x1)  =  lteD_in_a
lteD_out_a(x1)  =  lteD_out_a(x1)
U5_a(x1, x2)  =  U5_a(x1, x2)
evenE_in_g(x1)  =  evenE_in_g(x1)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
evenC_in_g(x1)  =  evenC_in_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
0  =  0
evenC_out_g(x1)  =  evenC_out_g(x1)
evenE_out_g(x1)  =  evenE_out_g(x1)
pB_out_a(x1)  =  pB_out_a(x1)
goalA_out_  =  goalA_out_
GOALA_IN_  =  GOALA_IN_
U1_¹(x1)  =  U1_¹(x1)
PB_IN_A(x1)  =  PB_IN_A
U4_A(x1, x2)  =  U4_A(x2)
LTED_IN_A(x1)  =  LTED_IN_A
U5_A(x1, x2)  =  U5_A(x1, x2)
EVENE_IN_G(x1)  =  EVENE_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
EVENC_IN_G(x1)  =  EVENC_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x1, x2)

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

(4) Obligation:

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

GOALA_IN_ → U1_¹(pB_in_a(X22))
GOALA_IN_ → PB_IN_A(X22)
PB_IN_A(T1) → U4_A(T1, lteD_in_a(T1))
PB_IN_A(T1) → LTED_IN_A(T1)
U4_A(T1, lteD_out_a(T1)) → U5_A(T1, evenE_in_g(T1))
U4_A(T1, lteD_out_a(T1)) → EVENE_IN_G(T1)
EVENE_IN_G(s(T7)) → U3_G(T7, evenC_in_g(T7))
EVENE_IN_G(s(T7)) → EVENC_IN_G(T7)
EVENC_IN_G(s(s(T13))) → U2_G(T13, evenC_in_g(T13))
EVENC_IN_G(s(s(T13))) → EVENC_IN_G(T13)

The TRS R consists of the following rules:

goalA_in_ → U1_(pB_in_a(X22))
pB_in_a(T1) → U4_a(T1, lteD_in_a(T1))
lteD_in_a(s(s(s(0)))) → lteD_out_a(s(s(s(0))))
lteD_in_a(s(s(0))) → lteD_out_a(s(s(0)))
lteD_in_a(s(0)) → lteD_out_a(s(0))
lteD_in_a(0) → lteD_out_a(0)
U4_a(T1, lteD_out_a(T1)) → U5_a(T1, evenE_in_g(T1))
evenE_in_g(s(T7)) → U3_g(T7, evenC_in_g(T7))
evenC_in_g(s(s(T13))) → U2_g(T13, evenC_in_g(T13))
evenC_in_g(0) → evenC_out_g(0)
U2_g(T13, evenC_out_g(T13)) → evenC_out_g(s(s(T13)))
U3_g(T7, evenC_out_g(T7)) → evenE_out_g(s(T7))
U5_a(T1, evenE_out_g(T1)) → pB_out_a(T1)
U1_(pB_out_a(X22)) → goalA_out_
goalA_in_ → goalA_out_

The argument filtering Pi contains the following mapping:
goalA_in_  =  goalA_in_
U1_(x1)  =  U1_(x1)
pB_in_a(x1)  =  pB_in_a
U4_a(x1, x2)  =  U4_a(x2)
lteD_in_a(x1)  =  lteD_in_a
lteD_out_a(x1)  =  lteD_out_a(x1)
U5_a(x1, x2)  =  U5_a(x1, x2)
evenE_in_g(x1)  =  evenE_in_g(x1)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
evenC_in_g(x1)  =  evenC_in_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
0  =  0
evenC_out_g(x1)  =  evenC_out_g(x1)
evenE_out_g(x1)  =  evenE_out_g(x1)
pB_out_a(x1)  =  pB_out_a(x1)
goalA_out_  =  goalA_out_
GOALA_IN_  =  GOALA_IN_
U1_¹(x1)  =  U1_¹(x1)
PB_IN_A(x1)  =  PB_IN_A
U4_A(x1, x2)  =  U4_A(x2)
LTED_IN_A(x1)  =  LTED_IN_A
U5_A(x1, x2)  =  U5_A(x1, x2)
EVENE_IN_G(x1)  =  EVENE_IN_G(x1)
U3_G(x1, x2)  =  U3_G(x1, x2)
EVENC_IN_G(x1)  =  EVENC_IN_G(x1)
U2_G(x1, x2)  =  U2_G(x1, x2)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 1 SCC with 9 less nodes.

(6) Obligation:

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

EVENC_IN_G(s(s(T13))) → EVENC_IN_G(T13)

The TRS R consists of the following rules:

goalA_in_ → U1_(pB_in_a(X22))
pB_in_a(T1) → U4_a(T1, lteD_in_a(T1))
lteD_in_a(s(s(s(0)))) → lteD_out_a(s(s(s(0))))
lteD_in_a(s(s(0))) → lteD_out_a(s(s(0)))
lteD_in_a(s(0)) → lteD_out_a(s(0))
lteD_in_a(0) → lteD_out_a(0)
U4_a(T1, lteD_out_a(T1)) → U5_a(T1, evenE_in_g(T1))
evenE_in_g(s(T7)) → U3_g(T7, evenC_in_g(T7))
evenC_in_g(s(s(T13))) → U2_g(T13, evenC_in_g(T13))
evenC_in_g(0) → evenC_out_g(0)
U2_g(T13, evenC_out_g(T13)) → evenC_out_g(s(s(T13)))
U3_g(T7, evenC_out_g(T7)) → evenE_out_g(s(T7))
U5_a(T1, evenE_out_g(T1)) → pB_out_a(T1)
U1_(pB_out_a(X22)) → goalA_out_
goalA_in_ → goalA_out_

The argument filtering Pi contains the following mapping:
goalA_in_  =  goalA_in_
U1_(x1)  =  U1_(x1)
pB_in_a(x1)  =  pB_in_a
U4_a(x1, x2)  =  U4_a(x2)
lteD_in_a(x1)  =  lteD_in_a
lteD_out_a(x1)  =  lteD_out_a(x1)
U5_a(x1, x2)  =  U5_a(x1, x2)
evenE_in_g(x1)  =  evenE_in_g(x1)
s(x1)  =  s(x1)
U3_g(x1, x2)  =  U3_g(x1, x2)
evenC_in_g(x1)  =  evenC_in_g(x1)
U2_g(x1, x2)  =  U2_g(x1, x2)
0  =  0
evenC_out_g(x1)  =  evenC_out_g(x1)
evenE_out_g(x1)  =  evenE_out_g(x1)
pB_out_a(x1)  =  pB_out_a(x1)
goalA_out_  =  goalA_out_
EVENC_IN_G(x1)  =  EVENC_IN_G(x1)

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

(7) UsableRulesProof (EQUIVALENT transformation)

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

(8) Obligation:

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

EVENC_IN_G(s(s(T13))) → EVENC_IN_G(T13)

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

(9) PiDPToQDPProof (EQUIVALENT transformation)

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

(10) Obligation:

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

EVENC_IN_G(s(s(T13))) → EVENC_IN_G(T13)

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

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

• EVENC_IN_G(s(s(T13))) → EVENC_IN_G(T13)
  The graph contains the following edges 1 > 1

(12) YES