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 PrologToPrologProblemTransformerProof (⇐)
↳2 Prolog
↳3 PrologToPiTRSProof (⇐)
↳4 PiTRS
↳5 DependencyPairsProof (⇔)
↳6 PiDP
↳7 DependencyGraphProof (⇔)
↳8 AND
    ↳9 PiDP
        ↳10 UsableRulesProof (⇔)
        ↳11 PiDP
        ↳12 PiDPToQDPProof (⇐)
        ↳13 QDP
        ↳14 QDPSizeChangeProof (⇔)
        ↳15 YES
    ↳16 PiDP
        ↳17 UsableRulesProof (⇔)
        ↳18 PiDP
        ↳19 PiDPToQDPProof (⇐)
        ↳20 QDP
        ↳21 QDPSizeChangeProof (⇔)
        ↳22 YES
    ↳23 PiDP
        ↳24 UsableRulesProof (⇔)
        ↳25 PiDP
        ↳26 PiDPToQDPProof (⇐)
        ↳27 QDP
        ↳28 QDPSizeChangeProof (⇔)
        ↳29 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) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

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

Queries:

rotate1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

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

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

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, append9_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append10_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, append9_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:

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)
ROTATE1_IN_GA(x1, x2)  =  ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x4)
APPEND9_IN_AAG(x1, x2, x3)  =  APPEND9_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(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, x6)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
APPEND26_IN_GA(x1, x2)  =  APPEND26_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)

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

(6) 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, append9_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append10_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, append9_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:

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)
ROTATE1_IN_GA(x1, x2)  =  ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x4)
APPEND9_IN_AAG(x1, x2, x3)  =  APPEND9_IN_AAG(x3)
U1_AAG(x1, x2, x3, x4, x5)  =  U1_AAG(x1, x5)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U6_GA(x1, x2, x3, x4)  =  U6_GA(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, x6)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
APPEND26_IN_GA(x1, x2)  =  APPEND26_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

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

The TRS R consists of the following rules:

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)
APPEND26_IN_GA(x1, x2)  =  APPEND26_IN_GA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

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

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(15) YES

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

The TRS R consists of the following rules:

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)
APPEND10_IN_GGGA(x1, x2, x3, x4)  =  APPEND10_IN_GGGA(x1, x2, x3)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

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.

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

(22) YES

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

The TRS R consists of the following rules:

rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append9_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append9_out_aag(X93, X94, T21)) → append9_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append9_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append9_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append9_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append10_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append10_out_ggga(T47, X141, T48, T50)) → append10_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append10_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append26_out_ga([], [])
U3_ga(T79, T80, T82, append26_out_ga(T80, T82)) → append26_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append26_out_ga(T63, T7)) → rotate1_out_ga(T63, T7)

The argument filtering Pi contains the following mapping:
rotate1_in_ga(x1, x2)  =  rotate1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
U4_ga(x1, x2, x3, x4)  =  U4_ga(x4)
append9_in_aag(x1, x2, x3)  =  append9_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5)  =  U1_aag(x1, x5)
append9_out_aag(x1, x2, x3)  =  append9_out_aag(x1, x2)
rotate1_out_ga(x1, x2)  =  rotate1_out_ga
U5_ga(x1, x2, x3, x4)  =  U5_ga(x1, x4)
U6_ga(x1, x2, x3, x4)  =  U6_ga(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, x6)
[]  =  []
append10_out_ggga(x1, x2, x3, x4)  =  append10_out_ggga(x4)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
append26_in_ga(x1, x2)  =  append26_in_ga(x1)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x1, x4)
append26_out_ga(x1, x2)  =  append26_out_ga(x2)
APPEND9_IN_AAG(x1, x2, x3)  =  APPEND9_IN_AAG(x3)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

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

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(29) YES