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 PrologToDTProblemTransformerProof (⇐)
↳2 TRIPLES
↳3 TriplesToPiDPProof (⇐)
↳4 PiDP
↳5 DependencyGraphProof (⇔)
↳6 AND
    ↳7 PiDP
        ↳8 UsableRulesProof (⇔)
        ↳9 PiDP
        ↳10 PiDPToQDPProof (⇐)
        ↳11 QDP
        ↳12 QDPSizeChangeProof (⇔)
        ↳13 YES
    ↳14 PiDP
        ↳15 UsableRulesProof (⇔)
        ↳16 PiDP
        ↳17 PiDPToQDPProof (⇐)
        ↳18 QDP
        ↳19 NonTerminationProof (⇔)
        ↳20 NO
    ↳21 PiDP
        ↳22 PiDPToQDPProof (⇐)
        ↳23 QDP
        ↳24 QDPSizeChangeProof (⇔)
        ↳25 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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

app24(.(X107, X108), T40, X109, .(X107, T42)) :- app24(X108, T40, X109, T42).
app38(.(T76, T79), T80, .(T76, X177)) :- app38(T79, T80, X177).
perm1(.(T15, T16), .(T15, T9)) :- ','(appc14(T16, T17), perm1(T17, T9)).
perm1(.(X63, T24), .(T22, T9)) :- app24(X64, T22, X65, T24).
perm1(.(X153, T24), .(T22, T9)) :- ','(appc24(T61, T22, T62, T24), app38(T61, T62, X154)).
perm1(.(T47, T24), .(T22, T9)) :- ','(appc24(T27, T22, T28, T24), ','(appc34(T47, T27, T28, T48), perm1(T48, T9))).

Clauses:

permc1([], []).
permc1(.(T15, T16), .(T15, T9)) :- ','(appc14(T16, T17), permc1(T17, T9)).
permc1(.(T47, T24), .(T22, T9)) :- ','(appc24(T27, T22, T28, T24), ','(appc34(T47, T27, T28, T48), permc1(T48, T9))).
appc24([], T35, X87, .(T35, X87)).
appc24(.(X107, X108), T40, X109, .(X107, T42)) :- appc24(X108, T40, X109, T42).
appc38([], T69, T69).
appc38(.(T76, T79), T80, .(T76, X177)) :- appc38(T79, T80, X177).
appc14(X40, X40).
appc34(X153, T61, T62, .(X153, X154)) :- appc38(T61, T62, X154).

Afs:

perm1(x1, x2)  =  perm1(x2)

(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: (f,b)
app24_in: (f,f,f,f)
appc24_in: (f,f,f,f)
app38_in: (b,f,f)
appc34_in: (f,b,f,f)
appc38_in: (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U3_AG(T15, T16, T9, appc14_in_aa(T16, T17))
U3_AG(T15, T16, T9, appc14_out_aa(T16, T17)) → U4_AG(T15, T16, T9, perm1_in_ag(T17, T9))
U3_AG(T15, T16, T9, appc14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U5_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(.(X153, T24), .(T22, T9)) → U6_AG(X153, T24, T22, T9, appc24_in_aaaa(T61, T22, T62, T24))
U6_AG(X153, T24, T22, T9, appc24_out_aaaa(T61, T22, T62, T24)) → U7_AG(X153, T24, T22, T9, app38_in_gaa(T61, T62, X154))
U6_AG(X153, T24, T22, T9, appc24_out_aaaa(T61, T22, T62, T24)) → 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)) → U8_AG(T47, T24, T22, T9, appc24_in_aaaa(T27, T22, T28, T24))
U8_AG(T47, T24, T22, T9, appc24_out_aaaa(T27, T22, T28, T24)) → U9_AG(T47, T24, T22, T9, appc34_in_agaa(T47, T27, T28, T48))
U9_AG(T47, T24, T22, T9, appc34_out_agaa(T47, T27, T28, T48)) → U10_AG(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U9_AG(T47, T24, T22, T9, appc34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

appc14_in_aa(X40, X40) → appc14_out_aa(X40, X40)
appc24_in_aaaa([], T35, X87, .(T35, X87)) → appc24_out_aaaa([], T35, X87, .(T35, X87))
appc24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U17_aaaa(X107, X108, T40, X109, T42, appc24_in_aaaa(X108, T40, X109, T42))
U17_aaaa(X107, X108, T40, X109, T42, appc24_out_aaaa(X108, T40, X109, T42)) → appc24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
appc34_in_agaa(X153, T61, T62, .(X153, X154)) → U19_agaa(X153, T61, T62, X154, appc38_in_gaa(T61, T62, X154))
appc38_in_gaa([], T69, T69) → appc38_out_gaa([], T69, T69)
appc38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U18_gaa(T76, T79, T80, X177, appc38_in_gaa(T79, T80, X177))
U18_gaa(T76, T79, T80, X177, appc38_out_gaa(T79, T80, X177)) → appc38_out_gaa(.(T76, T79), T80, .(T76, X177))
U19_agaa(X153, T61, T62, X154, appc38_out_gaa(T61, T62, X154)) → appc34_out_agaa(X153, T61, T62, .(X153, X154))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
.(x1, x2)  =  .(x2)
appc14_in_aa(x1, x2)  =  appc14_in_aa
appc14_out_aa(x1, x2)  =  appc14_out_aa
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
appc24_in_aaaa(x1, x2, x3, x4)  =  appc24_in_aaaa
appc24_out_aaaa(x1, x2, x3, x4)  =  appc24_out_aaaa(x1)
U17_aaaa(x1, x2, x3, x4, x5, x6)  =  U17_aaaa(x6)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
appc34_in_agaa(x1, x2, x3, x4)  =  appc34_in_agaa(x2)
U19_agaa(x1, x2, x3, x4, x5)  =  U19_agaa(x2, x5)
appc38_in_gaa(x1, x2, x3)  =  appc38_in_gaa(x1)
[]  =  []
appc38_out_gaa(x1, x2, x3)  =  appc38_out_gaa(x1)
U18_gaa(x1, x2, x3, x4, x5)  =  U18_gaa(x2, x5)
appc34_out_agaa(x1, x2, x3, x4)  =  appc34_out_agaa(x2)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x3, x4)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x3, x4)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x4, x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5, x6)  =  U1_AAAA(x6)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x4, x5)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x4, x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x2, x5)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x4, x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U3_AG(T15, T16, T9, appc14_in_aa(T16, T17))
U3_AG(T15, T16, T9, appc14_out_aa(T16, T17)) → U4_AG(T15, T16, T9, perm1_in_ag(T17, T9))
U3_AG(T15, T16, T9, appc14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(X63, T24), .(T22, T9)) → U5_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(.(X153, T24), .(T22, T9)) → U6_AG(X153, T24, T22, T9, appc24_in_aaaa(T61, T22, T62, T24))
U6_AG(X153, T24, T22, T9, appc24_out_aaaa(T61, T22, T62, T24)) → U7_AG(X153, T24, T22, T9, app38_in_gaa(T61, T62, X154))
U6_AG(X153, T24, T22, T9, appc24_out_aaaa(T61, T22, T62, T24)) → 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)) → U8_AG(T47, T24, T22, T9, appc24_in_aaaa(T27, T22, T28, T24))
U8_AG(T47, T24, T22, T9, appc24_out_aaaa(T27, T22, T28, T24)) → U9_AG(T47, T24, T22, T9, appc34_in_agaa(T47, T27, T28, T48))
U9_AG(T47, T24, T22, T9, appc34_out_agaa(T47, T27, T28, T48)) → U10_AG(T47, T24, T22, T9, perm1_in_ag(T48, T9))
U9_AG(T47, T24, T22, T9, appc34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

appc14_in_aa(X40, X40) → appc14_out_aa(X40, X40)
appc24_in_aaaa([], T35, X87, .(T35, X87)) → appc24_out_aaaa([], T35, X87, .(T35, X87))
appc24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U17_aaaa(X107, X108, T40, X109, T42, appc24_in_aaaa(X108, T40, X109, T42))
U17_aaaa(X107, X108, T40, X109, T42, appc24_out_aaaa(X108, T40, X109, T42)) → appc24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
appc34_in_agaa(X153, T61, T62, .(X153, X154)) → U19_agaa(X153, T61, T62, X154, appc38_in_gaa(T61, T62, X154))
appc38_in_gaa([], T69, T69) → appc38_out_gaa([], T69, T69)
appc38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U18_gaa(T76, T79, T80, X177, appc38_in_gaa(T79, T80, X177))
U18_gaa(T76, T79, T80, X177, appc38_out_gaa(T79, T80, X177)) → appc38_out_gaa(.(T76, T79), T80, .(T76, X177))
U19_agaa(X153, T61, T62, X154, appc38_out_gaa(T61, T62, X154)) → appc34_out_agaa(X153, T61, T62, .(X153, X154))

The argument filtering Pi contains the following mapping:
perm1_in_ag(x1, x2)  =  perm1_in_ag(x2)
.(x1, x2)  =  .(x2)
appc14_in_aa(x1, x2)  =  appc14_in_aa
appc14_out_aa(x1, x2)  =  appc14_out_aa
app24_in_aaaa(x1, x2, x3, x4)  =  app24_in_aaaa
appc24_in_aaaa(x1, x2, x3, x4)  =  appc24_in_aaaa
appc24_out_aaaa(x1, x2, x3, x4)  =  appc24_out_aaaa(x1)
U17_aaaa(x1, x2, x3, x4, x5, x6)  =  U17_aaaa(x6)
app38_in_gaa(x1, x2, x3)  =  app38_in_gaa(x1)
appc34_in_agaa(x1, x2, x3, x4)  =  appc34_in_agaa(x2)
U19_agaa(x1, x2, x3, x4, x5)  =  U19_agaa(x2, x5)
appc38_in_gaa(x1, x2, x3)  =  appc38_in_gaa(x1)
[]  =  []
appc38_out_gaa(x1, x2, x3)  =  appc38_out_gaa(x1)
U18_gaa(x1, x2, x3, x4, x5)  =  U18_gaa(x2, x5)
appc34_out_agaa(x1, x2, x3, x4)  =  appc34_out_agaa(x2)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x3, x4)
U4_AG(x1, x2, x3, x4)  =  U4_AG(x3, x4)
U5_AG(x1, x2, x3, x4, x5)  =  U5_AG(x4, x5)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA
U1_AAAA(x1, x2, x3, x4, x5, x6)  =  U1_AAAA(x6)
U6_AG(x1, x2, x3, x4, x5)  =  U6_AG(x4, x5)
U7_AG(x1, x2, x3, x4, x5)  =  U7_AG(x4, x5)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)
U2_GAA(x1, x2, x3, x4, x5)  =  U2_GAA(x2, x5)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x4, x5)
U10_AG(x1, x2, x3, x4, x5)  =  U10_AG(x4, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

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

appc14_in_aa(X40, X40) → appc14_out_aa(X40, X40)
appc24_in_aaaa([], T35, X87, .(T35, X87)) → appc24_out_aaaa([], T35, X87, .(T35, X87))
appc24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U17_aaaa(X107, X108, T40, X109, T42, appc24_in_aaaa(X108, T40, X109, T42))
U17_aaaa(X107, X108, T40, X109, T42, appc24_out_aaaa(X108, T40, X109, T42)) → appc24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
appc34_in_agaa(X153, T61, T62, .(X153, X154)) → U19_agaa(X153, T61, T62, X154, appc38_in_gaa(T61, T62, X154))
appc38_in_gaa([], T69, T69) → appc38_out_gaa([], T69, T69)
appc38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U18_gaa(T76, T79, T80, X177, appc38_in_gaa(T79, T80, X177))
U18_gaa(T76, T79, T80, X177, appc38_out_gaa(T79, T80, X177)) → appc38_out_gaa(.(T76, T79), T80, .(T76, X177))
U19_agaa(X153, T61, T62, X154, appc38_out_gaa(T61, T62, X154)) → appc34_out_agaa(X153, T61, T62, .(X153, X154))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
appc14_in_aa(x1, x2)  =  appc14_in_aa
appc14_out_aa(x1, x2)  =  appc14_out_aa
appc24_in_aaaa(x1, x2, x3, x4)  =  appc24_in_aaaa
appc24_out_aaaa(x1, x2, x3, x4)  =  appc24_out_aaaa(x1)
U17_aaaa(x1, x2, x3, x4, x5, x6)  =  U17_aaaa(x6)
appc34_in_agaa(x1, x2, x3, x4)  =  appc34_in_agaa(x2)
U19_agaa(x1, x2, x3, x4, x5)  =  U19_agaa(x2, x5)
appc38_in_gaa(x1, x2, x3)  =  appc38_in_gaa(x1)
[]  =  []
appc38_out_gaa(x1, x2, x3)  =  appc38_out_gaa(x1)
U18_gaa(x1, x2, x3, x4, x5)  =  U18_gaa(x2, x5)
appc34_out_agaa(x1, x2, x3, x4)  =  appc34_out_agaa(x2)
APP38_IN_GAA(x1, x2, x3)  =  APP38_IN_GAA(x1)

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:

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

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

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

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:

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

(13) YES

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

appc14_in_aa(X40, X40) → appc14_out_aa(X40, X40)
appc24_in_aaaa([], T35, X87, .(T35, X87)) → appc24_out_aaaa([], T35, X87, .(T35, X87))
appc24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U17_aaaa(X107, X108, T40, X109, T42, appc24_in_aaaa(X108, T40, X109, T42))
U17_aaaa(X107, X108, T40, X109, T42, appc24_out_aaaa(X108, T40, X109, T42)) → appc24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
appc34_in_agaa(X153, T61, T62, .(X153, X154)) → U19_agaa(X153, T61, T62, X154, appc38_in_gaa(T61, T62, X154))
appc38_in_gaa([], T69, T69) → appc38_out_gaa([], T69, T69)
appc38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U18_gaa(T76, T79, T80, X177, appc38_in_gaa(T79, T80, X177))
U18_gaa(T76, T79, T80, X177, appc38_out_gaa(T79, T80, X177)) → appc38_out_gaa(.(T76, T79), T80, .(T76, X177))
U19_agaa(X153, T61, T62, X154, appc38_out_gaa(T61, T62, X154)) → appc34_out_agaa(X153, T61, T62, .(X153, X154))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
appc14_in_aa(x1, x2)  =  appc14_in_aa
appc14_out_aa(x1, x2)  =  appc14_out_aa
appc24_in_aaaa(x1, x2, x3, x4)  =  appc24_in_aaaa
appc24_out_aaaa(x1, x2, x3, x4)  =  appc24_out_aaaa(x1)
U17_aaaa(x1, x2, x3, x4, x5, x6)  =  U17_aaaa(x6)
appc34_in_agaa(x1, x2, x3, x4)  =  appc34_in_agaa(x2)
U19_agaa(x1, x2, x3, x4, x5)  =  U19_agaa(x2, x5)
appc38_in_gaa(x1, x2, x3)  =  appc38_in_gaa(x1)
[]  =  []
appc38_out_gaa(x1, x2, x3)  =  appc38_out_gaa(x1)
U18_gaa(x1, x2, x3, x4, x5)  =  U18_gaa(x2, x5)
appc34_out_agaa(x1, x2, x3, x4)  =  appc34_out_agaa(x2)
APP24_IN_AAAA(x1, x2, x3, x4)  =  APP24_IN_AAAA

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:

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

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

APP24_IN_AAAA → APP24_IN_AAAA

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

(19) 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.



(20) NO

(21) Obligation:

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

U3_AG(T15, T16, T9, appc14_out_aa(T16, T17)) → PERM1_IN_AG(T17, T9)
PERM1_IN_AG(.(T15, T16), .(T15, T9)) → U3_AG(T15, T16, T9, appc14_in_aa(T16, T17))
PERM1_IN_AG(.(T47, T24), .(T22, T9)) → U8_AG(T47, T24, T22, T9, appc24_in_aaaa(T27, T22, T28, T24))
U8_AG(T47, T24, T22, T9, appc24_out_aaaa(T27, T22, T28, T24)) → U9_AG(T47, T24, T22, T9, appc34_in_agaa(T47, T27, T28, T48))
U9_AG(T47, T24, T22, T9, appc34_out_agaa(T47, T27, T28, T48)) → PERM1_IN_AG(T48, T9)

The TRS R consists of the following rules:

appc14_in_aa(X40, X40) → appc14_out_aa(X40, X40)
appc24_in_aaaa([], T35, X87, .(T35, X87)) → appc24_out_aaaa([], T35, X87, .(T35, X87))
appc24_in_aaaa(.(X107, X108), T40, X109, .(X107, T42)) → U17_aaaa(X107, X108, T40, X109, T42, appc24_in_aaaa(X108, T40, X109, T42))
U17_aaaa(X107, X108, T40, X109, T42, appc24_out_aaaa(X108, T40, X109, T42)) → appc24_out_aaaa(.(X107, X108), T40, X109, .(X107, T42))
appc34_in_agaa(X153, T61, T62, .(X153, X154)) → U19_agaa(X153, T61, T62, X154, appc38_in_gaa(T61, T62, X154))
appc38_in_gaa([], T69, T69) → appc38_out_gaa([], T69, T69)
appc38_in_gaa(.(T76, T79), T80, .(T76, X177)) → U18_gaa(T76, T79, T80, X177, appc38_in_gaa(T79, T80, X177))
U18_gaa(T76, T79, T80, X177, appc38_out_gaa(T79, T80, X177)) → appc38_out_gaa(.(T76, T79), T80, .(T76, X177))
U19_agaa(X153, T61, T62, X154, appc38_out_gaa(T61, T62, X154)) → appc34_out_agaa(X153, T61, T62, .(X153, X154))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x2)
appc14_in_aa(x1, x2)  =  appc14_in_aa
appc14_out_aa(x1, x2)  =  appc14_out_aa
appc24_in_aaaa(x1, x2, x3, x4)  =  appc24_in_aaaa
appc24_out_aaaa(x1, x2, x3, x4)  =  appc24_out_aaaa(x1)
U17_aaaa(x1, x2, x3, x4, x5, x6)  =  U17_aaaa(x6)
appc34_in_agaa(x1, x2, x3, x4)  =  appc34_in_agaa(x2)
U19_agaa(x1, x2, x3, x4, x5)  =  U19_agaa(x2, x5)
appc38_in_gaa(x1, x2, x3)  =  appc38_in_gaa(x1)
[]  =  []
appc38_out_gaa(x1, x2, x3)  =  appc38_out_gaa(x1)
U18_gaa(x1, x2, x3, x4, x5)  =  U18_gaa(x2, x5)
appc34_out_agaa(x1, x2, x3, x4)  =  appc34_out_agaa(x2)
PERM1_IN_AG(x1, x2)  =  PERM1_IN_AG(x2)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x3, x4)
U8_AG(x1, x2, x3, x4, x5)  =  U8_AG(x4, x5)
U9_AG(x1, x2, x3, x4, x5)  =  U9_AG(x4, x5)

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

(22) PiDPToQDPProof (SOUND transformation)

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

(23) Obligation:

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

U3_AG(T9, appc14_out_aa) → PERM1_IN_AG(T9)
PERM1_IN_AG(.(T9)) → U3_AG(T9, appc14_in_aa)
PERM1_IN_AG(.(T9)) → U8_AG(T9, appc24_in_aaaa)
U8_AG(T9, appc24_out_aaaa(T27)) → U9_AG(T9, appc34_in_agaa(T27))
U9_AG(T9, appc34_out_agaa(T27)) → PERM1_IN_AG(T9)

The TRS R consists of the following rules:

appc14_in_aa → appc14_out_aa
appc24_in_aaaa → appc24_out_aaaa([])
appc24_in_aaaa → U17_aaaa(appc24_in_aaaa)
U17_aaaa(appc24_out_aaaa(X108)) → appc24_out_aaaa(.(X108))
appc34_in_agaa(T61) → U19_agaa(T61, appc38_in_gaa(T61))
appc38_in_gaa([]) → appc38_out_gaa([])
appc38_in_gaa(.(T79)) → U18_gaa(T79, appc38_in_gaa(T79))
U18_gaa(T79, appc38_out_gaa(T79)) → appc38_out_gaa(.(T79))
U19_agaa(T61, appc38_out_gaa(T61)) → appc34_out_agaa(T61)

The set Q consists of the following terms:

appc14_in_aa
appc24_in_aaaa
U17_aaaa(x0)
appc34_in_agaa(x0)
appc38_in_gaa(x0)
U18_gaa(x0, x1)
U19_agaa(x0, x1)

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

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

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

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

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

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

  • U8_AG(T9, appc24_out_aaaa(T27)) → U9_AG(T9, appc34_in_agaa(T27))
    The graph contains the following edges 1 >= 1

(25) YES