(0) Obligation:
Clauses:
append([], Ys, Ys).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).
sublist(X, Y) :- ','(append(P, X1, Y), append(X2, X, P)).
Queries:
sublist(g,g).
(1) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
sublist_in: (b,b)
append_in: (f,f,b) (f,b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(2) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
SUBLIST_IN_GG(X, Y) → U2_GG(X, Y, append_in_aag(P, X1, Y))
SUBLIST_IN_GG(X, Y) → APPEND_IN_AAG(P, X1, Y)
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U1_AAG(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
U2_GG(X, Y, append_out_aag(P, X1, Y)) → U3_GG(X, Y, append_in_agg(X2, X, P))
U2_GG(X, Y, append_out_aag(P, X1, Y)) → APPEND_IN_AGG(X2, X, P)
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → U1_AGG(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg
SUBLIST_IN_GG(
x1,
x2) =
SUBLIST_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x1,
x3)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4,
x5) =
U1_AAG(
x1,
x5)
U3_GG(
x1,
x2,
x3) =
U3_GG(
x3)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
U1_AGG(
x1,
x2,
x3,
x4,
x5) =
U1_AGG(
x1,
x5)
We have to consider all (P,R,Pi)-chains
(4) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUBLIST_IN_GG(X, Y) → U2_GG(X, Y, append_in_aag(P, X1, Y))
SUBLIST_IN_GG(X, Y) → APPEND_IN_AAG(P, X1, Y)
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U1_AAG(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
U2_GG(X, Y, append_out_aag(P, X1, Y)) → U3_GG(X, Y, append_in_agg(X2, X, P))
U2_GG(X, Y, append_out_aag(P, X1, Y)) → APPEND_IN_AGG(X2, X, P)
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → U1_AGG(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg
SUBLIST_IN_GG(
x1,
x2) =
SUBLIST_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x1,
x3)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4,
x5) =
U1_AAG(
x1,
x5)
U3_GG(
x1,
x2,
x3) =
U3_GG(
x3)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
U1_AGG(
x1,
x2,
x3,
x4,
x5) =
U1_AGG(
x1,
x5)
We have to consider all (P,R,Pi)-chains
(5) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 6 less nodes.
(6) Complex Obligation (AND)
(7) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
We have to consider all (P,R,Pi)-chains
(8) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
We have to consider all (P,R,Pi)-chains
(10) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND_IN_AGG(Ys, .(X, Zs)) → APPEND_IN_AGG(Ys, Zs)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- APPEND_IN_AGG(Ys, .(X, Zs)) → APPEND_IN_AGG(Ys, Zs)
The graph contains the following edges 1 >= 1, 2 > 2
(13) TRUE
(14) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
We have to consider all (P,R,Pi)-chains
(15) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
We have to consider all (P,R,Pi)-chains
(17) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(18) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND_IN_AAG(.(X, Zs)) → APPEND_IN_AAG(Zs)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(19) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- APPEND_IN_AAG(.(X, Zs)) → APPEND_IN_AAG(Zs)
The graph contains the following edges 1 > 1
(20) TRUE
(21) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
sublist_in: (b,b)
append_in: (f,f,b) (f,b,b)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x2,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x4,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x1,
x2,
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1,
x2,
x3)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x3,
x4,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg(
x1,
x2)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(22) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x2,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x4,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x1,
x2,
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1,
x2,
x3)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x3,
x4,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg(
x1,
x2)
(23) 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:
SUBLIST_IN_GG(X, Y) → U2_GG(X, Y, append_in_aag(P, X1, Y))
SUBLIST_IN_GG(X, Y) → APPEND_IN_AAG(P, X1, Y)
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U1_AAG(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
U2_GG(X, Y, append_out_aag(P, X1, Y)) → U3_GG(X, Y, append_in_agg(X2, X, P))
U2_GG(X, Y, append_out_aag(P, X1, Y)) → APPEND_IN_AGG(X2, X, P)
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → U1_AGG(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x2,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x4,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x1,
x2,
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1,
x2,
x3)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x3,
x4,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg(
x1,
x2)
SUBLIST_IN_GG(
x1,
x2) =
SUBLIST_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x1,
x2,
x3)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4,
x5) =
U1_AAG(
x1,
x4,
x5)
U3_GG(
x1,
x2,
x3) =
U3_GG(
x1,
x2,
x3)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
U1_AGG(
x1,
x2,
x3,
x4,
x5) =
U1_AGG(
x1,
x3,
x4,
x5)
We have to consider all (P,R,Pi)-chains
(24) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
SUBLIST_IN_GG(X, Y) → U2_GG(X, Y, append_in_aag(P, X1, Y))
SUBLIST_IN_GG(X, Y) → APPEND_IN_AAG(P, X1, Y)
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → U1_AAG(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
U2_GG(X, Y, append_out_aag(P, X1, Y)) → U3_GG(X, Y, append_in_agg(X2, X, P))
U2_GG(X, Y, append_out_aag(P, X1, Y)) → APPEND_IN_AGG(X2, X, P)
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → U1_AGG(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x2,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x4,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x1,
x2,
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1,
x2,
x3)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x3,
x4,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg(
x1,
x2)
SUBLIST_IN_GG(
x1,
x2) =
SUBLIST_IN_GG(
x1,
x2)
U2_GG(
x1,
x2,
x3) =
U2_GG(
x1,
x2,
x3)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
U1_AAG(
x1,
x2,
x3,
x4,
x5) =
U1_AAG(
x1,
x4,
x5)
U3_GG(
x1,
x2,
x3) =
U3_GG(
x1,
x2,
x3)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
U1_AGG(
x1,
x2,
x3,
x4,
x5) =
U1_AGG(
x1,
x3,
x4,
x5)
We have to consider all (P,R,Pi)-chains
(25) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 6 less nodes.
(26) Complex Obligation (AND)
(27) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x2,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x4,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x1,
x2,
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1,
x2,
x3)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x3,
x4,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg(
x1,
x2)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
We have to consider all (P,R,Pi)-chains
(28) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(29) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AGG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AGG(Xs, Ys, Zs)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPEND_IN_AGG(
x1,
x2,
x3) =
APPEND_IN_AGG(
x2,
x3)
We have to consider all (P,R,Pi)-chains
(30) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND_IN_AGG(Ys, .(X, Zs)) → APPEND_IN_AGG(Ys, Zs)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(32) 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:
- APPEND_IN_AGG(Ys, .(X, Zs)) → APPEND_IN_AGG(Ys, Zs)
The graph contains the following edges 1 >= 1, 2 > 2
(33) TRUE
(34) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
The TRS R consists of the following rules:
sublist_in_gg(X, Y) → U2_gg(X, Y, append_in_aag(P, X1, Y))
append_in_aag([], Ys, Ys) → append_out_aag([], Ys, Ys)
append_in_aag(.(X, Xs), Ys, .(X, Zs)) → U1_aag(X, Xs, Ys, Zs, append_in_aag(Xs, Ys, Zs))
U1_aag(X, Xs, Ys, Zs, append_out_aag(Xs, Ys, Zs)) → append_out_aag(.(X, Xs), Ys, .(X, Zs))
U2_gg(X, Y, append_out_aag(P, X1, Y)) → U3_gg(X, Y, append_in_agg(X2, X, P))
append_in_agg([], Ys, Ys) → append_out_agg([], Ys, Ys)
append_in_agg(.(X, Xs), Ys, .(X, Zs)) → U1_agg(X, Xs, Ys, Zs, append_in_agg(Xs, Ys, Zs))
U1_agg(X, Xs, Ys, Zs, append_out_agg(Xs, Ys, Zs)) → append_out_agg(.(X, Xs), Ys, .(X, Zs))
U3_gg(X, Y, append_out_agg(X2, X, P)) → sublist_out_gg(X, Y)
The argument filtering Pi contains the following mapping:
sublist_in_gg(
x1,
x2) =
sublist_in_gg(
x1,
x2)
U2_gg(
x1,
x2,
x3) =
U2_gg(
x1,
x2,
x3)
append_in_aag(
x1,
x2,
x3) =
append_in_aag(
x3)
append_out_aag(
x1,
x2,
x3) =
append_out_aag(
x1,
x2,
x3)
.(
x1,
x2) =
.(
x1,
x2)
U1_aag(
x1,
x2,
x3,
x4,
x5) =
U1_aag(
x1,
x4,
x5)
U3_gg(
x1,
x2,
x3) =
U3_gg(
x1,
x2,
x3)
append_in_agg(
x1,
x2,
x3) =
append_in_agg(
x2,
x3)
append_out_agg(
x1,
x2,
x3) =
append_out_agg(
x1,
x2,
x3)
U1_agg(
x1,
x2,
x3,
x4,
x5) =
U1_agg(
x1,
x3,
x4,
x5)
sublist_out_gg(
x1,
x2) =
sublist_out_gg(
x1,
x2)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
We have to consider all (P,R,Pi)-chains
(35) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(36) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
APPEND_IN_AAG(.(X, Xs), Ys, .(X, Zs)) → APPEND_IN_AAG(Xs, Ys, Zs)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
APPEND_IN_AAG(
x1,
x2,
x3) =
APPEND_IN_AAG(
x3)
We have to consider all (P,R,Pi)-chains
(37) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
APPEND_IN_AAG(.(X, Zs)) → APPEND_IN_AAG(Zs)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.