(0) Obligation:

Clauses:

append2(parts([], Y), is(sum(Y))).
append2(parts(.(H, X), Y), is(sum(.(H, Z)))) :- append2(parts(X, Y), is(sum(Z))).
append1(parts([], Y), is(sum(Y))).
append1(parts(.(H, X), Y), is(sum(.(H, Z)))) :- append1(parts(X, Y), is(sum(Z))).
perm([], []).
perm(L, .(H, T)) :- ','(append2(parts(V, .(H, U)), is(sum(L))), ','(append1(parts(V, U), is(sum(W))), perm(W, T))).

Queries:

perm(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

append234(.(X118, X119), T57, X120, .(X118, T58)) :- append234(X119, T57, X120, T58).
perm19(T37, .(T36, T38)) :- append234(X75, T36, X76, T37).
perm19(T37, .(T36, T43)) :- ','(append2c34(T41, T36, T42, T37), p35(T41, T42, X77, T43)).
append144(.(T78, T81), T82, .(T78, X153)) :- append144(T81, T82, X153).
p35(T41, T42, X77, T43) :- append144(T41, T42, X77).
p35(T41, T42, T63, T64) :- ','(append1c44(T41, T42, T63), perm19(T63, T64)).
perm1(.(T23, T25), .(T23, T24)) :- ','(append1c18(T25, T26), perm19(T26, T24)).
perm1(.(X178, T90), .(T91, T92)) :- append234(X179, T91, X180, T90).
perm1(.(X178, T90), .(T91, T97)) :- ','(append2c34(T95, T91, T96, T90), p35(.(X178, T95), T96, X30, T97)).

Clauses:

append2c34([], T50, X98, .(T50, X98)).
append2c34(.(X118, X119), T57, X120, .(X118, T58)) :- append2c34(X119, T57, X120, T58).
permc19([], []).
permc19(T37, .(T36, T43)) :- ','(append2c34(T41, T36, T42, T37), qc35(T41, T42, X77, T43)).
append1c44([], T71, T71).
append1c44(.(T78, T81), T82, .(T78, X153)) :- append1c44(T81, T82, X153).
qc35(T41, T42, T63, T64) :- ','(append1c44(T41, T42, T63), permc19(T63, T64)).
append1c18(X58, X58).

Afs:

perm1(x1, x2)  =  perm1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1_in: (b,f)
perm19_in: (b,f)
append234_in: (f,f,f,b)
append2c34_in: (f,f,f,b)
p35_in: (b,b,f,f)
append144_in: (b,b,f)
append1c44_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN_GA(.(T23, T25), .(T23, T24)) → U9_GA(T23, T25, T24, append1c18_in_ga(T25, T26))
U9_GA(T23, T25, T24, append1c18_out_ga(T25, T26)) → U10_GA(T23, T25, T24, perm19_in_ga(T26, T24))
U9_GA(T23, T25, T24, append1c18_out_ga(T25, T26)) → PERM19_IN_GA(T26, T24)
PERM19_IN_GA(T37, .(T36, T38)) → U2_GA(T37, T36, T38, append234_in_aaag(X75, T36, X76, T37))
PERM19_IN_GA(T37, .(T36, T38)) → APPEND234_IN_AAAG(X75, T36, X76, T37)
APPEND234_IN_AAAG(.(X118, X119), T57, X120, .(X118, T58)) → U1_AAAG(X118, X119, T57, X120, T58, append234_in_aaag(X119, T57, X120, T58))
APPEND234_IN_AAAG(.(X118, X119), T57, X120, .(X118, T58)) → APPEND234_IN_AAAG(X119, T57, X120, T58)
PERM19_IN_GA(T37, .(T36, T43)) → U3_GA(T37, T36, T43, append2c34_in_aaag(T41, T36, T42, T37))
U3_GA(T37, T36, T43, append2c34_out_aaag(T41, T36, T42, T37)) → U4_GA(T37, T36, T43, p35_in_ggaa(T41, T42, X77, T43))
U3_GA(T37, T36, T43, append2c34_out_aaag(T41, T36, T42, T37)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, X77, T43) → U6_GGAA(T41, T42, X77, T43, append144_in_gga(T41, T42, X77))
P35_IN_GGAA(T41, T42, X77, T43) → APPEND144_IN_GGA(T41, T42, X77)
APPEND144_IN_GGA(.(T78, T81), T82, .(T78, X153)) → U5_GGA(T78, T81, T82, X153, append144_in_gga(T81, T82, X153))
APPEND144_IN_GGA(.(T78, T81), T82, .(T78, X153)) → APPEND144_IN_GGA(T81, T82, X153)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, append1c44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, append1c44_out_gga(T41, T42, T63)) → U8_GGAA(T41, T42, T63, T64, perm19_in_ga(T63, T64))
U7_GGAA(T41, T42, T63, T64, append1c44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → U11_GA(X178, T90, T91, T92, append234_in_aaag(X179, T91, X180, T90))
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → APPEND234_IN_AAAG(X179, T91, X180, T90)
PERM1_IN_GA(.(X178, T90), .(T91, T97)) → U12_GA(X178, T90, T91, T97, append2c34_in_aaag(T95, T91, T96, T90))
U12_GA(X178, T90, T91, T97, append2c34_out_aaag(T95, T91, T96, T90)) → U13_GA(X178, T90, T91, T97, p35_in_ggaa(.(X178, T95), T96, X30, T97))
U12_GA(X178, T90, T91, T97, append2c34_out_aaag(T95, T91, T96, T90)) → P35_IN_GGAA(.(X178, T95), T96, X30, T97)

The TRS R consists of the following rules:

append1c18_in_ga(X58, X58) → append1c18_out_ga(X58, X58)
append2c34_in_aaag([], T50, X98, .(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, X119), T57, X120, .(X118, T58)) → U15_aaag(X118, X119, T57, X120, T58, append2c34_in_aaag(X119, T57, X120, T58))
U15_aaag(X118, X119, T57, X120, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
append1c44_in_gga([], T71, T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, append1c44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1c18_in_ga(x1, x2)  =  append1c18_in_ga(x1)
append1c18_out_ga(x1, x2)  =  append1c18_out_ga(x1, x2)
perm19_in_ga(x1, x2)  =  perm19_in_ga(x1)
append234_in_aaag(x1, x2, x3, x4)  =  append234_in_aaag(x4)
append2c34_in_aaag(x1, x2, x3, x4)  =  append2c34_in_aaag(x4)
append2c34_out_aaag(x1, x2, x3, x4)  =  append2c34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
p35_in_ggaa(x1, x2, x3, x4)  =  p35_in_ggaa(x1, x2)
append144_in_gga(x1, x2, x3)  =  append144_in_gga(x1, x2)
append1c44_in_gga(x1, x2, x3)  =  append1c44_in_gga(x1, x2)
[]  =  []
append1c44_out_gga(x1, x2, x3)  =  append1c44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x2, x4)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
PERM19_IN_GA(x1, x2)  =  PERM19_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
APPEND234_IN_AAAG(x1, x2, x3, x4)  =  APPEND234_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6)  =  U1_AAAG(x1, x5, x6)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
P35_IN_GGAA(x1, x2, x3, x4)  =  P35_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x1, x2, x5)
APPEND144_IN_GGA(x1, x2, x3)  =  APPEND144_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5)  =  U5_GGA(x1, x2, x3, x5)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x5)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

PERM1_IN_GA(.(T23, T25), .(T23, T24)) → U9_GA(T23, T25, T24, append1c18_in_ga(T25, T26))
U9_GA(T23, T25, T24, append1c18_out_ga(T25, T26)) → U10_GA(T23, T25, T24, perm19_in_ga(T26, T24))
U9_GA(T23, T25, T24, append1c18_out_ga(T25, T26)) → PERM19_IN_GA(T26, T24)
PERM19_IN_GA(T37, .(T36, T38)) → U2_GA(T37, T36, T38, append234_in_aaag(X75, T36, X76, T37))
PERM19_IN_GA(T37, .(T36, T38)) → APPEND234_IN_AAAG(X75, T36, X76, T37)
APPEND234_IN_AAAG(.(X118, X119), T57, X120, .(X118, T58)) → U1_AAAG(X118, X119, T57, X120, T58, append234_in_aaag(X119, T57, X120, T58))
APPEND234_IN_AAAG(.(X118, X119), T57, X120, .(X118, T58)) → APPEND234_IN_AAAG(X119, T57, X120, T58)
PERM19_IN_GA(T37, .(T36, T43)) → U3_GA(T37, T36, T43, append2c34_in_aaag(T41, T36, T42, T37))
U3_GA(T37, T36, T43, append2c34_out_aaag(T41, T36, T42, T37)) → U4_GA(T37, T36, T43, p35_in_ggaa(T41, T42, X77, T43))
U3_GA(T37, T36, T43, append2c34_out_aaag(T41, T36, T42, T37)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, X77, T43) → U6_GGAA(T41, T42, X77, T43, append144_in_gga(T41, T42, X77))
P35_IN_GGAA(T41, T42, X77, T43) → APPEND144_IN_GGA(T41, T42, X77)
APPEND144_IN_GGA(.(T78, T81), T82, .(T78, X153)) → U5_GGA(T78, T81, T82, X153, append144_in_gga(T81, T82, X153))
APPEND144_IN_GGA(.(T78, T81), T82, .(T78, X153)) → APPEND144_IN_GGA(T81, T82, X153)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, append1c44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, append1c44_out_gga(T41, T42, T63)) → U8_GGAA(T41, T42, T63, T64, perm19_in_ga(T63, T64))
U7_GGAA(T41, T42, T63, T64, append1c44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → U11_GA(X178, T90, T91, T92, append234_in_aaag(X179, T91, X180, T90))
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → APPEND234_IN_AAAG(X179, T91, X180, T90)
PERM1_IN_GA(.(X178, T90), .(T91, T97)) → U12_GA(X178, T90, T91, T97, append2c34_in_aaag(T95, T91, T96, T90))
U12_GA(X178, T90, T91, T97, append2c34_out_aaag(T95, T91, T96, T90)) → U13_GA(X178, T90, T91, T97, p35_in_ggaa(.(X178, T95), T96, X30, T97))
U12_GA(X178, T90, T91, T97, append2c34_out_aaag(T95, T91, T96, T90)) → P35_IN_GGAA(.(X178, T95), T96, X30, T97)

The TRS R consists of the following rules:

append1c18_in_ga(X58, X58) → append1c18_out_ga(X58, X58)
append2c34_in_aaag([], T50, X98, .(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, X119), T57, X120, .(X118, T58)) → U15_aaag(X118, X119, T57, X120, T58, append2c34_in_aaag(X119, T57, X120, T58))
U15_aaag(X118, X119, T57, X120, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
append1c44_in_gga([], T71, T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, append1c44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1c18_in_ga(x1, x2)  =  append1c18_in_ga(x1)
append1c18_out_ga(x1, x2)  =  append1c18_out_ga(x1, x2)
perm19_in_ga(x1, x2)  =  perm19_in_ga(x1)
append234_in_aaag(x1, x2, x3, x4)  =  append234_in_aaag(x4)
append2c34_in_aaag(x1, x2, x3, x4)  =  append2c34_in_aaag(x4)
append2c34_out_aaag(x1, x2, x3, x4)  =  append2c34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
p35_in_ggaa(x1, x2, x3, x4)  =  p35_in_ggaa(x1, x2)
append144_in_gga(x1, x2, x3)  =  append144_in_gga(x1, x2)
append1c44_in_gga(x1, x2, x3)  =  append1c44_in_gga(x1, x2)
[]  =  []
append1c44_out_gga(x1, x2, x3)  =  append1c44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x2, x4)
U10_GA(x1, x2, x3, x4)  =  U10_GA(x1, x2, x4)
PERM19_IN_GA(x1, x2)  =  PERM19_IN_GA(x1)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x1, x4)
APPEND234_IN_AAAG(x1, x2, x3, x4)  =  APPEND234_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6)  =  U1_AAAG(x1, x5, x6)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
P35_IN_GGAA(x1, x2, x3, x4)  =  P35_IN_GGAA(x1, x2)
U6_GGAA(x1, x2, x3, x4, x5)  =  U6_GGAA(x1, x2, x5)
APPEND144_IN_GGA(x1, x2, x3)  =  APPEND144_IN_GGA(x1, x2)
U5_GGA(x1, x2, x3, x4, x5)  =  U5_GGA(x1, x2, x3, x5)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)
U8_GGAA(x1, x2, x3, x4, x5)  =  U8_GGAA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x5)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 3 SCCs with 16 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APPEND144_IN_GGA(.(T78, T81), T82, .(T78, X153)) → APPEND144_IN_GGA(T81, T82, X153)

The TRS R consists of the following rules:

append1c18_in_ga(X58, X58) → append1c18_out_ga(X58, X58)
append2c34_in_aaag([], T50, X98, .(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, X119), T57, X120, .(X118, T58)) → U15_aaag(X118, X119, T57, X120, T58, append2c34_in_aaag(X119, T57, X120, T58))
U15_aaag(X118, X119, T57, X120, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
append1c44_in_gga([], T71, T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, append1c44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1c18_in_ga(x1, x2)  =  append1c18_in_ga(x1)
append1c18_out_ga(x1, x2)  =  append1c18_out_ga(x1, x2)
append2c34_in_aaag(x1, x2, x3, x4)  =  append2c34_in_aaag(x4)
append2c34_out_aaag(x1, x2, x3, x4)  =  append2c34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
append1c44_in_gga(x1, x2, x3)  =  append1c44_in_gga(x1, x2)
[]  =  []
append1c44_out_gga(x1, x2, x3)  =  append1c44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
APPEND144_IN_GGA(x1, x2, x3)  =  APPEND144_IN_GGA(x1, x2)

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:

APPEND144_IN_GGA(.(T78, T81), T82, .(T78, X153)) → APPEND144_IN_GGA(T81, T82, X153)

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

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:

APPEND144_IN_GGA(.(T78, T81), T82) → APPEND144_IN_GGA(T81, T82)

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:

  • APPEND144_IN_GGA(.(T78, T81), T82) → APPEND144_IN_GGA(T81, T82)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

APPEND234_IN_AAAG(.(X118, X119), T57, X120, .(X118, T58)) → APPEND234_IN_AAAG(X119, T57, X120, T58)

The TRS R consists of the following rules:

append1c18_in_ga(X58, X58) → append1c18_out_ga(X58, X58)
append2c34_in_aaag([], T50, X98, .(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, X119), T57, X120, .(X118, T58)) → U15_aaag(X118, X119, T57, X120, T58, append2c34_in_aaag(X119, T57, X120, T58))
U15_aaag(X118, X119, T57, X120, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
append1c44_in_gga([], T71, T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, append1c44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1c18_in_ga(x1, x2)  =  append1c18_in_ga(x1)
append1c18_out_ga(x1, x2)  =  append1c18_out_ga(x1, x2)
append2c34_in_aaag(x1, x2, x3, x4)  =  append2c34_in_aaag(x4)
append2c34_out_aaag(x1, x2, x3, x4)  =  append2c34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
append1c44_in_gga(x1, x2, x3)  =  append1c44_in_gga(x1, x2)
[]  =  []
append1c44_out_gga(x1, x2, x3)  =  append1c44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
APPEND234_IN_AAAG(x1, x2, x3, x4)  =  APPEND234_IN_AAAG(x4)

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:

APPEND234_IN_AAAG(.(X118, X119), T57, X120, .(X118, T58)) → APPEND234_IN_AAAG(X119, T57, X120, T58)

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

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:

APPEND234_IN_AAAG(.(X118, T58)) → APPEND234_IN_AAAG(T58)

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:

  • APPEND234_IN_AAAG(.(X118, T58)) → APPEND234_IN_AAAG(T58)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PERM19_IN_GA(T37, .(T36, T43)) → U3_GA(T37, T36, T43, append2c34_in_aaag(T41, T36, T42, T37))
U3_GA(T37, T36, T43, append2c34_out_aaag(T41, T36, T42, T37)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, append1c44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, append1c44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)

The TRS R consists of the following rules:

append1c18_in_ga(X58, X58) → append1c18_out_ga(X58, X58)
append2c34_in_aaag([], T50, X98, .(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, X119), T57, X120, .(X118, T58)) → U15_aaag(X118, X119, T57, X120, T58, append2c34_in_aaag(X119, T57, X120, T58))
U15_aaag(X118, X119, T57, X120, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
append1c44_in_gga([], T71, T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, append1c44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append1c18_in_ga(x1, x2)  =  append1c18_in_ga(x1)
append1c18_out_ga(x1, x2)  =  append1c18_out_ga(x1, x2)
append2c34_in_aaag(x1, x2, x3, x4)  =  append2c34_in_aaag(x4)
append2c34_out_aaag(x1, x2, x3, x4)  =  append2c34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
append1c44_in_gga(x1, x2, x3)  =  append1c44_in_gga(x1, x2)
[]  =  []
append1c44_out_gga(x1, x2, x3)  =  append1c44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
PERM19_IN_GA(x1, x2)  =  PERM19_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
P35_IN_GGAA(x1, x2, x3, x4)  =  P35_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

PERM19_IN_GA(T37, .(T36, T43)) → U3_GA(T37, T36, T43, append2c34_in_aaag(T41, T36, T42, T37))
U3_GA(T37, T36, T43, append2c34_out_aaag(T41, T36, T42, T37)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, append1c44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, append1c44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)

The TRS R consists of the following rules:

append2c34_in_aaag([], T50, X98, .(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, X119), T57, X120, .(X118, T58)) → U15_aaag(X118, X119, T57, X120, T58, append2c34_in_aaag(X119, T57, X120, T58))
append1c44_in_gga([], T71, T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, append1c44_in_gga(T81, T82, X153))
U15_aaag(X118, X119, T57, X120, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
U18_gga(T78, T81, T82, X153, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append2c34_in_aaag(x1, x2, x3, x4)  =  append2c34_in_aaag(x4)
append2c34_out_aaag(x1, x2, x3, x4)  =  append2c34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
append1c44_in_gga(x1, x2, x3)  =  append1c44_in_gga(x1, x2)
[]  =  []
append1c44_out_gga(x1, x2, x3)  =  append1c44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
PERM19_IN_GA(x1, x2)  =  PERM19_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
P35_IN_GGAA(x1, x2, x3, x4)  =  P35_IN_GGAA(x1, x2)
U7_GGAA(x1, x2, x3, x4, x5)  =  U7_GGAA(x1, x2, x5)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

PERM19_IN_GA(T37) → U3_GA(T37, append2c34_in_aaag(T37))
U3_GA(T37, append2c34_out_aaag(T41, T36, T42, T37)) → P35_IN_GGAA(T41, T42)
P35_IN_GGAA(T41, T42) → U7_GGAA(T41, T42, append1c44_in_gga(T41, T42))
U7_GGAA(T41, T42, append1c44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63)

The TRS R consists of the following rules:

append2c34_in_aaag(.(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, T58)) → U15_aaag(X118, T58, append2c34_in_aaag(T58))
append1c44_in_gga([], T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82) → U18_gga(T78, T81, T82, append1c44_in_gga(T81, T82))
U15_aaag(X118, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
U18_gga(T78, T81, T82, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The set Q consists of the following terms:

append2c34_in_aaag(x0)
append1c44_in_gga(x0, x1)
U15_aaag(x0, x1, x2)
U18_gga(x0, x1, x2, x3)

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

(26) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


P35_IN_GGAA(T41, T42) → U7_GGAA(T41, T42, append1c44_in_gga(T41, T42))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 1 + x2   
POL(P35_IN_GGAA(x1, x2)) = 1 + x1 + x2   
POL(PERM19_IN_GA(x1)) = x1   
POL(U15_aaag(x1, x2, x3)) = 1 + x3   
POL(U18_gga(x1, x2, x3, x4)) = 1 + x4   
POL(U3_GA(x1, x2)) = x2   
POL(U7_GGAA(x1, x2, x3)) = x3   
POL([]) = 0   
POL(append1c44_in_gga(x1, x2)) = x1 + x2   
POL(append1c44_out_gga(x1, x2, x3)) = x3   
POL(append2c34_in_aaag(x1)) = x1   
POL(append2c34_out_aaag(x1, x2, x3, x4)) = 1 + x1 + x3   

The following usable rules [FROCOS05] were oriented:

append2c34_in_aaag(.(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, T58)) → U15_aaag(X118, T58, append2c34_in_aaag(T58))
append1c44_in_gga([], T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82) → U18_gga(T78, T81, T82, append1c44_in_gga(T81, T82))
U15_aaag(X118, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
U18_gga(T78, T81, T82, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

(27) Obligation:

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

PERM19_IN_GA(T37) → U3_GA(T37, append2c34_in_aaag(T37))
U3_GA(T37, append2c34_out_aaag(T41, T36, T42, T37)) → P35_IN_GGAA(T41, T42)
U7_GGAA(T41, T42, append1c44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63)

The TRS R consists of the following rules:

append2c34_in_aaag(.(T50, X98)) → append2c34_out_aaag([], T50, X98, .(T50, X98))
append2c34_in_aaag(.(X118, T58)) → U15_aaag(X118, T58, append2c34_in_aaag(T58))
append1c44_in_gga([], T71) → append1c44_out_gga([], T71, T71)
append1c44_in_gga(.(T78, T81), T82) → U18_gga(T78, T81, T82, append1c44_in_gga(T81, T82))
U15_aaag(X118, T58, append2c34_out_aaag(X119, T57, X120, T58)) → append2c34_out_aaag(.(X118, X119), T57, X120, .(X118, T58))
U18_gga(T78, T81, T82, append1c44_out_gga(T81, T82, X153)) → append1c44_out_gga(.(T78, T81), T82, .(T78, X153))

The set Q consists of the following terms:

append2c34_in_aaag(x0)
append1c44_in_gga(x0, x1)
U15_aaag(x0, x1, x2)
U18_gga(x0, x1, x2, x3)

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

(28) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 3 less nodes.

(29) TRUE