(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) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:append29(.(X92, X93), X94, .(X92, T21)) :- append29(X93, X94, T21).
append29([], T25, T25).
append110(.(T46, T47), X141, T48, .(T46, T50)) :- append110(T47, X141, T48, T50).
append110([], X156, T57, .(X156, T57)).
append126(.(T79, T80), .(T79, T82)) :- append126(T80, T82).
append126([], []).
rotate1(.(X39, T12), T7) :- append29(X40, X41, T12).
rotate1(.(X39, T12), T7) :- ','(append29(T14, T15, T12), append110(T15, X39, T14, T7)).
rotate1(T63, T7) :- append126(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)
append29_in: (f,f,b)
append110_in: (b,b,b,f)
append126_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, 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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_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, 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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_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, 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, append29_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append110_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, append29_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:
rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_out_ga(x2)
ROTATE1_IN_GA(x1, x2) = ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4) = U4_GA(x4)
APPEND29_IN_AAG(x1, x2, x3) = APPEND29_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)
APPEND110_IN_GGGA(x1, x2, x3, x4) = APPEND110_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)
APPEND126_IN_GA(x1, x2) = APPEND126_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, 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, append29_in_aag(T14, T15, T12))
U5_GA(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_GA(X39, T12, T7, append110_in_ggga(T15, X39, T14, T7))
U5_GA(X39, T12, T7, append29_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:
rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_out_ga(x2)
ROTATE1_IN_GA(x1, x2) = ROTATE1_IN_GA(x1)
U4_GA(x1, x2, x3, x4) = U4_GA(x4)
APPEND29_IN_AAG(x1, x2, x3) = APPEND29_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)
APPEND110_IN_GGGA(x1, x2, x3, x4) = APPEND110_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)
APPEND126_IN_GA(x1, x2) = APPEND126_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:
APPEND126_IN_GA(.(T79, T80), .(T79, T82)) → APPEND126_IN_GA(T80, T82)
The TRS R consists of the following rules:
rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_out_ga(x2)
APPEND126_IN_GA(x1, x2) = APPEND126_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:
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
(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:
APPEND126_IN_GA(.(T79, T80)) → APPEND126_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:
- APPEND126_IN_GA(.(T79, T80)) → APPEND126_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:
APPEND110_IN_GGGA(.(T46, T47), X141, T48, .(T46, T50)) → APPEND110_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, 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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_out_ga(x2)
APPEND110_IN_GGGA(x1, x2, x3, x4) = APPEND110_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:
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
(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:
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.
(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:
- 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
(22) YES
(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)
The TRS R consists of the following rules:
rotate1_in_ga(.(X39, T12), T7) → U4_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([], T25, T25) → append29_out_aag([], T25, T25)
U1_aag(X92, X93, X94, T21, append29_out_aag(X93, X94, T21)) → append29_out_aag(.(X92, X93), X94, .(X92, T21))
U4_ga(X39, T12, T7, append29_out_aag(X40, X41, T12)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(.(X39, T12), T7) → U5_ga(X39, T12, T7, append29_in_aag(T14, T15, T12))
U5_ga(X39, T12, T7, append29_out_aag(T14, T15, T12)) → U6_ga(X39, T12, T7, 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([], X156, T57, .(X156, T57)) → append110_out_ggga([], X156, T57, .(X156, T57))
U2_ggga(T46, T47, X141, T48, T50, append110_out_ggga(T47, X141, T48, T50)) → append110_out_ggga(.(T46, T47), X141, T48, .(T46, T50))
U6_ga(X39, T12, T7, append110_out_ggga(T15, X39, T14, T7)) → rotate1_out_ga(.(X39, T12), T7)
rotate1_in_ga(T63, T7) → U7_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([], []) → append126_out_ga([], [])
U3_ga(T79, T80, T82, append126_out_ga(T80, T82)) → append126_out_ga(.(T79, T80), .(T79, T82))
U7_ga(T63, T7, append126_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)
append29_in_aag(x1, x2, x3) = append29_in_aag(x3)
U1_aag(x1, x2, x3, x4, x5) = U1_aag(x1, x5)
append29_out_aag(x1, x2, x3) = append29_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)
append110_in_ggga(x1, x2, x3, x4) = append110_in_ggga(x1, x2, x3)
U2_ggga(x1, x2, x3, x4, x5, x6) = U2_ggga(x1, x6)
[] = []
append110_out_ggga(x1, x2, x3, x4) = append110_out_ggga(x4)
U7_ga(x1, x2, x3) = U7_ga(x3)
append126_in_ga(x1, x2) = append126_in_ga(x1)
U3_ga(x1, x2, x3, x4) = U3_ga(x1, x4)
append126_out_ga(x1, x2) = append126_out_ga(x2)
APPEND29_IN_AAG(x1, x2, x3) = APPEND29_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:
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
(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:
APPEND29_IN_AAG(.(X92, T21)) → APPEND29_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:
- APPEND29_IN_AAG(.(X92, T21)) → APPEND29_IN_AAG(T21)
The graph contains the following edges 1 > 1