(0) Obligation:

Clauses:

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

Queries:

perm(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

app210(.(X98, X99), T40, X100, .(X98, T39)) :- app210(X99, T40, X100, T39).
app125(.(T83, T84), T85, .(T83, X200)) :- app125(T84, T85, X200).
app240(.(X294, X295), T131, X296, .(X294, T130)) :- app240(X295, T131, X296, T130).
perm21(T110, .(T111, T112)) :- app240(X242, T111, X243, T110).
perm21(T110, .(T111, T117)) :- ','(app2c40(T115, T111, T116, T110), app150(T115, T116, X244)).
perm21(T110, .(T111, T141)) :- ','(app2c40(T115, T111, T116, T110), ','(app1c50(T115, T116, T140), perm21(T140, T141))).
app150(.(T157, T160), T161, .(T157, X349)) :- app150(T160, T161, X349).
perm1(.(X45, T20), .(T21, T22)) :- app210(X46, T21, X47, T20).
perm1(.(X169, T20), .(T21, T27)) :- ','(app2c10(T66, T21, T67, T20), app125(T66, T67, X170)).
perm1(.(T48, T20), .(T21, T27)) :- ','(app2c10(T25, T21, T26, T20), ','(app1c20(T48, T25, T26, T49), perm21(T49, T27))).
perm1(.(T175, T179), .(T175, T176)) :- ','(app1c67(T179, T180), perm21(T180, T176)).

Clauses:

app2c10(.(X98, X99), T40, X100, .(X98, T39)) :- app2c10(X99, T40, X100, T39).
app2c10([], T45, X117, .(T45, X117)).
app1c25(.(T83, T84), T85, .(T83, X200)) :- app1c25(T84, T85, X200).
app1c25([], T91, T91).
app2c40(.(X294, X295), T131, X296, .(X294, T130)) :- app2c40(X295, T131, X296, T130).
app2c40([], T136, X313, .(T136, X313)).
permc21(T110, .(T111, T141)) :- ','(app2c40(T115, T111, T116, T110), ','(app1c50(T115, T116, T140), permc21(T140, T141))).
permc21([], []).
app1c50(.(T157, T160), T161, .(T157, X349)) :- app1c50(T160, T161, X349).
app1c50([], T167, T167).
app1c20(X169, T66, T67, .(X169, X170)) :- app1c25(T66, T67, X170).
app1c67(X408, X408).

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)
app210_in: (f,f,f,b)
app2c10_in: (f,f,f,b)
app125_in: (b,b,f)
app1c20_in: (b,b,b,f)
app1c25_in: (b,b,f)
perm21_in: (b,f)
app240_in: (f,f,f,b)
app2c40_in: (f,f,f,b)
app150_in: (b,b,f)
app1c50_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(.(X45, T20), .(T21, T22)) → U11_GA(X45, T20, T21, T22, app210_in_aaag(X46, T21, X47, T20))
PERM1_IN_GA(.(X45, T20), .(T21, T22)) → APP210_IN_AAAG(X46, T21, X47, T20)
APP210_IN_AAAG(.(X98, X99), T40, X100, .(X98, T39)) → U1_AAAG(X98, X99, T40, X100, T39, app210_in_aaag(X99, T40, X100, T39))
APP210_IN_AAAG(.(X98, X99), T40, X100, .(X98, T39)) → APP210_IN_AAAG(X99, T40, X100, T39)
PERM1_IN_GA(.(X169, T20), .(T21, T27)) → U12_GA(X169, T20, T21, T27, app2c10_in_aaag(T66, T21, T67, T20))
U12_GA(X169, T20, T21, T27, app2c10_out_aaag(T66, T21, T67, T20)) → U13_GA(X169, T20, T21, T27, app125_in_gga(T66, T67, X170))
U12_GA(X169, T20, T21, T27, app2c10_out_aaag(T66, T21, T67, T20)) → APP125_IN_GGA(T66, T67, X170)
APP125_IN_GGA(.(T83, T84), T85, .(T83, X200)) → U2_GGA(T83, T84, T85, X200, app125_in_gga(T84, T85, X200))
APP125_IN_GGA(.(T83, T84), T85, .(T83, X200)) → APP125_IN_GGA(T84, T85, X200)
PERM1_IN_GA(.(T48, T20), .(T21, T27)) → U14_GA(T48, T20, T21, T27, app2c10_in_aaag(T25, T21, T26, T20))
U14_GA(T48, T20, T21, T27, app2c10_out_aaag(T25, T21, T26, T20)) → U15_GA(T48, T20, T21, T27, app1c20_in_ggga(T48, T25, T26, T49))
U15_GA(T48, T20, T21, T27, app1c20_out_ggga(T48, T25, T26, T49)) → U16_GA(T48, T20, T21, T27, perm21_in_ga(T49, T27))
U15_GA(T48, T20, T21, T27, app1c20_out_ggga(T48, T25, T26, T49)) → PERM21_IN_GA(T49, T27)
PERM21_IN_GA(T110, .(T111, T112)) → U4_GA(T110, T111, T112, app240_in_aaag(X242, T111, X243, T110))
PERM21_IN_GA(T110, .(T111, T112)) → APP240_IN_AAAG(X242, T111, X243, T110)
APP240_IN_AAAG(.(X294, X295), T131, X296, .(X294, T130)) → U3_AAAG(X294, X295, T131, X296, T130, app240_in_aaag(X295, T131, X296, T130))
APP240_IN_AAAG(.(X294, X295), T131, X296, .(X294, T130)) → APP240_IN_AAAG(X295, T131, X296, T130)
PERM21_IN_GA(T110, .(T111, T117)) → U5_GA(T110, T111, T117, app2c40_in_aaag(T115, T111, T116, T110))
U5_GA(T110, T111, T117, app2c40_out_aaag(T115, T111, T116, T110)) → U6_GA(T110, T111, T117, app150_in_gga(T115, T116, X244))
U5_GA(T110, T111, T117, app2c40_out_aaag(T115, T111, T116, T110)) → APP150_IN_GGA(T115, T116, X244)
APP150_IN_GGA(.(T157, T160), T161, .(T157, X349)) → U10_GGA(T157, T160, T161, X349, app150_in_gga(T160, T161, X349))
APP150_IN_GGA(.(T157, T160), T161, .(T157, X349)) → APP150_IN_GGA(T160, T161, X349)
PERM21_IN_GA(T110, .(T111, T141)) → U7_GA(T110, T111, T141, app2c40_in_aaag(T115, T111, T116, T110))
U7_GA(T110, T111, T141, app2c40_out_aaag(T115, T111, T116, T110)) → U8_GA(T110, T111, T141, app1c50_in_gga(T115, T116, T140))
U8_GA(T110, T111, T141, app1c50_out_gga(T115, T116, T140)) → U9_GA(T110, T111, T141, perm21_in_ga(T140, T141))
U8_GA(T110, T111, T141, app1c50_out_gga(T115, T116, T140)) → PERM21_IN_GA(T140, T141)
PERM1_IN_GA(.(T175, T179), .(T175, T176)) → U17_GA(T175, T179, T176, app1c67_in_ga(T179, T180))
U17_GA(T175, T179, T176, app1c67_out_ga(T179, T180)) → U18_GA(T175, T179, T176, perm21_in_ga(T180, T176))
U17_GA(T175, T179, T176, app1c67_out_ga(T179, T180)) → PERM21_IN_GA(T180, T176)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app210_in_aaag(x1, x2, x3, x4)  =  app210_in_aaag(x4)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app125_in_gga(x1, x2, x3)  =  app125_in_gga(x1, x2)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
perm21_in_ga(x1, x2)  =  perm21_in_ga(x1)
app240_in_aaag(x1, x2, x3, x4)  =  app240_in_aaag(x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app150_in_gga(x1, x2, x3)  =  app150_in_gga(x1, x2)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x5)
APP210_IN_AAAG(x1, x2, x3, x4)  =  APP210_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6)  =  U1_AAAG(x1, x5, x6)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x5)
APP125_IN_GGA(x1, x2, x3)  =  APP125_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x5)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x5)
U16_GA(x1, x2, x3, x4, x5)  =  U16_GA(x1, x2, x5)
PERM21_IN_GA(x1, x2)  =  PERM21_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
APP240_IN_AAAG(x1, x2, x3, x4)  =  APP240_IN_AAAG(x4)
U3_AAAG(x1, x2, x3, x4, x5, x6)  =  U3_AAAG(x1, x5, x6)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
APP150_IN_GGA(x1, x2, x3)  =  APP150_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4, x5)  =  U10_GGA(x1, x2, x3, x5)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x1, x2, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)

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(.(X45, T20), .(T21, T22)) → U11_GA(X45, T20, T21, T22, app210_in_aaag(X46, T21, X47, T20))
PERM1_IN_GA(.(X45, T20), .(T21, T22)) → APP210_IN_AAAG(X46, T21, X47, T20)
APP210_IN_AAAG(.(X98, X99), T40, X100, .(X98, T39)) → U1_AAAG(X98, X99, T40, X100, T39, app210_in_aaag(X99, T40, X100, T39))
APP210_IN_AAAG(.(X98, X99), T40, X100, .(X98, T39)) → APP210_IN_AAAG(X99, T40, X100, T39)
PERM1_IN_GA(.(X169, T20), .(T21, T27)) → U12_GA(X169, T20, T21, T27, app2c10_in_aaag(T66, T21, T67, T20))
U12_GA(X169, T20, T21, T27, app2c10_out_aaag(T66, T21, T67, T20)) → U13_GA(X169, T20, T21, T27, app125_in_gga(T66, T67, X170))
U12_GA(X169, T20, T21, T27, app2c10_out_aaag(T66, T21, T67, T20)) → APP125_IN_GGA(T66, T67, X170)
APP125_IN_GGA(.(T83, T84), T85, .(T83, X200)) → U2_GGA(T83, T84, T85, X200, app125_in_gga(T84, T85, X200))
APP125_IN_GGA(.(T83, T84), T85, .(T83, X200)) → APP125_IN_GGA(T84, T85, X200)
PERM1_IN_GA(.(T48, T20), .(T21, T27)) → U14_GA(T48, T20, T21, T27, app2c10_in_aaag(T25, T21, T26, T20))
U14_GA(T48, T20, T21, T27, app2c10_out_aaag(T25, T21, T26, T20)) → U15_GA(T48, T20, T21, T27, app1c20_in_ggga(T48, T25, T26, T49))
U15_GA(T48, T20, T21, T27, app1c20_out_ggga(T48, T25, T26, T49)) → U16_GA(T48, T20, T21, T27, perm21_in_ga(T49, T27))
U15_GA(T48, T20, T21, T27, app1c20_out_ggga(T48, T25, T26, T49)) → PERM21_IN_GA(T49, T27)
PERM21_IN_GA(T110, .(T111, T112)) → U4_GA(T110, T111, T112, app240_in_aaag(X242, T111, X243, T110))
PERM21_IN_GA(T110, .(T111, T112)) → APP240_IN_AAAG(X242, T111, X243, T110)
APP240_IN_AAAG(.(X294, X295), T131, X296, .(X294, T130)) → U3_AAAG(X294, X295, T131, X296, T130, app240_in_aaag(X295, T131, X296, T130))
APP240_IN_AAAG(.(X294, X295), T131, X296, .(X294, T130)) → APP240_IN_AAAG(X295, T131, X296, T130)
PERM21_IN_GA(T110, .(T111, T117)) → U5_GA(T110, T111, T117, app2c40_in_aaag(T115, T111, T116, T110))
U5_GA(T110, T111, T117, app2c40_out_aaag(T115, T111, T116, T110)) → U6_GA(T110, T111, T117, app150_in_gga(T115, T116, X244))
U5_GA(T110, T111, T117, app2c40_out_aaag(T115, T111, T116, T110)) → APP150_IN_GGA(T115, T116, X244)
APP150_IN_GGA(.(T157, T160), T161, .(T157, X349)) → U10_GGA(T157, T160, T161, X349, app150_in_gga(T160, T161, X349))
APP150_IN_GGA(.(T157, T160), T161, .(T157, X349)) → APP150_IN_GGA(T160, T161, X349)
PERM21_IN_GA(T110, .(T111, T141)) → U7_GA(T110, T111, T141, app2c40_in_aaag(T115, T111, T116, T110))
U7_GA(T110, T111, T141, app2c40_out_aaag(T115, T111, T116, T110)) → U8_GA(T110, T111, T141, app1c50_in_gga(T115, T116, T140))
U8_GA(T110, T111, T141, app1c50_out_gga(T115, T116, T140)) → U9_GA(T110, T111, T141, perm21_in_ga(T140, T141))
U8_GA(T110, T111, T141, app1c50_out_gga(T115, T116, T140)) → PERM21_IN_GA(T140, T141)
PERM1_IN_GA(.(T175, T179), .(T175, T176)) → U17_GA(T175, T179, T176, app1c67_in_ga(T179, T180))
U17_GA(T175, T179, T176, app1c67_out_ga(T179, T180)) → U18_GA(T175, T179, T176, perm21_in_ga(T180, T176))
U17_GA(T175, T179, T176, app1c67_out_ga(T179, T180)) → PERM21_IN_GA(T180, T176)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app210_in_aaag(x1, x2, x3, x4)  =  app210_in_aaag(x4)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app125_in_gga(x1, x2, x3)  =  app125_in_gga(x1, x2)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
perm21_in_ga(x1, x2)  =  perm21_in_ga(x1)
app240_in_aaag(x1, x2, x3, x4)  =  app240_in_aaag(x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app150_in_gga(x1, x2, x3)  =  app150_in_gga(x1, x2)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x5)
APP210_IN_AAAG(x1, x2, x3, x4)  =  APP210_IN_AAAG(x4)
U1_AAAG(x1, x2, x3, x4, x5, x6)  =  U1_AAAG(x1, x5, x6)
U12_GA(x1, x2, x3, x4, x5)  =  U12_GA(x1, x2, x5)
U13_GA(x1, x2, x3, x4, x5)  =  U13_GA(x1, x2, x5)
APP125_IN_GGA(x1, x2, x3)  =  APP125_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U14_GA(x1, x2, x3, x4, x5)  =  U14_GA(x1, x2, x5)
U15_GA(x1, x2, x3, x4, x5)  =  U15_GA(x1, x2, x5)
U16_GA(x1, x2, x3, x4, x5)  =  U16_GA(x1, x2, x5)
PERM21_IN_GA(x1, x2)  =  PERM21_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
APP240_IN_AAAG(x1, x2, x3, x4)  =  APP240_IN_AAAG(x4)
U3_AAAG(x1, x2, x3, x4, x5, x6)  =  U3_AAAG(x1, x5, x6)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x4)
APP150_IN_GGA(x1, x2, x3)  =  APP150_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4, x5)  =  U10_GGA(x1, x2, x3, x5)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x1, x2, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 22 less nodes.

(6) Complex Obligation (AND)

(7) Obligation:

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

APP150_IN_GGA(.(T157, T160), T161, .(T157, X349)) → APP150_IN_GGA(T160, T161, X349)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
APP150_IN_GGA(x1, x2, x3)  =  APP150_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:

APP150_IN_GGA(.(T157, T160), T161, .(T157, X349)) → APP150_IN_GGA(T160, T161, X349)

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

APP150_IN_GGA(.(T157, T160), T161) → APP150_IN_GGA(T160, T161)

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:

  • APP150_IN_GGA(.(T157, T160), T161) → APP150_IN_GGA(T160, T161)
    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:

APP240_IN_AAAG(.(X294, X295), T131, X296, .(X294, T130)) → APP240_IN_AAAG(X295, T131, X296, T130)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
APP240_IN_AAAG(x1, x2, x3, x4)  =  APP240_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:

APP240_IN_AAAG(.(X294, X295), T131, X296, .(X294, T130)) → APP240_IN_AAAG(X295, T131, X296, T130)

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

APP240_IN_AAAG(.(X294, T130)) → APP240_IN_AAAG(T130)

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:

  • APP240_IN_AAAG(.(X294, T130)) → APP240_IN_AAAG(T130)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

PERM21_IN_GA(T110, .(T111, T141)) → U7_GA(T110, T111, T141, app2c40_in_aaag(T115, T111, T116, T110))
U7_GA(T110, T111, T141, app2c40_out_aaag(T115, T111, T116, T110)) → U8_GA(T110, T111, T141, app1c50_in_gga(T115, T116, T140))
U8_GA(T110, T111, T141, app1c50_out_gga(T115, T116, T140)) → PERM21_IN_GA(T140, T141)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
PERM21_IN_GA(x1, x2)  =  PERM21_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)

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:

PERM21_IN_GA(T110, .(T111, T141)) → U7_GA(T110, T111, T141, app2c40_in_aaag(T115, T111, T116, T110))
U7_GA(T110, T111, T141, app2c40_out_aaag(T115, T111, T116, T110)) → U8_GA(T110, T111, T141, app1c50_in_gga(T115, T116, T140))
U8_GA(T110, T111, T141, app1c50_out_gga(T115, T116, T140)) → PERM21_IN_GA(T140, T141)

The TRS R consists of the following rules:

app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
PERM21_IN_GA(x1, x2)  =  PERM21_IN_GA(x1)
U7_GA(x1, x2, x3, x4)  =  U7_GA(x1, x4)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x4)

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:

PERM21_IN_GA(T110) → U7_GA(T110, app2c40_in_aaag(T110))
U7_GA(T110, app2c40_out_aaag(T115, T111, T116, T110)) → U8_GA(T110, app1c50_in_gga(T115, T116))
U8_GA(T110, app1c50_out_gga(T115, T116, T140)) → PERM21_IN_GA(T140)

The TRS R consists of the following rules:

app2c40_in_aaag(.(X294, T130)) → U22_aaag(X294, T130, app2c40_in_aaag(T130))
app2c40_in_aaag(.(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
app1c50_in_gga(.(T157, T160), T161) → U26_gga(T157, T160, T161, app1c50_in_gga(T160, T161))
app1c50_in_gga([], T167) → app1c50_out_gga([], T167, T167)
U22_aaag(X294, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
U26_gga(T157, T160, T161, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))

The set Q consists of the following terms:

app2c40_in_aaag(x0)
app1c50_in_gga(x0, x1)
U22_aaag(x0, x1, x2)
U26_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.


U8_GA(T110, app1c50_out_gga(T115, T116, T140)) → PERM21_IN_GA(T140)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:

POL( U7_GA(x1, x2) ) = x2 + 2


POL( app2c40_in_aaag(x1) ) = 2x1


POL( .(x1, x2) ) = x1 + x2 + 1


POL( U22_aaag(x1, ..., x3) ) = 2x1 + x3 + 2


POL( app2c40_out_aaag(x1, ..., x4) ) = max{0, 2x1 + 2x2 + 2x3 - 2}


POL( [] ) = 2


POL( U8_GA(x1, x2) ) = max{0, 2x2 - 1}


POL( app1c50_in_gga(x1, x2) ) = x1 + x2


POL( U26_gga(x1, ..., x4) ) = x1 + x4 + 1


POL( app1c50_out_gga(x1, ..., x3) ) = x3 + 2


POL( PERM21_IN_GA(x1) ) = 2x1 + 2



The following usable rules [FROCOS05] were oriented:

app2c40_in_aaag(.(X294, T130)) → U22_aaag(X294, T130, app2c40_in_aaag(T130))
app2c40_in_aaag(.(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
app1c50_in_gga(.(T157, T160), T161) → U26_gga(T157, T160, T161, app1c50_in_gga(T160, T161))
app1c50_in_gga([], T167) → app1c50_out_gga([], T167, T167)
U22_aaag(X294, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
U26_gga(T157, T160, T161, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))

(27) Obligation:

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

PERM21_IN_GA(T110) → U7_GA(T110, app2c40_in_aaag(T110))
U7_GA(T110, app2c40_out_aaag(T115, T111, T116, T110)) → U8_GA(T110, app1c50_in_gga(T115, T116))

The TRS R consists of the following rules:

app2c40_in_aaag(.(X294, T130)) → U22_aaag(X294, T130, app2c40_in_aaag(T130))
app2c40_in_aaag(.(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
app1c50_in_gga(.(T157, T160), T161) → U26_gga(T157, T160, T161, app1c50_in_gga(T160, T161))
app1c50_in_gga([], T167) → app1c50_out_gga([], T167, T167)
U22_aaag(X294, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
U26_gga(T157, T160, T161, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))

The set Q consists of the following terms:

app2c40_in_aaag(x0)
app1c50_in_gga(x0, x1)
U22_aaag(x0, x1, x2)
U26_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 2 less nodes.

(29) TRUE

(30) Obligation:

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

APP125_IN_GGA(.(T83, T84), T85, .(T83, X200)) → APP125_IN_GGA(T84, T85, X200)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
APP125_IN_GGA(x1, x2, x3)  =  APP125_IN_GGA(x1, x2)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

APP125_IN_GGA(.(T83, T84), T85, .(T83, X200)) → APP125_IN_GGA(T84, T85, X200)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

APP125_IN_GGA(.(T83, T84), T85) → APP125_IN_GGA(T84, T85)

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

(35) 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:

  • APP125_IN_GGA(.(T83, T84), T85) → APP125_IN_GGA(T84, T85)
    The graph contains the following edges 1 > 1, 2 >= 2

(36) YES

(37) Obligation:

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

APP210_IN_AAAG(.(X98, X99), T40, X100, .(X98, T39)) → APP210_IN_AAAG(X99, T40, X100, T39)

The TRS R consists of the following rules:

app2c10_in_aaag(.(X98, X99), T40, X100, .(X98, T39)) → U20_aaag(X98, X99, T40, X100, T39, app2c10_in_aaag(X99, T40, X100, T39))
app2c10_in_aaag([], T45, X117, .(T45, X117)) → app2c10_out_aaag([], T45, X117, .(T45, X117))
U20_aaag(X98, X99, T40, X100, T39, app2c10_out_aaag(X99, T40, X100, T39)) → app2c10_out_aaag(.(X98, X99), T40, X100, .(X98, T39))
app1c20_in_ggga(X169, T66, T67, .(X169, X170)) → U27_ggga(X169, T66, T67, X170, app1c25_in_gga(T66, T67, X170))
app1c25_in_gga(.(T83, T84), T85, .(T83, X200)) → U21_gga(T83, T84, T85, X200, app1c25_in_gga(T84, T85, X200))
app1c25_in_gga([], T91, T91) → app1c25_out_gga([], T91, T91)
U21_gga(T83, T84, T85, X200, app1c25_out_gga(T84, T85, X200)) → app1c25_out_gga(.(T83, T84), T85, .(T83, X200))
U27_ggga(X169, T66, T67, X170, app1c25_out_gga(T66, T67, X170)) → app1c20_out_ggga(X169, T66, T67, .(X169, X170))
app2c40_in_aaag(.(X294, X295), T131, X296, .(X294, T130)) → U22_aaag(X294, X295, T131, X296, T130, app2c40_in_aaag(X295, T131, X296, T130))
app2c40_in_aaag([], T136, X313, .(T136, X313)) → app2c40_out_aaag([], T136, X313, .(T136, X313))
U22_aaag(X294, X295, T131, X296, T130, app2c40_out_aaag(X295, T131, X296, T130)) → app2c40_out_aaag(.(X294, X295), T131, X296, .(X294, T130))
app1c50_in_gga(.(T157, T160), T161, .(T157, X349)) → U26_gga(T157, T160, T161, X349, app1c50_in_gga(T160, T161, X349))
app1c50_in_gga([], T167, T167) → app1c50_out_gga([], T167, T167)
U26_gga(T157, T160, T161, X349, app1c50_out_gga(T160, T161, X349)) → app1c50_out_gga(.(T157, T160), T161, .(T157, X349))
app1c67_in_ga(X408, X408) → app1c67_out_ga(X408, X408)

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
app2c10_in_aaag(x1, x2, x3, x4)  =  app2c10_in_aaag(x4)
U20_aaag(x1, x2, x3, x4, x5, x6)  =  U20_aaag(x1, x5, x6)
app2c10_out_aaag(x1, x2, x3, x4)  =  app2c10_out_aaag(x1, x2, x3, x4)
app1c20_in_ggga(x1, x2, x3, x4)  =  app1c20_in_ggga(x1, x2, x3)
U27_ggga(x1, x2, x3, x4, x5)  =  U27_ggga(x1, x2, x3, x5)
app1c25_in_gga(x1, x2, x3)  =  app1c25_in_gga(x1, x2)
U21_gga(x1, x2, x3, x4, x5)  =  U21_gga(x1, x2, x3, x5)
[]  =  []
app1c25_out_gga(x1, x2, x3)  =  app1c25_out_gga(x1, x2, x3)
app1c20_out_ggga(x1, x2, x3, x4)  =  app1c20_out_ggga(x1, x2, x3, x4)
app2c40_in_aaag(x1, x2, x3, x4)  =  app2c40_in_aaag(x4)
U22_aaag(x1, x2, x3, x4, x5, x6)  =  U22_aaag(x1, x5, x6)
app2c40_out_aaag(x1, x2, x3, x4)  =  app2c40_out_aaag(x1, x2, x3, x4)
app1c50_in_gga(x1, x2, x3)  =  app1c50_in_gga(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
app1c50_out_gga(x1, x2, x3)  =  app1c50_out_gga(x1, x2, x3)
app1c67_in_ga(x1, x2)  =  app1c67_in_ga(x1)
app1c67_out_ga(x1, x2)  =  app1c67_out_ga(x1, x2)
APP210_IN_AAAG(x1, x2, x3, x4)  =  APP210_IN_AAAG(x4)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

APP210_IN_AAAG(.(X98, X99), T40, X100, .(X98, T39)) → APP210_IN_AAAG(X99, T40, X100, T39)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

APP210_IN_AAAG(.(X98, T39)) → APP210_IN_AAAG(T39)

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

(42) 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:

  • APP210_IN_AAAG(.(X98, T39)) → APP210_IN_AAAG(T39)
    The graph contains the following edges 1 > 1

(43) YES