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

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 QDPSizeChangeProof (⇔)
        ↳20 YES
    ↳21 PiDP
        ↳22 PiDPToQDPProof (⇐)
        ↳23 QDP
        ↳24 Rewriting (⇔)
        ↳25 QDP
        ↳26 UsableRulesProof (⇔)
        ↳27 QDP
        ↳28 QReductionProof (⇔)
        ↳29 QDP
        ↳30 Rewriting (⇔)
        ↳31 QDP
        ↳32 UsableRulesProof (⇔)
        ↳33 QDP
        ↳34 QReductionProof (⇔)
        ↳35 QDP
        ↳36 Instantiation (⇔)
        ↳37 QDP
        ↳38 QDPOrderProof (⇔)
        ↳39 QDP
        ↳40 DependencyGraphProof (⇔)
        ↳41 QDP
        ↳42 QDPOrderProof (⇔)
        ↳43 QDP
        ↳44 DependencyGraphProof (⇔)
        ↳45 TRUE

(0) Obligation:

Clauses:

append(nil, XS, XS).
append(cons(X, XS1), XS2, cons(X, YS)) :- append(XS1, XS2, YS).
split(XS, nil, XS).
split(cons(X, XS), cons(X, YS1), YS2) :- split(XS, YS1, YS2).
perm(nil, nil).
perm(XS, cons(Y, YS)) :- ','(split(XS, YS1, cons(Y, YS2)), ','(append(YS1, YS2, ZS), perm(ZS, YS))).

Queries:

perm(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

split28(cons(T88, T89), cons(T88, X95), T91, X96) :- split28(T89, X95, T91, X96).
append42(cons(T129, T130), T131, cons(T129, X157)) :- append42(T130, T131, X157).
perm1(cons(T30, T31), cons(T30, T32)) :- ','(appendc18(T31, T34), perm1(T34, T32)).
perm1(cons(T47, T48), cons(T50, T51)) :- split28(T48, X63, T50, X64).
perm1(cons(T113, T48), cons(T50, T60)) :- ','(splitc28(T48, T114, T50, T115), append42(T114, T115, X134)).
perm1(cons(T47, T48), cons(T50, T60)) :- ','(splitc28(T48, T58, T50, T59), ','(appendc38(T47, T58, T59, T101), perm1(T101, T60))).

Clauses:

permc1(nil, nil).
permc1(cons(T30, T31), cons(T30, T32)) :- ','(appendc18(T31, T34), permc1(T34, T32)).
permc1(cons(T47, T48), cons(T50, T60)) :- ','(splitc28(T48, T58, T50, T59), ','(appendc38(T47, T58, T59, T101), permc1(T101, T60))).
splitc28(cons(T80, T81), nil, T80, T81).
splitc28(cons(T88, T89), cons(T88, X95), T91, X96) :- splitc28(T89, X95, T91, X96).
appendc42(nil, T122, T122).
appendc42(cons(T129, T130), T131, cons(T129, X157)) :- appendc42(T130, T131, X157).
appendc18(T40, T40).
appendc38(T113, T114, T115, cons(T113, X134)) :- appendc42(T114, T115, X134).

Afs:

perm1(x1, x2)  =  perm1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
perm1_in: (b,f)
split28_in: (b,f,f,f)
splitc28_in: (b,f,f,f)
append42_in: (b,b,f)
appendc38_in: (b,b,b,f)
appendc42_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

PERM1_IN_GA(cons(T30, T31), cons(T30, T32)) → U3_GA(T30, T31, T32, appendc18_in_ga(T31, T34))
U3_GA(T30, T31, T32, appendc18_out_ga(T31, T34)) → U4_GA(T30, T31, T32, perm1_in_ga(T34, T32))
U3_GA(T30, T31, T32, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34, T32)
PERM1_IN_GA(cons(T47, T48), cons(T50, T51)) → U5_GA(T47, T48, T50, T51, split28_in_gaaa(T48, X63, T50, X64))
PERM1_IN_GA(cons(T47, T48), cons(T50, T51)) → SPLIT28_IN_GAAA(T48, X63, T50, X64)
SPLIT28_IN_GAAA(cons(T88, T89), cons(T88, X95), T91, X96) → U1_GAAA(T88, T89, X95, T91, X96, split28_in_gaaa(T89, X95, T91, X96))
SPLIT28_IN_GAAA(cons(T88, T89), cons(T88, X95), T91, X96) → SPLIT28_IN_GAAA(T89, X95, T91, X96)
PERM1_IN_GA(cons(T113, T48), cons(T50, T60)) → U6_GA(T113, T48, T50, T60, splitc28_in_gaaa(T48, T114, T50, T115))
U6_GA(T113, T48, T50, T60, splitc28_out_gaaa(T48, T114, T50, T115)) → U7_GA(T113, T48, T50, T60, append42_in_gga(T114, T115, X134))
U6_GA(T113, T48, T50, T60, splitc28_out_gaaa(T48, T114, T50, T115)) → APPEND42_IN_GGA(T114, T115, X134)
APPEND42_IN_GGA(cons(T129, T130), T131, cons(T129, X157)) → U2_GGA(T129, T130, T131, X157, append42_in_gga(T130, T131, X157))
APPEND42_IN_GGA(cons(T129, T130), T131, cons(T129, X157)) → APPEND42_IN_GGA(T130, T131, X157)
PERM1_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitc28_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, T50, T60, appendc38_in_ggga(T47, T58, T59, T101))
U9_GA(T47, T48, T50, T60, appendc38_out_ggga(T47, T58, T59, T101)) → U10_GA(T47, T48, T50, T60, perm1_in_ga(T101, T60))
U9_GA(T47, T48, T50, T60, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101, T60)

The TRS R consists of the following rules:

appendc18_in_ga(T40, T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81), nil, T80, T81) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89), cons(T88, X95), T91, X96) → U17_gaaa(T88, T89, X95, T91, X96, splitc28_in_gaaa(T89, X95, T91, X96))
U17_gaaa(T88, T89, X95, T91, X96, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115, cons(T113, X134)) → U19_ggga(T113, T114, T115, X134, appendc42_in_gga(T114, T115, X134))
appendc42_in_gga(nil, T122, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131, cons(T129, X157)) → U18_gga(T129, T130, T131, X157, appendc42_in_gga(T130, T131, X157))
U18_gga(T129, T130, T131, X157, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, X134, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The argument filtering Pi contains the following mapping:
perm1_in_ga(x1, x2)  =  perm1_in_ga(x1)
cons(x1, x2)  =  cons(x1, x2)
appendc18_in_ga(x1, x2)  =  appendc18_in_ga(x1)
appendc18_out_ga(x1, x2)  =  appendc18_out_ga(x1, x2)
split28_in_gaaa(x1, x2, x3, x4)  =  split28_in_gaaa(x1)
splitc28_in_gaaa(x1, x2, x3, x4)  =  splitc28_in_gaaa(x1)
splitc28_out_gaaa(x1, x2, x3, x4)  =  splitc28_out_gaaa(x1, x2, x3, x4)
U17_gaaa(x1, x2, x3, x4, x5, x6)  =  U17_gaaa(x1, x2, x6)
append42_in_gga(x1, x2, x3)  =  append42_in_gga(x1, x2)
appendc38_in_ggga(x1, x2, x3, x4)  =  appendc38_in_ggga(x1, x2, x3)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x1, x2, x3, x5)
appendc42_in_gga(x1, x2, x3)  =  appendc42_in_gga(x1, x2)
nil  =  nil
appendc42_out_gga(x1, x2, x3)  =  appendc42_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
appendc38_out_ggga(x1, x2, x3, x4)  =  appendc38_out_ggga(x1, x2, x3, x4)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x5)
SPLIT28_IN_GAAA(x1, x2, x3, x4)  =  SPLIT28_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5, x6)  =  U1_GAAA(x1, x2, x6)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x5)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x5)
APPEND42_IN_GGA(x1, x2, x3)  =  APPEND42_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

PERM1_IN_GA(cons(T30, T31), cons(T30, T32)) → U3_GA(T30, T31, T32, appendc18_in_ga(T31, T34))
U3_GA(T30, T31, T32, appendc18_out_ga(T31, T34)) → U4_GA(T30, T31, T32, perm1_in_ga(T34, T32))
U3_GA(T30, T31, T32, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34, T32)
PERM1_IN_GA(cons(T47, T48), cons(T50, T51)) → U5_GA(T47, T48, T50, T51, split28_in_gaaa(T48, X63, T50, X64))
PERM1_IN_GA(cons(T47, T48), cons(T50, T51)) → SPLIT28_IN_GAAA(T48, X63, T50, X64)
SPLIT28_IN_GAAA(cons(T88, T89), cons(T88, X95), T91, X96) → U1_GAAA(T88, T89, X95, T91, X96, split28_in_gaaa(T89, X95, T91, X96))
SPLIT28_IN_GAAA(cons(T88, T89), cons(T88, X95), T91, X96) → SPLIT28_IN_GAAA(T89, X95, T91, X96)
PERM1_IN_GA(cons(T113, T48), cons(T50, T60)) → U6_GA(T113, T48, T50, T60, splitc28_in_gaaa(T48, T114, T50, T115))
U6_GA(T113, T48, T50, T60, splitc28_out_gaaa(T48, T114, T50, T115)) → U7_GA(T113, T48, T50, T60, append42_in_gga(T114, T115, X134))
U6_GA(T113, T48, T50, T60, splitc28_out_gaaa(T48, T114, T50, T115)) → APPEND42_IN_GGA(T114, T115, X134)
APPEND42_IN_GGA(cons(T129, T130), T131, cons(T129, X157)) → U2_GGA(T129, T130, T131, X157, append42_in_gga(T130, T131, X157))
APPEND42_IN_GGA(cons(T129, T130), T131, cons(T129, X157)) → APPEND42_IN_GGA(T130, T131, X157)
PERM1_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitc28_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, T50, T60, appendc38_in_ggga(T47, T58, T59, T101))
U9_GA(T47, T48, T50, T60, appendc38_out_ggga(T47, T58, T59, T101)) → U10_GA(T47, T48, T50, T60, perm1_in_ga(T101, T60))
U9_GA(T47, T48, T50, T60, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101, T60)

The TRS R consists of the following rules:

appendc18_in_ga(T40, T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81), nil, T80, T81) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89), cons(T88, X95), T91, X96) → U17_gaaa(T88, T89, X95, T91, X96, splitc28_in_gaaa(T89, X95, T91, X96))
U17_gaaa(T88, T89, X95, T91, X96, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115, cons(T113, X134)) → U19_ggga(T113, T114, T115, X134, appendc42_in_gga(T114, T115, X134))
appendc42_in_gga(nil, T122, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131, cons(T129, X157)) → U18_gga(T129, T130, T131, X157, appendc42_in_gga(T130, T131, X157))
U18_gga(T129, T130, T131, X157, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, X134, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The argument filtering Pi contains the following mapping:
perm1_in_ga(x1, x2)  =  perm1_in_ga(x1)
cons(x1, x2)  =  cons(x1, x2)
appendc18_in_ga(x1, x2)  =  appendc18_in_ga(x1)
appendc18_out_ga(x1, x2)  =  appendc18_out_ga(x1, x2)
split28_in_gaaa(x1, x2, x3, x4)  =  split28_in_gaaa(x1)
splitc28_in_gaaa(x1, x2, x3, x4)  =  splitc28_in_gaaa(x1)
splitc28_out_gaaa(x1, x2, x3, x4)  =  splitc28_out_gaaa(x1, x2, x3, x4)
U17_gaaa(x1, x2, x3, x4, x5, x6)  =  U17_gaaa(x1, x2, x6)
append42_in_gga(x1, x2, x3)  =  append42_in_gga(x1, x2)
appendc38_in_ggga(x1, x2, x3, x4)  =  appendc38_in_ggga(x1, x2, x3)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x1, x2, x3, x5)
appendc42_in_gga(x1, x2, x3)  =  appendc42_in_gga(x1, x2)
nil  =  nil
appendc42_out_gga(x1, x2, x3)  =  appendc42_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
appendc38_out_ggga(x1, x2, x3, x4)  =  appendc38_out_ggga(x1, x2, x3, x4)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x5)
SPLIT28_IN_GAAA(x1, x2, x3, x4)  =  SPLIT28_IN_GAAA(x1)
U1_GAAA(x1, x2, x3, x4, x5, x6)  =  U1_GAAA(x1, x2, x6)
U6_GA(x1, x2, x3, x4, x5)  =  U6_GA(x1, x2, x5)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x5)
APPEND42_IN_GGA(x1, x2, x3)  =  APPEND42_IN_GGA(x1, x2)
U2_GGA(x1, x2, x3, x4, x5)  =  U2_GGA(x1, x2, x3, x5)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, x5)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x5)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APPEND42_IN_GGA(cons(T129, T130), T131, cons(T129, X157)) → APPEND42_IN_GGA(T130, T131, X157)

The TRS R consists of the following rules:

appendc18_in_ga(T40, T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81), nil, T80, T81) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89), cons(T88, X95), T91, X96) → U17_gaaa(T88, T89, X95, T91, X96, splitc28_in_gaaa(T89, X95, T91, X96))
U17_gaaa(T88, T89, X95, T91, X96, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115, cons(T113, X134)) → U19_ggga(T113, T114, T115, X134, appendc42_in_gga(T114, T115, X134))
appendc42_in_gga(nil, T122, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131, cons(T129, X157)) → U18_gga(T129, T130, T131, X157, appendc42_in_gga(T130, T131, X157))
U18_gga(T129, T130, T131, X157, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, X134, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
appendc18_in_ga(x1, x2)  =  appendc18_in_ga(x1)
appendc18_out_ga(x1, x2)  =  appendc18_out_ga(x1, x2)
splitc28_in_gaaa(x1, x2, x3, x4)  =  splitc28_in_gaaa(x1)
splitc28_out_gaaa(x1, x2, x3, x4)  =  splitc28_out_gaaa(x1, x2, x3, x4)
U17_gaaa(x1, x2, x3, x4, x5, x6)  =  U17_gaaa(x1, x2, x6)
appendc38_in_ggga(x1, x2, x3, x4)  =  appendc38_in_ggga(x1, x2, x3)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x1, x2, x3, x5)
appendc42_in_gga(x1, x2, x3)  =  appendc42_in_gga(x1, x2)
nil  =  nil
appendc42_out_gga(x1, x2, x3)  =  appendc42_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
appendc38_out_ggga(x1, x2, x3, x4)  =  appendc38_out_ggga(x1, x2, x3, x4)
APPEND42_IN_GGA(x1, x2, x3)  =  APPEND42_IN_GGA(x1, x2)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APPEND42_IN_GGA(cons(T129, T130), T131, cons(T129, X157)) → APPEND42_IN_GGA(T130, T131, X157)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APPEND42_IN_GGA(cons(T129, T130), T131) → APPEND42_IN_GGA(T130, T131)

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:

  • APPEND42_IN_GGA(cons(T129, T130), T131) → APPEND42_IN_GGA(T130, T131)
    The graph contains the following edges 1 > 1, 2 >= 2

(13) YES

(14) Obligation:

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

SPLIT28_IN_GAAA(cons(T88, T89), cons(T88, X95), T91, X96) → SPLIT28_IN_GAAA(T89, X95, T91, X96)

The TRS R consists of the following rules:

appendc18_in_ga(T40, T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81), nil, T80, T81) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89), cons(T88, X95), T91, X96) → U17_gaaa(T88, T89, X95, T91, X96, splitc28_in_gaaa(T89, X95, T91, X96))
U17_gaaa(T88, T89, X95, T91, X96, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115, cons(T113, X134)) → U19_ggga(T113, T114, T115, X134, appendc42_in_gga(T114, T115, X134))
appendc42_in_gga(nil, T122, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131, cons(T129, X157)) → U18_gga(T129, T130, T131, X157, appendc42_in_gga(T130, T131, X157))
U18_gga(T129, T130, T131, X157, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, X134, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
appendc18_in_ga(x1, x2)  =  appendc18_in_ga(x1)
appendc18_out_ga(x1, x2)  =  appendc18_out_ga(x1, x2)
splitc28_in_gaaa(x1, x2, x3, x4)  =  splitc28_in_gaaa(x1)
splitc28_out_gaaa(x1, x2, x3, x4)  =  splitc28_out_gaaa(x1, x2, x3, x4)
U17_gaaa(x1, x2, x3, x4, x5, x6)  =  U17_gaaa(x1, x2, x6)
appendc38_in_ggga(x1, x2, x3, x4)  =  appendc38_in_ggga(x1, x2, x3)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x1, x2, x3, x5)
appendc42_in_gga(x1, x2, x3)  =  appendc42_in_gga(x1, x2)
nil  =  nil
appendc42_out_gga(x1, x2, x3)  =  appendc42_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
appendc38_out_ggga(x1, x2, x3, x4)  =  appendc38_out_ggga(x1, x2, x3, x4)
SPLIT28_IN_GAAA(x1, x2, x3, x4)  =  SPLIT28_IN_GAAA(x1)

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:

SPLIT28_IN_GAAA(cons(T88, T89), cons(T88, X95), T91, X96) → SPLIT28_IN_GAAA(T89, X95, T91, X96)

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

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:

SPLIT28_IN_GAAA(cons(T88, T89)) → SPLIT28_IN_GAAA(T89)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • SPLIT28_IN_GAAA(cons(T88, T89)) → SPLIT28_IN_GAAA(T89)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

U3_GA(T30, T31, T32, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34, T32)
PERM1_IN_GA(cons(T30, T31), cons(T30, T32)) → U3_GA(T30, T31, T32, appendc18_in_ga(T31, T34))
PERM1_IN_GA(cons(T47, T48), cons(T50, T60)) → U8_GA(T47, T48, T50, T60, splitc28_in_gaaa(T48, T58, T50, T59))
U8_GA(T47, T48, T50, T60, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, T50, T60, appendc38_in_ggga(T47, T58, T59, T101))
U9_GA(T47, T48, T50, T60, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101, T60)

The TRS R consists of the following rules:

appendc18_in_ga(T40, T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81), nil, T80, T81) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89), cons(T88, X95), T91, X96) → U17_gaaa(T88, T89, X95, T91, X96, splitc28_in_gaaa(T89, X95, T91, X96))
U17_gaaa(T88, T89, X95, T91, X96, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115, cons(T113, X134)) → U19_ggga(T113, T114, T115, X134, appendc42_in_gga(T114, T115, X134))
appendc42_in_gga(nil, T122, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131, cons(T129, X157)) → U18_gga(T129, T130, T131, X157, appendc42_in_gga(T130, T131, X157))
U18_gga(T129, T130, T131, X157, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, X134, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The argument filtering Pi contains the following mapping:
cons(x1, x2)  =  cons(x1, x2)
appendc18_in_ga(x1, x2)  =  appendc18_in_ga(x1)
appendc18_out_ga(x1, x2)  =  appendc18_out_ga(x1, x2)
splitc28_in_gaaa(x1, x2, x3, x4)  =  splitc28_in_gaaa(x1)
splitc28_out_gaaa(x1, x2, x3, x4)  =  splitc28_out_gaaa(x1, x2, x3, x4)
U17_gaaa(x1, x2, x3, x4, x5, x6)  =  U17_gaaa(x1, x2, x6)
appendc38_in_ggga(x1, x2, x3, x4)  =  appendc38_in_ggga(x1, x2, x3)
U19_ggga(x1, x2, x3, x4, x5)  =  U19_ggga(x1, x2, x3, x5)
appendc42_in_gga(x1, x2, x3)  =  appendc42_in_gga(x1, x2)
nil  =  nil
appendc42_out_gga(x1, x2, x3)  =  appendc42_out_gga(x1, x2, x3)
U18_gga(x1, x2, x3, x4, x5)  =  U18_gga(x1, x2, x3, x5)
appendc38_out_ggga(x1, x2, x3, x4)  =  appendc38_out_ggga(x1, x2, x3, x4)
PERM1_IN_GA(x1, x2)  =  PERM1_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)
U8_GA(x1, x2, x3, x4, x5)  =  U8_GA(x1, x2, x5)
U9_GA(x1, x2, x3, x4, x5)  =  U9_GA(x1, x2, 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_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_in_ga(T31))
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, appendc38_in_ggga(T47, T58, T59))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)

The TRS R consists of the following rules:

appendc18_in_ga(T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115) → U19_ggga(T113, T114, T115, appendc42_in_gga(T114, T115))
appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The set Q consists of the following terms:

appendc18_in_ga(x0)
splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc38_in_ggga(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(24) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_in_ga(T31)) at position [2] we obtained the following new rules [LPAR04]:

PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))

(25) Obligation:

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

U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, appendc38_in_ggga(T47, T58, T59))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))

The TRS R consists of the following rules:

appendc18_in_ga(T40) → appendc18_out_ga(T40, T40)
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)
appendc38_in_ggga(T113, T114, T115) → U19_ggga(T113, T114, T115, appendc42_in_gga(T114, T115))
appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))

The set Q consists of the following terms:

appendc18_in_ga(x0)
splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc38_in_ggga(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(26) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(27) Obligation:

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

U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, appendc38_in_ggga(T47, T58, T59))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))

The TRS R consists of the following rules:

appendc38_in_ggga(T113, T114, T115) → U19_ggga(T113, T114, T115, appendc42_in_gga(T114, T115))
appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

appendc18_in_ga(x0)
splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc38_in_ggga(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(28) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appendc18_in_ga(x0)

(29) Obligation:

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

U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, appendc38_in_ggga(T47, T58, T59))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))

The TRS R consists of the following rules:

appendc38_in_ggga(T113, T114, T115) → U19_ggga(T113, T114, T115, appendc42_in_gga(T114, T115))
appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc38_in_ggga(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(30) Rewriting (EQUIVALENT transformation)

By rewriting [LPAR04] the rule U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, appendc38_in_ggga(T47, T58, T59)) at position [2] we obtained the following new rules [LPAR04]:

U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))

(31) Obligation:

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

U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendc38_in_ggga(T113, T114, T115) → U19_ggga(T113, T114, T115, appendc42_in_gga(T114, T115))
appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc38_in_ggga(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(32) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(33) Obligation:

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

U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc38_in_ggga(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(34) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

appendc38_in_ggga(x0, x1, x2)

(35) Obligation:

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

U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(36) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U3_GA(T30, T31, appendc18_out_ga(T31, T34)) → PERM1_IN_GA(T34) we obtained the following new rules [LPAR04]:

U3_GA(z0, z1, appendc18_out_ga(z1, z1)) → PERM1_IN_GA(z1)

(37) Obligation:

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

PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))
U3_GA(z0, z1, appendc18_out_ga(z1, z1)) → PERM1_IN_GA(z1)

The TRS R consists of the following rules:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(38) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U3_GA(z0, z1, appendc18_out_ga(z1, z1)) → PERM1_IN_GA(z1)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(PERM1_IN_GA(x1)) = 0 +
[0,1]
·x1

POL(cons(x1, x2)) =
/0\
\1/
 +
/00\
\00/
·x1 +
/00\
\01/
·x2

POL(U8_GA(x1, x2, x3)) = 1 +
[0,0]
·x1 +
[0,0]
·x2 +
[1,0]
·x3

POL(splitc28_in_gaaa(x1)) =
/0\
\0/
 +
/01\
\00/
·x1

POL(U9_GA(x1, x2, x3)) = 0 +
[0,0]
·x1 +
[0,0]
·x2 +
[0,1]
·x3

POL(appendc38_out_ggga(x1, x2, x3, x4)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\00/
·x3 +
/00\
\01/
·x4

POL(U3_GA(x1, x2, x3)) = 1 +
[0,0]
·x1 +
[0,1]
·x2 +
[0,0]
·x3

POL(appendc18_out_ga(x1, x2)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2

POL(splitc28_out_gaaa(x1, x2, x3, x4)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/01\
\00/
·x2 +
/00\
\00/
·x3 +
/01\
\00/
·x4

POL(U19_ggga(x1, x2, x3, x4)) =
/0\
\1/
 +
/10\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\00/
·x3 +
/10\
\10/
·x4

POL(appendc42_in_gga(x1, x2)) =
/0\
\0/
 +
/01\
\00/
·x1 +
/01\
\10/
·x2

POL(nil) =
/0\
\0/

POL(U17_gaaa(x1, x2, x3)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/10\
\00/
·x3

POL(appendc42_out_gga(x1, x2, x3)) =
/0\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/01\
\00/
·x3

POL(U18_gga(x1, x2, x3, x4)) =
/1\
\0/
 +
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\00/
·x3 +
/10\
\00/
·x4

The following usable rules [FROCOS05] were oriented:

splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

(39) Obligation:

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

PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T30, T31)) → U3_GA(T30, T31, appendc18_out_ga(T31, T31))
U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))

The TRS R consists of the following rules:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(40) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.

(41) Obligation:

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

U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)
PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))

The TRS R consists of the following rules:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(42) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


PERM1_IN_GA(cons(T47, T48)) → U8_GA(T47, T48, splitc28_in_gaaa(T48))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO]:

POL(PERM1_IN_GA(x1)) = x1   
POL(U17_gaaa(x1, x2, x3)) = 1 + x3   
POL(U18_gga(x1, x2, x3, x4)) = 1 + x4   
POL(U19_ggga(x1, x2, x3, x4)) = x4   
POL(U8_GA(x1, x2, x3)) = x3   
POL(U9_GA(x1, x2, x3)) = x3   
POL(appendc38_out_ggga(x1, x2, x3, x4)) = x4   
POL(appendc42_in_gga(x1, x2)) = x1 + x2   
POL(appendc42_out_gga(x1, x2, x3)) = 1 + x3   
POL(cons(x1, x2)) = 1 + x2   
POL(nil) = 1   
POL(splitc28_in_gaaa(x1)) = x1   
POL(splitc28_out_gaaa(x1, x2, x3, x4)) = x2 + x4   

The following usable rules [FROCOS05] were oriented:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

(43) Obligation:

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

U8_GA(T47, T48, splitc28_out_gaaa(T48, T58, T50, T59)) → U9_GA(T47, T48, U19_ggga(T47, T58, T59, appendc42_in_gga(T58, T59)))
U9_GA(T47, T48, appendc38_out_ggga(T47, T58, T59, T101)) → PERM1_IN_GA(T101)

The TRS R consists of the following rules:

appendc42_in_gga(nil, T122) → appendc42_out_gga(nil, T122, T122)
appendc42_in_gga(cons(T129, T130), T131) → U18_gga(T129, T130, T131, appendc42_in_gga(T130, T131))
U19_ggga(T113, T114, T115, appendc42_out_gga(T114, T115, X134)) → appendc38_out_ggga(T113, T114, T115, cons(T113, X134))
U18_gga(T129, T130, T131, appendc42_out_gga(T130, T131, X157)) → appendc42_out_gga(cons(T129, T130), T131, cons(T129, X157))
splitc28_in_gaaa(cons(T80, T81)) → splitc28_out_gaaa(cons(T80, T81), nil, T80, T81)
splitc28_in_gaaa(cons(T88, T89)) → U17_gaaa(T88, T89, splitc28_in_gaaa(T89))
U17_gaaa(T88, T89, splitc28_out_gaaa(T89, X95, T91, X96)) → splitc28_out_gaaa(cons(T88, T89), cons(T88, X95), T91, X96)

The set Q consists of the following terms:

splitc28_in_gaaa(x0)
U17_gaaa(x0, x1, x2)
appendc42_in_gga(x0, x1)
U18_gga(x0, x1, x2, x3)
U19_ggga(x0, x1, x2, x3)

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

(44) DependencyGraphProof (EQUIVALENT transformation)

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

(45) TRUE