(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(a,g).
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:append17([], T42, T42).
append17(.(X97, X98), X99, .(X97, T45)) :- append17(X98, X99, T45).
append32([], T84, T84).
append32(.(X158, X159), T91, .(X158, T90)) :- append32(X159, T91, T90).
sublist1([], T16).
sublist1(T7, .(X56, T27)) :- append17(X57, X58, T27).
sublist1(.(T66, T67), .(T66, T27)) :- append17(T67, T36, T27).
sublist1(T77, .(X132, T27)) :- ','(append17(T76, T36, T27), append32(X133, T77, T76)).
Queries:
sublist1(a,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: (f,b)
append17_in: (f,f,b)
append32_in: (f,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
sublist1_in_ag([], T16) → sublist1_out_ag([], T16)
sublist1_in_ag(T7, .(X56, T27)) → U3_ag(T7, X56, T27, append17_in_aag(X57, X58, T27))
append17_in_aag([], T42, T42) → append17_out_aag([], T42, T42)
append17_in_aag(.(X97, X98), X99, .(X97, T45)) → U1_aag(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
U1_aag(X97, X98, X99, T45, append17_out_aag(X98, X99, T45)) → append17_out_aag(.(X97, X98), X99, .(X97, T45))
U3_ag(T7, X56, T27, append17_out_aag(X57, X58, T27)) → sublist1_out_ag(T7, .(X56, T27))
sublist1_in_ag(.(T66, T67), .(T66, T27)) → U4_ag(T66, T67, T27, append17_in_aag(T67, T36, T27))
U4_ag(T66, T67, T27, append17_out_aag(T67, T36, T27)) → sublist1_out_ag(.(T66, T67), .(T66, T27))
sublist1_in_ag(T77, .(X132, T27)) → U5_ag(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_ag(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_ag(T77, X132, T27, append32_in_aag(X133, T77, T76))
append32_in_aag([], T84, T84) → append32_out_aag([], T84, T84)
append32_in_aag(.(X158, X159), T91, .(X158, T90)) → U2_aag(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
U2_aag(X158, X159, T91, T90, append32_out_aag(X159, T91, T90)) → append32_out_aag(.(X158, X159), T91, .(X158, T90))
U6_ag(T77, X132, T27, append32_out_aag(X133, T77, T76)) → sublist1_out_ag(T77, .(X132, T27))
The argument filtering Pi contains the following mapping:
sublist1_in_ag(x1, x2) = sublist1_in_ag(x2)
sublist1_out_ag(x1, x2) = sublist1_out_ag(x2)
.(x1, x2) = .(x1, x2)
U3_ag(x1, x2, x3, x4) = U3_ag(x2, x3, x4)
append17_in_aag(x1, x2, x3) = append17_in_aag(x3)
append17_out_aag(x1, x2, x3) = append17_out_aag(x1, x2, x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x4, x5)
U4_ag(x1, x2, x3, x4) = U4_ag(x1, x3, x4)
U5_ag(x1, x2, x3, x4) = U5_ag(x2, x3, x4)
U6_ag(x1, x2, x3, x4) = U6_ag(x2, x3, x4)
append32_in_aag(x1, x2, x3) = append32_in_aag(x3)
append32_out_aag(x1, x2, x3) = append32_out_aag(x1, x2, x3)
U2_aag(x1, x2, x3, x4, x5) = U2_aag(x1, x4, 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_ag([], T16) → sublist1_out_ag([], T16)
sublist1_in_ag(T7, .(X56, T27)) → U3_ag(T7, X56, T27, append17_in_aag(X57, X58, T27))
append17_in_aag([], T42, T42) → append17_out_aag([], T42, T42)
append17_in_aag(.(X97, X98), X99, .(X97, T45)) → U1_aag(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
U1_aag(X97, X98, X99, T45, append17_out_aag(X98, X99, T45)) → append17_out_aag(.(X97, X98), X99, .(X97, T45))
U3_ag(T7, X56, T27, append17_out_aag(X57, X58, T27)) → sublist1_out_ag(T7, .(X56, T27))
sublist1_in_ag(.(T66, T67), .(T66, T27)) → U4_ag(T66, T67, T27, append17_in_aag(T67, T36, T27))
U4_ag(T66, T67, T27, append17_out_aag(T67, T36, T27)) → sublist1_out_ag(.(T66, T67), .(T66, T27))
sublist1_in_ag(T77, .(X132, T27)) → U5_ag(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_ag(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_ag(T77, X132, T27, append32_in_aag(X133, T77, T76))
append32_in_aag([], T84, T84) → append32_out_aag([], T84, T84)
append32_in_aag(.(X158, X159), T91, .(X158, T90)) → U2_aag(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
U2_aag(X158, X159, T91, T90, append32_out_aag(X159, T91, T90)) → append32_out_aag(.(X158, X159), T91, .(X158, T90))
U6_ag(T77, X132, T27, append32_out_aag(X133, T77, T76)) → sublist1_out_ag(T77, .(X132, T27))
The argument filtering Pi contains the following mapping:
sublist1_in_ag(x1, x2) = sublist1_in_ag(x2)
sublist1_out_ag(x1, x2) = sublist1_out_ag(x2)
.(x1, x2) = .(x1, x2)
U3_ag(x1, x2, x3, x4) = U3_ag(x2, x3, x4)
append17_in_aag(x1, x2, x3) = append17_in_aag(x3)
append17_out_aag(x1, x2, x3) = append17_out_aag(x1, x2, x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x4, x5)
U4_ag(x1, x2, x3, x4) = U4_ag(x1, x3, x4)
U5_ag(x1, x2, x3, x4) = U5_ag(x2, x3, x4)
U6_ag(x1, x2, x3, x4) = U6_ag(x2, x3, x4)
append32_in_aag(x1, x2, x3) = append32_in_aag(x3)
append32_out_aag(x1, x2, x3) = append32_out_aag(x1, x2, x3)
U2_aag(x1, x2, x3, x4, x5) = U2_aag(x1, x4, 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_AG(T7, .(X56, T27)) → U3_AG(T7, X56, T27, append17_in_aag(X57, X58, T27))
SUBLIST1_IN_AG(T7, .(X56, T27)) → APPEND17_IN_AAG(X57, X58, T27)
APPEND17_IN_AAG(.(X97, X98), X99, .(X97, T45)) → U1_AAG(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
APPEND17_IN_AAG(.(X97, X98), X99, .(X97, T45)) → APPEND17_IN_AAG(X98, X99, T45)
SUBLIST1_IN_AG(.(T66, T67), .(T66, T27)) → U4_AG(T66, T67, T27, append17_in_aag(T67, T36, T27))
SUBLIST1_IN_AG(.(T66, T67), .(T66, T27)) → APPEND17_IN_AAG(T67, T36, T27)
SUBLIST1_IN_AG(T77, .(X132, T27)) → U5_AG(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_AG(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_AG(T77, X132, T27, append32_in_aag(X133, T77, T76))
U5_AG(T77, X132, T27, append17_out_aag(T76, T36, T27)) → APPEND32_IN_AAG(X133, T77, T76)
APPEND32_IN_AAG(.(X158, X159), T91, .(X158, T90)) → U2_AAG(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
APPEND32_IN_AAG(.(X158, X159), T91, .(X158, T90)) → APPEND32_IN_AAG(X159, T91, T90)
The TRS R consists of the following rules:
sublist1_in_ag([], T16) → sublist1_out_ag([], T16)
sublist1_in_ag(T7, .(X56, T27)) → U3_ag(T7, X56, T27, append17_in_aag(X57, X58, T27))
append17_in_aag([], T42, T42) → append17_out_aag([], T42, T42)
append17_in_aag(.(X97, X98), X99, .(X97, T45)) → U1_aag(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
U1_aag(X97, X98, X99, T45, append17_out_aag(X98, X99, T45)) → append17_out_aag(.(X97, X98), X99, .(X97, T45))
U3_ag(T7, X56, T27, append17_out_aag(X57, X58, T27)) → sublist1_out_ag(T7, .(X56, T27))
sublist1_in_ag(.(T66, T67), .(T66, T27)) → U4_ag(T66, T67, T27, append17_in_aag(T67, T36, T27))
U4_ag(T66, T67, T27, append17_out_aag(T67, T36, T27)) → sublist1_out_ag(.(T66, T67), .(T66, T27))
sublist1_in_ag(T77, .(X132, T27)) → U5_ag(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_ag(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_ag(T77, X132, T27, append32_in_aag(X133, T77, T76))
append32_in_aag([], T84, T84) → append32_out_aag([], T84, T84)
append32_in_aag(.(X158, X159), T91, .(X158, T90)) → U2_aag(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
U2_aag(X158, X159, T91, T90, append32_out_aag(X159, T91, T90)) → append32_out_aag(.(X158, X159), T91, .(X158, T90))
U6_ag(T77, X132, T27, append32_out_aag(X133, T77, T76)) → sublist1_out_ag(T77, .(X132, T27))
The argument filtering Pi contains the following mapping:
sublist1_in_ag(x1, x2) = sublist1_in_ag(x2)
sublist1_out_ag(x1, x2) = sublist1_out_ag(x2)
.(x1, x2) = .(x1, x2)
U3_ag(x1, x2, x3, x4) = U3_ag(x2, x3, x4)
append17_in_aag(x1, x2, x3) = append17_in_aag(x3)
append17_out_aag(x1, x2, x3) = append17_out_aag(x1, x2, x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x4, x5)
U4_ag(x1, x2, x3, x4) = U4_ag(x1, x3, x4)
U5_ag(x1, x2, x3, x4) = U5_ag(x2, x3, x4)
U6_ag(x1, x2, x3, x4) = U6_ag(x2, x3, x4)
append32_in_aag(x1, x2, x3) = append32_in_aag(x3)
append32_out_aag(x1, x2, x3) = append32_out_aag(x1, x2, x3)
U2_aag(x1, x2, x3, x4, x5) = U2_aag(x1, x4, x5)
SUBLIST1_IN_AG(x1, x2) = SUBLIST1_IN_AG(x2)
U3_AG(x1, x2, x3, x4) = U3_AG(x2, x3, x4)
APPEND17_IN_AAG(x1, x2, x3) = APPEND17_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5) = U1_AAG(x1, x4, x5)
U4_AG(x1, x2, x3, x4) = U4_AG(x1, x3, x4)
U5_AG(x1, x2, x3, x4) = U5_AG(x2, x3, x4)
U6_AG(x1, x2, x3, x4) = U6_AG(x2, x3, x4)
APPEND32_IN_AAG(x1, x2, x3) = APPEND32_IN_AAG(x3)
U2_AAG(x1, x2, x3, x4, x5) = U2_AAG(x1, x4, 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_AG(T7, .(X56, T27)) → U3_AG(T7, X56, T27, append17_in_aag(X57, X58, T27))
SUBLIST1_IN_AG(T7, .(X56, T27)) → APPEND17_IN_AAG(X57, X58, T27)
APPEND17_IN_AAG(.(X97, X98), X99, .(X97, T45)) → U1_AAG(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
APPEND17_IN_AAG(.(X97, X98), X99, .(X97, T45)) → APPEND17_IN_AAG(X98, X99, T45)
SUBLIST1_IN_AG(.(T66, T67), .(T66, T27)) → U4_AG(T66, T67, T27, append17_in_aag(T67, T36, T27))
SUBLIST1_IN_AG(.(T66, T67), .(T66, T27)) → APPEND17_IN_AAG(T67, T36, T27)
SUBLIST1_IN_AG(T77, .(X132, T27)) → U5_AG(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_AG(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_AG(T77, X132, T27, append32_in_aag(X133, T77, T76))
U5_AG(T77, X132, T27, append17_out_aag(T76, T36, T27)) → APPEND32_IN_AAG(X133, T77, T76)
APPEND32_IN_AAG(.(X158, X159), T91, .(X158, T90)) → U2_AAG(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
APPEND32_IN_AAG(.(X158, X159), T91, .(X158, T90)) → APPEND32_IN_AAG(X159, T91, T90)
The TRS R consists of the following rules:
sublist1_in_ag([], T16) → sublist1_out_ag([], T16)
sublist1_in_ag(T7, .(X56, T27)) → U3_ag(T7, X56, T27, append17_in_aag(X57, X58, T27))
append17_in_aag([], T42, T42) → append17_out_aag([], T42, T42)
append17_in_aag(.(X97, X98), X99, .(X97, T45)) → U1_aag(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
U1_aag(X97, X98, X99, T45, append17_out_aag(X98, X99, T45)) → append17_out_aag(.(X97, X98), X99, .(X97, T45))
U3_ag(T7, X56, T27, append17_out_aag(X57, X58, T27)) → sublist1_out_ag(T7, .(X56, T27))
sublist1_in_ag(.(T66, T67), .(T66, T27)) → U4_ag(T66, T67, T27, append17_in_aag(T67, T36, T27))
U4_ag(T66, T67, T27, append17_out_aag(T67, T36, T27)) → sublist1_out_ag(.(T66, T67), .(T66, T27))
sublist1_in_ag(T77, .(X132, T27)) → U5_ag(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_ag(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_ag(T77, X132, T27, append32_in_aag(X133, T77, T76))
append32_in_aag([], T84, T84) → append32_out_aag([], T84, T84)
append32_in_aag(.(X158, X159), T91, .(X158, T90)) → U2_aag(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
U2_aag(X158, X159, T91, T90, append32_out_aag(X159, T91, T90)) → append32_out_aag(.(X158, X159), T91, .(X158, T90))
U6_ag(T77, X132, T27, append32_out_aag(X133, T77, T76)) → sublist1_out_ag(T77, .(X132, T27))
The argument filtering Pi contains the following mapping:
sublist1_in_ag(x1, x2) = sublist1_in_ag(x2)
sublist1_out_ag(x1, x2) = sublist1_out_ag(x2)
.(x1, x2) = .(x1, x2)
U3_ag(x1, x2, x3, x4) = U3_ag(x2, x3, x4)
append17_in_aag(x1, x2, x3) = append17_in_aag(x3)
append17_out_aag(x1, x2, x3) = append17_out_aag(x1, x2, x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x4, x5)
U4_ag(x1, x2, x3, x4) = U4_ag(x1, x3, x4)
U5_ag(x1, x2, x3, x4) = U5_ag(x2, x3, x4)
U6_ag(x1, x2, x3, x4) = U6_ag(x2, x3, x4)
append32_in_aag(x1, x2, x3) = append32_in_aag(x3)
append32_out_aag(x1, x2, x3) = append32_out_aag(x1, x2, x3)
U2_aag(x1, x2, x3, x4, x5) = U2_aag(x1, x4, x5)
SUBLIST1_IN_AG(x1, x2) = SUBLIST1_IN_AG(x2)
U3_AG(x1, x2, x3, x4) = U3_AG(x2, x3, x4)
APPEND17_IN_AAG(x1, x2, x3) = APPEND17_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5) = U1_AAG(x1, x4, x5)
U4_AG(x1, x2, x3, x4) = U4_AG(x1, x3, x4)
U5_AG(x1, x2, x3, x4) = U5_AG(x2, x3, x4)
U6_AG(x1, x2, x3, x4) = U6_AG(x2, x3, x4)
APPEND32_IN_AAG(x1, x2, x3) = APPEND32_IN_AAG(x3)
U2_AAG(x1, x2, x3, x4, x5) = U2_AAG(x1, x4, x5)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 2 SCCs with 9 less nodes.(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND32_IN_AAG(.(X158, X159), T91, .(X158, T90)) → APPEND32_IN_AAG(X159, T91, T90)
The TRS R consists of the following rules:
sublist1_in_ag([], T16) → sublist1_out_ag([], T16)
sublist1_in_ag(T7, .(X56, T27)) → U3_ag(T7, X56, T27, append17_in_aag(X57, X58, T27))
append17_in_aag([], T42, T42) → append17_out_aag([], T42, T42)
append17_in_aag(.(X97, X98), X99, .(X97, T45)) → U1_aag(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
U1_aag(X97, X98, X99, T45, append17_out_aag(X98, X99, T45)) → append17_out_aag(.(X97, X98), X99, .(X97, T45))
U3_ag(T7, X56, T27, append17_out_aag(X57, X58, T27)) → sublist1_out_ag(T7, .(X56, T27))
sublist1_in_ag(.(T66, T67), .(T66, T27)) → U4_ag(T66, T67, T27, append17_in_aag(T67, T36, T27))
U4_ag(T66, T67, T27, append17_out_aag(T67, T36, T27)) → sublist1_out_ag(.(T66, T67), .(T66, T27))
sublist1_in_ag(T77, .(X132, T27)) → U5_ag(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_ag(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_ag(T77, X132, T27, append32_in_aag(X133, T77, T76))
append32_in_aag([], T84, T84) → append32_out_aag([], T84, T84)
append32_in_aag(.(X158, X159), T91, .(X158, T90)) → U2_aag(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
U2_aag(X158, X159, T91, T90, append32_out_aag(X159, T91, T90)) → append32_out_aag(.(X158, X159), T91, .(X158, T90))
U6_ag(T77, X132, T27, append32_out_aag(X133, T77, T76)) → sublist1_out_ag(T77, .(X132, T27))
The argument filtering Pi contains the following mapping:
sublist1_in_ag(x1, x2) = sublist1_in_ag(x2)
sublist1_out_ag(x1, x2) = sublist1_out_ag(x2)
.(x1, x2) = .(x1, x2)
U3_ag(x1, x2, x3, x4) = U3_ag(x2, x3, x4)
append17_in_aag(x1, x2, x3) = append17_in_aag(x3)
append17_out_aag(x1, x2, x3) = append17_out_aag(x1, x2, x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x4, x5)
U4_ag(x1, x2, x3, x4) = U4_ag(x1, x3, x4)
U5_ag(x1, x2, x3, x4) = U5_ag(x2, x3, x4)
U6_ag(x1, x2, x3, x4) = U6_ag(x2, x3, x4)
append32_in_aag(x1, x2, x3) = append32_in_aag(x3)
append32_out_aag(x1, x2, x3) = append32_out_aag(x1, x2, x3)
U2_aag(x1, x2, x3, x4, x5) = U2_aag(x1, x4, x5)
APPEND32_IN_AAG(x1, x2, x3) = APPEND32_IN_AAG(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:
APPEND32_IN_AAG(.(X158, X159), T91, .(X158, T90)) → APPEND32_IN_AAG(X159, T91, T90)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPEND32_IN_AAG(x1, x2, x3) = APPEND32_IN_AAG(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:
APPEND32_IN_AAG(.(X158, T90)) → APPEND32_IN_AAG(T90)
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:
- APPEND32_IN_AAG(.(X158, T90)) → APPEND32_IN_AAG(T90)
The graph contains the following edges 1 > 1
(15) YES
(16) Obligation:
Pi DP problem:The TRS P consists of the following rules:
APPEND17_IN_AAG(.(X97, X98), X99, .(X97, T45)) → APPEND17_IN_AAG(X98, X99, T45)
The TRS R consists of the following rules:
sublist1_in_ag([], T16) → sublist1_out_ag([], T16)
sublist1_in_ag(T7, .(X56, T27)) → U3_ag(T7, X56, T27, append17_in_aag(X57, X58, T27))
append17_in_aag([], T42, T42) → append17_out_aag([], T42, T42)
append17_in_aag(.(X97, X98), X99, .(X97, T45)) → U1_aag(X97, X98, X99, T45, append17_in_aag(X98, X99, T45))
U1_aag(X97, X98, X99, T45, append17_out_aag(X98, X99, T45)) → append17_out_aag(.(X97, X98), X99, .(X97, T45))
U3_ag(T7, X56, T27, append17_out_aag(X57, X58, T27)) → sublist1_out_ag(T7, .(X56, T27))
sublist1_in_ag(.(T66, T67), .(T66, T27)) → U4_ag(T66, T67, T27, append17_in_aag(T67, T36, T27))
U4_ag(T66, T67, T27, append17_out_aag(T67, T36, T27)) → sublist1_out_ag(.(T66, T67), .(T66, T27))
sublist1_in_ag(T77, .(X132, T27)) → U5_ag(T77, X132, T27, append17_in_aag(T76, T36, T27))
U5_ag(T77, X132, T27, append17_out_aag(T76, T36, T27)) → U6_ag(T77, X132, T27, append32_in_aag(X133, T77, T76))
append32_in_aag([], T84, T84) → append32_out_aag([], T84, T84)
append32_in_aag(.(X158, X159), T91, .(X158, T90)) → U2_aag(X158, X159, T91, T90, append32_in_aag(X159, T91, T90))
U2_aag(X158, X159, T91, T90, append32_out_aag(X159, T91, T90)) → append32_out_aag(.(X158, X159), T91, .(X158, T90))
U6_ag(T77, X132, T27, append32_out_aag(X133, T77, T76)) → sublist1_out_ag(T77, .(X132, T27))
The argument filtering Pi contains the following mapping:
sublist1_in_ag(x1, x2) = sublist1_in_ag(x2)
sublist1_out_ag(x1, x2) = sublist1_out_ag(x2)
.(x1, x2) = .(x1, x2)
U3_ag(x1, x2, x3, x4) = U3_ag(x2, x3, x4)
append17_in_aag(x1, x2, x3) = append17_in_aag(x3)
append17_out_aag(x1, x2, x3) = append17_out_aag(x1, x2, x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x4, x5)
U4_ag(x1, x2, x3, x4) = U4_ag(x1, x3, x4)
U5_ag(x1, x2, x3, x4) = U5_ag(x2, x3, x4)
U6_ag(x1, x2, x3, x4) = U6_ag(x2, x3, x4)
append32_in_aag(x1, x2, x3) = append32_in_aag(x3)
append32_out_aag(x1, x2, x3) = append32_out_aag(x1, x2, x3)
U2_aag(x1, x2, x3, x4, x5) = U2_aag(x1, x4, x5)
APPEND17_IN_AAG(x1, x2, x3) = APPEND17_IN_AAG(x3)
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:
APPEND17_IN_AAG(.(X97, X98), X99, .(X97, T45)) → APPEND17_IN_AAG(X98, X99, T45)
R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2) = .(x1, x2)
APPEND17_IN_AAG(x1, x2, x3) = APPEND17_IN_AAG(x3)
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:
APPEND17_IN_AAG(.(X97, T45)) → APPEND17_IN_AAG(T45)
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:
- APPEND17_IN_AAG(.(X97, T45)) → APPEND17_IN_AAG(T45)
The graph contains the following edges 1 > 1