(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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

vl6(0, []).
vl6(s(T5), .(X23, X24)) :- vl6(T5, X24).
select20(X39, .(T8, T10), .(T8, X40)) :- select20(X39, T10, X40).
select20(X45, .(X45, T11), T11).
p7(X7, T3, X8, X9) :- select20(X7, T3, X8).
p7(T6, T3, T7, X9) :- ','(select20(T6, T3, T7), vl30(X9, T7)).
p7(T6, T3, T7, T17) :- ','(select20(T6, T3, T7), ','(vl30(T17, T7), vl43(T17, X53))).
p7(T6, T3, T7, T17) :- ','(select20(T6, T3, T7), ','(vl30(T17, T7), ','(vl43(T17, T18), p7(X54, T18, X55, X56)))).
p7(T6, T3, T7, 0) :- ','(select20(T6, T3, T7), vl30(0, T7)).
vl43(0, []).
vl43(0, .(X70, [])).
vl43(s(T22), .(X70, X71)) :- vl43(T22, X71).
vl43(s(T24), .(X70, X71)) :- vl43(T24, X71).
vl30(0, []).
vlcnd1(T2) :- vl6(T2, X6).
vlcnd1(T2) :- ','(vl6(T2, T3), select20(X7, T3, X8)).
vlcnd1(T2) :- ','(vl6(T2, T3), ','(select20(T6, T3, T7), vl30(X9, T7))).
vlcnd1(T2) :- ','(vl6(T2, T3), ','(select20(T6, T3, T7), ','(vl30(T17, T7), vl43(T17, X53)))).
vlcnd1(T2) :- ','(vl6(T2, T3), ','(select20(T6, T3, T7), ','(vl30(T17, T7), ','(vl43(T17, T18), p7(X54, T18, X55, X56))))).
vlcnd1(T2) :- ','(vl6(T2, T3), ','(select20(T6, T3, T7), vl30(0, T7))).
vlcnd1(0).

Queries:

vlcnd1(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:
vlcnd1_in: (b)
vl6_in: (b,f)
select20_in: (f,b,f)
vl43_in: (b,f)
p7_in: (f,b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)

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

VLCND1_IN_G(T2) → U15_G(T2, vl6_in_ga(T2, X6))
VLCND1_IN_G(T2) → VL6_IN_GA(T2, X6)
VL6_IN_GA(s(T5), .(X23, X24)) → U1_GA(T5, X23, X24, vl6_in_ga(T5, X24))
VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)
VLCND1_IN_G(T2) → U16_G(T2, vl6_in_ga(T2, T3))
U16_G(T2, vl6_out_ga(T2, T3)) → U17_G(T2, select20_in_aga(X7, T3, X8))
U16_G(T2, vl6_out_ga(T2, T3)) → SELECT20_IN_AGA(X7, T3, X8)
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → U2_AGA(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)
U16_G(T2, vl6_out_ga(T2, T3)) → U18_G(T2, select20_in_aga(T6, T3, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → U19_G(T2, vl30_in_ag(X9, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U20_G(T2, vl30_in_ag(T17, T7))
U20_G(T2, vl30_out_ag(T17, T7)) → U21_G(T2, vl43_in_ga(T17, X53))
U20_G(T2, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
VL43_IN_GA(s(T22), .(X70, X71)) → U13_GA(T22, X70, X71, vl43_in_ga(T22, X71))
VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)
VL43_IN_GA(s(T24), .(X70, X71)) → U14_GA(T24, X70, X71, vl43_in_ga(T24, X71))
U20_G(T2, vl30_out_ag(T17, T7)) → U22_G(T2, vl43_in_ga(T17, T18))
U22_G(T2, vl43_out_ga(T17, T18)) → U23_G(T2, p7_in_agaa(X54, T18, X55, X56))
U22_G(T2, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(X7, T3, X8, X9) → U3_AGAA(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
P7_IN_AGAA(X7, T3, X8, X9) → SELECT20_IN_AGA(X7, T3, X8)
P7_IN_AGAA(T6, T3, T7, X9) → U4_AGAA(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_AGAA(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(T17, T7)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_AGAA(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(T6, T3, T7, 0) → U11_AGAA(T6, T3, T7, select20_in_aga(T6, T3, T7))
P7_IN_AGAA(T6, T3, T7, 0) → SELECT20_IN_AGA(T6, T3, T7)
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_AGAA(T6, T3, T7, vl30_in_gg(0, T7))
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U24_G(T2, vl30_in_gg(0, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)
VLCND1_IN_G(x1)  =  VLCND1_IN_G(x1)
U15_G(x1, x2)  =  U15_G(x1, x2)
VL6_IN_GA(x1, x2)  =  VL6_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U16_G(x1, x2)  =  U16_G(x1, x2)
U17_G(x1, x2)  =  U17_G(x1, x2)
SELECT20_IN_AGA(x1, x2, x3)  =  SELECT20_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5)  =  U2_AGA(x3, x5)
U18_G(x1, x2)  =  U18_G(x1, x2)
U19_G(x1, x2)  =  U19_G(x1, x2)
VL30_IN_AG(x1, x2)  =  VL30_IN_AG(x2)
U20_G(x1, x2)  =  U20_G(x1, x2)
U21_G(x1, x2)  =  U21_G(x1, x2)
VL43_IN_GA(x1, x2)  =  VL43_IN_GA(x1)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x4)
U22_G(x1, x2)  =  U22_G(x1, x2)
U23_G(x1, x2)  =  U23_G(x1, x2)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x2, x5)
U4_AGAA(x1, x2, x3, x4, x5)  =  U4_AGAA(x2, x5)
U5_AGAA(x1, x2, x3, x4, x5)  =  U5_AGAA(x2, x3, x5)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x3, x5)
U8_AGAA(x1, x2, x3, x4, x5)  =  U8_AGAA(x2, x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x3, x5)
U10_AGAA(x1, x2, x3, x4, x5)  =  U10_AGAA(x2, x3, x5)
U11_AGAA(x1, x2, x3, x4)  =  U11_AGAA(x2, x4)
U12_AGAA(x1, x2, x3, x4)  =  U12_AGAA(x2, x3, x4)
VL30_IN_GG(x1, x2)  =  VL30_IN_GG(x1, x2)
U24_G(x1, x2)  =  U24_G(x1, x2)

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

(6) Obligation:

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

VLCND1_IN_G(T2) → U15_G(T2, vl6_in_ga(T2, X6))
VLCND1_IN_G(T2) → VL6_IN_GA(T2, X6)
VL6_IN_GA(s(T5), .(X23, X24)) → U1_GA(T5, X23, X24, vl6_in_ga(T5, X24))
VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)
VLCND1_IN_G(T2) → U16_G(T2, vl6_in_ga(T2, T3))
U16_G(T2, vl6_out_ga(T2, T3)) → U17_G(T2, select20_in_aga(X7, T3, X8))
U16_G(T2, vl6_out_ga(T2, T3)) → SELECT20_IN_AGA(X7, T3, X8)
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → U2_AGA(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)
U16_G(T2, vl6_out_ga(T2, T3)) → U18_G(T2, select20_in_aga(T6, T3, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → U19_G(T2, vl30_in_ag(X9, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U20_G(T2, vl30_in_ag(T17, T7))
U20_G(T2, vl30_out_ag(T17, T7)) → U21_G(T2, vl43_in_ga(T17, X53))
U20_G(T2, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
VL43_IN_GA(s(T22), .(X70, X71)) → U13_GA(T22, X70, X71, vl43_in_ga(T22, X71))
VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)
VL43_IN_GA(s(T24), .(X70, X71)) → U14_GA(T24, X70, X71, vl43_in_ga(T24, X71))
U20_G(T2, vl30_out_ag(T17, T7)) → U22_G(T2, vl43_in_ga(T17, T18))
U22_G(T2, vl43_out_ga(T17, T18)) → U23_G(T2, p7_in_agaa(X54, T18, X55, X56))
U22_G(T2, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(X7, T3, X8, X9) → U3_AGAA(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
P7_IN_AGAA(X7, T3, X8, X9) → SELECT20_IN_AGA(X7, T3, X8)
P7_IN_AGAA(T6, T3, T7, X9) → U4_AGAA(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_AGAA(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(T17, T7)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_AGAA(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(T6, T3, T7, 0) → U11_AGAA(T6, T3, T7, select20_in_aga(T6, T3, T7))
P7_IN_AGAA(T6, T3, T7, 0) → SELECT20_IN_AGA(T6, T3, T7)
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_AGAA(T6, T3, T7, vl30_in_gg(0, T7))
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U24_G(T2, vl30_in_gg(0, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)
VLCND1_IN_G(x1)  =  VLCND1_IN_G(x1)
U15_G(x1, x2)  =  U15_G(x1, x2)
VL6_IN_GA(x1, x2)  =  VL6_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x1, x4)
U16_G(x1, x2)  =  U16_G(x1, x2)
U17_G(x1, x2)  =  U17_G(x1, x2)
SELECT20_IN_AGA(x1, x2, x3)  =  SELECT20_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5)  =  U2_AGA(x3, x5)
U18_G(x1, x2)  =  U18_G(x1, x2)
U19_G(x1, x2)  =  U19_G(x1, x2)
VL30_IN_AG(x1, x2)  =  VL30_IN_AG(x2)
U20_G(x1, x2)  =  U20_G(x1, x2)
U21_G(x1, x2)  =  U21_G(x1, x2)
VL43_IN_GA(x1, x2)  =  VL43_IN_GA(x1)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x4)
U22_G(x1, x2)  =  U22_G(x1, x2)
U23_G(x1, x2)  =  U23_G(x1, x2)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x2, x5)
U4_AGAA(x1, x2, x3, x4, x5)  =  U4_AGAA(x2, x5)
U5_AGAA(x1, x2, x3, x4, x5)  =  U5_AGAA(x2, x3, x5)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x3, x5)
U8_AGAA(x1, x2, x3, x4, x5)  =  U8_AGAA(x2, x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x3, x5)
U10_AGAA(x1, x2, x3, x4, x5)  =  U10_AGAA(x2, x3, x5)
U11_AGAA(x1, x2, x3, x4)  =  U11_AGAA(x2, x4)
U12_AGAA(x1, x2, x3, x4)  =  U12_AGAA(x2, x3, x4)
VL30_IN_GG(x1, x2)  =  VL30_IN_GG(x1, x2)
U24_G(x1, x2)  =  U24_G(x1, x2)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 33 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)
VL43_IN_GA(x1, x2)  =  VL43_IN_GA(x1)

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:

VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)

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

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:

VL43_IN_GA(s(T22)) → VL43_IN_GA(T22)

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

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

  • VL43_IN_GA(s(T22)) → VL43_IN_GA(T22)
    The graph contains the following edges 1 > 1

(15) TRUE

(16) Obligation:

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

SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)
SELECT20_IN_AGA(x1, x2, x3)  =  SELECT20_IN_AGA(x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

SELECT20_IN_AGA(.(T10)) → SELECT20_IN_AGA(T10)

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

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

  • SELECT20_IN_AGA(.(T10)) → SELECT20_IN_AGA(T10)
    The graph contains the following edges 1 > 1

(22) TRUE

(23) Obligation:

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

P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x3, x5)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)

The TRS R consists of the following rules:

select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
vl30_in_ag(0, []) → vl30_out_ag(0, [])
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x2, x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x2, x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x2, x3, x5)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U6_AGAA(T3, select20_out_aga(T3, T7)) → U7_AGAA(T3, T7, vl30_in_ag(T7))
U7_AGAA(T3, T7, vl30_out_ag(T17, T7)) → U9_AGAA(T3, T7, vl43_in_ga(T17))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
vl30_in_ag([]) → vl30_out_ag(0, [])
vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
vl43_in_ga(s(T22)) → U13_ga(T22, vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(T24, vl43_in_ga(T24))
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))
U13_ga(T22, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X71))
U14_ga(T24, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X71))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)
U13_ga(x0, x1)
U14_ga(x0, x1)

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

(28) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U6_AGAA(T3, select20_out_aga(T3, T7)) → U7_AGAA(T3, T7, vl30_in_ag(T7)) at position [2] we obtained the following new rules [LPAR04]:

U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))

(29) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U7_AGAA(T3, T7, vl30_out_ag(T17, T7)) → U9_AGAA(T3, T7, vl43_in_ga(T17))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
vl30_in_ag([]) → vl30_out_ag(0, [])
vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
vl43_in_ga(s(T22)) → U13_ga(T22, vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(T24, vl43_in_ga(T24))
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))
U13_ga(T22, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X71))
U14_ga(T24, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X71))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)
U13_ga(x0, x1)
U14_ga(x0, x1)

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

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

(31) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U7_AGAA(T3, T7, vl30_out_ag(T17, T7)) → U9_AGAA(T3, T7, vl43_in_ga(T17))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
vl43_in_ga(s(T22)) → U13_ga(T22, vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(T24, vl43_in_ga(T24))
U14_ga(T24, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X71))
U13_ga(T22, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X71))
select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)
U13_ga(x0, x1)
U14_ga(x0, x1)

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

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

vl30_in_ag(x0)

(33) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U7_AGAA(T3, T7, vl30_out_ag(T17, T7)) → U9_AGAA(T3, T7, vl43_in_ga(T17))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
vl43_in_ga(s(T22)) → U13_ga(T22, vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(T24, vl43_in_ga(T24))
U14_ga(T24, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X71))
U13_ga(T22, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X71))
select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)
U13_ga(x0, x1)
U14_ga(x0, x1)

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

(34) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_AGAA(T3, T7, vl30_out_ag(T17, T7)) → U9_AGAA(T3, T7, vl43_in_ga(T17)) we obtained the following new rules [LPAR04]:

U7_AGAA(z0, [], vl30_out_ag(0, [])) → U9_AGAA(z0, [], vl43_in_ga(0))

(35) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(z0, [], vl30_out_ag(0, [])) → U9_AGAA(z0, [], vl43_in_ga(0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
vl43_in_ga(s(T22)) → U13_ga(T22, vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(T24, vl43_in_ga(T24))
U14_ga(T24, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X71))
U13_ga(T22, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X71))
select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)
U13_ga(x0, x1)
U14_ga(x0, x1)

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

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

(37) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(z0, [], vl30_out_ag(0, [])) → U9_AGAA(z0, [], vl43_in_ga(0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)
U13_ga(x0, x1)
U14_ga(x0, x1)

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

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

U13_ga(x0, x1)
U14_ga(x0, x1)

(39) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(z0, [], vl30_out_ag(0, [])) → U9_AGAA(z0, [], vl43_in_ga(0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)

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

(40) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U7_AGAA(z0, [], vl30_out_ag(0, [])) → U9_AGAA(z0, [], vl43_in_ga(0)) at position [2] we obtained the following new rules [LPAR04]:

U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

(41) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(0, [])
vl43_in_ga(0) → vl43_out_ga(0, .([]))
select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)

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

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

(43) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl43_in_ga(x0)
U2_aga(x0, x1)

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

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

vl43_in_ga(x0)

(45) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18)
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
U2_aga(x0, x1)

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

(46) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U9_AGAA(T3, T7, vl43_out_ga(T17, T18)) → P7_IN_AGAA(T18) we obtained the following new rules [LPAR04]:

U9_AGAA(z0, [], vl43_out_ga(0, [])) → P7_IN_AGAA([])
U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))

(47) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))
U9_AGAA(z0, [], vl43_out_ga(0, [])) → P7_IN_AGAA([])
U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
U2_aga(x0, x1)

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

(48) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P7_IN_AGAA(T3) → U6_AGAA(T3, select20_in_aga(T3)) at position [1] we obtained the following new rules [LPAR04]:

P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), U2_aga(x0, select20_in_aga(x0)))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))

(49) Obligation:

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

U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))
U9_AGAA(z0, [], vl43_out_ga(0, [])) → P7_IN_AGAA([])
U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), U2_aga(x0, select20_in_aga(x0)))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
U2_aga(x0, x1)

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

(50) DependencyGraphProof (EQUIVALENT transformation)

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

(51) Obligation:

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

U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))
U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), U2_aga(x0, select20_in_aga(x0)))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
U2_aga(x0, x1)

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

(52) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), U2_aga(x0, select20_in_aga(x0))) at position [1,1] we obtained the following new rules [LPAR04]:

P7_IN_AGAA(.(.(x0))) → U6_AGAA(.(.(x0)), U2_aga(.(x0), U2_aga(x0, select20_in_aga(x0))))
P7_IN_AGAA(.(.(x0))) → U6_AGAA(.(.(x0)), U2_aga(.(x0), select20_out_aga(.(x0), x0)))

(53) Obligation:

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

U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))
U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))
P7_IN_AGAA(.(.(x0))) → U6_AGAA(.(.(x0)), U2_aga(.(x0), U2_aga(x0, select20_in_aga(x0))))
P7_IN_AGAA(.(.(x0))) → U6_AGAA(.(.(x0)), U2_aga(.(x0), select20_out_aga(.(x0), x0)))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
U2_aga(x0, x1)

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

(54) DependencyGraphProof (EQUIVALENT transformation)

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

(55) Obligation:

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

U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(T10, select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(.(T11), T11)
U2_aga(T10, select20_out_aga(T10, X40)) → select20_out_aga(.(T10), .(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
U2_aga(x0, x1)

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

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

(57) Obligation:

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

U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

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

select20_in_aga(x0)
U2_aga(x0, x1)

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

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

select20_in_aga(x0)
U2_aga(x0, x1)

(59) Obligation:

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

U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))

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

(60) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule P7_IN_AGAA(.(x0)) → U6_AGAA(.(x0), select20_out_aga(.(x0), x0)) we obtained the following new rules [LPAR04]:

P7_IN_AGAA(.([])) → U6_AGAA(.([]), select20_out_aga(.([]), []))

(61) Obligation:

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

U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, []))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))
P7_IN_AGAA(.([])) → U6_AGAA(.([]), select20_out_aga(.([]), []))

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

(62) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U6_AGAA(y0, select20_out_aga(y0, [])) → U7_AGAA(y0, [], vl30_out_ag(0, [])) we obtained the following new rules [LPAR04]:

U6_AGAA(.([]), select20_out_aga(.([]), [])) → U7_AGAA(.([]), [], vl30_out_ag(0, []))

(63) Obligation:

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

U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([])))
P7_IN_AGAA(.([])) → U6_AGAA(.([]), select20_out_aga(.([]), []))
U6_AGAA(.([]), select20_out_aga(.([]), [])) → U7_AGAA(.([]), [], vl30_out_ag(0, []))

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

(64) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_AGAA(y0, [], vl30_out_ag(0, [])) → U9_AGAA(y0, [], vl43_out_ga(0, .([]))) we obtained the following new rules [LPAR04]:

U7_AGAA(.([]), [], vl30_out_ag(0, [])) → U9_AGAA(.([]), [], vl43_out_ga(0, .([])))

(65) Obligation:

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

U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.([])) → U6_AGAA(.([]), select20_out_aga(.([]), []))
U6_AGAA(.([]), select20_out_aga(.([]), [])) → U7_AGAA(.([]), [], vl30_out_ag(0, []))
U7_AGAA(.([]), [], vl30_out_ag(0, [])) → U9_AGAA(.([]), [], vl43_out_ga(0, .([])))

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

(66) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U9_AGAA(z0, [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([])) we obtained the following new rules [LPAR04]:

U9_AGAA(.([]), [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))

(67) Obligation:

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

P7_IN_AGAA(.([])) → U6_AGAA(.([]), select20_out_aga(.([]), []))
U6_AGAA(.([]), select20_out_aga(.([]), [])) → U7_AGAA(.([]), [], vl30_out_ag(0, []))
U7_AGAA(.([]), [], vl30_out_ag(0, [])) → U9_AGAA(.([]), [], vl43_out_ga(0, .([])))
U9_AGAA(.([]), [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([]))

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

(68) 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_AGAA(.([]), select20_out_aga(.([]), [])) evaluates to t =U6_AGAA(.([]), select20_out_aga(.([]), []))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]




Rewriting sequence

U6_AGAA(.([]), select20_out_aga(.([]), []))U7_AGAA(.([]), [], vl30_out_ag(0, []))
with rule U6_AGAA(.([]), select20_out_aga(.([]), [])) → U7_AGAA(.([]), [], vl30_out_ag(0, [])) at position [] and matcher [ ]

U7_AGAA(.([]), [], vl30_out_ag(0, []))U9_AGAA(.([]), [], vl43_out_ga(0, .([])))
with rule U7_AGAA(.([]), [], vl30_out_ag(0, [])) → U9_AGAA(.([]), [], vl43_out_ga(0, .([]))) at position [] and matcher [ ]

U9_AGAA(.([]), [], vl43_out_ga(0, .([])))P7_IN_AGAA(.([]))
with rule U9_AGAA(.([]), [], vl43_out_ga(0, .([]))) → P7_IN_AGAA(.([])) at position [] and matcher [ ]

P7_IN_AGAA(.([]))U6_AGAA(.([]), select20_out_aga(.([]), []))
with rule P7_IN_AGAA(.([])) → U6_AGAA(.([]), select20_out_aga(.([]), []))

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.



(69) FALSE

(70) Obligation:

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

VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x1, x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x1, x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x1, x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g(x1)
U16_g(x1, x2)  =  U16_g(x1, x2)
U17_g(x1, x2)  =  U17_g(x1, x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x3, x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x2, x3)
U18_g(x1, x2)  =  U18_g(x1, x2)
U19_g(x1, x2)  =  U19_g(x1, x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1, x2)
U20_g(x1, x2)  =  U20_g(x1, x2)
U21_g(x1, x2)  =  U21_g(x1, x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x1, x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x1, x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x4)
U22_g(x1, x2)  =  U22_g(x1, x2)
U23_g(x1, x2)  =  U23_g(x1, x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x2, x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x2, x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x2, x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x2, x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x2, x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x2, x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x2, x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x2, x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x2, x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x2, x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg(x1, x2)
U24_g(x1, x2)  =  U24_g(x1, x2)
VL6_IN_GA(x1, x2)  =  VL6_IN_GA(x1)

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

(71) UsableRulesProof (EQUIVALENT transformation)

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

(72) Obligation:

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

VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)

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

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

(73) PiDPToQDPProof (SOUND transformation)

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

(74) Obligation:

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

VL6_IN_GA(s(T5)) → VL6_IN_GA(T5)

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

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

  • VL6_IN_GA(s(T5)) → VL6_IN_GA(T5)
    The graph contains the following edges 1 > 1

(76) TRUE

(77) PrologToPiTRSProof (SOUND transformation)

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

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(78) Obligation:

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

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)

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

VLCND1_IN_G(T2) → U15_G(T2, vl6_in_ga(T2, X6))
VLCND1_IN_G(T2) → VL6_IN_GA(T2, X6)
VL6_IN_GA(s(T5), .(X23, X24)) → U1_GA(T5, X23, X24, vl6_in_ga(T5, X24))
VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)
VLCND1_IN_G(T2) → U16_G(T2, vl6_in_ga(T2, T3))
U16_G(T2, vl6_out_ga(T2, T3)) → U17_G(T2, select20_in_aga(X7, T3, X8))
U16_G(T2, vl6_out_ga(T2, T3)) → SELECT20_IN_AGA(X7, T3, X8)
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → U2_AGA(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)
U16_G(T2, vl6_out_ga(T2, T3)) → U18_G(T2, select20_in_aga(T6, T3, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → U19_G(T2, vl30_in_ag(X9, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U20_G(T2, vl30_in_ag(T17, T7))
U20_G(T2, vl30_out_ag(T17, T7)) → U21_G(T2, vl43_in_ga(T17, X53))
U20_G(T2, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
VL43_IN_GA(s(T22), .(X70, X71)) → U13_GA(T22, X70, X71, vl43_in_ga(T22, X71))
VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)
VL43_IN_GA(s(T24), .(X70, X71)) → U14_GA(T24, X70, X71, vl43_in_ga(T24, X71))
U20_G(T2, vl30_out_ag(T17, T7)) → U22_G(T2, vl43_in_ga(T17, T18))
U22_G(T2, vl43_out_ga(T17, T18)) → U23_G(T2, p7_in_agaa(X54, T18, X55, X56))
U22_G(T2, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(X7, T3, X8, X9) → U3_AGAA(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
P7_IN_AGAA(X7, T3, X8, X9) → SELECT20_IN_AGA(X7, T3, X8)
P7_IN_AGAA(T6, T3, T7, X9) → U4_AGAA(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_AGAA(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(T17, T7)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_AGAA(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(T6, T3, T7, 0) → U11_AGAA(T6, T3, T7, select20_in_aga(T6, T3, T7))
P7_IN_AGAA(T6, T3, T7, 0) → SELECT20_IN_AGA(T6, T3, T7)
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_AGAA(T6, T3, T7, vl30_in_gg(0, T7))
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U24_G(T2, vl30_in_gg(0, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)
VLCND1_IN_G(x1)  =  VLCND1_IN_G(x1)
U15_G(x1, x2)  =  U15_G(x2)
VL6_IN_GA(x1, x2)  =  VL6_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U16_G(x1, x2)  =  U16_G(x2)
U17_G(x1, x2)  =  U17_G(x2)
SELECT20_IN_AGA(x1, x2, x3)  =  SELECT20_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5)  =  U2_AGA(x5)
U18_G(x1, x2)  =  U18_G(x2)
U19_G(x1, x2)  =  U19_G(x2)
VL30_IN_AG(x1, x2)  =  VL30_IN_AG(x2)
U20_G(x1, x2)  =  U20_G(x2)
U21_G(x1, x2)  =  U21_G(x2)
VL43_IN_GA(x1, x2)  =  VL43_IN_GA(x1)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x4)
U22_G(x1, x2)  =  U22_G(x2)
U23_G(x1, x2)  =  U23_G(x2)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x5)
U4_AGAA(x1, x2, x3, x4, x5)  =  U4_AGAA(x5)
U5_AGAA(x1, x2, x3, x4, x5)  =  U5_AGAA(x3, x5)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x3, x5)
U8_AGAA(x1, x2, x3, x4, x5)  =  U8_AGAA(x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x3, x5)
U10_AGAA(x1, x2, x3, x4, x5)  =  U10_AGAA(x3, x5)
U11_AGAA(x1, x2, x3, x4)  =  U11_AGAA(x4)
U12_AGAA(x1, x2, x3, x4)  =  U12_AGAA(x3, x4)
VL30_IN_GG(x1, x2)  =  VL30_IN_GG(x1, x2)
U24_G(x1, x2)  =  U24_G(x2)

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

(80) Obligation:

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

VLCND1_IN_G(T2) → U15_G(T2, vl6_in_ga(T2, X6))
VLCND1_IN_G(T2) → VL6_IN_GA(T2, X6)
VL6_IN_GA(s(T5), .(X23, X24)) → U1_GA(T5, X23, X24, vl6_in_ga(T5, X24))
VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)
VLCND1_IN_G(T2) → U16_G(T2, vl6_in_ga(T2, T3))
U16_G(T2, vl6_out_ga(T2, T3)) → U17_G(T2, select20_in_aga(X7, T3, X8))
U16_G(T2, vl6_out_ga(T2, T3)) → SELECT20_IN_AGA(X7, T3, X8)
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → U2_AGA(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)
U16_G(T2, vl6_out_ga(T2, T3)) → U18_G(T2, select20_in_aga(T6, T3, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → U19_G(T2, vl30_in_ag(X9, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U20_G(T2, vl30_in_ag(T17, T7))
U20_G(T2, vl30_out_ag(T17, T7)) → U21_G(T2, vl43_in_ga(T17, X53))
U20_G(T2, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
VL43_IN_GA(s(T22), .(X70, X71)) → U13_GA(T22, X70, X71, vl43_in_ga(T22, X71))
VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)
VL43_IN_GA(s(T24), .(X70, X71)) → U14_GA(T24, X70, X71, vl43_in_ga(T24, X71))
U20_G(T2, vl30_out_ag(T17, T7)) → U22_G(T2, vl43_in_ga(T17, T18))
U22_G(T2, vl43_out_ga(T17, T18)) → U23_G(T2, p7_in_agaa(X54, T18, X55, X56))
U22_G(T2, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(X7, T3, X8, X9) → U3_AGAA(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
P7_IN_AGAA(X7, T3, X8, X9) → SELECT20_IN_AGA(X7, T3, X8)
P7_IN_AGAA(T6, T3, T7, X9) → U4_AGAA(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_AGAA(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U4_AGAA(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(X9, T7)
P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → VL30_IN_AG(T17, T7)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → VL43_IN_GA(T17, X53)
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_AGAA(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)
P7_IN_AGAA(T6, T3, T7, 0) → U11_AGAA(T6, T3, T7, select20_in_aga(T6, T3, T7))
P7_IN_AGAA(T6, T3, T7, 0) → SELECT20_IN_AGA(T6, T3, T7)
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_AGAA(T6, T3, T7, vl30_in_gg(0, T7))
U11_AGAA(T6, T3, T7, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)
U18_G(T2, select20_out_aga(T6, T3, T7)) → U24_G(T2, vl30_in_gg(0, T7))
U18_G(T2, select20_out_aga(T6, T3, T7)) → VL30_IN_GG(0, T7)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)
VLCND1_IN_G(x1)  =  VLCND1_IN_G(x1)
U15_G(x1, x2)  =  U15_G(x2)
VL6_IN_GA(x1, x2)  =  VL6_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U16_G(x1, x2)  =  U16_G(x2)
U17_G(x1, x2)  =  U17_G(x2)
SELECT20_IN_AGA(x1, x2, x3)  =  SELECT20_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5)  =  U2_AGA(x5)
U18_G(x1, x2)  =  U18_G(x2)
U19_G(x1, x2)  =  U19_G(x2)
VL30_IN_AG(x1, x2)  =  VL30_IN_AG(x2)
U20_G(x1, x2)  =  U20_G(x2)
U21_G(x1, x2)  =  U21_G(x2)
VL43_IN_GA(x1, x2)  =  VL43_IN_GA(x1)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x4)
U22_G(x1, x2)  =  U22_G(x2)
U23_G(x1, x2)  =  U23_G(x2)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x5)
U4_AGAA(x1, x2, x3, x4, x5)  =  U4_AGAA(x5)
U5_AGAA(x1, x2, x3, x4, x5)  =  U5_AGAA(x3, x5)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x3, x5)
U8_AGAA(x1, x2, x3, x4, x5)  =  U8_AGAA(x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x3, x5)
U10_AGAA(x1, x2, x3, x4, x5)  =  U10_AGAA(x3, x5)
U11_AGAA(x1, x2, x3, x4)  =  U11_AGAA(x4)
U12_AGAA(x1, x2, x3, x4)  =  U12_AGAA(x3, x4)
VL30_IN_GG(x1, x2)  =  VL30_IN_GG(x1, x2)
U24_G(x1, x2)  =  U24_G(x2)

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

(81) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 33 less nodes.

(82) Complex Obligation (AND)

(83) Obligation:

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

VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)
VL43_IN_GA(x1, x2)  =  VL43_IN_GA(x1)

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

(84) UsableRulesProof (EQUIVALENT transformation)

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

(85) Obligation:

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

VL43_IN_GA(s(T22), .(X70, X71)) → VL43_IN_GA(T22, X71)

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

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

(86) PiDPToQDPProof (SOUND transformation)

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

(87) Obligation:

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

VL43_IN_GA(s(T22)) → VL43_IN_GA(T22)

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

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

  • VL43_IN_GA(s(T22)) → VL43_IN_GA(T22)
    The graph contains the following edges 1 > 1

(89) TRUE

(90) Obligation:

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

SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)
SELECT20_IN_AGA(x1, x2, x3)  =  SELECT20_IN_AGA(x2)

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

(91) UsableRulesProof (EQUIVALENT transformation)

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

(92) Obligation:

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

SELECT20_IN_AGA(X39, .(T8, T10), .(T8, X40)) → SELECT20_IN_AGA(X39, T10, X40)

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

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

(93) PiDPToQDPProof (SOUND transformation)

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

(94) Obligation:

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

SELECT20_IN_AGA(.(T10)) → SELECT20_IN_AGA(T10)

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

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

  • SELECT20_IN_AGA(.(T10)) → SELECT20_IN_AGA(T10)
    The graph contains the following edges 1 > 1

(96) TRUE

(97) Obligation:

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

P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x3, x5)

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

(98) UsableRulesProof (EQUIVALENT transformation)

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

(99) Obligation:

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

P7_IN_AGAA(T6, T3, T7, T17) → U6_AGAA(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_AGAA(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_AGAA(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_AGAA(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_AGAA(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_AGAA(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → P7_IN_AGAA(X54, T18, X55, X56)

The TRS R consists of the following rules:

select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
vl30_in_ag(0, []) → vl30_out_ag(0, [])
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))

The argument filtering Pi contains the following mapping:
0  =  0
s(x1)  =  s(x1)
.(x1, x2)  =  .(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
P7_IN_AGAA(x1, x2, x3, x4)  =  P7_IN_AGAA(x2)
U6_AGAA(x1, x2, x3, x4, x5)  =  U6_AGAA(x5)
U7_AGAA(x1, x2, x3, x4, x5)  =  U7_AGAA(x3, x5)
U9_AGAA(x1, x2, x3, x4, x5)  =  U9_AGAA(x3, x5)

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

(100) PiDPToQDPProof (SOUND transformation)

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

(101) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

select20_in_aga(.(T10)) → U2_aga(select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(T11)
vl30_in_ag([]) → vl30_out_ag(0)
vl43_in_ga(0) → vl43_out_ga([])
vl43_in_ga(0) → vl43_out_ga(.([]))
vl43_in_ga(s(T22)) → U13_ga(vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(vl43_in_ga(T24))
U2_aga(select20_out_aga(X40)) → select20_out_aga(.(X40))
U13_ga(vl43_out_ga(X71)) → vl43_out_ga(.(X71))
U14_ga(vl43_out_ga(X71)) → vl43_out_ga(.(X71))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)
U13_ga(x0)
U14_ga(x0)

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

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

vl43_in_ga(s(T22)) → U13_ga(vl43_in_ga(T22))
vl43_in_ga(s(T24)) → U14_ga(vl43_in_ga(T24))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x1)) = 2·x1   
POL(0) = 0   
POL(P7_IN_AGAA(x1)) = 2·x1   
POL(U13_ga(x1)) = 2·x1   
POL(U14_ga(x1)) = 2·x1   
POL(U2_aga(x1)) = 2·x1   
POL(U6_AGAA(x1)) = 2·x1   
POL(U7_AGAA(x1, x2)) = x1 + x2   
POL(U9_AGAA(x1, x2)) = x1 + 2·x2   
POL([]) = 0   
POL(s(x1)) = 1 + 2·x1   
POL(select20_in_aga(x1)) = x1   
POL(select20_out_aga(x1)) = x1   
POL(vl30_in_ag(x1)) = x1   
POL(vl30_out_ag(x1)) = 2·x1   
POL(vl43_in_ga(x1)) = x1   
POL(vl43_out_ga(x1)) = x1   

(103) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga([])
vl43_in_ga(0) → vl43_out_ga(.([]))
U14_ga(vl43_out_ga(X71)) → vl43_out_ga(.(X71))
U13_ga(vl43_out_ga(X71)) → vl43_out_ga(.(X71))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T10)) → U2_aga(select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(T11)
U2_aga(select20_out_aga(X40)) → select20_out_aga(.(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)
U13_ga(x0)
U14_ga(x0)

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

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

(105) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga([])
vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T10)) → U2_aga(select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(T11)
U2_aga(select20_out_aga(X40)) → select20_out_aga(.(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)
U13_ga(x0)
U14_ga(x0)

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

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

U13_ga(x0)
U14_ga(x0)

(107) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga([])
vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T10)) → U2_aga(select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(T11)
U2_aga(select20_out_aga(X40)) → select20_out_aga(.(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)

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

(108) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

vl43_in_ga(0) → vl43_out_ga([])

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1)) = 1 + x1   
POL(0) = 0   
POL(P7_IN_AGAA(x1)) = 2·x1   
POL(U2_aga(x1)) = 1 + x1   
POL(U6_AGAA(x1)) = 2·x1   
POL(U7_AGAA(x1, x2)) = x1 + x2   
POL(U9_AGAA(x1, x2)) = x1 + x2   
POL([]) = 0   
POL(select20_in_aga(x1)) = x1   
POL(select20_out_aga(x1)) = 1 + x1   
POL(vl30_in_ag(x1)) = 2 + x1   
POL(vl30_out_ag(x1)) = 2 + 2·x1   
POL(vl43_in_ga(x1)) = 2 + 2·x1   
POL(vl43_out_ga(x1)) = 2·x1   

(109) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T10)) → U2_aga(select20_in_aga(T10))
select20_in_aga(.(T11)) → select20_out_aga(T11)
U2_aga(select20_out_aga(X40)) → select20_out_aga(.(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)

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

(110) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

select20_in_aga(.(T10)) → U2_aga(select20_in_aga(T10))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1)) = 1 + 2·x1   
POL(0) = 0   
POL(P7_IN_AGAA(x1)) = 2·x1   
POL(U2_aga(x1)) = 2·x1   
POL(U6_AGAA(x1)) = x1   
POL(U7_AGAA(x1, x2)) = 1 + x1 + x2   
POL(U9_AGAA(x1, x2)) = x1 + 2·x2   
POL([]) = 0   
POL(select20_in_aga(x1)) = 2·x1   
POL(select20_out_aga(x1)) = 2 + 2·x1   
POL(vl30_in_ag(x1)) = 1 + x1   
POL(vl30_out_ag(x1)) = 1 + 2·x1   
POL(vl43_in_ga(x1)) = 1 + x1   
POL(vl43_out_ga(x1)) = x1   

(111) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T11)) → select20_out_aga(T11)
U2_aga(select20_out_aga(X40)) → select20_out_aga(.(X40))

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)

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

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

(113) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T11)) → select20_out_aga(T11)

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)
U2_aga(x0)

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

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

U2_aga(x0)

(115) Obligation:

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

P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3))
U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T11)) → select20_out_aga(T11)

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)

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

(116) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P7_IN_AGAA(T3) → U6_AGAA(select20_in_aga(T3)) at position [0] we obtained the following new rules [LPAR04]:

P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))

(117) Obligation:

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

U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)
select20_in_aga(.(T11)) → select20_out_aga(T11)

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)

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

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

(119) Obligation:

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

U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)

The set Q consists of the following terms:

select20_in_aga(x0)
vl30_in_ag(x0)
vl43_in_ga(x0)

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

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

select20_in_aga(x0)

(121) Obligation:

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

U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7))
U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)

The set Q consists of the following terms:

vl30_in_ag(x0)
vl43_in_ga(x0)

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

(122) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U6_AGAA(select20_out_aga(T7)) → U7_AGAA(T7, vl30_in_ag(T7)) at position [1] we obtained the following new rules [LPAR04]:

U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))

(123) Obligation:

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

U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))
vl30_in_ag([]) → vl30_out_ag(0)

The set Q consists of the following terms:

vl30_in_ag(x0)
vl43_in_ga(x0)

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

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

(125) Obligation:

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

U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))

The set Q consists of the following terms:

vl30_in_ag(x0)
vl43_in_ga(x0)

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

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

vl30_in_ag(x0)

(127) Obligation:

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

U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17))
U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))

The set Q consists of the following terms:

vl43_in_ga(x0)

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

(128) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule U7_AGAA(T7, vl30_out_ag(T17)) → U9_AGAA(T7, vl43_in_ga(T17)) at position [1] we obtained the following new rules [LPAR04]:

U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([])))

(129) Obligation:

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

U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([])))

The TRS R consists of the following rules:

vl43_in_ga(0) → vl43_out_ga(.([]))

The set Q consists of the following terms:

vl43_in_ga(x0)

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

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

(131) Obligation:

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

U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([])))

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

vl43_in_ga(x0)

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

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

vl43_in_ga(x0)

(133) Obligation:

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

U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18)
P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([])))

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

(134) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U9_AGAA(T7, vl43_out_ga(T18)) → P7_IN_AGAA(T18) we obtained the following new rules [LPAR04]:

U9_AGAA(z0, vl43_out_ga(.([]))) → P7_IN_AGAA(.([]))

(135) Obligation:

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

P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0))
U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([])))
U9_AGAA(z0, vl43_out_ga(.([]))) → P7_IN_AGAA(.([]))

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

(136) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule P7_IN_AGAA(.(x0)) → U6_AGAA(select20_out_aga(x0)) we obtained the following new rules [LPAR04]:

P7_IN_AGAA(.([])) → U6_AGAA(select20_out_aga([]))

(137) Obligation:

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

U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([])))
U9_AGAA(z0, vl43_out_ga(.([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.([])) → U6_AGAA(select20_out_aga([]))

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

(138) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_AGAA(y0, vl30_out_ag(0)) → U9_AGAA(y0, vl43_out_ga(.([]))) we obtained the following new rules [LPAR04]:

U7_AGAA([], vl30_out_ag(0)) → U9_AGAA([], vl43_out_ga(.([])))

(139) Obligation:

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

U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
U9_AGAA(z0, vl43_out_ga(.([]))) → P7_IN_AGAA(.([]))
P7_IN_AGAA(.([])) → U6_AGAA(select20_out_aga([]))
U7_AGAA([], vl30_out_ag(0)) → U9_AGAA([], vl43_out_ga(.([])))

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

(140) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U9_AGAA(z0, vl43_out_ga(.([]))) → P7_IN_AGAA(.([])) we obtained the following new rules [LPAR04]:

U9_AGAA([], vl43_out_ga(.([]))) → P7_IN_AGAA(.([]))

(141) Obligation:

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

U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(0))
P7_IN_AGAA(.([])) → U6_AGAA(select20_out_aga([]))
U7_AGAA([], vl30_out_ag(0)) → U9_AGAA([], vl43_out_ga(.([])))
U9_AGAA([], vl43_out_ga(.([]))) → P7_IN_AGAA(.([]))

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

(142) 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 = U7_AGAA([], vl30_out_ag(0)) evaluates to t =U7_AGAA([], vl30_out_ag(0))

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]




Rewriting sequence

U7_AGAA([], vl30_out_ag(0))U9_AGAA([], vl43_out_ga(.([])))
with rule U7_AGAA([], vl30_out_ag(0)) → U9_AGAA([], vl43_out_ga(.([]))) at position [] and matcher [ ]

U9_AGAA([], vl43_out_ga(.([])))P7_IN_AGAA(.([]))
with rule U9_AGAA([], vl43_out_ga(.([]))) → P7_IN_AGAA(.([])) at position [] and matcher [ ]

P7_IN_AGAA(.([]))U6_AGAA(select20_out_aga([]))
with rule P7_IN_AGAA(.([])) → U6_AGAA(select20_out_aga([])) at position [] and matcher [ ]

U6_AGAA(select20_out_aga([]))U7_AGAA([], vl30_out_ag(0))
with rule U6_AGAA(select20_out_aga([])) → U7_AGAA([], vl30_out_ag(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.



(143) FALSE

(144) Obligation:

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

VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)

The TRS R consists of the following rules:

vlcnd1_in_g(T2) → U15_g(T2, vl6_in_ga(T2, X6))
vl6_in_ga(0, []) → vl6_out_ga(0, [])
vl6_in_ga(s(T5), .(X23, X24)) → U1_ga(T5, X23, X24, vl6_in_ga(T5, X24))
U1_ga(T5, X23, X24, vl6_out_ga(T5, X24)) → vl6_out_ga(s(T5), .(X23, X24))
U15_g(T2, vl6_out_ga(T2, X6)) → vlcnd1_out_g(T2)
vlcnd1_in_g(T2) → U16_g(T2, vl6_in_ga(T2, T3))
U16_g(T2, vl6_out_ga(T2, T3)) → U17_g(T2, select20_in_aga(X7, T3, X8))
select20_in_aga(X39, .(T8, T10), .(T8, X40)) → U2_aga(X39, T8, T10, X40, select20_in_aga(X39, T10, X40))
select20_in_aga(X45, .(X45, T11), T11) → select20_out_aga(X45, .(X45, T11), T11)
U2_aga(X39, T8, T10, X40, select20_out_aga(X39, T10, X40)) → select20_out_aga(X39, .(T8, T10), .(T8, X40))
U17_g(T2, select20_out_aga(X7, T3, X8)) → vlcnd1_out_g(T2)
U16_g(T2, vl6_out_ga(T2, T3)) → U18_g(T2, select20_in_aga(T6, T3, T7))
U18_g(T2, select20_out_aga(T6, T3, T7)) → U19_g(T2, vl30_in_ag(X9, T7))
vl30_in_ag(0, []) → vl30_out_ag(0, [])
U19_g(T2, vl30_out_ag(X9, T7)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U20_g(T2, vl30_in_ag(T17, T7))
U20_g(T2, vl30_out_ag(T17, T7)) → U21_g(T2, vl43_in_ga(T17, X53))
vl43_in_ga(0, []) → vl43_out_ga(0, [])
vl43_in_ga(0, .(X70, [])) → vl43_out_ga(0, .(X70, []))
vl43_in_ga(s(T22), .(X70, X71)) → U13_ga(T22, X70, X71, vl43_in_ga(T22, X71))
vl43_in_ga(s(T24), .(X70, X71)) → U14_ga(T24, X70, X71, vl43_in_ga(T24, X71))
U14_ga(T24, X70, X71, vl43_out_ga(T24, X71)) → vl43_out_ga(s(T24), .(X70, X71))
U13_ga(T22, X70, X71, vl43_out_ga(T22, X71)) → vl43_out_ga(s(T22), .(X70, X71))
U21_g(T2, vl43_out_ga(T17, X53)) → vlcnd1_out_g(T2)
U20_g(T2, vl30_out_ag(T17, T7)) → U22_g(T2, vl43_in_ga(T17, T18))
U22_g(T2, vl43_out_ga(T17, T18)) → U23_g(T2, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(X7, T3, X8, X9) → U3_agaa(X7, T3, X8, X9, select20_in_aga(X7, T3, X8))
U3_agaa(X7, T3, X8, X9, select20_out_aga(X7, T3, X8)) → p7_out_agaa(X7, T3, X8, X9)
p7_in_agaa(T6, T3, T7, X9) → U4_agaa(T6, T3, T7, X9, select20_in_aga(T6, T3, T7))
U4_agaa(T6, T3, T7, X9, select20_out_aga(T6, T3, T7)) → U5_agaa(T6, T3, T7, X9, vl30_in_ag(X9, T7))
U5_agaa(T6, T3, T7, X9, vl30_out_ag(X9, T7)) → p7_out_agaa(T6, T3, T7, X9)
p7_in_agaa(T6, T3, T7, T17) → U6_agaa(T6, T3, T7, T17, select20_in_aga(T6, T3, T7))
U6_agaa(T6, T3, T7, T17, select20_out_aga(T6, T3, T7)) → U7_agaa(T6, T3, T7, T17, vl30_in_ag(T17, T7))
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U8_agaa(T6, T3, T7, T17, vl43_in_ga(T17, X53))
U8_agaa(T6, T3, T7, T17, vl43_out_ga(T17, X53)) → p7_out_agaa(T6, T3, T7, T17)
U7_agaa(T6, T3, T7, T17, vl30_out_ag(T17, T7)) → U9_agaa(T6, T3, T7, T17, vl43_in_ga(T17, T18))
U9_agaa(T6, T3, T7, T17, vl43_out_ga(T17, T18)) → U10_agaa(T6, T3, T7, T17, p7_in_agaa(X54, T18, X55, X56))
p7_in_agaa(T6, T3, T7, 0) → U11_agaa(T6, T3, T7, select20_in_aga(T6, T3, T7))
U11_agaa(T6, T3, T7, select20_out_aga(T6, T3, T7)) → U12_agaa(T6, T3, T7, vl30_in_gg(0, T7))
vl30_in_gg(0, []) → vl30_out_gg(0, [])
U12_agaa(T6, T3, T7, vl30_out_gg(0, T7)) → p7_out_agaa(T6, T3, T7, 0)
U10_agaa(T6, T3, T7, T17, p7_out_agaa(X54, T18, X55, X56)) → p7_out_agaa(T6, T3, T7, T17)
U23_g(T2, p7_out_agaa(X54, T18, X55, X56)) → vlcnd1_out_g(T2)
U18_g(T2, select20_out_aga(T6, T3, T7)) → U24_g(T2, vl30_in_gg(0, T7))
U24_g(T2, vl30_out_gg(0, T7)) → vlcnd1_out_g(T2)
vlcnd1_in_g(0) → vlcnd1_out_g(0)

The argument filtering Pi contains the following mapping:
vlcnd1_in_g(x1)  =  vlcnd1_in_g(x1)
U15_g(x1, x2)  =  U15_g(x2)
vl6_in_ga(x1, x2)  =  vl6_in_ga(x1)
0  =  0
vl6_out_ga(x1, x2)  =  vl6_out_ga(x2)
s(x1)  =  s(x1)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
.(x1, x2)  =  .(x2)
vlcnd1_out_g(x1)  =  vlcnd1_out_g
U16_g(x1, x2)  =  U16_g(x2)
U17_g(x1, x2)  =  U17_g(x2)
select20_in_aga(x1, x2, x3)  =  select20_in_aga(x2)
U2_aga(x1, x2, x3, x4, x5)  =  U2_aga(x5)
select20_out_aga(x1, x2, x3)  =  select20_out_aga(x3)
U18_g(x1, x2)  =  U18_g(x2)
U19_g(x1, x2)  =  U19_g(x2)
vl30_in_ag(x1, x2)  =  vl30_in_ag(x2)
[]  =  []
vl30_out_ag(x1, x2)  =  vl30_out_ag(x1)
U20_g(x1, x2)  =  U20_g(x2)
U21_g(x1, x2)  =  U21_g(x2)
vl43_in_ga(x1, x2)  =  vl43_in_ga(x1)
vl43_out_ga(x1, x2)  =  vl43_out_ga(x2)
U13_ga(x1, x2, x3, x4)  =  U13_ga(x4)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
U22_g(x1, x2)  =  U22_g(x2)
U23_g(x1, x2)  =  U23_g(x2)
p7_in_agaa(x1, x2, x3, x4)  =  p7_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
p7_out_agaa(x1, x2, x3, x4)  =  p7_out_agaa(x3)
U4_agaa(x1, x2, x3, x4, x5)  =  U4_agaa(x5)
U5_agaa(x1, x2, x3, x4, x5)  =  U5_agaa(x3, x5)
U6_agaa(x1, x2, x3, x4, x5)  =  U6_agaa(x5)
U7_agaa(x1, x2, x3, x4, x5)  =  U7_agaa(x3, x5)
U8_agaa(x1, x2, x3, x4, x5)  =  U8_agaa(x3, x5)
U9_agaa(x1, x2, x3, x4, x5)  =  U9_agaa(x3, x5)
U10_agaa(x1, x2, x3, x4, x5)  =  U10_agaa(x3, x5)
U11_agaa(x1, x2, x3, x4)  =  U11_agaa(x4)
U12_agaa(x1, x2, x3, x4)  =  U12_agaa(x3, x4)
vl30_in_gg(x1, x2)  =  vl30_in_gg(x1, x2)
vl30_out_gg(x1, x2)  =  vl30_out_gg
U24_g(x1, x2)  =  U24_g(x2)
VL6_IN_GA(x1, x2)  =  VL6_IN_GA(x1)

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

(145) UsableRulesProof (EQUIVALENT transformation)

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

(146) Obligation:

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

VL6_IN_GA(s(T5), .(X23, X24)) → VL6_IN_GA(T5, X24)

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

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

(147) PiDPToQDPProof (SOUND transformation)

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

(148) Obligation:

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

VL6_IN_GA(s(T5)) → VL6_IN_GA(T5)

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

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

  • VL6_IN_GA(s(T5)) → VL6_IN_GA(T5)
    The graph contains the following edges 1 > 1

(150) TRUE