Left Termination of the query pattern rotate_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 UsableRulesProof (⇔)
        ↳23 PiDP
        ↳24 PiDPToQDPProof (⇐)
        ↳25 QDP
        ↳26 QDPSizeChangeProof (⇔)
        ↳27 YES

(0) Obligation:

Clauses:

rotate(X, Y) :- ','(append(A, B, X), append(B, A, Y)).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).
append([], Ys, Ys).

Queries:

rotate(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

append9(.(X92, X93), X94, .(X92, T21)) :- append9(X93, X94, T21).
append10(.(T46, T47), X141, T48, .(T46, T50)) :- append10(T47, X141, T48, T50).
append26(.(T79, T80), .(T79, T82)) :- append26(T80, T82).
rotate1(.(X39, T12), T7) :- append9(X40, X41, T12).
rotate1(.(X39, T12), T7) :- ','(appendc9(T14, T15, T12), append10(T15, X39, T14, T7)).
rotate1(T63, T7) :- append26(T63, T7).

Clauses:

appendc9(.(X92, X93), X94, .(X92, T21)) :- appendc9(X93, X94, T21).
appendc9([], T25, T25).
appendc10(.(T46, T47), X141, T48, .(T46, T50)) :- appendc10(T47, X141, T48, T50).
appendc10([], X156, T57, .(X156, T57)).
appendc26(.(T79, T80), .(T79, T82)) :- appendc26(T80, T82).
appendc26([], []).

Afs:

rotate1(x1, x2)  =  rotate1(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:
rotate1_in: (b,f)
append9_in: (f,f,b)
appendc9_in: (f,f,b)
append10_in: (b,b,b,f)
append26_in: (b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

ROTATE1_IN_GA(.(X39, T12), T7) → U4_GA(X39, T12, T7, append9_in_aag(X40, X41, T12))
ROTATE1_IN_GA(.(X39, T12), T7) → APPEND9_IN_AAG(X40, X41, T12)
APPEND9_IN_AAG(.(X92, X93), X94, .(X92, T21)) → U1_AAG(X92, X93, X94, T21, append9_in_aag(X93, X94, T21))
APPEND9_IN_AAG(.(X92, X93), X94, .(X92, T21)) → APPEND9_IN_AAG(X93, X94, T21)
ROTATE1_IN_GA(.(X39, T12), T7) → U5_GA(X39, T12, T7, appendc9_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, appendc9_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append10_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, appendc9_out_aag(T14, T15, T12)) → APPEND10_IN_GGGA(T15, X39, T14, T7)
APPEND10_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → U2_GGGA(T46, T47, X141, T48, T50, append10_in_ggga(T47, X141, T48, T50))
APPEND10_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND10_IN_GGGA(T47, X141, T48, T50)
ROTATE1_IN_GA(T63, T7) → U7_GA(T63, T7, append26_in_ga(T63, T7))
ROTATE1_IN_GA(T63, T7) → APPEND26_IN_GA(T63, T7)
APPEND26_IN_GA(.(T79, T80), .(T79, T82)) → U3_GA(T79, T80, T82, append26_in_ga(T80, T82))
APPEND26_IN_GA(.(T79, T80), .(T79, T82)) → APPEND26_IN_GA(T80, T82)

The TRS R consists of the following rules:

appendc9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, appendc9_in_aag(X93, X94, T21))
appendc9_in_aag([], T25, T25) → appendc9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, appendc9_out_aag(X93, X94, T21)) → appendc9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
appendc9_in_aag(x1, x2, x3)  =  appendc9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
appendc9_out_aag(x1, x2, x3)  =  appendc9_out_aag(x1, x2, x3)
append10_in_ggga(x1, x2, x3, x4)  =  append10_in_ggga(x1, x2, x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
ROTATE1_IN_GA(x1, x2)  =  ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
APPEND9_IN_AAG(x1, x2, x3)  =  APPEND9_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x4, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
APPEND10_IN_GGGA(x1, x2, x3, x4)  =  APPEND10_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGA(x1, x2, x3, x4, x6)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
APPEND26_IN_GA(x1, x2)  =  APPEND26_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

ROTATE1_IN_GA(.(X39, T12), T7) → U4_GA(X39, T12, T7, append9_in_aag(X40, X41, T12))
ROTATE1_IN_GA(.(X39, T12), T7) → APPEND9_IN_AAG(X40, X41, T12)
APPEND9_IN_AAG(.(X92, X93), X94, .(X92, T21)) → U1_AAG(X92, X93, X94, T21, append9_in_aag(X93, X94, T21))
APPEND9_IN_AAG(.(X92, X93), X94, .(X92, T21)) → APPEND9_IN_AAG(X93, X94, T21)
ROTATE1_IN_GA(.(X39, T12), T7) → U5_GA(X39, T12, T7, appendc9_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, appendc9_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append10_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, appendc9_out_aag(T14, T15, T12)) → APPEND10_IN_GGGA(T15, X39, T14, T7)
APPEND10_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → U2_GGGA(T46, T47, X141, T48, T50, append10_in_ggga(T47, X141, T48, T50))
APPEND10_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND10_IN_GGGA(T47, X141, T48, T50)
ROTATE1_IN_GA(T63, T7) → U7_GA(T63, T7, append26_in_ga(T63, T7))
ROTATE1_IN_GA(T63, T7) → APPEND26_IN_GA(T63, T7)
APPEND26_IN_GA(.(T79, T80), .(T79, T82)) → U3_GA(T79, T80, T82, append26_in_ga(T80, T82))
APPEND26_IN_GA(.(T79, T80), .(T79, T82)) → APPEND26_IN_GA(T80, T82)

The TRS R consists of the following rules:

appendc9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, appendc9_in_aag(X93, X94, T21))
appendc9_in_aag([], T25, T25) → appendc9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, appendc9_out_aag(X93, X94, T21)) → appendc9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
appendc9_in_aag(x1, x2, x3)  =  appendc9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
appendc9_out_aag(x1, x2, x3)  =  appendc9_out_aag(x1, x2, x3)
append10_in_ggga(x1, x2, x3, x4)  =  append10_in_ggga(x1, x2, x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
ROTATE1_IN_GA(x1, x2)  =  ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
APPEND9_IN_AAG(x1, x2, x3)  =  APPEND9_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x4, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x2, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(x1, x2, x4)
APPEND10_IN_GGGA(x1, x2, x3, x4)  =  APPEND10_IN_GGGA(x1, x2, x3)
U2_GGGA(x1, x2, x3, x4, x5, x6)  =  U2_GGGA(x1, x2, x3, x4, x6)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
APPEND26_IN_GA(x1, x2)  =  APPEND26_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x2, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APPEND26_IN_GA(.(T79, T80), .(T79, T82)) → APPEND26_IN_GA(T80, T82)

The TRS R consists of the following rules:

appendc9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, appendc9_in_aag(X93, X94, T21))
appendc9_in_aag([], T25, T25) → appendc9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, appendc9_out_aag(X93, X94, T21)) → appendc9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appendc9_in_aag(x1, x2, x3)  =  appendc9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
appendc9_out_aag(x1, x2, x3)  =  appendc9_out_aag(x1, x2, x3)
APPEND26_IN_GA(x1, x2)  =  APPEND26_IN_GA(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:

APPEND26_IN_GA(.(T79, T80), .(T79, T82)) → APPEND26_IN_GA(T80, T82)

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

APPEND26_IN_GA(.(T79, T80)) → APPEND26_IN_GA(T80)

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:

  • APPEND26_IN_GA(.(T79, T80)) → APPEND26_IN_GA(T80)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

APPEND10_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND10_IN_GGGA(T47, X141, T48, T50)

The TRS R consists of the following rules:

appendc9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, appendc9_in_aag(X93, X94, T21))
appendc9_in_aag([], T25, T25) → appendc9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, appendc9_out_aag(X93, X94, T21)) → appendc9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appendc9_in_aag(x1, x2, x3)  =  appendc9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
appendc9_out_aag(x1, x2, x3)  =  appendc9_out_aag(x1, x2, x3)
APPEND10_IN_GGGA(x1, x2, x3, x4)  =  APPEND10_IN_GGGA(x1, x2, x3)

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:

APPEND10_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND10_IN_GGGA(T47, X141, T48, T50)

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

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:

APPEND10_IN_GGGA(.(T46, T47), X141, T48) → APPEND10_IN_GGGA(T47, X141, T48)

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:

  • APPEND10_IN_GGGA(.(T46, T47), X141, T48) → APPEND10_IN_GGGA(T47, X141, T48)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(20) YES

(21) Obligation:

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

APPEND9_IN_AAG(.(X92, X93), X94, .(X92, T21)) → APPEND9_IN_AAG(X93, X94, T21)

The TRS R consists of the following rules:

appendc9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, appendc9_in_aag(X93, X94, T21))
appendc9_in_aag([], T25, T25) → appendc9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, appendc9_out_aag(X93, X94, T21)) → appendc9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
appendc9_in_aag(x1, x2, x3)  =  appendc9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
appendc9_out_aag(x1, x2, x3)  =  appendc9_out_aag(x1, x2, x3)
APPEND9_IN_AAG(x1, x2, x3)  =  APPEND9_IN_AAG(x3)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

APPEND9_IN_AAG(.(X92, X93), X94, .(X92, T21)) → APPEND9_IN_AAG(X93, X94, T21)

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

APPEND9_IN_AAG(.(X92, T21)) → APPEND9_IN_AAG(T21)

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

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

  • APPEND9_IN_AAG(.(X92, T21)) → APPEND9_IN_AAG(T21)
    The graph contains the following edges 1 > 1

(27) YES