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) :- ','(append2(A, B, X), append1(B, A, Y)).
append1(.(X, Xs), Ys, .(X, Zs)) :- append1(Xs, Ys, Zs).
append1([], Ys, Ys).
append2(.(X, Xs), Ys, .(X, Zs)) :- append2(Xs, Ys, Zs).
append2([], Ys, Ys).

Queries:

rotate(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

append29(.(X92, X93), X94, .(X92, T21)) :- append29(X93, X94, T21).
append110(.(T46, T47), X141, T48, .(T46, T50)) :- append110(T47, X141, T48, T50).
append126(.(T79, T80), .(T79, T82)) :- append126(T80, T82).
rotate1(.(X39, T12), T7) :- append29(X40, X41, T12).
rotate1(.(X39, T12), T7) :- ','(append2c9(T14, T15, T12), append110(T15, X39, T14, T7)).
rotate1(T63, T7) :- append126(T63, T7).

Clauses:

append2c9(.(X92, X93), X94, .(X92, T21)) :- append2c9(X93, X94, T21).
append2c9([], T25, T25).
append1c10(.(T46, T47), X141, T48, .(T46, T50)) :- append1c10(T47, X141, T48, T50).
append1c10([], X156, T57, .(X156, T57)).
append1c26(.(T79, T80), .(T79, T82)) :- append1c26(T80, T82).
append1c26([], []).

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)
append29_in: (f,f,b)
append2c9_in: (f,f,b)
append110_in: (b,b,b,f)
append126_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, append29_in_aag(X40, X41, T12))
ROTATE1_IN_GA(.(X39, T12), T7) → APPEND29_IN_AAG(X40, X41, T12)
APPEND29_IN_AAG(.(X92, X93), X94, .(X92, T21)) → U1_AAG(X92, X93, X94, T21, append29_in_aag(X93, X94, T21))
APPEND29_IN_AAG(.(X92, X93), X94, .(X92, T21)) → APPEND29_IN_AAG(X93, X94, T21)
ROTATE1_IN_GA(.(X39, T12), T7) → U5_GA(X39, T12, T7, append2c9_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, append2c9_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append110_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, append2c9_out_aag(T14, T15, T12)) → APPEND110_IN_GGGA(T15, X39, T14, T7)
APPEND110_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → U2_GGGA(T46, T47, X141, T48, T50, append110_in_ggga(T47, X141, T48, T50))
APPEND110_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND110_IN_GGGA(T47, X141, T48, T50)
ROTATE1_IN_GA(T63, T7) → U7_GA(T63, T7, append126_in_ga(T63, T7))
ROTATE1_IN_GA(T63, T7) → APPEND126_IN_GA(T63, T7)
APPEND126_IN_GA(.(T79, T80), .(T79, T82)) → U3_GA(T79, T80, T82, append126_in_ga(T80, T82))
APPEND126_IN_GA(.(T79, T80), .(T79, T82)) → APPEND126_IN_GA(T80, T82)

The TRS R consists of the following rules:

append2c9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, append2c9_in_aag(X93, X94, T21))
append2c9_in_aag([], T25, T25) → append2c9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, append2c9_out_aag(X93, X94, T21)) → append2c9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append29_in_aag(x1, x2, x3)  =  append29_in_aag(x3)
append2c9_in_aag(x1, x2, x3)  =  append2c9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2c9_out_aag(x1, x2, x3)  =  append2c9_out_aag(x1, x2, x3)
append110_in_ggga(x1, x2, x3, x4)  =  append110_in_ggga(x1, x2, x3)
append126_in_ga(x1, x2)  =  append126_in_ga(x1)
ROTATE1_IN_GA(x1, x2)  =  ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
APPEND29_IN_AAG(x1, x2, x3)  =  APPEND29_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)
APPEND110_IN_GGGA(x1, x2, x3, x4)  =  APPEND110_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)
APPEND126_IN_GA(x1, x2)  =  APPEND126_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, append29_in_aag(X40, X41, T12))
ROTATE1_IN_GA(.(X39, T12), T7) → APPEND29_IN_AAG(X40, X41, T12)
APPEND29_IN_AAG(.(X92, X93), X94, .(X92, T21)) → U1_AAG(X92, X93, X94, T21, append29_in_aag(X93, X94, T21))
APPEND29_IN_AAG(.(X92, X93), X94, .(X92, T21)) → APPEND29_IN_AAG(X93, X94, T21)
ROTATE1_IN_GA(.(X39, T12), T7) → U5_GA(X39, T12, T7, append2c9_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, append2c9_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append110_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, append2c9_out_aag(T14, T15, T12)) → APPEND110_IN_GGGA(T15, X39, T14, T7)
APPEND110_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → U2_GGGA(T46, T47, X141, T48, T50, append110_in_ggga(T47, X141, T48, T50))
APPEND110_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND110_IN_GGGA(T47, X141, T48, T50)
ROTATE1_IN_GA(T63, T7) → U7_GA(T63, T7, append126_in_ga(T63, T7))
ROTATE1_IN_GA(T63, T7) → APPEND126_IN_GA(T63, T7)
APPEND126_IN_GA(.(T79, T80), .(T79, T82)) → U3_GA(T79, T80, T82, append126_in_ga(T80, T82))
APPEND126_IN_GA(.(T79, T80), .(T79, T82)) → APPEND126_IN_GA(T80, T82)

The TRS R consists of the following rules:

append2c9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, append2c9_in_aag(X93, X94, T21))
append2c9_in_aag([], T25, T25) → append2c9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, append2c9_out_aag(X93, X94, T21)) → append2c9_out_aag(.(X92, X93), X94, .(X92, T21))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
append29_in_aag(x1, x2, x3)  =  append29_in_aag(x3)
append2c9_in_aag(x1, x2, x3)  =  append2c9_in_aag(x3)
U9_aag(x1, x2, x3, x4, x5)  =  U9_aag(x1, x4, x5)
append2c9_out_aag(x1, x2, x3)  =  append2c9_out_aag(x1, x2, x3)
append110_in_ggga(x1, x2, x3, x4)  =  append110_in_ggga(x1, x2, x3)
append126_in_ga(x1, x2)  =  append126_in_ga(x1)
ROTATE1_IN_GA(x1, x2)  =  ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x2, x4)
APPEND29_IN_AAG(x1, x2, x3)  =  APPEND29_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)
APPEND110_IN_GGGA(x1, x2, x3, x4)  =  APPEND110_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)
APPEND126_IN_GA(x1, x2)  =  APPEND126_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:

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

The TRS R consists of the following rules:

append2c9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, append2c9_in_aag(X93, X94, T21))
append2c9_in_aag([], T25, T25) → append2c9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, append2c9_out_aag(X93, X94, T21)) → append2c9_out_aag(.(X92, X93), X94, .(X92, T21))

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

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

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

APPEND126_IN_GA(.(T79, T80)) → APPEND126_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:

  • APPEND126_IN_GA(.(T79, T80)) → APPEND126_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:

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

The TRS R consists of the following rules:

append2c9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, append2c9_in_aag(X93, X94, T21))
append2c9_in_aag([], T25, T25) → append2c9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, append2c9_out_aag(X93, X94, T21)) → append2c9_out_aag(.(X92, X93), X94, .(X92, T21))

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

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

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

APPEND110_IN_GGGA(.(T46, T47), X141, T48) → APPEND110_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:

  • APPEND110_IN_GGGA(.(T46, T47), X141, T48) → APPEND110_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:

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

The TRS R consists of the following rules:

append2c9_in_aag(.(X92, X93), X94, .(X92, T21)) → U9_aag(X92, X93, X94, T21, append2c9_in_aag(X93, X94, T21))
append2c9_in_aag([], T25, T25) → append2c9_out_aag([], T25, T25)
U9_aag(X92, X93, X94, T21, append2c9_out_aag(X93, X94, T21)) → append2c9_out_aag(.(X92, X93), X94, .(X92, T21))

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

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

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

APPEND29_IN_AAG(.(X92, T21)) → APPEND29_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:

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

(27) YES