(0) Obligation:

Clauses:

perm([], []).
perm(Xs, .(X, Ys)) :- ','(app(X1s, .(X, X2s), Xs), ','(app(X1s, X2s, Zs), perm(Zs, Ys))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Queries:

perm(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

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

Clauses:

appc34([], T50, X98, .(T50, X98)).
appc34(.(X118, X119), T58, X120, .(X118, T57)) :- appc34(X119, T58, X120, T57).
permc19([], []).
permc19(T36, .(T37, T43)) :- ','(appc34(T41, T37, T42, T36), qc35(T41, T42, X77, T43)).
appc44([], T71, T71).
appc44(.(T78, T81), T82, .(T78, X153)) :- appc44(T81, T82, X153).
qc35(T41, T42, T63, T64) :- ','(appc44(T41, T42, T63), permc19(T63, T64)).
appc18(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)
app34_in: (f,f,f,b)
appc34_in: (f,f,f,b)
p35_in: (b,b,f,f)
app44_in: (b,b,f)
appc44_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, appc18_in_ga(T25, T26))
U9_GA(T23, T25, T24, appc18_out_ga(T25, T26)) → U10_GA(T23, T25, T24, perm19_in_ga(T26, T24))
U9_GA(T23, T25, T24, appc18_out_ga(T25, T26)) → PERM19_IN_GA(T26, T24)
PERM19_IN_GA(T36, .(T37, T38)) → U2_GA(T36, T37, T38, app34_in_aaag(X75, T37, X76, T36))
PERM19_IN_GA(T36, .(T37, T38)) → APP34_IN_AAAG(X75, T37, X76, T36)
APP34_IN_AAAG(.(X118, X119), T58, X120, .(X118, T57)) → U1_AAAG(X118, X119, T58, X120, T57, app34_in_aaag(X119, T58, X120, T57))
APP34_IN_AAAG(.(X118, X119), T58, X120, .(X118, T57)) → APP34_IN_AAAG(X119, T58, X120, T57)
PERM19_IN_GA(T36, .(T37, T43)) → U3_GA(T36, T37, T43, appc34_in_aaag(T41, T37, T42, T36))
U3_GA(T36, T37, T43, appc34_out_aaag(T41, T37, T42, T36)) → U4_GA(T36, T37, T43, p35_in_ggaa(T41, T42, X77, T43))
U3_GA(T36, T37, T43, appc34_out_aaag(T41, T37, T42, T36)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, X77, T43) → U6_GGAA(T41, T42, X77, T43, app44_in_gga(T41, T42, X77))
P35_IN_GGAA(T41, T42, X77, T43) → APP44_IN_GGA(T41, T42, X77)
APP44_IN_GGA(.(T78, T81), T82, .(T78, X153)) → U5_GGA(T78, T81, T82, X153, app44_in_gga(T81, T82, X153))
APP44_IN_GGA(.(T78, T81), T82, .(T78, X153)) → APP44_IN_GGA(T81, T82, X153)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, appc44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, appc44_out_gga(T41, T42, T63)) → U8_GGAA(T41, T42, T63, T64, perm19_in_ga(T63, T64))
U7_GGAA(T41, T42, T63, T64, appc44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → U11_GA(X178, T90, T91, T92, app34_in_aaag(X179, T91, X180, T90))
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → APP34_IN_AAAG(X179, T91, X180, T90)
PERM1_IN_GA(.(X178, T90), .(T91, T97)) → U12_GA(X178, T90, T91, T97, appc34_in_aaag(T95, T91, T96, T90))
U12_GA(X178, T90, T91, T97, appc34_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, appc34_out_aaag(T95, T91, T96, T90)) → P35_IN_GGAA(.(X178, T95), T96, X30, T97)

The TRS R consists of the following rules:

appc18_in_ga(X58, X58) → appc18_out_ga(X58, X58)
appc34_in_aaag([], T50, X98, .(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, X119), T58, X120, .(X118, T57)) → U15_aaag(X118, X119, T58, X120, T57, appc34_in_aaag(X119, T58, X120, T57))
U15_aaag(X118, X119, T58, X120, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
appc44_in_gga([], T71, T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, appc44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_ga(x1, x2)  =  appc18_in_ga(x1)
appc18_out_ga(x1, x2)  =  appc18_out_ga(x1, x2)
perm19_in_ga(x1, x2)  =  perm19_in_ga(x1)
app34_in_aaag(x1, x2, x3, x4)  =  app34_in_aaag(x4)
appc34_in_aaag(x1, x2, x3, x4)  =  appc34_in_aaag(x4)
appc34_out_aaag(x1, x2, x3, x4)  =  appc34_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)
app44_in_gga(x1, x2, x3)  =  app44_in_gga(x1, x2)
appc44_in_gga(x1, x2, x3)  =  appc44_in_gga(x1, x2)
[]  =  []
appc44_out_gga(x1, x2, x3)  =  appc44_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)
APP34_IN_AAAG(x1, x2, x3, x4)  =  APP34_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)
APP44_IN_GGA(x1, x2, x3)  =  APP44_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, appc18_in_ga(T25, T26))
U9_GA(T23, T25, T24, appc18_out_ga(T25, T26)) → U10_GA(T23, T25, T24, perm19_in_ga(T26, T24))
U9_GA(T23, T25, T24, appc18_out_ga(T25, T26)) → PERM19_IN_GA(T26, T24)
PERM19_IN_GA(T36, .(T37, T38)) → U2_GA(T36, T37, T38, app34_in_aaag(X75, T37, X76, T36))
PERM19_IN_GA(T36, .(T37, T38)) → APP34_IN_AAAG(X75, T37, X76, T36)
APP34_IN_AAAG(.(X118, X119), T58, X120, .(X118, T57)) → U1_AAAG(X118, X119, T58, X120, T57, app34_in_aaag(X119, T58, X120, T57))
APP34_IN_AAAG(.(X118, X119), T58, X120, .(X118, T57)) → APP34_IN_AAAG(X119, T58, X120, T57)
PERM19_IN_GA(T36, .(T37, T43)) → U3_GA(T36, T37, T43, appc34_in_aaag(T41, T37, T42, T36))
U3_GA(T36, T37, T43, appc34_out_aaag(T41, T37, T42, T36)) → U4_GA(T36, T37, T43, p35_in_ggaa(T41, T42, X77, T43))
U3_GA(T36, T37, T43, appc34_out_aaag(T41, T37, T42, T36)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, X77, T43) → U6_GGAA(T41, T42, X77, T43, app44_in_gga(T41, T42, X77))
P35_IN_GGAA(T41, T42, X77, T43) → APP44_IN_GGA(T41, T42, X77)
APP44_IN_GGA(.(T78, T81), T82, .(T78, X153)) → U5_GGA(T78, T81, T82, X153, app44_in_gga(T81, T82, X153))
APP44_IN_GGA(.(T78, T81), T82, .(T78, X153)) → APP44_IN_GGA(T81, T82, X153)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, appc44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, appc44_out_gga(T41, T42, T63)) → U8_GGAA(T41, T42, T63, T64, perm19_in_ga(T63, T64))
U7_GGAA(T41, T42, T63, T64, appc44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → U11_GA(X178, T90, T91, T92, app34_in_aaag(X179, T91, X180, T90))
PERM1_IN_GA(.(X178, T90), .(T91, T92)) → APP34_IN_AAAG(X179, T91, X180, T90)
PERM1_IN_GA(.(X178, T90), .(T91, T97)) → U12_GA(X178, T90, T91, T97, appc34_in_aaag(T95, T91, T96, T90))
U12_GA(X178, T90, T91, T97, appc34_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, appc34_out_aaag(T95, T91, T96, T90)) → P35_IN_GGAA(.(X178, T95), T96, X30, T97)

The TRS R consists of the following rules:

appc18_in_ga(X58, X58) → appc18_out_ga(X58, X58)
appc34_in_aaag([], T50, X98, .(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, X119), T58, X120, .(X118, T57)) → U15_aaag(X118, X119, T58, X120, T57, appc34_in_aaag(X119, T58, X120, T57))
U15_aaag(X118, X119, T58, X120, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
appc44_in_gga([], T71, T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, appc44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_ga(x1, x2)  =  appc18_in_ga(x1)
appc18_out_ga(x1, x2)  =  appc18_out_ga(x1, x2)
perm19_in_ga(x1, x2)  =  perm19_in_ga(x1)
app34_in_aaag(x1, x2, x3, x4)  =  app34_in_aaag(x4)
appc34_in_aaag(x1, x2, x3, x4)  =  appc34_in_aaag(x4)
appc34_out_aaag(x1, x2, x3, x4)  =  appc34_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)
app44_in_gga(x1, x2, x3)  =  app44_in_gga(x1, x2)
appc44_in_gga(x1, x2, x3)  =  appc44_in_gga(x1, x2)
[]  =  []
appc44_out_gga(x1, x2, x3)  =  appc44_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)
APP34_IN_AAAG(x1, x2, x3, x4)  =  APP34_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)
APP44_IN_GGA(x1, x2, x3)  =  APP44_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:

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

The TRS R consists of the following rules:

appc18_in_ga(X58, X58) → appc18_out_ga(X58, X58)
appc34_in_aaag([], T50, X98, .(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, X119), T58, X120, .(X118, T57)) → U15_aaag(X118, X119, T58, X120, T57, appc34_in_aaag(X119, T58, X120, T57))
U15_aaag(X118, X119, T58, X120, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
appc44_in_gga([], T71, T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, appc44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_ga(x1, x2)  =  appc18_in_ga(x1)
appc18_out_ga(x1, x2)  =  appc18_out_ga(x1, x2)
appc34_in_aaag(x1, x2, x3, x4)  =  appc34_in_aaag(x4)
appc34_out_aaag(x1, x2, x3, x4)  =  appc34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
appc44_in_gga(x1, x2, x3)  =  appc44_in_gga(x1, x2)
[]  =  []
appc44_out_gga(x1, x2, x3)  =  appc44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
APP44_IN_GGA(x1, x2, x3)  =  APP44_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:

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

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP44_IN_GGA(x1, x2, x3)  =  APP44_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:

APP44_IN_GGA(.(T78, T81), T82) → APP44_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:

  • APP44_IN_GGA(.(T78, T81), T82) → APP44_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:

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

The TRS R consists of the following rules:

appc18_in_ga(X58, X58) → appc18_out_ga(X58, X58)
appc34_in_aaag([], T50, X98, .(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, X119), T58, X120, .(X118, T57)) → U15_aaag(X118, X119, T58, X120, T57, appc34_in_aaag(X119, T58, X120, T57))
U15_aaag(X118, X119, T58, X120, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
appc44_in_gga([], T71, T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, appc44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_ga(x1, x2)  =  appc18_in_ga(x1)
appc18_out_ga(x1, x2)  =  appc18_out_ga(x1, x2)
appc34_in_aaag(x1, x2, x3, x4)  =  appc34_in_aaag(x4)
appc34_out_aaag(x1, x2, x3, x4)  =  appc34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
appc44_in_gga(x1, x2, x3)  =  appc44_in_gga(x1, x2)
[]  =  []
appc44_out_gga(x1, x2, x3)  =  appc44_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
APP34_IN_AAAG(x1, x2, x3, x4)  =  APP34_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:

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

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
APP34_IN_AAAG(x1, x2, x3, x4)  =  APP34_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:

APP34_IN_AAAG(.(X118, T57)) → APP34_IN_AAAG(T57)

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:

  • APP34_IN_AAAG(.(X118, T57)) → APP34_IN_AAAG(T57)
    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(T36, .(T37, T43)) → U3_GA(T36, T37, T43, appc34_in_aaag(T41, T37, T42, T36))
U3_GA(T36, T37, T43, appc34_out_aaag(T41, T37, T42, T36)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, appc44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, appc44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)

The TRS R consists of the following rules:

appc18_in_ga(X58, X58) → appc18_out_ga(X58, X58)
appc34_in_aaag([], T50, X98, .(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, X119), T58, X120, .(X118, T57)) → U15_aaag(X118, X119, T58, X120, T57, appc34_in_aaag(X119, T58, X120, T57))
U15_aaag(X118, X119, T58, X120, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
appc44_in_gga([], T71, T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, appc44_in_gga(T81, T82, X153))
U18_gga(T78, T81, T82, X153, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc18_in_ga(x1, x2)  =  appc18_in_ga(x1)
appc18_out_ga(x1, x2)  =  appc18_out_ga(x1, x2)
appc34_in_aaag(x1, x2, x3, x4)  =  appc34_in_aaag(x4)
appc34_out_aaag(x1, x2, x3, x4)  =  appc34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
appc44_in_gga(x1, x2, x3)  =  appc44_in_gga(x1, x2)
[]  =  []
appc44_out_gga(x1, x2, x3)  =  appc44_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(T36, .(T37, T43)) → U3_GA(T36, T37, T43, appc34_in_aaag(T41, T37, T42, T36))
U3_GA(T36, T37, T43, appc34_out_aaag(T41, T37, T42, T36)) → P35_IN_GGAA(T41, T42, X77, T43)
P35_IN_GGAA(T41, T42, T63, T64) → U7_GGAA(T41, T42, T63, T64, appc44_in_gga(T41, T42, T63))
U7_GGAA(T41, T42, T63, T64, appc44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63, T64)

The TRS R consists of the following rules:

appc34_in_aaag([], T50, X98, .(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, X119), T58, X120, .(X118, T57)) → U15_aaag(X118, X119, T58, X120, T57, appc34_in_aaag(X119, T58, X120, T57))
appc44_in_gga([], T71, T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82, .(T78, X153)) → U18_gga(T78, T81, T82, X153, appc44_in_gga(T81, T82, X153))
U15_aaag(X118, X119, T58, X120, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
U18_gga(T78, T81, T82, X153, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appc34_in_aaag(x1, x2, x3, x4)  =  appc34_in_aaag(x4)
appc34_out_aaag(x1, x2, x3, x4)  =  appc34_out_aaag(x1, x2, x3, x4)
U15_aaag(x1, x2, x3, x4, x5, x6)  =  U15_aaag(x1, x5, x6)
appc44_in_gga(x1, x2, x3)  =  appc44_in_gga(x1, x2)
[]  =  []
appc44_out_gga(x1, x2, x3)  =  appc44_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(T36) → U3_GA(T36, appc34_in_aaag(T36))
U3_GA(T36, appc34_out_aaag(T41, T37, T42, T36)) → P35_IN_GGAA(T41, T42)
P35_IN_GGAA(T41, T42) → U7_GGAA(T41, T42, appc44_in_gga(T41, T42))
U7_GGAA(T41, T42, appc44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63)

The TRS R consists of the following rules:

appc34_in_aaag(.(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, T57)) → U15_aaag(X118, T57, appc34_in_aaag(T57))
appc44_in_gga([], T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82) → U18_gga(T78, T81, T82, appc44_in_gga(T81, T82))
U15_aaag(X118, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
U18_gga(T78, T81, T82, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The set Q consists of the following terms:

appc34_in_aaag(x0)
appc44_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, appc44_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(appc34_in_aaag(x1)) = x1   
POL(appc34_out_aaag(x1, x2, x3, x4)) = 1 + x1 + x3   
POL(appc44_in_gga(x1, x2)) = x1 + x2   
POL(appc44_out_gga(x1, x2, x3)) = x3   

The following usable rules [FROCOS05] were oriented:

appc34_in_aaag(.(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, T57)) → U15_aaag(X118, T57, appc34_in_aaag(T57))
appc44_in_gga([], T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82) → U18_gga(T78, T81, T82, appc44_in_gga(T81, T82))
U15_aaag(X118, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
U18_gga(T78, T81, T82, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

(27) Obligation:

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

PERM19_IN_GA(T36) → U3_GA(T36, appc34_in_aaag(T36))
U3_GA(T36, appc34_out_aaag(T41, T37, T42, T36)) → P35_IN_GGAA(T41, T42)
U7_GGAA(T41, T42, appc44_out_gga(T41, T42, T63)) → PERM19_IN_GA(T63)

The TRS R consists of the following rules:

appc34_in_aaag(.(T50, X98)) → appc34_out_aaag([], T50, X98, .(T50, X98))
appc34_in_aaag(.(X118, T57)) → U15_aaag(X118, T57, appc34_in_aaag(T57))
appc44_in_gga([], T71) → appc44_out_gga([], T71, T71)
appc44_in_gga(.(T78, T81), T82) → U18_gga(T78, T81, T82, appc44_in_gga(T81, T82))
U15_aaag(X118, T57, appc34_out_aaag(X119, T58, X120, T57)) → appc34_out_aaag(.(X118, X119), T58, X120, .(X118, T57))
U18_gga(T78, T81, T82, appc44_out_gga(T81, T82, X153)) → appc44_out_gga(.(T78, T81), T82, .(T78, X153))

The set Q consists of the following terms:

appc34_in_aaag(x0)
appc44_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