Left Termination of the query pattern perm_in_2(a, g) w.r.t. the given Prolog program could not be shown:

0 Prolog
↳1 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
    ↳3 PrologToPiTRSProof (⇐)
        ↳4 PiTRS
        ↳5 DependencyPairsProof (⇔)
        ↳6 PiDP
        ↳7 DependencyGraphProof (⇔)
        ↳8 AND
            ↳9 PiDP
                ↳10 UsableRulesProof (⇔)
                ↳11 PiDP
                ↳12 PiDPToQDPProof (⇐)
                ↳13 QDP
                ↳14 QDPSizeChangeProof (⇔)
                ↳15 YES
            ↳16 PiDP
                ↳17 UsableRulesProof (⇔)
                ↳18 PiDP
                ↳19 PiDPToQDPProof (⇐)
                ↳20 QDP
                ↳21 NonTerminationProof (⇔)
                ↳22 NO
            ↳23 PiDP
                ↳24 UsableRulesProof (⇔)
                ↳25 PiDP
                ↳26 PiDPToQDPProof (⇐)
                ↳27 QDP
                ↳28 QDPSizeChangeProof (⇔)
                ↳29 YES
    ↳30 PrologToPiTRSProof (⇐)
        ↳31 PiTRS
        ↳32 DependencyPairsProof (⇔)
        ↳33 PiDP
        ↳34 DependencyGraphProof (⇔)
        ↳35 AND
            ↳36 PiDP
                ↳37 UsableRulesProof (⇔)
                ↳38 PiDP
                ↳39 PiDPToQDPProof (⇐)
                ↳40 QDP
                ↳41 QDPSizeChangeProof (⇔)
                ↳42 YES
            ↳43 PiDP
                ↳44 UsableRulesProof (⇔)
                ↳45 PiDP
                ↳46 PiDPToQDPProof (⇐)
                ↳47 QDP
                ↳48 NonTerminationProof (⇔)
                ↳49 NO
            ↳50 PiDP
                ↳51 UsableRulesProof (⇔)
                ↳52 PiDP
                ↳53 PiDPToQDPProof (⇐)
                ↳54 QDP
                ↳55 QDPSizeChangeProof (⇔)
                ↳56 YES

(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(a,g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

app24([], T35, X87, .(T35, X87)).
app24(.(X107, X108), T40, X109, .(X107, T42)) :- app24(X108, T40, X109, T42).
app38([], T69, T69).
app38(.(T76, T79), T80, .(T76, X177)) :- app38(T79, T80, X177).
app14(X40, X40).
app34(X153, T61, T62, .(X153, X154)) :- app38(T61, T62, X154).
perm1([], []).
perm1(.(T15, X25), .(T15, T9)) :- app14(X25, X12).
perm1(.(T15, T16), .(T15, T9)) :- ','(app14(T16, T17), perm1(T17, T9)).
perm1(.(X63, T24), .(T22, T9)) :- app24(X64, T22, X65, T24).
perm1(.(X63, T24), .(T22, T9)) :- ','(app24(T27, T22, T28, T24), app34(X63, T27, T28, X12)).
perm1(.(T47, T24), .(T22, T9)) :- ','(app24(T27, T22, T28, T24), ','(app34(T47, T27, T28, T48), perm1(T48, T9))).

Queries:

perm1(a,g).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1_in: (f,b)
app24_in: (f,f,f,f)
app34_in: (f,b,f,f)
app38_in: (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN_AG(.(T15, X25), .(T15, T9)) → U4_AG(T15, X25, T9, app14_in_aa(X25, X12))
PERM1_IN_AG(.(T15, X25), .(T15, T9)) → APP14_IN_AA(X25, X12)
PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → U6_AG(T15, T16, T9, perm1_in_ag(T17, T9))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U7_AG(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → APP24_IN_AAAA(X64, T22, X65, T24)
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → U1_AAAA(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U8_AG(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_AG(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(X63, T27, T28, X12)
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → U3_AGAA(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → APP38_IN_GAA(T61, T62, X154)
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → U2_GAA(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(T47, T27, T28, T48)
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_AG(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x4)
APP14_IN_AA(x1, x2)  =  APP14_IN_AA
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x4)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5, x6)  =  U1_AAAA(x6)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x5)
APP34_IN_AGAA(x1, x2, x3, x4)  =  APP34_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x5)

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

(6) Obligation:

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

PERM1_IN_AG(.(T15, X25), .(T15, T9)) → U4_AG(T15, X25, T9, app14_in_aa(X25, X12))
PERM1_IN_AG(.(T15, X25), .(T15, T9)) → APP14_IN_AA(X25, X12)
PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → U6_AG(T15, T16, T9, perm1_in_ag(T17, T9))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U7_AG(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → APP24_IN_AAAA(X64, T22, X65, T24)
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → U1_AAAA(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U8_AG(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_AG(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(X63, T27, T28, X12)
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → U3_AGAA(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → APP38_IN_GAA(T61, T62, X154)
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → U2_GAA(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(T47, T27, T28, T48)
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_AG(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x4)
APP14_IN_AA(x1, x2)  =  APP14_IN_AA
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x4)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5, x6)  =  U1_AAAA(x6)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x5)
APP34_IN_AGAA(x1, x2, x3, x4)  =  APP34_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

APP38_IN_GAA(.(T79)) → APP38_IN_GAA(T79)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APP38_IN_GAA(.(T79)) → APP38_IN_GAA(T79)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

APP24_IN_AAAA → APP24_IN_AAAA

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

(21) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = APP24_IN_AAAA evaluates to t =APP24_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP24_IN_AAAA to APP24_IN_AAAA.



(22) NO

(23) Obligation:

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

PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x5)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x2)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

PERM1_IN_AG(.(T9)) → U5_AG(T9, app14_in_aa)
U5_AG(T9, app14_out_aa) → PERM1_IN_AG(T9)
PERM1_IN_AG(.(T9)) → U10_AG(T9, app24_in_aaaa)
U10_AG(T9, app24_out_aaaa(T27)) → U11_AG(T9, app34_in_agaa(T27))
U11_AG(T9, app34_out_agaa) → PERM1_IN_AG(T9)

The TRS R consists of the following rules:

app14_in_aa → app14_out_aa
app24_in_aaaa → app24_out_aaaa([])
app24_in_aaaa → U1_aaaa(app24_in_aaaa)
app34_in_agaa(T61) → U3_agaa(app38_in_gaa(T61))
U1_aaaa(app24_out_aaaa(X108)) → app24_out_aaaa(.(X108))
U3_agaa(app38_out_gaa) → app34_out_agaa
app38_in_gaa([]) → app38_out_gaa
app38_in_gaa(.(T79)) → U2_gaa(app38_in_gaa(T79))
U2_gaa(app38_out_gaa) → app38_out_gaa

The set Q consists of the following terms:

app14_in_aa
app24_in_aaaa
app34_in_agaa(x0)
U1_aaaa(x0)
U3_agaa(x0)
app38_in_gaa(x0)
U2_gaa(x0)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U5_AG(T9, app14_out_aa) → PERM1_IN_AG(T9)
    The graph contains the following edges 1 >= 1

  • U11_AG(T9, app34_out_agaa) → PERM1_IN_AG(T9)
    The graph contains the following edges 1 >= 1

  • PERM1_IN_AG(.(T9)) → U5_AG(T9, app14_in_aa)
    The graph contains the following edges 1 > 1

  • PERM1_IN_AG(.(T9)) → U10_AG(T9, app24_in_aaaa)
    The graph contains the following edges 1 > 1

  • U10_AG(T9, app24_out_aaaa(T27)) → U11_AG(T9, app34_in_agaa(T27))
    The graph contains the following edges 1 >= 1

(29) YES

(30) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1_in: (f,b)
app24_in: (f,f,f,f)
app34_in: (f,b,f,f)
app38_in: (b,f,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(31) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)

(32) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN_AG(.(T15, X25), .(T15, T9)) → U4_AG(T15, X25, T9, app14_in_aa(X25, X12))
PERM1_IN_AG(.(T15, X25), .(T15, T9)) → APP14_IN_AA(X25, X12)
PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → U6_AG(T15, T16, T9, perm1_in_ag(T17, T9))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U7_AG(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → APP24_IN_AAAA(X64, T22, X65, T24)
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → U1_AAAA(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U8_AG(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_AG(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(X63, T27, T28, X12)
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → U3_AGAA(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → APP38_IN_GAA(T61, T62, X154)
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → U2_GAA(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(T47, T27, T28, T48)
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_AG(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x3, x4)
APP14_IN_AA(x1, x2)  =  APP14_IN_AA
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x4, x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5, x6)  =  U1_AAAA(x6)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x4, x5)
APP34_IN_AGAA(x1, x2, x3, x4)  =  APP34_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x2, x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x2, x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x4, x5)

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

(33) Obligation:

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

PERM1_IN_AG(.(T15, X25), .(T15, T9)) → U4_AG(T15, X25, T9, app14_in_aa(X25, X12))
PERM1_IN_AG(.(T15, X25), .(T15, T9)) → APP14_IN_AA(X25, X12)
PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → U6_AG(T15, T16, T9, perm1_in_ag(T17, T9))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U7_AG(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → APP24_IN_AAAA(X64, T22, X65, T24)
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → U1_AAAA(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U8_AG(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_AG(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
U8_AG(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(X63, T27, T28, X12)
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → U3_AGAA(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
APP34_IN_AGAA(X153, T61, T62, .(X153, X154)) → APP38_IN_GAA(T61, T62, X154)
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → U2_GAA(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → APP34_IN_AGAA(T47, T27, T28, T48)
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_AG(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x3, x4)
APP14_IN_AA(x1, x2)  =  APP14_IN_AA
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U6_AG(x1, x2, x3, x4)  =  U6_AG(x3, x4)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x4, x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5, x6)  =  U1_AAAA(x6)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x4, x5)
APP34_IN_AGAA(x1, x2, x3, x4)  =  APP34_IN_AGAA(x2)
U3_AGAA(x1, x2, x3, x4, x5)  =  U3_AGAA(x2, x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x2, x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)
U12_AG(x1, x2, x3, x4, x5)  =  U12_AG(x4, x5)

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

(34) DependencyGraphProof (EQUIVALENT transformation)

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

(35) Complex Obligation (AND)

(36) Obligation:

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

APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)

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

(37) UsableRulesProof (EQUIVALENT transformation)

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

(38) Obligation:

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

APP38_IN_GAA(.(T76, T79), T80, .(T76, X177)) → APP38_IN_GAA(T79, T80, X177)

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

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

(39) PiDPToQDPProof (SOUND transformation)

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

(40) Obligation:

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

APP38_IN_GAA(.(T79)) → APP38_IN_GAA(T79)

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

(41) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • APP38_IN_GAA(.(T79)) → APP38_IN_GAA(T79)
    The graph contains the following edges 1 > 1

(42) YES

(43) Obligation:

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

APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA

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

(44) UsableRulesProof (EQUIVALENT transformation)

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

(45) Obligation:

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

APP24_IN_AAAA(.(X107, X108), T40, X109, .(X107, T42)) → APP24_IN_AAAA(X108, T40, X109, T42)

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

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

(46) PiDPToQDPProof (SOUND transformation)

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

(47) Obligation:

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

APP24_IN_AAAA → APP24_IN_AAAA

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

(48) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = APP24_IN_AAAA evaluates to t =APP24_IN_AAAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APP24_IN_AAAA to APP24_IN_AAAA.



(49) NO

(50) Obligation:

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

PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

perm1_in_ag([], []) → perm1_out_ag([], [])
perm1_in_ag(.(T15, X25), .(T15, T9)) → U4_ag(T15, X25, T9, app14_in_aa(X25, X12))
app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
U4_ag(T15, X25, T9, app14_out_aa(X25, X12)) → perm1_out_ag(.(T15, X25), .(T15, T9))
perm1_in_ag(.(T15, T16), .(T15, T9)) → U5_ag(T15, T16, T9, app14_in_aa(T16, T17))
U5_ag(T15, T16, T9, app14_out_aa(T16, T17)) → U6_ag(T15, T16, T9, perm1_in_ag(T17, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U7_ag(X63, T24, T22, T9, app24_in_aaaa(X64, T22, X65, T24))
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U7_ag(X63, T24, T22, T9, app24_out_aaaa(X64, T22, X65, T24)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(X63, T24), .(T22, T9)) → U8_ag(X63, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U8_ag(X63, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U9_ag(X63, T24, T22, T9, app34_in_agaa(X63, T27, T28, X12))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
U9_ag(X63, T24, T22, T9, app34_out_agaa(X63, T27, T28, X12)) → perm1_out_ag(.(X63, T24), .(T22, T9))
perm1_in_ag(.(T47, T24), .(T22, T9)) → U10_ag(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_ag(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_ag(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_ag(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → U12_ag(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U12_ag(T47, T24, T22, T9, perm1_out_ag(T48, T9)) → perm1_out_ag(.(T47, T24), .(T22, T9))
U6_ag(T15, T16, T9, perm1_out_ag(T17, T9)) → perm1_out_ag(.(T15, T16), .(T15, T9))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
[]  =  []
perm1_out_ag(x1, x2)  =  perm1_out_ag(x2)
.(x1, x2)  =  .(x2)
U4_ag(x1, x2, x3, x4)  =  U4_ag(x3, x4)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
U5_ag(x1, x2, x3, x4)  =  U5_ag(x3, x4)
U6_ag(x1, x2, x3, x4)  =  U6_ag(x3, x4)
U7_ag(x1, x2, x3, x4, x5)  =  U7_ag(x4, x5)
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
U8_ag(x1, x2, x3, x4, x5)  =  U8_ag(x4, x5)
U9_ag(x1, x2, x3, x4, x5)  =  U9_ag(x4, x5)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
U10_ag(x1, x2, x3, x4, x5)  =  U10_ag(x4, x5)
U11_ag(x1, x2, x3, x4, x5)  =  U11_ag(x4, x5)
U12_ag(x1, x2, x3, x4, x5)  =  U12_ag(x4, x5)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)

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

(51) UsableRulesProof (EQUIVALENT transformation)

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

(52) Obligation:

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

PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U5_AG(T15, T16, T9, app14_in_aa(T16, T17))
U5_AG(T15, T16, T9, app14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U10_AG(T47, T24, T22, T9, app24_in_aaaa(T27, T22, T28, T24))
U10_AG(T47, T24, T22, T9, app24_out_aaaa(T27, T22, T28, T24)) → U11_AG(T47, T24, T22, T9, app34_in_agaa(T47, T27, T28, T48))
U11_AG(T47, T24, T22, T9, app34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

app14_in_aa(X40, X40) → app14_out_aa(X40, X40)
app24_in_aaaa([], T35, X87, .(T35, X87)) → app24_out_aaaa([], T35, X87, .(T35, X87))
app24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U1_aaaa(X107, X108, T40, X109, T42, app24_in_aaaa(X108, T40, X109, T42))
app34_in_agaa(X153, T61, T62, .(X153, X154)) → U3_agaa(X153, T61, T62, X154, app38_in_gaa(T61, T62, X154))
U1_aaaa(X107, X108, T40, X109, T42, app24_out_aaaa(X108, T40, X109, T42)) → app24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
U3_agaa(X153, T61, T62, X154, app38_out_gaa(T61, T62, X154)) → app34_out_agaa(X153, T61, T62, .(X153, X154))
app38_in_gaa([], T69, T69) → app38_out_gaa([], T69, T69)
app38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U2_gaa(T76, T79, T80, X177, app38_in_gaa(T79, T80, X177))
U2_gaa(T76, T79, T80, X177, app38_out_gaa(T79, T80, X177)) → app38_out_gaa(.(T76, T79), T80, .(T76, X177))

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x2)
app14_in_aa(x1, x2)  =  app14_in_aa
app14_out_aa(x1, x2)  =  app14_out_aa
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
app24_out_aaaa(x1, x2, x3, x4)  =  app24_out_aaaa(x1)
U1_aaaa(x1, x2, x3, x4, x5, x6)  =  U1_aaaa(x6)
app34_in_agaa(x1, x2, x3, x4)  =  app34_in_agaa(x2)
U3_agaa(x1, x2, x3, x4, x5)  =  U3_agaa(x2, x5)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
app38_out_gaa(x1, x2, x3)  =  app38_out_gaa(x1)
U2_gaa(x1, x2, x3, x4, x5)  =  U2_gaa(x2, x5)
app34_out_agaa(x1, x2, x3, x4)  =  app34_out_agaa(x2)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U5_AG(x1, x2, x3, x4)  =  U5_AG(x3, x4)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)
U11_AG(x1, x2, x3, x4, x5)  =  U11_AG(x4, x5)

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

PERM1_IN_AG(.(T9)) → U5_AG(T9, app14_in_aa)
U5_AG(T9, app14_out_aa) → PERM1_IN_AG(T9)
PERM1_IN_AG(.(T9)) → U10_AG(T9, app24_in_aaaa)
U10_AG(T9, app24_out_aaaa(T27)) → U11_AG(T9, app34_in_agaa(T27))
U11_AG(T9, app34_out_agaa(T27)) → PERM1_IN_AG(T9)

The TRS R consists of the following rules:

app14_in_aa → app14_out_aa
app24_in_aaaa → app24_out_aaaa([])
app24_in_aaaa → U1_aaaa(app24_in_aaaa)
app34_in_agaa(T61) → U3_agaa(T61, app38_in_gaa(T61))
U1_aaaa(app24_out_aaaa(X108)) → app24_out_aaaa(.(X108))
U3_agaa(T61, app38_out_gaa(T61)) → app34_out_agaa(T61)
app38_in_gaa([]) → app38_out_gaa([])
app38_in_gaa(.(T79)) → U2_gaa(T79, app38_in_gaa(T79))
U2_gaa(T79, app38_out_gaa(T79)) → app38_out_gaa(.(T79))

The set Q consists of the following terms:

app14_in_aa
app24_in_aaaa
app34_in_agaa(x0)
U1_aaaa(x0)
U3_agaa(x0, x1)
app38_in_gaa(x0)
U2_gaa(x0, x1)

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

(55) QDPSizeChangeProof (EQUIVALENT transformation)

By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:

  • U5_AG(T9, app14_out_aa) → PERM1_IN_AG(T9)
    The graph contains the following edges 1 >= 1

  • U11_AG(T9, app34_out_agaa(T27)) → PERM1_IN_AG(T9)
    The graph contains the following edges 1 >= 1

  • PERM1_IN_AG(.(T9)) → U5_AG(T9, app14_in_aa)
    The graph contains the following edges 1 > 1

  • PERM1_IN_AG(.(T9)) → U10_AG(T9, app24_in_aaaa)
    The graph contains the following edges 1 > 1

  • U10_AG(T9, app24_out_aaaa(T27)) → U11_AG(T9, app34_in_agaa(T27))
    The graph contains the following edges 1 >= 1

(56) YES