Left Termination of the query pattern vlcnd_in_1(g) w.r.t. the given Prolog program could not be shown:

(0) Obligation:

Clauses:

vlcnd(N) :- ','(vl(N, Xs), ','(select(X1, Xs, Ys), ','(vl(M, Ys), vlcnd(M)))).
vlcnd(0).
vl(0, L) :- ','(!, eq(L, [])).
vl(N, .(X2, Xs)) :- ','(p(N, P), vl(P, Xs)).
select(X, .(Y, Xs), .(Y, Ys)) :- select(X, Xs, Ys).
select(X, .(X, Xs), Xs).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

vlcnd(g).

(1) CutEliminatorProof (SOUND transformation)

Eliminated all cuts by simply ignoring them[PROLOG].

(2) Obligation:

Clauses:

vlcnd(N) :- ','(vl(N, Xs), ','(select(X1, Xs, Ys), ','(vl(M, Ys), vlcnd(M)))).
vlcnd(0).
vl(0, L) :- eq(L, []).
vl(N, .(X2, Xs)) :- ','(p(N, P), vl(P, Xs)).
select(X, .(Y, Xs), .(Y, Ys)) :- select(X, Xs, Ys).
select(X, .(X, Xs), Xs).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

vlcnd(g).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
vlcnd_in: (b) (f)
vl_in: (b,f) (f,b) (f,f)
select_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)

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

VLCND_IN_G(N) → U1_G(N, vl_in_ga(N, Xs))
VLCND_IN_G(N) → VL_IN_GA(N, Xs)
VL_IN_GA(0, L) → U5_GA(L, eq_in_ag(L, []))
VL_IN_GA(0, L) → EQ_IN_AG(L, [])
VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
VL_IN_GA(N, .(X2, Xs)) → P_IN_GA(N, P)
U6_GA(N, X2, Xs, p_out_ga(N, P)) → U7_GA(N, X2, Xs, vl_in_ga(P, Xs))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)
U1_G(N, vl_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Ys))
U1_G(N, vl_out_ga(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → U8_AGA(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
U2_G(N, select_out_aga(X1, Xs, Ys)) → U3_G(N, vl_in_ag(M, Ys))
U2_G(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
VL_IN_AG(0, L) → U5_AG(L, eq_in_gg(L, []))
VL_IN_AG(0, L) → EQ_IN_GG(L, [])
VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
VL_IN_AG(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AG(N, X2, Xs, p_out_aa(N, P)) → U7_AG(N, X2, Xs, vl_in_ag(P, Xs))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)
U3_G(N, vl_out_ag(M, Ys)) → U4_G(N, vlcnd_in_a(M))
U3_G(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))
VLCND_IN_A(N) → VL_IN_AA(N, Xs)
VL_IN_AA(0, L) → U5_AA(L, eq_in_ag(L, []))
VL_IN_AA(0, L) → EQ_IN_AG(L, [])
VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
VL_IN_AA(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AA(N, X2, Xs, p_out_aa(N, P)) → U7_AA(N, X2, Xs, vl_in_aa(P, Xs))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)
U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U1_A(N, vl_out_aa(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
U3_A(N, vl_out_ag(M, Ys)) → U4_A(N, vlcnd_in_a(M))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
VLCND_IN_G(x1)  =  VLCND_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U5_GA(x1, x2)  =  U5_GA(x2)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U2_G(x1, x2)  =  U2_G(x1, x2)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)
U8_AGA(x1, x2, x3, x4, x5)  =  U8_AGA(x3, x5)
U3_G(x1, x2)  =  U3_G(x1, x2)
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U5_AG(x1, x2)  =  U5_AG(x1, x2)
EQ_IN_GG(x1, x2)  =  EQ_IN_GG(x1, x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)
P_IN_AA(x1, x2)  =  P_IN_AA
U7_AG(x1, x2, x3, x4)  =  U7_AG(x3, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
VL_IN_AA(x1, x2)  =  VL_IN_AA
U5_AA(x1, x2)  =  U5_AA(x2)
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)
U7_AA(x1, x2, x3, x4)  =  U7_AA(x4)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2)  =  U4_A(x2)

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

(6) Obligation:

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

VLCND_IN_G(N) → U1_G(N, vl_in_ga(N, Xs))
VLCND_IN_G(N) → VL_IN_GA(N, Xs)
VL_IN_GA(0, L) → U5_GA(L, eq_in_ag(L, []))
VL_IN_GA(0, L) → EQ_IN_AG(L, [])
VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
VL_IN_GA(N, .(X2, Xs)) → P_IN_GA(N, P)
U6_GA(N, X2, Xs, p_out_ga(N, P)) → U7_GA(N, X2, Xs, vl_in_ga(P, Xs))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)
U1_G(N, vl_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Ys))
U1_G(N, vl_out_ga(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → U8_AGA(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
U2_G(N, select_out_aga(X1, Xs, Ys)) → U3_G(N, vl_in_ag(M, Ys))
U2_G(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
VL_IN_AG(0, L) → U5_AG(L, eq_in_gg(L, []))
VL_IN_AG(0, L) → EQ_IN_GG(L, [])
VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
VL_IN_AG(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AG(N, X2, Xs, p_out_aa(N, P)) → U7_AG(N, X2, Xs, vl_in_ag(P, Xs))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)
U3_G(N, vl_out_ag(M, Ys)) → U4_G(N, vlcnd_in_a(M))
U3_G(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))
VLCND_IN_A(N) → VL_IN_AA(N, Xs)
VL_IN_AA(0, L) → U5_AA(L, eq_in_ag(L, []))
VL_IN_AA(0, L) → EQ_IN_AG(L, [])
VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
VL_IN_AA(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AA(N, X2, Xs, p_out_aa(N, P)) → U7_AA(N, X2, Xs, vl_in_aa(P, Xs))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)
U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U1_A(N, vl_out_aa(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
U3_A(N, vl_out_ag(M, Ys)) → U4_A(N, vlcnd_in_a(M))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
VLCND_IN_G(x1)  =  VLCND_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x1, x2)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U5_GA(x1, x2)  =  U5_GA(x2)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U2_G(x1, x2)  =  U2_G(x1, x2)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)
U8_AGA(x1, x2, x3, x4, x5)  =  U8_AGA(x3, x5)
U3_G(x1, x2)  =  U3_G(x1, x2)
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U5_AG(x1, x2)  =  U5_AG(x1, x2)
EQ_IN_GG(x1, x2)  =  EQ_IN_GG(x1, x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)
P_IN_AA(x1, x2)  =  P_IN_AA
U7_AG(x1, x2, x3, x4)  =  U7_AG(x3, x4)
U4_G(x1, x2)  =  U4_G(x1, x2)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
VL_IN_AA(x1, x2)  =  VL_IN_AA
U5_AA(x1, x2)  =  U5_AA(x2)
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)
U7_AA(x1, x2, x3, x4)  =  U7_AA(x4)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2)  =  U4_A(x2)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
VL_IN_AA(x1, x2)  =  VL_IN_AA
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
VL_IN_AA(x1, x2)  =  VL_IN_AA
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

VL_IN_AA → U6_AA(p_in_aa)
U6_AA(p_out_aa) → VL_IN_AA

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(14) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VL_IN_AA → U6_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

VL_IN_AA → U6_AA(p_out_aa)

(15) Obligation:

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

U6_AA(p_out_aa) → VL_IN_AA
VL_IN_AA → U6_AA(p_out_aa)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(16) 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.

(17) Obligation:

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

U6_AA(p_out_aa) → VL_IN_AA
VL_IN_AA → U6_AA(p_out_aa)

R is empty.
The set Q consists of the following terms:

p_in_aa

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

(18) 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].

p_in_aa

(19) Obligation:

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

U6_AA(p_out_aa) → VL_IN_AA
VL_IN_AA → U6_AA(p_out_aa)

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

(20) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = VL_IN_AA evaluates to t =VL_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

VL_IN_AA → U6_AA(p_out_aa)
with rule VL_IN_AA → U6_AA(p_out_aa) at position [] and matcher [ ]

U6_AA(p_out_aa) → VL_IN_AA
with rule U6_AA(p_out_aa) → VL_IN_AA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(21) FALSE

(22) Obligation:

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

VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)

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

(23) UsableRulesProof (EQUIVALENT transformation)

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

(24) Obligation:

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

VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)

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

(25) PiDPToQDPProof (SOUND transformation)

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

(26) Obligation:

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

VL_IN_AG(.(Xs)) → U6_AG(Xs, p_in_aa)
U6_AG(Xs, p_out_aa) → VL_IN_AG(Xs)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

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

• U6_AG(Xs, p_out_aa) → VL_IN_AG(Xs)
  The graph contains the following edges 1 >= 1

• VL_IN_AG(.(Xs)) → U6_AG(Xs, p_in_aa)
  The graph contains the following edges 1 > 1

(28) TRUE

(29) Obligation:

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

SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)

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

(30) UsableRulesProof (EQUIVALENT transformation)

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

(31) Obligation:

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

SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)

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

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

(32) PiDPToQDPProof (SOUND transformation)

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

(33) Obligation:

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

SELECT_IN_AGA(.(Xs)) → SELECT_IN_AGA(Xs)

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

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

• SELECT_IN_AGA(.(Xs)) → SELECT_IN_AGA(Xs)
  The graph contains the following edges 1 > 1

(35) TRUE

(36) Obligation:

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

U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)

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

(37) UsableRulesProof (EQUIVALENT transformation)

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

(38) Obligation:

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

U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))

The TRS R consists of the following rules:

select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
eq_in_ag(X, X) → eq_out_ag(X, X)
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))

The argument filtering Pi contains the following mapping:
0  =  0
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)

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

(39) PiDPToQDPProof (SOUND transformation)

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

(40) Obligation:

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

U1_A(vl_out_aa(Xs)) → U2_A(select_in_aga(Xs))
U2_A(select_out_aga(Xs, Ys)) → U3_A(vl_in_ag(Ys))
U3_A(vl_out_ag(Ys)) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(41) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U1_A(vl_out_aa(Xs)) → U2_A(select_in_aga(Xs)) at position [0] we obtained the following new rules [LPAR04]:

U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))

(42) Obligation:

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

U2_A(select_out_aga(Xs, Ys)) → U3_A(vl_in_ag(Ys))
U3_A(vl_out_ag(Ys)) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(43) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_A(select_out_aga(Xs, Ys)) → U3_A(vl_in_ag(Ys)) at position [0] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_in_aa))

(44) Obligation:

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

U3_A(vl_out_ag(Ys)) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_in_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(45) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_in_aa)) at position [0,1] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))

(46) Obligation:

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

U3_A(vl_out_ag(Ys)) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(47) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule VLCND_IN_A → U1_A(vl_in_aa) at position [0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(U5_aa(eq_in_ag([])))
VLCND_IN_A → U1_A(U6_aa(p_in_aa))

(48) Obligation:

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

U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U5_aa(eq_in_ag([])))
VLCND_IN_A → U1_A(U6_aa(p_in_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(49) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VLCND_IN_A → U1_A(U5_aa(eq_in_ag([]))) at position [0,0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(U5_aa(eq_out_ag([], [])))

(50) Obligation:

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

U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U6_aa(p_in_aa))
VLCND_IN_A → U1_A(U5_aa(eq_out_ag([], [])))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(51) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VLCND_IN_A → U1_A(U6_aa(p_in_aa)) at position [0,0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(U6_aa(p_out_aa))

(52) Obligation:

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

U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U5_aa(eq_out_ag([], [])))
VLCND_IN_A → U1_A(U6_aa(p_out_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(53) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VLCND_IN_A → U1_A(U5_aa(eq_out_ag([], []))) at position [0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(vl_out_aa([]))

(54) Obligation:

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

U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U6_aa(p_out_aa))
VLCND_IN_A → U1_A(vl_out_aa([]))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(55) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(56) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, [])))
U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(57) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_A(select_out_aga(y0, x0)) → U3_A(U5_ag(x0, eq_in_gg(x0, []))) at position [0,1] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga(y0, [])) → U3_A(U5_ag([], eq_out_gg([], [])))

(58) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, [])) → U3_A(U5_ag([], eq_out_gg([], [])))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(59) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_A(select_out_aga(y0, [])) → U3_A(U5_ag([], eq_out_gg([], []))) at position [0] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga(y0, [])) → U3_A(vl_out_ag([]))

(60) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0))
U2_A(select_out_aga(y0, [])) → U3_A(vl_out_ag([]))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(61) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(.(x0), x0)) we obtained the following new rules [LPAR04]:

U1_A(vl_out_aa(.(.(y_1)))) → U2_A(select_out_aga(.(.(y_1)), .(y_1)))
U1_A(vl_out_aa(.([]))) → U2_A(select_out_aga(.([]), []))

(62) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(x0, select_in_aga(x0)))
U3_A(vl_out_ag(Ys)) → VLCND_IN_A
U2_A(select_out_aga(y0, .(x0))) → U3_A(U6_ag(x0, p_out_aa))
U2_A(select_out_aga(y0, [])) → U3_A(vl_out_ag([]))
U1_A(vl_out_aa(.(.(y_1)))) → U2_A(select_out_aga(.(.(y_1)), .(y_1)))
U1_A(vl_out_aa(.([]))) → U2_A(select_out_aga(.([]), []))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(Xs, select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(.(Xs), Xs)
vl_in_ag(L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(Xs, select_out_aga(Xs, Ys)) → select_out_aga(.(Xs), .(Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(L)
U6_ag(Xs, p_out_aa) → U7_ag(Xs, vl_in_ag(Xs))
U5_aa(eq_out_ag(L, [])) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa → p_out_aa
U7_ag(Xs, vl_out_ag(Xs)) → vl_out_ag(.(Xs))
eq_in_ag(X) → eq_out_ag(X, X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0, x1)
U5_ag(x0, x1)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0, x1)
eq_in_ag(x0)
U7_aa(x0)

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

(63) Obligation:

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

VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x1, x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1, x2)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x1, x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x1, x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x1, x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x1, x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x3, x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x2, x3)
U3_g(x1, x2)  =  U3_g(x1, x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x1, x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg(x1, x2)
vl_out_ag(x1, x2)  =  vl_out_ag(x2)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x3, x4)
U4_g(x1, x2)  =  U4_g(x1, x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g(x1)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)

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

(64) UsableRulesProof (EQUIVALENT transformation)

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

(65) Obligation:

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

VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)

The TRS R consists of the following rules:

p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)

The argument filtering Pi contains the following mapping:
0  =  0
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x1, x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)

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

(66) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
vlcnd_in: (b) (f)
vl_in: (b,f) (f,b) (f,f)
select_in: (f,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(67) Obligation:

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

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g

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

VLCND_IN_G(N) → U1_G(N, vl_in_ga(N, Xs))
VLCND_IN_G(N) → VL_IN_GA(N, Xs)
VL_IN_GA(0, L) → U5_GA(L, eq_in_ag(L, []))
VL_IN_GA(0, L) → EQ_IN_AG(L, [])
VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
VL_IN_GA(N, .(X2, Xs)) → P_IN_GA(N, P)
U6_GA(N, X2, Xs, p_out_ga(N, P)) → U7_GA(N, X2, Xs, vl_in_ga(P, Xs))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)
U1_G(N, vl_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Ys))
U1_G(N, vl_out_ga(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → U8_AGA(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
U2_G(N, select_out_aga(X1, Xs, Ys)) → U3_G(N, vl_in_ag(M, Ys))
U2_G(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
VL_IN_AG(0, L) → U5_AG(L, eq_in_gg(L, []))
VL_IN_AG(0, L) → EQ_IN_GG(L, [])
VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
VL_IN_AG(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AG(N, X2, Xs, p_out_aa(N, P)) → U7_AG(N, X2, Xs, vl_in_ag(P, Xs))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)
U3_G(N, vl_out_ag(M, Ys)) → U4_G(N, vlcnd_in_a(M))
U3_G(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))
VLCND_IN_A(N) → VL_IN_AA(N, Xs)
VL_IN_AA(0, L) → U5_AA(L, eq_in_ag(L, []))
VL_IN_AA(0, L) → EQ_IN_AG(L, [])
VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
VL_IN_AA(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AA(N, X2, Xs, p_out_aa(N, P)) → U7_AA(N, X2, Xs, vl_in_aa(P, Xs))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)
U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U1_A(N, vl_out_aa(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
U3_A(N, vl_out_ag(M, Ys)) → U4_A(N, vlcnd_in_a(M))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
VLCND_IN_G(x1)  =  VLCND_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x2)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U5_GA(x1, x2)  =  U5_GA(x2)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x4)
U2_G(x1, x2)  =  U2_G(x2)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)
U8_AGA(x1, x2, x3, x4, x5)  =  U8_AGA(x5)
U3_G(x1, x2)  =  U3_G(x2)
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U5_AG(x1, x2)  =  U5_AG(x2)
EQ_IN_GG(x1, x2)  =  EQ_IN_GG(x1, x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)
P_IN_AA(x1, x2)  =  P_IN_AA
U7_AG(x1, x2, x3, x4)  =  U7_AG(x4)
U4_G(x1, x2)  =  U4_G(x2)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
VL_IN_AA(x1, x2)  =  VL_IN_AA
U5_AA(x1, x2)  =  U5_AA(x2)
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)
U7_AA(x1, x2, x3, x4)  =  U7_AA(x4)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2)  =  U4_A(x2)

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

(69) Obligation:

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

VLCND_IN_G(N) → U1_G(N, vl_in_ga(N, Xs))
VLCND_IN_G(N) → VL_IN_GA(N, Xs)
VL_IN_GA(0, L) → U5_GA(L, eq_in_ag(L, []))
VL_IN_GA(0, L) → EQ_IN_AG(L, [])
VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
VL_IN_GA(N, .(X2, Xs)) → P_IN_GA(N, P)
U6_GA(N, X2, Xs, p_out_ga(N, P)) → U7_GA(N, X2, Xs, vl_in_ga(P, Xs))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)
U1_G(N, vl_out_ga(N, Xs)) → U2_G(N, select_in_aga(X1, Xs, Ys))
U1_G(N, vl_out_ga(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → U8_AGA(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)
U2_G(N, select_out_aga(X1, Xs, Ys)) → U3_G(N, vl_in_ag(M, Ys))
U2_G(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
VL_IN_AG(0, L) → U5_AG(L, eq_in_gg(L, []))
VL_IN_AG(0, L) → EQ_IN_GG(L, [])
VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
VL_IN_AG(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AG(N, X2, Xs, p_out_aa(N, P)) → U7_AG(N, X2, Xs, vl_in_ag(P, Xs))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)
U3_G(N, vl_out_ag(M, Ys)) → U4_G(N, vlcnd_in_a(M))
U3_G(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))
VLCND_IN_A(N) → VL_IN_AA(N, Xs)
VL_IN_AA(0, L) → U5_AA(L, eq_in_ag(L, []))
VL_IN_AA(0, L) → EQ_IN_AG(L, [])
VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
VL_IN_AA(N, .(X2, Xs)) → P_IN_AA(N, P)
U6_AA(N, X2, Xs, p_out_aa(N, P)) → U7_AA(N, X2, Xs, vl_in_aa(P, Xs))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)
U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U1_A(N, vl_out_aa(N, Xs)) → SELECT_IN_AGA(X1, Xs, Ys)
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → VL_IN_AG(M, Ys)
U3_A(N, vl_out_ag(M, Ys)) → U4_A(N, vlcnd_in_a(M))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
VLCND_IN_G(x1)  =  VLCND_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x2)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U5_GA(x1, x2)  =  U5_GA(x2)
EQ_IN_AG(x1, x2)  =  EQ_IN_AG(x2)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)
P_IN_GA(x1, x2)  =  P_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x4)
U2_G(x1, x2)  =  U2_G(x2)
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)
U8_AGA(x1, x2, x3, x4, x5)  =  U8_AGA(x5)
U3_G(x1, x2)  =  U3_G(x2)
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U5_AG(x1, x2)  =  U5_AG(x2)
EQ_IN_GG(x1, x2)  =  EQ_IN_GG(x1, x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)
P_IN_AA(x1, x2)  =  P_IN_AA
U7_AG(x1, x2, x3, x4)  =  U7_AG(x4)
U4_G(x1, x2)  =  U4_G(x2)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
VL_IN_AA(x1, x2)  =  VL_IN_AA
U5_AA(x1, x2)  =  U5_AA(x2)
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)
U7_AA(x1, x2, x3, x4)  =  U7_AA(x4)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)
U4_A(x1, x2)  =  U4_A(x2)

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

(70) DependencyGraphProof (EQUIVALENT transformation)

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

(71) Complex Obligation (AND)

(72) Obligation:

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

VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
VL_IN_AA(x1, x2)  =  VL_IN_AA
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)

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

(73) UsableRulesProof (EQUIVALENT transformation)

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

(74) Obligation:

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

VL_IN_AA(N, .(X2, Xs)) → U6_AA(N, X2, Xs, p_in_aa(N, P))
U6_AA(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AA(P, Xs)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
VL_IN_AA(x1, x2)  =  VL_IN_AA
U6_AA(x1, x2, x3, x4)  =  U6_AA(x4)

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

(75) PiDPToQDPProof (SOUND transformation)

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

(76) Obligation:

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

VL_IN_AA → U6_AA(p_in_aa)
U6_AA(p_out_aa) → VL_IN_AA

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(77) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VL_IN_AA → U6_AA(p_in_aa) at position [0] we obtained the following new rules [LPAR04]:

VL_IN_AA → U6_AA(p_out_aa)

(78) Obligation:

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

U6_AA(p_out_aa) → VL_IN_AA
VL_IN_AA → U6_AA(p_out_aa)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

(79) 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.

(80) Obligation:

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

U6_AA(p_out_aa) → VL_IN_AA
VL_IN_AA → U6_AA(p_out_aa)

R is empty.
The set Q consists of the following terms:

p_in_aa

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

(81) 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].

p_in_aa

(82) Obligation:

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

U6_AA(p_out_aa) → VL_IN_AA
VL_IN_AA → U6_AA(p_out_aa)

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

(83) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = VL_IN_AA evaluates to t =VL_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

VL_IN_AA → U6_AA(p_out_aa)
with rule VL_IN_AA → U6_AA(p_out_aa) at position [] and matcher [ ]

U6_AA(p_out_aa) → VL_IN_AA
with rule U6_AA(p_out_aa) → VL_IN_AA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(84) FALSE

(85) Obligation:

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

VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)

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

(86) UsableRulesProof (EQUIVALENT transformation)

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

(87) Obligation:

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

VL_IN_AG(N, .(X2, Xs)) → U6_AG(N, X2, Xs, p_in_aa(N, P))
U6_AG(N, X2, Xs, p_out_aa(N, P)) → VL_IN_AG(P, Xs)

The TRS R consists of the following rules:

p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
VL_IN_AG(x1, x2)  =  VL_IN_AG(x2)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)

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

(88) PiDPToQDPProof (SOUND transformation)

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

(89) Obligation:

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

VL_IN_AG(.(Xs)) → U6_AG(Xs, p_in_aa)
U6_AG(Xs, p_out_aa) → VL_IN_AG(Xs)

The TRS R consists of the following rules:

p_in_aa → p_out_aa

The set Q consists of the following terms:

p_in_aa

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

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

• U6_AG(Xs, p_out_aa) → VL_IN_AG(Xs)
  The graph contains the following edges 1 >= 1

• VL_IN_AG(.(Xs)) → U6_AG(Xs, p_in_aa)
  The graph contains the following edges 1 > 1

(91) TRUE

(92) Obligation:

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

SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
SELECT_IN_AGA(x1, x2, x3)  =  SELECT_IN_AGA(x2)

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

(93) UsableRulesProof (EQUIVALENT transformation)

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

(94) Obligation:

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

SELECT_IN_AGA(X, .(Y, Xs), .(Y, Ys)) → SELECT_IN_AGA(X, Xs, Ys)

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

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

(95) PiDPToQDPProof (SOUND transformation)

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

(96) Obligation:

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

SELECT_IN_AGA(.(Xs)) → SELECT_IN_AGA(Xs)

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

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

• SELECT_IN_AGA(.(Xs)) → SELECT_IN_AGA(Xs)
  The graph contains the following edges 1 > 1

(98) TRUE

(99) Obligation:

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

U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)

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

(100) UsableRulesProof (EQUIVALENT transformation)

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

(101) Obligation:

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

U1_A(N, vl_out_aa(N, Xs)) → U2_A(N, select_in_aga(X1, Xs, Ys))
U2_A(N, select_out_aga(X1, Xs, Ys)) → U3_A(N, vl_in_ag(M, Ys))
U3_A(N, vl_out_ag(M, Ys)) → VLCND_IN_A(M)
VLCND_IN_A(N) → U1_A(N, vl_in_aa(N, Xs))

The TRS R consists of the following rules:

select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
eq_in_gg(X, X) → eq_out_gg(X, X)
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
eq_in_ag(X, X) → eq_out_ag(X, X)
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))

The argument filtering Pi contains the following mapping:
0  =  0
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
VLCND_IN_A(x1)  =  VLCND_IN_A
U1_A(x1, x2)  =  U1_A(x2)
U2_A(x1, x2)  =  U2_A(x2)
U3_A(x1, x2)  =  U3_A(x2)

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

(102) PiDPToQDPProof (SOUND transformation)

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

(103) Obligation:

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

U1_A(vl_out_aa(Xs)) → U2_A(select_in_aga(Xs))
U2_A(select_out_aga(Ys)) → U3_A(vl_in_ag(Ys))
U3_A(vl_out_ag) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(104) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U1_A(vl_out_aa(Xs)) → U2_A(select_in_aga(Xs)) at position [0] we obtained the following new rules [LPAR04]:

U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))

(105) Obligation:

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

U2_A(select_out_aga(Ys)) → U3_A(vl_in_ag(Ys))
U3_A(vl_out_ag) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(106) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_A(select_out_aga(Ys)) → U3_A(vl_in_ag(Ys)) at position [0] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_in_aa))

(107) Obligation:

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

U3_A(vl_out_ag) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_in_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(108) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_in_aa)) at position [0,1] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))

(109) Obligation:

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

U3_A(vl_out_ag) → VLCND_IN_A
VLCND_IN_A → U1_A(vl_in_aa)
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(110) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule VLCND_IN_A → U1_A(vl_in_aa) at position [0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(U5_aa(eq_in_ag([])))
VLCND_IN_A → U1_A(U6_aa(p_in_aa))

(111) Obligation:

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

U3_A(vl_out_ag) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U5_aa(eq_in_ag([])))
VLCND_IN_A → U1_A(U6_aa(p_in_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(112) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VLCND_IN_A → U1_A(U5_aa(eq_in_ag([]))) at position [0,0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(U5_aa(eq_out_ag([])))

(113) Obligation:

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

U3_A(vl_out_ag) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U6_aa(p_in_aa))
VLCND_IN_A → U1_A(U5_aa(eq_out_ag([])))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(114) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VLCND_IN_A → U1_A(U6_aa(p_in_aa)) at position [0,0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(U6_aa(p_out_aa))

(115) Obligation:

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

U3_A(vl_out_ag) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U5_aa(eq_out_ag([])))
VLCND_IN_A → U1_A(U6_aa(p_out_aa))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(116) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule VLCND_IN_A → U1_A(U5_aa(eq_out_ag([]))) at position [0] we obtained the following new rules [LPAR04]:

VLCND_IN_A → U1_A(vl_out_aa([]))

(117) Obligation:

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

U3_A(vl_out_ag) → VLCND_IN_A
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
VLCND_IN_A → U1_A(U6_aa(p_out_aa))
VLCND_IN_A → U1_A(vl_out_aa([]))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(118) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(119) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, [])))
U3_A(vl_out_ag) → VLCND_IN_A
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(120) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U2_A(select_out_aga(x0)) → U3_A(U5_ag(eq_in_gg(x0, []))) at position [0,0] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga([])) → U3_A(U5_ag(eq_out_gg))

(121) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U3_A(vl_out_ag) → VLCND_IN_A
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga([])) → U3_A(U5_ag(eq_out_gg))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(122) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U2_A(select_out_aga([])) → U3_A(U5_ag(eq_out_gg)) at position [0] we obtained the following new rules [LPAR04]:

U2_A(select_out_aga([])) → U3_A(vl_out_ag)

(123) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U3_A(vl_out_ag) → VLCND_IN_A
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0))
U2_A(select_out_aga([])) → U3_A(vl_out_ag)

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(124) ForwardInstantiation (EQUIVALENT transformation)

By forward instantiating [JAR06] the rule U1_A(vl_out_aa(.(x0))) → U2_A(select_out_aga(x0)) we obtained the following new rules [LPAR04]:

U1_A(vl_out_aa(.(.(y_0)))) → U2_A(select_out_aga(.(y_0)))
U1_A(vl_out_aa(.([]))) → U2_A(select_out_aga([]))

(125) Obligation:

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

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
U1_A(vl_out_aa(.(x0))) → U2_A(U8_aga(select_in_aga(x0)))
U3_A(vl_out_ag) → VLCND_IN_A
U2_A(select_out_aga(.(x0))) → U3_A(U6_ag(x0, p_out_aa))
U2_A(select_out_aga([])) → U3_A(vl_out_ag)
U1_A(vl_out_aa(.(.(y_0)))) → U2_A(select_out_aga(.(y_0)))
U1_A(vl_out_aa(.([]))) → U2_A(select_out_aga([]))

The TRS R consists of the following rules:

select_in_aga(.(Xs)) → U8_aga(select_in_aga(Xs))
select_in_aga(.(Xs)) → select_out_aga(Xs)
vl_in_ag(L) → U5_ag(eq_in_gg(L, []))
vl_in_ag(.(Xs)) → U6_ag(Xs, p_in_aa)
vl_in_aa → U5_aa(eq_in_ag([]))
vl_in_aa → U6_aa(p_in_aa)
U8_aga(select_out_aga(Ys)) → select_out_aga(.(Ys))
U5_ag(eq_out_gg) → vl_out_ag
U6_ag(Xs, p_out_aa) → U7_ag(vl_in_ag(Xs))
U5_aa(eq_out_ag(L)) → vl_out_aa(L)
U6_aa(p_out_aa) → U7_aa(vl_in_aa)
eq_in_gg(X, X) → eq_out_gg
p_in_aa → p_out_aa
U7_ag(vl_out_ag) → vl_out_ag
eq_in_ag(X) → eq_out_ag(X)
U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs))

The set Q consists of the following terms:

select_in_aga(x0)
vl_in_ag(x0)
vl_in_aa
U8_aga(x0)
U5_ag(x0)
U6_ag(x0, x1)
U5_aa(x0)
U6_aa(x0)
eq_in_gg(x0, x1)
p_in_aa
U7_ag(x0)
eq_in_ag(x0)
U7_aa(x0)

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

(126) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the right:

s = VLCND_IN_A evaluates to t =VLCND_IN_A

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Matcher: [ ]
• Semiunifier: [ ]

---

Rewriting sequence

VLCND_IN_A → U1_A(U6_aa(p_out_aa))
with rule VLCND_IN_A → U1_A(U6_aa(p_out_aa)) and matcher [ ].

U1_A(U6_aa(p_out_aa)) → U1_A(U7_aa(vl_in_aa))
with rule U6_aa(p_out_aa) → U7_aa(vl_in_aa) at position [0] and matcher [ ]

U1_A(U7_aa(vl_in_aa)) → U1_A(U7_aa(U5_aa(eq_in_ag([]))))
with rule vl_in_aa → U5_aa(eq_in_ag([])) at position [0,0] and matcher [ ]

U1_A(U7_aa(U5_aa(eq_in_ag([])))) → U1_A(U7_aa(U5_aa(eq_out_ag([]))))
with rule eq_in_ag(X) → eq_out_ag(X) at position [0,0,0] and matcher [X / []]

U1_A(U7_aa(U5_aa(eq_out_ag([])))) → U1_A(U7_aa(vl_out_aa([])))
with rule U5_aa(eq_out_ag(L)) → vl_out_aa(L) at position [0,0] and matcher [L / []]

U1_A(U7_aa(vl_out_aa([]))) → U1_A(vl_out_aa(.([])))
with rule U7_aa(vl_out_aa(Xs)) → vl_out_aa(.(Xs)) at position [0] and matcher [Xs / []]

U1_A(vl_out_aa(.([]))) → U2_A(select_out_aga([]))
with rule U1_A(vl_out_aa(.([]))) → U2_A(select_out_aga([])) at position [] and matcher [ ]

U2_A(select_out_aga([])) → U3_A(vl_out_ag)
with rule U2_A(select_out_aga([])) → U3_A(vl_out_ag) at position [] and matcher [ ]

U3_A(vl_out_ag) → VLCND_IN_A
with rule U3_A(vl_out_ag) → VLCND_IN_A at position [] and matcher [ ]

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(127) FALSE

(128) Obligation:

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

VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)

The TRS R consists of the following rules:

vlcnd_in_g(N) → U1_g(N, vl_in_ga(N, Xs))
vl_in_ga(0, L) → U5_ga(L, eq_in_ag(L, []))
eq_in_ag(X, X) → eq_out_ag(X, X)
U5_ga(L, eq_out_ag(L, [])) → vl_out_ga(0, L)
vl_in_ga(N, .(X2, Xs)) → U6_ga(N, X2, Xs, p_in_ga(N, P))
p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)
U6_ga(N, X2, Xs, p_out_ga(N, P)) → U7_ga(N, X2, Xs, vl_in_ga(P, Xs))
U7_ga(N, X2, Xs, vl_out_ga(P, Xs)) → vl_out_ga(N, .(X2, Xs))
U1_g(N, vl_out_ga(N, Xs)) → U2_g(N, select_in_aga(X1, Xs, Ys))
select_in_aga(X, .(Y, Xs), .(Y, Ys)) → U8_aga(X, Y, Xs, Ys, select_in_aga(X, Xs, Ys))
select_in_aga(X, .(X, Xs), Xs) → select_out_aga(X, .(X, Xs), Xs)
U8_aga(X, Y, Xs, Ys, select_out_aga(X, Xs, Ys)) → select_out_aga(X, .(Y, Xs), .(Y, Ys))
U2_g(N, select_out_aga(X1, Xs, Ys)) → U3_g(N, vl_in_ag(M, Ys))
vl_in_ag(0, L) → U5_ag(L, eq_in_gg(L, []))
eq_in_gg(X, X) → eq_out_gg(X, X)
U5_ag(L, eq_out_gg(L, [])) → vl_out_ag(0, L)
vl_in_ag(N, .(X2, Xs)) → U6_ag(N, X2, Xs, p_in_aa(N, P))
p_in_aa(0, 0) → p_out_aa(0, 0)
p_in_aa(s(X), X) → p_out_aa(s(X), X)
U6_ag(N, X2, Xs, p_out_aa(N, P)) → U7_ag(N, X2, Xs, vl_in_ag(P, Xs))
U7_ag(N, X2, Xs, vl_out_ag(P, Xs)) → vl_out_ag(N, .(X2, Xs))
U3_g(N, vl_out_ag(M, Ys)) → U4_g(N, vlcnd_in_a(M))
vlcnd_in_a(N) → U1_a(N, vl_in_aa(N, Xs))
vl_in_aa(0, L) → U5_aa(L, eq_in_ag(L, []))
U5_aa(L, eq_out_ag(L, [])) → vl_out_aa(0, L)
vl_in_aa(N, .(X2, Xs)) → U6_aa(N, X2, Xs, p_in_aa(N, P))
U6_aa(N, X2, Xs, p_out_aa(N, P)) → U7_aa(N, X2, Xs, vl_in_aa(P, Xs))
U7_aa(N, X2, Xs, vl_out_aa(P, Xs)) → vl_out_aa(N, .(X2, Xs))
U1_a(N, vl_out_aa(N, Xs)) → U2_a(N, select_in_aga(X1, Xs, Ys))
U2_a(N, select_out_aga(X1, Xs, Ys)) → U3_a(N, vl_in_ag(M, Ys))
U3_a(N, vl_out_ag(M, Ys)) → U4_a(N, vlcnd_in_a(M))
vlcnd_in_a(0) → vlcnd_out_a(0)
U4_a(N, vlcnd_out_a(M)) → vlcnd_out_a(N)
U4_g(N, vlcnd_out_a(M)) → vlcnd_out_g(N)
vlcnd_in_g(0) → vlcnd_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd_in_g(x1)  =  vlcnd_in_g(x1)
U1_g(x1, x2)  =  U1_g(x2)
vl_in_ga(x1, x2)  =  vl_in_ga(x1)
0  =  0
U5_ga(x1, x2)  =  U5_ga(x2)
eq_in_ag(x1, x2)  =  eq_in_ag(x2)
eq_out_ag(x1, x2)  =  eq_out_ag(x1)
[]  =  []
vl_out_ga(x1, x2)  =  vl_out_ga(x2)
U6_ga(x1, x2, x3, x4)  =  U6_ga(x4)
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
U7_ga(x1, x2, x3, x4)  =  U7_ga(x4)
.(x1, x2)  =  .(x2)
U2_g(x1, x2)  =  U2_g(x2)
select_in_aga(x1, x2, x3)  =  select_in_aga(x2)
U8_aga(x1, x2, x3, x4, x5)  =  U8_aga(x5)
select_out_aga(x1, x2, x3)  =  select_out_aga(x3)
U3_g(x1, x2)  =  U3_g(x2)
vl_in_ag(x1, x2)  =  vl_in_ag(x2)
U5_ag(x1, x2)  =  U5_ag(x2)
eq_in_gg(x1, x2)  =  eq_in_gg(x1, x2)
eq_out_gg(x1, x2)  =  eq_out_gg
vl_out_ag(x1, x2)  =  vl_out_ag
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
p_in_aa(x1, x2)  =  p_in_aa
p_out_aa(x1, x2)  =  p_out_aa
U7_ag(x1, x2, x3, x4)  =  U7_ag(x4)
U4_g(x1, x2)  =  U4_g(x2)
vlcnd_in_a(x1)  =  vlcnd_in_a
U1_a(x1, x2)  =  U1_a(x2)
vl_in_aa(x1, x2)  =  vl_in_aa
U5_aa(x1, x2)  =  U5_aa(x2)
vl_out_aa(x1, x2)  =  vl_out_aa(x2)
U6_aa(x1, x2, x3, x4)  =  U6_aa(x4)
U7_aa(x1, x2, x3, x4)  =  U7_aa(x4)
U2_a(x1, x2)  =  U2_a(x2)
U3_a(x1, x2)  =  U3_a(x2)
U4_a(x1, x2)  =  U4_a(x2)
vlcnd_out_a(x1)  =  vlcnd_out_a
vlcnd_out_g(x1)  =  vlcnd_out_g
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)

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

(129) UsableRulesProof (EQUIVALENT transformation)

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

(130) Obligation:

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

VL_IN_GA(N, .(X2, Xs)) → U6_GA(N, X2, Xs, p_in_ga(N, P))
U6_GA(N, X2, Xs, p_out_ga(N, P)) → VL_IN_GA(P, Xs)

The TRS R consists of the following rules:

p_in_ga(0, 0) → p_out_ga(0, 0)
p_in_ga(s(X), X) → p_out_ga(s(X), X)

The argument filtering Pi contains the following mapping:
0  =  0
p_in_ga(x1, x2)  =  p_in_ga(x1)
p_out_ga(x1, x2)  =  p_out_ga(x2)
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
VL_IN_GA(x1, x2)  =  VL_IN_GA(x1)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x4)

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

(131) PiDPToQDPProof (SOUND transformation)

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

(132) Obligation:

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

VL_IN_GA(N) → U6_GA(p_in_ga(N))
U6_GA(p_out_ga(P)) → VL_IN_GA(P)

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)
p_in_ga(s(X)) → p_out_ga(X)

The set Q consists of the following terms:

p_in_ga(x0)

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

(133) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

p_in_ga(s(X)) → p_out_ga(X)

Used ordering: POLO with Polynomial interpretation [POLO]:

POL(0) = 0   
POL(U6_GA(x₁)) = x₁   
POL(VL_IN_GA(x₁)) = x₁   
POL(p_in_ga(x₁)) = x₁   
POL(p_out_ga(x₁)) = 2·x₁   
POL(s(x₁)) = 2·x₁   

(134) Obligation:

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

VL_IN_GA(N) → U6_GA(p_in_ga(N))
U6_GA(p_out_ga(P)) → VL_IN_GA(P)

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)

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

(135) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule VL_IN_GA(N) → U6_GA(p_in_ga(N)) at position [0] we obtained the following new rules [LPAR04]:

VL_IN_GA(0) → U6_GA(p_out_ga(0))

(136) Obligation:

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

U6_GA(p_out_ga(P)) → VL_IN_GA(P)
VL_IN_GA(0) → U6_GA(p_out_ga(0))

The TRS R consists of the following rules:

p_in_ga(0) → p_out_ga(0)

The set Q consists of the following terms:

p_in_ga(x0)

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

(137) 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.

(138) Obligation:

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

U6_GA(p_out_ga(P)) → VL_IN_GA(P)
VL_IN_GA(0) → U6_GA(p_out_ga(0))

R is empty.
The set Q consists of the following terms:

p_in_ga(x0)

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

(139) 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].

p_in_ga(x0)

(140) Obligation:

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

U6_GA(p_out_ga(P)) → VL_IN_GA(P)
VL_IN_GA(0) → U6_GA(p_out_ga(0))

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

(141) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_GA(p_out_ga(P)) → VL_IN_GA(P) we obtained the following new rules [LPAR04]:

U6_GA(p_out_ga(0)) → VL_IN_GA(0)

(142) Obligation:

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

VL_IN_GA(0) → U6_GA(p_out_ga(0))
U6_GA(p_out_ga(0)) → VL_IN_GA(0)

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

(143) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = U6_GA(p_out_ga(0)) evaluates to t =U6_GA(p_out_ga(0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:

• Semiunifier: [ ]
• Matcher: [ ]

---

Rewriting sequence

U6_GA(p_out_ga(0)) → VL_IN_GA(0)
with rule U6_GA(p_out_ga(0)) → VL_IN_GA(0) at position [] and matcher [ ]

VL_IN_GA(0) → U6_GA(p_out_ga(0))
with rule VL_IN_GA(0) → U6_GA(p_out_ga(0))

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.

(144) FALSE