(0) Obligation:
Clauses:append1([], Ys, Ys).
append1(.(X, Xs), Ys, .(X, Zs)) :- append1(Xs, Ys, Zs).
append2([], Ys, Ys).
append2(.(X, Xs), Ys, .(X, Zs)) :- append2(Xs, Ys, Zs).
sublist(X, Y) :- ','(append1(U, X, V), append2(V, W, Y)).
Queries:
sublist(g,g).
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:append27([], T22, T22).
append27(.(T29, T30), X50, .(T29, T31)) :- append27(T30, X50, T31).
append117([], T48, T48).
append117(.(X125, X126), T52, .(X125, X127)) :- append117(X126, T52, X127).
append227([], T69, T69).
append227(.(T76, T79), X189, .(T76, T78)) :- append227(T79, X189, T78).
sublist1(T15, T6) :- append27(T15, X7, T6).
sublist1(T38, T6) :- append117(X88, T38, X89).
sublist1(T38, .(X154, T61)) :- ','(append117(T41, T38, T62), append227(T62, X155, T61)).
Queries:
sublist1(g,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:sublist1_in: (b,b)
append27_in: (b,f,b)
append117_in: (f,b,f)
append227_in: (b,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
(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:
SUBLIST1_IN_GG(T15, T6) → U4_GG(T15, T6, append27_in_gag(T15, X7, T6))
SUBLIST1_IN_GG(T15, T6) → APPEND27_IN_GAG(T15, X7, T6)
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → U1_GAG(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
SUBLIST1_IN_GG(T38, T6) → U5_GG(T38, T6, append117_in_aga(X88, T38, X89))
SUBLIST1_IN_GG(T38, T6) → APPEND117_IN_AGA(X88, T38, X89)
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → U2_AGA(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
SUBLIST1_IN_GG(T38, .(X154, T61)) → U6_GG(T38, X154, T61, append117_in_aga(T41, T38, T62))
SUBLIST1_IN_GG(T38, .(X154, T61)) → APPEND117_IN_AGA(T41, T38, T62)
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_GG(T38, X154, T61, append227_in_gag(T62, X155, T61))
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → APPEND227_IN_GAG(T62, X155, T61)
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → U3_GAG(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
SUBLIST1_IN_GG(x1, x2) = SUBLIST1_IN_GG(x1, x2)
U4_GG(x1, x2, x3) = U4_GG(x3)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5) = U1_GAG(x5)
U5_GG(x1, x2, x3) = U5_GG(x3)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5) = U2_AGA(x5)
U6_GG(x1, x2, x3, x4) = U6_GG(x3, x4)
U7_GG(x1, x2, x3, x4) = U7_GG(x4)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5) = U3_GAG(x5)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:The TRS P consists of the following rules:
SUBLIST1_IN_GG(T15, T6) → U4_GG(T15, T6, append27_in_gag(T15, X7, T6))
SUBLIST1_IN_GG(T15, T6) → APPEND27_IN_GAG(T15, X7, T6)
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → U1_GAG(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
SUBLIST1_IN_GG(T38, T6) → U5_GG(T38, T6, append117_in_aga(X88, T38, X89))
SUBLIST1_IN_GG(T38, T6) → APPEND117_IN_AGA(X88, T38, X89)
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → U2_AGA(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
SUBLIST1_IN_GG(T38, .(X154, T61)) → U6_GG(T38, X154, T61, append117_in_aga(T41, T38, T62))
SUBLIST1_IN_GG(T38, .(X154, T61)) → APPEND117_IN_AGA(T41, T38, T62)
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_GG(T38, X154, T61, append227_in_gag(T62, X155, T61))
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → APPEND227_IN_GAG(T62, X155, T61)
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → U3_GAG(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
SUBLIST1_IN_GG(x1, x2) = SUBLIST1_IN_GG(x1, x2)
U4_GG(x1, x2, x3) = U4_GG(x3)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5) = U1_GAG(x5)
U5_GG(x1, x2, x3) = U5_GG(x3)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5) = U2_AGA(x5)
U6_GG(x1, x2, x3, x4) = U6_GG(x3, x4)
U7_GG(x1, x2, x3, x4) = U7_GG(x4)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5) = U3_GAG(x5)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 11 less nodes.(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
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:
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
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:
APPEND227_IN_GAG(.(T79), .(T78)) → APPEND227_IN_GAG(T79, T78)
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:
- APPEND227_IN_GAG(.(T79), .(T78)) → APPEND227_IN_GAG(T79, T78)
The graph contains the following edges 1 > 1, 2 > 2
(15) YES
(16) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_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:
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_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:
APPEND117_IN_AGA(T52) → APPEND117_IN_AGA(T52)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.Found a loop by semiunifying a rule from P directly.
s = APPEND117_IN_AGA(T52) evaluates to t =APPEND117_IN_AGA(T52)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from APPEND117_IN_AGA(T52) to APPEND117_IN_AGA(T52).
(22) NO
(23) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x2)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg
U5_gg(x1, x2, x3) = U5_gg(x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x2)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x5)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
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:
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
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:
APPEND27_IN_GAG(.(T30), .(T31)) → APPEND27_IN_GAG(T30, T31)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(28) 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:
- APPEND27_IN_GAG(.(T30), .(T31)) → APPEND27_IN_GAG(T30, T31)
The graph contains the following edges 1 > 1, 2 > 2
(29) YES
(30) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:sublist1_in: (b,b)
append27_in: (b,f,b)
append117_in: (f,b,f)
append227_in: (b,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(31) Obligation:
Pi-finite rewrite system:The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
(32) 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:
SUBLIST1_IN_GG(T15, T6) → U4_GG(T15, T6, append27_in_gag(T15, X7, T6))
SUBLIST1_IN_GG(T15, T6) → APPEND27_IN_GAG(T15, X7, T6)
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → U1_GAG(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
SUBLIST1_IN_GG(T38, T6) → U5_GG(T38, T6, append117_in_aga(X88, T38, X89))
SUBLIST1_IN_GG(T38, T6) → APPEND117_IN_AGA(X88, T38, X89)
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → U2_AGA(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
SUBLIST1_IN_GG(T38, .(X154, T61)) → U6_GG(T38, X154, T61, append117_in_aga(T41, T38, T62))
SUBLIST1_IN_GG(T38, .(X154, T61)) → APPEND117_IN_AGA(T41, T38, T62)
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_GG(T38, X154, T61, append227_in_gag(T62, X155, T61))
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → APPEND227_IN_GAG(T62, X155, T61)
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → U3_GAG(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
SUBLIST1_IN_GG(x1, x2) = SUBLIST1_IN_GG(x1, x2)
U4_GG(x1, x2, x3) = U4_GG(x1, x2, x3)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5) = U1_GAG(x2, x4, x5)
U5_GG(x1, x2, x3) = U5_GG(x1, x2, x3)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5) = U2_AGA(x3, x5)
U6_GG(x1, x2, x3, x4) = U6_GG(x1, x3, x4)
U7_GG(x1, x2, x3, x4) = U7_GG(x1, x3, x4)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5) = U3_GAG(x2, x4, x5)
We have to consider all (P,R,Pi)-chains
(33) Obligation:
Pi DP problem:The TRS P consists of the following rules:
SUBLIST1_IN_GG(T15, T6) → U4_GG(T15, T6, append27_in_gag(T15, X7, T6))
SUBLIST1_IN_GG(T15, T6) → APPEND27_IN_GAG(T15, X7, T6)
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → U1_GAG(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
SUBLIST1_IN_GG(T38, T6) → U5_GG(T38, T6, append117_in_aga(X88, T38, X89))
SUBLIST1_IN_GG(T38, T6) → APPEND117_IN_AGA(X88, T38, X89)
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → U2_AGA(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
SUBLIST1_IN_GG(T38, .(X154, T61)) → U6_GG(T38, X154, T61, append117_in_aga(T41, T38, T62))
SUBLIST1_IN_GG(T38, .(X154, T61)) → APPEND117_IN_AGA(T41, T38, T62)
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_GG(T38, X154, T61, append227_in_gag(T62, X155, T61))
U6_GG(T38, X154, T61, append117_out_aga(T41, T38, T62)) → APPEND227_IN_GAG(T62, X155, T61)
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → U3_GAG(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
SUBLIST1_IN_GG(x1, x2) = SUBLIST1_IN_GG(x1, x2)
U4_GG(x1, x2, x3) = U4_GG(x1, x2, x3)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
U1_GAG(x1, x2, x3, x4, x5) = U1_GAG(x2, x4, x5)
U5_GG(x1, x2, x3) = U5_GG(x1, x2, x3)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_IN_AGA(x2)
U2_AGA(x1, x2, x3, x4, x5) = U2_AGA(x3, x5)
U6_GG(x1, x2, x3, x4) = U6_GG(x1, x3, x4)
U7_GG(x1, x2, x3, x4) = U7_GG(x1, x3, x4)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
U3_GAG(x1, x2, x3, x4, x5) = U3_GAG(x2, x4, x5)
We have to consider all (P,R,Pi)-chains
(34) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 11 less nodes.(35) Complex Obligation (AND)
(36) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
We have to consider all (P,R,Pi)-chains
(37) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(38) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND227_IN_GAG(.(T76, T79), X189, .(T76, T78)) → APPEND227_IN_GAG(T79, X189, T78)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
APPEND227_IN_GAG(x1, x2, x3) = APPEND227_IN_GAG(x1, x3)
We have to consider all (P,R,Pi)-chains
(39) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(40) Obligation:
Q DP problem:The TRS P consists of the following rules:
APPEND227_IN_GAG(.(T79), .(T78)) → APPEND227_IN_GAG(T79, T78)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(41) 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:
- APPEND227_IN_GAG(.(T79), .(T78)) → APPEND227_IN_GAG(T79, T78)
The graph contains the following edges 1 > 1, 2 > 2
(42) YES
(43) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_IN_AGA(x2)
We have to consider all (P,R,Pi)-chains
(44) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(45) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND117_IN_AGA(.(X125, X126), T52, .(X125, X127)) → APPEND117_IN_AGA(X126, T52, X127)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
APPEND117_IN_AGA(x1, x2, x3) = APPEND117_IN_AGA(x2)
We have to consider all (P,R,Pi)-chains
(46) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(47) Obligation:
Q DP problem:The TRS P consists of the following rules:
APPEND117_IN_AGA(T52) → APPEND117_IN_AGA(T52)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(48) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.Found a loop by semiunifying a rule from P directly.
s = APPEND117_IN_AGA(T52) evaluates to t =APPEND117_IN_AGA(T52)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [ ]
Rewriting sequence
The DP semiunifies directly so there is only one rewrite step from APPEND117_IN_AGA(T52) to APPEND117_IN_AGA(T52).
(49) NO
(50) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
The TRS R consists of the following rules:
sublist1_in_gg(T15, T6) → U4_gg(T15, T6, append27_in_gag(T15, X7, T6))
append27_in_gag([], T22, T22) → append27_out_gag([], T22, T22)
append27_in_gag(.(T29, T30), X50, .(T29, T31)) → U1_gag(T29, T30, X50, T31, append27_in_gag(T30, X50, T31))
U1_gag(T29, T30, X50, T31, append27_out_gag(T30, X50, T31)) → append27_out_gag(.(T29, T30), X50, .(T29, T31))
U4_gg(T15, T6, append27_out_gag(T15, X7, T6)) → sublist1_out_gg(T15, T6)
sublist1_in_gg(T38, T6) → U5_gg(T38, T6, append117_in_aga(X88, T38, X89))
append117_in_aga([], T48, T48) → append117_out_aga([], T48, T48)
append117_in_aga(.(X125, X126), T52, .(X125, X127)) → U2_aga(X125, X126, T52, X127, append117_in_aga(X126, T52, X127))
U2_aga(X125, X126, T52, X127, append117_out_aga(X126, T52, X127)) → append117_out_aga(.(X125, X126), T52, .(X125, X127))
U5_gg(T38, T6, append117_out_aga(X88, T38, X89)) → sublist1_out_gg(T38, T6)
sublist1_in_gg(T38, .(X154, T61)) → U6_gg(T38, X154, T61, append117_in_aga(T41, T38, T62))
U6_gg(T38, X154, T61, append117_out_aga(T41, T38, T62)) → U7_gg(T38, X154, T61, append227_in_gag(T62, X155, T61))
append227_in_gag([], T69, T69) → append227_out_gag([], T69, T69)
append227_in_gag(.(T76, T79), X189, .(T76, T78)) → U3_gag(T76, T79, X189, T78, append227_in_gag(T79, X189, T78))
U3_gag(T76, T79, X189, T78, append227_out_gag(T79, X189, T78)) → append227_out_gag(.(T76, T79), X189, .(T76, T78))
U7_gg(T38, X154, T61, append227_out_gag(T62, X155, T61)) → sublist1_out_gg(T38, .(X154, T61))
The argument filtering Pi contains the following mapping:
sublist1_in_gg(x1, x2) = sublist1_in_gg(x1, x2)
U4_gg(x1, x2, x3) = U4_gg(x1, x2, x3)
append27_in_gag(x1, x2, x3) = append27_in_gag(x1, x3)
[] = []
append27_out_gag(x1, x2, x3) = append27_out_gag(x1, x2, x3)
.(x1, x2) = .(x2)
U1_gag(x1, x2, x3, x4, x5) = U1_gag(x2, x4, x5)
sublist1_out_gg(x1, x2) = sublist1_out_gg(x1, x2)
U5_gg(x1, x2, x3) = U5_gg(x1, x2, x3)
append117_in_aga(x1, x2, x3) = append117_in_aga(x2)
append117_out_aga(x1, x2, x3) = append117_out_aga(x1, x2, x3)
U2_aga(x1, x2, x3, x4, x5) = U2_aga(x3, x5)
U6_gg(x1, x2, x3, x4) = U6_gg(x1, x3, x4)
U7_gg(x1, x2, x3, x4) = U7_gg(x1, x3, x4)
append227_in_gag(x1, x2, x3) = append227_in_gag(x1, x3)
append227_out_gag(x1, x2, x3) = append227_out_gag(x1, x2, x3)
U3_gag(x1, x2, x3, x4, x5) = U3_gag(x2, x4, x5)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
We have to consider all (P,R,Pi)-chains
(51) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.(52) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND27_IN_GAG(.(T29, T30), X50, .(T29, T31)) → APPEND27_IN_GAG(T30, X50, T31)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x2)
APPEND27_IN_GAG(x1, x2, x3) = APPEND27_IN_GAG(x1, x3)
We have to consider all (P,R,Pi)-chains
(53) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.(54) Obligation:
Q DP problem:The TRS P consists of the following rules:
APPEND27_IN_GAG(.(T30), .(T31)) → APPEND27_IN_GAG(T30, T31)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(55) 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:
- APPEND27_IN_GAG(.(T30), .(T31)) → APPEND27_IN_GAG(T30, T31)
The graph contains the following edges 1 > 1, 2 > 2