Left Termination of the query pattern query_in_1(g) w.r.t. the given Prolog program could not be shown:

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 NonTerminationProof (⇔)
                ↳22 NO
            ↳23 PiDP
                ↳24 UsableRulesProof (⇔)
                ↳25 PiDP
                ↳26 PiDPToQDPProof (⇐)
                ↳27 QDP
                ↳28 NonTerminationProof (⇔)
                ↳29 NO
            ↳30 PiDP
                ↳31 UsableRulesProof (⇔)
                ↳32 PiDP
                ↳33 PiDPToQDPProof (⇐)
                ↳34 QDP
                ↳35 Narrowing (⇐)
                ↳36 QDP
                ↳37 NonTerminationProof (⇔)
                ↳38 NO
            ↳39 PiDP
                ↳40 UsableRulesProof (⇔)
                ↳41 PiDP
                ↳42 PiDPToQDPProof (⇐)
                ↳43 QDP
                ↳44 QDPSizeChangeProof (⇔)
                ↳45 YES
    ↳46 PrologToPiTRSProof (⇐)
        ↳47 PiTRS
        ↳48 DependencyPairsProof (⇔)
        ↳49 PiDP
        ↳50 DependencyGraphProof (⇔)
        ↳51 AND
            ↳52 PiDP
                ↳53 UsableRulesProof (⇔)
                ↳54 PiDP
                ↳55 PiDPToQDPProof (⇐)
                ↳56 QDP
                ↳57 QDPSizeChangeProof (⇔)
                ↳58 YES
            ↳59 PiDP
                ↳60 UsableRulesProof (⇔)
                ↳61 PiDP
                ↳62 PiDPToQDPProof (⇐)
                ↳63 QDP
                ↳64 NonTerminationProof (⇔)
                ↳65 NO
            ↳66 PiDP
                ↳67 UsableRulesProof (⇔)
                ↳68 PiDP
                ↳69 PiDPToQDPProof (⇐)
                ↳70 QDP
                ↳71 NonTerminationProof (⇔)
                ↳72 NO
            ↳73 PiDP
                ↳74 UsableRulesProof (⇔)
                ↳75 PiDP
                ↳76 PiDPToQDPProof (⇐)
                ↳77 QDP
                ↳78 Narrowing (⇐)
                ↳79 QDP
                ↳80 NonTerminationProof (⇔)
                ↳81 NO
            ↳82 PiDP
                ↳83 UsableRulesProof (⇔)
                ↳84 PiDP
                ↳85 PiDPToQDPProof (⇐)
                ↳86 QDP
                ↳87 QDPSizeChangeProof (⇔)
                ↳88 YES

(0) Obligation:

Clauses:

append(nil, XS, XS).
append(cons(X, XS), YS, cons(X, ZS)) :- append(XS, YS, ZS).
reverse(nil, nil).
reverse(cons(X, nil), cons(X, nil)).
reverse(cons(X, XS), YS) :- ','(reverse(XS, ZS), append(ZS, cons(X, nil), YS)).
shuffle(nil, nil).
shuffle(cons(X, XS), cons(X, YS)) :- ','(reverse(XS, ZS), shuffle(ZS, YS)).
query(XS) :- shuffle(cons(X, XS), YS).

Queries:

query(g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

reverse7(nil, nil).
reverse7(cons(T12, nil), cons(T12, nil)).
reverse7(cons(T17, T18), X41) :- reverse7(T18, X40).
reverse7(cons(T17, T18), X41) :- ','(reverse7(T18, T19), append23(T19, T17, X41)).
append23(nil, T26, cons(T26, nil)).
append23(cons(T33, T34), T35, cons(T33, X67)) :- append23(T34, T35, X67).
p6(T6, X19, X21) :- reverse7(T6, X19).
p6(T6, nil, nil) :- reverse7(T6, nil).
p6(T6, cons(T42, T43), cons(T42, X87)) :- ','(reverse7(T6, cons(T42, T43)), p6(T43, X86, X87)).
query1(T6) :- p6(T6, X19, X21).

Queries:

query1(g).

(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:
query1_in: (b)
p6_in: (b,f,f) (f,f,f)
reverse7_in: (b,f) (b,b) (f,f) (f,b)
append23_in: (f,f,f) (f,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)

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

QUERY1_IN_G(T6) → U9_G(T6, p6_in_gaa(T6, X19, X21))
QUERY1_IN_G(T6) → P6_IN_GAA(T6, X19, X21)
P6_IN_GAA(T6, X19, X21) → U5_GAA(T6, X19, X21, reverse7_in_ga(T6, X19))
P6_IN_GAA(T6, X19, X21) → REVERSE7_IN_GA(T6, X19)
REVERSE7_IN_GA(cons(T17, T18), X41) → U1_GA(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GA(cons(T17, T18), X41) → U2_GA(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → U4_AAA(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)
P6_IN_GAA(T6, nil, nil) → U6_GAA(T6, reverse7_in_gg(T6, nil))
P6_IN_GAA(T6, nil, nil) → REVERSE7_IN_GG(T6, nil)
REVERSE7_IN_GG(cons(T17, T18), X41) → U1_GG(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GG(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GG(cons(T17, T18), X41) → U2_GG(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → U4_AAG(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → U7_GAA(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_GA(T6, cons(T42, T43))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_GAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)
P6_IN_AAA(T6, X19, X21) → U5_AAA(T6, X19, X21, reverse7_in_aa(T6, X19))
P6_IN_AAA(T6, X19, X21) → REVERSE7_IN_AA(T6, X19)
REVERSE7_IN_AA(cons(T17, T18), X41) → U1_AA(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AA(cons(T17, T18), X41) → U2_AA(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
P6_IN_AAA(T6, nil, nil) → U6_AAA(T6, reverse7_in_ag(T6, nil))
P6_IN_AAA(T6, nil, nil) → REVERSE7_IN_AG(T6, nil)
REVERSE7_IN_AG(cons(T17, T18), X41) → U1_AG(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AG(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AG(cons(T17, T18), X41) → U2_AG(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_AA(T6, cons(T42, T43))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_AAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
QUERY1_IN_G(x1)  =  QUERY1_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x1, x2)
P6_IN_GAA(x1, x2, x3)  =  P6_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
REVERSE7_IN_GA(x1, x2)  =  REVERSE7_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x2, x4)
APPEND23_IN_AAA(x1, x2, x3)  =  APPEND23_IN_AAA
U4_AAA(x1, x2, x3, x4, x5)  =  U4_AAA(x5)
U6_GAA(x1, x2)  =  U6_GAA(x1, x2)
REVERSE7_IN_GG(x1, x2)  =  REVERSE7_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x2, x3, x4)
U2_GG(x1, x2, x3, x4)  =  U2_GG(x2, x3, x4)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x2, x3, x4)
APPEND23_IN_AAG(x1, x2, x3)  =  APPEND23_IN_AAG(x3)
U4_AAG(x1, x2, x3, x4, x5)  =  U4_AAG(x4, x5)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x1, x5)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x1, x5)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
REVERSE7_IN_AA(x1, x2)  =  REVERSE7_IN_AA
U1_AA(x1, x2, x3, x4)  =  U1_AA(x4)
U2_AA(x1, x2, x3, x4)  =  U2_AA(x4)
U3_AA(x1, x2, x3, x4)  =  U3_AA(x2, x4)
U6_AAA(x1, x2)  =  U6_AAA(x2)
REVERSE7_IN_AG(x1, x2)  =  REVERSE7_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x3, x4)
U2_AG(x1, x2, x3, x4)  =  U2_AG(x3, x4)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x2, x3, x4)
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x1, x5)

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

(6) Obligation:

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

QUERY1_IN_G(T6) → U9_G(T6, p6_in_gaa(T6, X19, X21))
QUERY1_IN_G(T6) → P6_IN_GAA(T6, X19, X21)
P6_IN_GAA(T6, X19, X21) → U5_GAA(T6, X19, X21, reverse7_in_ga(T6, X19))
P6_IN_GAA(T6, X19, X21) → REVERSE7_IN_GA(T6, X19)
REVERSE7_IN_GA(cons(T17, T18), X41) → U1_GA(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GA(cons(T17, T18), X41) → U2_GA(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → U4_AAA(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)
P6_IN_GAA(T6, nil, nil) → U6_GAA(T6, reverse7_in_gg(T6, nil))
P6_IN_GAA(T6, nil, nil) → REVERSE7_IN_GG(T6, nil)
REVERSE7_IN_GG(cons(T17, T18), X41) → U1_GG(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GG(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GG(cons(T17, T18), X41) → U2_GG(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → U4_AAG(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → U7_GAA(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_GA(T6, cons(T42, T43))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_GAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)
P6_IN_AAA(T6, X19, X21) → U5_AAA(T6, X19, X21, reverse7_in_aa(T6, X19))
P6_IN_AAA(T6, X19, X21) → REVERSE7_IN_AA(T6, X19)
REVERSE7_IN_AA(cons(T17, T18), X41) → U1_AA(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AA(cons(T17, T18), X41) → U2_AA(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
P6_IN_AAA(T6, nil, nil) → U6_AAA(T6, reverse7_in_ag(T6, nil))
P6_IN_AAA(T6, nil, nil) → REVERSE7_IN_AG(T6, nil)
REVERSE7_IN_AG(cons(T17, T18), X41) → U1_AG(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AG(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AG(cons(T17, T18), X41) → U2_AG(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_AA(T6, cons(T42, T43))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_AAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
QUERY1_IN_G(x1)  =  QUERY1_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x1, x2)
P6_IN_GAA(x1, x2, x3)  =  P6_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
REVERSE7_IN_GA(x1, x2)  =  REVERSE7_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x2, x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x2, x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x2, x4)
APPEND23_IN_AAA(x1, x2, x3)  =  APPEND23_IN_AAA
U4_AAA(x1, x2, x3, x4, x5)  =  U4_AAA(x5)
U6_GAA(x1, x2)  =  U6_GAA(x1, x2)
REVERSE7_IN_GG(x1, x2)  =  REVERSE7_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x2, x3, x4)
U2_GG(x1, x2, x3, x4)  =  U2_GG(x2, x3, x4)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x2, x3, x4)
APPEND23_IN_AAG(x1, x2, x3)  =  APPEND23_IN_AAG(x3)
U4_AAG(x1, x2, x3, x4, x5)  =  U4_AAG(x4, x5)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x1, x5)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x1, x5)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
REVERSE7_IN_AA(x1, x2)  =  REVERSE7_IN_AA
U1_AA(x1, x2, x3, x4)  =  U1_AA(x4)
U2_AA(x1, x2, x3, x4)  =  U2_AA(x4)
U3_AA(x1, x2, x3, x4)  =  U3_AA(x2, x4)
U6_AAA(x1, x2)  =  U6_AAA(x2)
REVERSE7_IN_AG(x1, x2)  =  REVERSE7_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x3, x4)
U2_AG(x1, x2, x3, x4)  =  U2_AG(x3, x4)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x2, x3, x4)
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x1, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 36 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
APPEND23_IN_AAG(x1, x2, x3)  =  APPEND23_IN_AAG(x3)

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:

APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)

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

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:

APPEND23_IN_AAG(cons(X67)) → APPEND23_IN_AAG(X67)

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:

  • APPEND23_IN_AAG(cons(X67)) → APPEND23_IN_AAG(X67)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
APPEND23_IN_AAA(x1, x2, x3)  =  APPEND23_IN_AAA

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:

APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)

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

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:

APPEND23_IN_AAA → APPEND23_IN_AAA

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

(21) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = APPEND23_IN_AAA evaluates to t =APPEND23_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APPEND23_IN_AAA to APPEND23_IN_AAA.



(22) NO

(23) Obligation:

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

REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
REVERSE7_IN_AA(x1, x2)  =  REVERSE7_IN_AA

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:

REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)

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

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:

REVERSE7_IN_AA → REVERSE7_IN_AA

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

(28) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = REVERSE7_IN_AA evaluates to t =REVERSE7_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE7_IN_AA to REVERSE7_IN_AA.



(29) NO

(30) Obligation:

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

P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))

The argument filtering Pi contains the following mapping:
nil  =  nil
cons(x1, x2)  =  cons(x2)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

P6_IN_AAA → U7_AAA(reverse7_in_aa)
U7_AAA(reverse7_out_aa(T6)) → P6_IN_AAA

The TRS R consists of the following rules:

reverse7_in_aa → reverse7_out_aa(cons(nil))
reverse7_in_aa → U1_aa(reverse7_in_aa)
reverse7_in_aa → U2_aa(reverse7_in_aa)
U1_aa(reverse7_out_aa(T18)) → reverse7_out_aa(cons(T18))
U2_aa(reverse7_out_aa(T18)) → U3_aa(T18, append23_in_aaa)
reverse7_in_aa → reverse7_out_aa(nil)
U3_aa(T18, append23_out_aaa(T19, X41)) → reverse7_out_aa(cons(T18))
append23_in_aaa → append23_out_aaa(nil, cons(nil))
append23_in_aaa → U4_aaa(append23_in_aaa)
U4_aaa(append23_out_aaa(T34, X67)) → append23_out_aaa(cons(T34), cons(X67))

The set Q consists of the following terms:

reverse7_in_aa
U1_aa(x0)
U2_aa(x0)
U3_aa(x0, x1)
append23_in_aaa
U4_aaa(x0)

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

(35) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P6_IN_AAA → U7_AAA(reverse7_in_aa) at position [0] we obtained the following new rules [LPAR04]:

P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil)))
P6_IN_AAA → U7_AAA(U1_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(U2_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(reverse7_out_aa(nil))

(36) Obligation:

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

U7_AAA(reverse7_out_aa(T6)) → P6_IN_AAA
P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil)))
P6_IN_AAA → U7_AAA(U1_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(U2_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(reverse7_out_aa(nil))

The TRS R consists of the following rules:

reverse7_in_aa → reverse7_out_aa(cons(nil))
reverse7_in_aa → U1_aa(reverse7_in_aa)
reverse7_in_aa → U2_aa(reverse7_in_aa)
U1_aa(reverse7_out_aa(T18)) → reverse7_out_aa(cons(T18))
U2_aa(reverse7_out_aa(T18)) → U3_aa(T18, append23_in_aaa)
reverse7_in_aa → reverse7_out_aa(nil)
U3_aa(T18, append23_out_aaa(T19, X41)) → reverse7_out_aa(cons(T18))
append23_in_aaa → append23_out_aaa(nil, cons(nil))
append23_in_aaa → U4_aaa(append23_in_aaa)
U4_aaa(append23_out_aaa(T34, X67)) → append23_out_aaa(cons(T34), cons(X67))

The set Q consists of the following terms:

reverse7_in_aa
U1_aa(x0)
U2_aa(x0)
U3_aa(x0, x1)
append23_in_aaa
U4_aaa(x0)

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

(37) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = P6_IN_AAA evaluates to t =P6_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil)))
with rule P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil))) at position [] and matcher [ ]

U7_AAA(reverse7_out_aa(cons(nil))) → P6_IN_AAA
with rule U7_AAA(reverse7_out_aa(T6)) → P6_IN_AAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(38) NO

(39) Obligation:

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

REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x1, x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x1, x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga(x1)
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x2, x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x2, x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x2, x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa(x1)
U6_gaa(x1, x2)  =  U6_gaa(x1, x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg(x1, x2)
U1_gg(x1, x2, x3, x4)  =  U1_gg(x2, x3, x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x2, x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x2, x3, x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1, x3)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x4, x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x1, x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x1, x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1, x2)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x3, x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x3, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g(x1)
REVERSE7_IN_GA(x1, x2)  =  REVERSE7_IN_GA(x1)

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

(40) UsableRulesProof (EQUIVALENT transformation)

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

(41) Obligation:

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

REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)

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

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

(42) PiDPToQDPProof (SOUND transformation)

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

(43) Obligation:

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

REVERSE7_IN_GA(cons(T18)) → REVERSE7_IN_GA(T18)

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

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

  • REVERSE7_IN_GA(cons(T18)) → REVERSE7_IN_GA(T18)
    The graph contains the following edges 1 > 1

(45) YES

(46) PrologToPiTRSProof (SOUND transformation)

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

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(47) Obligation:

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

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g

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

QUERY1_IN_G(T6) → U9_G(T6, p6_in_gaa(T6, X19, X21))
QUERY1_IN_G(T6) → P6_IN_GAA(T6, X19, X21)
P6_IN_GAA(T6, X19, X21) → U5_GAA(T6, X19, X21, reverse7_in_ga(T6, X19))
P6_IN_GAA(T6, X19, X21) → REVERSE7_IN_GA(T6, X19)
REVERSE7_IN_GA(cons(T17, T18), X41) → U1_GA(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GA(cons(T17, T18), X41) → U2_GA(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → U4_AAA(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)
P6_IN_GAA(T6, nil, nil) → U6_GAA(T6, reverse7_in_gg(T6, nil))
P6_IN_GAA(T6, nil, nil) → REVERSE7_IN_GG(T6, nil)
REVERSE7_IN_GG(cons(T17, T18), X41) → U1_GG(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GG(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GG(cons(T17, T18), X41) → U2_GG(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → U4_AAG(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → U7_GAA(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_GA(T6, cons(T42, T43))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_GAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)
P6_IN_AAA(T6, X19, X21) → U5_AAA(T6, X19, X21, reverse7_in_aa(T6, X19))
P6_IN_AAA(T6, X19, X21) → REVERSE7_IN_AA(T6, X19)
REVERSE7_IN_AA(cons(T17, T18), X41) → U1_AA(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AA(cons(T17, T18), X41) → U2_AA(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
P6_IN_AAA(T6, nil, nil) → U6_AAA(T6, reverse7_in_ag(T6, nil))
P6_IN_AAA(T6, nil, nil) → REVERSE7_IN_AG(T6, nil)
REVERSE7_IN_AG(cons(T17, T18), X41) → U1_AG(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AG(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AG(cons(T17, T18), X41) → U2_AG(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_AA(T6, cons(T42, T43))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_AAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
QUERY1_IN_G(x1)  =  QUERY1_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x2)
P6_IN_GAA(x1, x2, x3)  =  P6_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)
REVERSE7_IN_GA(x1, x2)  =  REVERSE7_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x4)
APPEND23_IN_AAA(x1, x2, x3)  =  APPEND23_IN_AAA
U4_AAA(x1, x2, x3, x4, x5)  =  U4_AAA(x5)
U6_GAA(x1, x2)  =  U6_GAA(x2)
REVERSE7_IN_GG(x1, x2)  =  REVERSE7_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x4)
U2_GG(x1, x2, x3, x4)  =  U2_GG(x3, x4)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x4)
APPEND23_IN_AAG(x1, x2, x3)  =  APPEND23_IN_AAG(x3)
U4_AAG(x1, x2, x3, x4, x5)  =  U4_AAG(x5)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x5)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x5)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
REVERSE7_IN_AA(x1, x2)  =  REVERSE7_IN_AA
U1_AA(x1, x2, x3, x4)  =  U1_AA(x4)
U2_AA(x1, x2, x3, x4)  =  U2_AA(x4)
U3_AA(x1, x2, x3, x4)  =  U3_AA(x2, x4)
U6_AAA(x1, x2)  =  U6_AAA(x2)
REVERSE7_IN_AG(x1, x2)  =  REVERSE7_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x4)
U2_AG(x1, x2, x3, x4)  =  U2_AG(x3, x4)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x2, x4)
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x1, x5)

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

(49) Obligation:

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

QUERY1_IN_G(T6) → U9_G(T6, p6_in_gaa(T6, X19, X21))
QUERY1_IN_G(T6) → P6_IN_GAA(T6, X19, X21)
P6_IN_GAA(T6, X19, X21) → U5_GAA(T6, X19, X21, reverse7_in_ga(T6, X19))
P6_IN_GAA(T6, X19, X21) → REVERSE7_IN_GA(T6, X19)
REVERSE7_IN_GA(cons(T17, T18), X41) → U1_GA(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GA(cons(T17, T18), X41) → U2_GA(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_GA(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → U4_AAA(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)
P6_IN_GAA(T6, nil, nil) → U6_GAA(T6, reverse7_in_gg(T6, nil))
P6_IN_GAA(T6, nil, nil) → REVERSE7_IN_GG(T6, nil)
REVERSE7_IN_GG(cons(T17, T18), X41) → U1_GG(T17, T18, X41, reverse7_in_ga(T18, X40))
REVERSE7_IN_GG(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)
REVERSE7_IN_GG(cons(T17, T18), X41) → U2_GG(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_GG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_GG(T17, T18, X41, reverse7_out_ga(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → U4_AAG(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → U7_GAA(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
P6_IN_GAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_GA(T6, cons(T42, T43))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_GAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_GAA(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)
P6_IN_AAA(T6, X19, X21) → U5_AAA(T6, X19, X21, reverse7_in_aa(T6, X19))
P6_IN_AAA(T6, X19, X21) → REVERSE7_IN_AA(T6, X19)
REVERSE7_IN_AA(cons(T17, T18), X41) → U1_AA(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AA(cons(T17, T18), X41) → U2_AA(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AA(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U2_AA(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAA(T19, T17, X41)
P6_IN_AAA(T6, nil, nil) → U6_AAA(T6, reverse7_in_ag(T6, nil))
P6_IN_AAA(T6, nil, nil) → REVERSE7_IN_AG(T6, nil)
REVERSE7_IN_AG(cons(T17, T18), X41) → U1_AG(T17, T18, X41, reverse7_in_aa(T18, X40))
REVERSE7_IN_AG(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)
REVERSE7_IN_AG(cons(T17, T18), X41) → U2_AG(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_AG(T17, T18, X41, append23_in_aag(T19, T17, X41))
U2_AG(T17, T18, X41, reverse7_out_aa(T18, T19)) → APPEND23_IN_AAG(T19, T17, X41)
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → REVERSE7_IN_AA(T6, cons(T42, T43))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_AAA(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
QUERY1_IN_G(x1)  =  QUERY1_IN_G(x1)
U9_G(x1, x2)  =  U9_G(x2)
P6_IN_GAA(x1, x2, x3)  =  P6_IN_GAA(x1)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x4)
REVERSE7_IN_GA(x1, x2)  =  REVERSE7_IN_GA(x1)
U1_GA(x1, x2, x3, x4)  =  U1_GA(x4)
U2_GA(x1, x2, x3, x4)  =  U2_GA(x4)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x4)
APPEND23_IN_AAA(x1, x2, x3)  =  APPEND23_IN_AAA
U4_AAA(x1, x2, x3, x4, x5)  =  U4_AAA(x5)
U6_GAA(x1, x2)  =  U6_GAA(x2)
REVERSE7_IN_GG(x1, x2)  =  REVERSE7_IN_GG(x1, x2)
U1_GG(x1, x2, x3, x4)  =  U1_GG(x4)
U2_GG(x1, x2, x3, x4)  =  U2_GG(x3, x4)
U3_GG(x1, x2, x3, x4)  =  U3_GG(x4)
APPEND23_IN_AAG(x1, x2, x3)  =  APPEND23_IN_AAG(x3)
U4_AAG(x1, x2, x3, x4, x5)  =  U4_AAG(x5)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x5)
U8_GAA(x1, x2, x3, x4, x5)  =  U8_GAA(x5)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U5_AAA(x1, x2, x3, x4)  =  U5_AAA(x4)
REVERSE7_IN_AA(x1, x2)  =  REVERSE7_IN_AA
U1_AA(x1, x2, x3, x4)  =  U1_AA(x4)
U2_AA(x1, x2, x3, x4)  =  U2_AA(x4)
U3_AA(x1, x2, x3, x4)  =  U3_AA(x2, x4)
U6_AAA(x1, x2)  =  U6_AAA(x2)
REVERSE7_IN_AG(x1, x2)  =  REVERSE7_IN_AG(x2)
U1_AG(x1, x2, x3, x4)  =  U1_AG(x4)
U2_AG(x1, x2, x3, x4)  =  U2_AG(x3, x4)
U3_AG(x1, x2, x3, x4)  =  U3_AG(x2, x4)
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x1, x5)

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

(50) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 36 less nodes.

(51) Complex Obligation (AND)

(52) Obligation:

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

APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
APPEND23_IN_AAG(x1, x2, x3)  =  APPEND23_IN_AAG(x3)

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

(53) UsableRulesProof (EQUIVALENT transformation)

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

(54) Obligation:

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

APPEND23_IN_AAG(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAG(T34, T35, X67)

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

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

(55) PiDPToQDPProof (SOUND transformation)

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

(56) Obligation:

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

APPEND23_IN_AAG(cons(X67)) → APPEND23_IN_AAG(X67)

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

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

  • APPEND23_IN_AAG(cons(X67)) → APPEND23_IN_AAG(X67)
    The graph contains the following edges 1 > 1

(58) YES

(59) Obligation:

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

APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
APPEND23_IN_AAA(x1, x2, x3)  =  APPEND23_IN_AAA

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

(60) UsableRulesProof (EQUIVALENT transformation)

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

(61) Obligation:

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

APPEND23_IN_AAA(cons(T33, T34), T35, cons(T33, X67)) → APPEND23_IN_AAA(T34, T35, X67)

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

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

(62) PiDPToQDPProof (SOUND transformation)

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

(63) Obligation:

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

APPEND23_IN_AAA → APPEND23_IN_AAA

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

(64) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = APPEND23_IN_AAA evaluates to t =APPEND23_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from APPEND23_IN_AAA to APPEND23_IN_AAA.



(65) NO

(66) Obligation:

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

REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
REVERSE7_IN_AA(x1, x2)  =  REVERSE7_IN_AA

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

(67) UsableRulesProof (EQUIVALENT transformation)

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

(68) Obligation:

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

REVERSE7_IN_AA(cons(T17, T18), X41) → REVERSE7_IN_AA(T18, X40)

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

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

(69) PiDPToQDPProof (SOUND transformation)

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

(70) Obligation:

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

REVERSE7_IN_AA → REVERSE7_IN_AA

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

(71) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.

s = REVERSE7_IN_AA evaluates to t =REVERSE7_IN_AA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Matcher: [ ]
  • Semiunifier: [ ]



Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from REVERSE7_IN_AA to REVERSE7_IN_AA.



(72) NO

(73) Obligation:

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

P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)

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

(74) UsableRulesProof (EQUIVALENT transformation)

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

(75) Obligation:

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

P6_IN_AAA(T6, cons(T42, T43), cons(T42, X87)) → U7_AAA(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_AAA(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → P6_IN_AAA(T43, X86, X87)

The TRS R consists of the following rules:

reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))

The argument filtering Pi contains the following mapping:
nil  =  nil
cons(x1, x2)  =  cons(x2)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
P6_IN_AAA(x1, x2, x3)  =  P6_IN_AAA
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)

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

(76) PiDPToQDPProof (SOUND transformation)

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

(77) Obligation:

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

P6_IN_AAA → U7_AAA(reverse7_in_aa)
U7_AAA(reverse7_out_aa(T6)) → P6_IN_AAA

The TRS R consists of the following rules:

reverse7_in_aa → reverse7_out_aa(cons(nil))
reverse7_in_aa → U1_aa(reverse7_in_aa)
reverse7_in_aa → U2_aa(reverse7_in_aa)
U1_aa(reverse7_out_aa(T18)) → reverse7_out_aa(cons(T18))
U2_aa(reverse7_out_aa(T18)) → U3_aa(T18, append23_in_aaa)
reverse7_in_aa → reverse7_out_aa(nil)
U3_aa(T18, append23_out_aaa(T19, X41)) → reverse7_out_aa(cons(T18))
append23_in_aaa → append23_out_aaa(nil, cons(nil))
append23_in_aaa → U4_aaa(append23_in_aaa)
U4_aaa(append23_out_aaa(T34, X67)) → append23_out_aaa(cons(T34), cons(X67))

The set Q consists of the following terms:

reverse7_in_aa
U1_aa(x0)
U2_aa(x0)
U3_aa(x0, x1)
append23_in_aaa
U4_aaa(x0)

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

(78) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule P6_IN_AAA → U7_AAA(reverse7_in_aa) at position [0] we obtained the following new rules [LPAR04]:

P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil)))
P6_IN_AAA → U7_AAA(U1_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(U2_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(reverse7_out_aa(nil))

(79) Obligation:

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

U7_AAA(reverse7_out_aa(T6)) → P6_IN_AAA
P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil)))
P6_IN_AAA → U7_AAA(U1_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(U2_aa(reverse7_in_aa))
P6_IN_AAA → U7_AAA(reverse7_out_aa(nil))

The TRS R consists of the following rules:

reverse7_in_aa → reverse7_out_aa(cons(nil))
reverse7_in_aa → U1_aa(reverse7_in_aa)
reverse7_in_aa → U2_aa(reverse7_in_aa)
U1_aa(reverse7_out_aa(T18)) → reverse7_out_aa(cons(T18))
U2_aa(reverse7_out_aa(T18)) → U3_aa(T18, append23_in_aaa)
reverse7_in_aa → reverse7_out_aa(nil)
U3_aa(T18, append23_out_aaa(T19, X41)) → reverse7_out_aa(cons(T18))
append23_in_aaa → append23_out_aaa(nil, cons(nil))
append23_in_aaa → U4_aaa(append23_in_aaa)
U4_aaa(append23_out_aaa(T34, X67)) → append23_out_aaa(cons(T34), cons(X67))

The set Q consists of the following terms:

reverse7_in_aa
U1_aa(x0)
U2_aa(x0)
U3_aa(x0, x1)
append23_in_aaa
U4_aaa(x0)

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

(80) NonTerminationProof (EQUIVALENT transformation)

We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:

s = P6_IN_AAA evaluates to t =P6_IN_AAA

Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
  • Semiunifier: [ ]
  • Matcher: [ ]



Rewriting sequence

P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil)))
with rule P6_IN_AAA → U7_AAA(reverse7_out_aa(cons(nil))) at position [] and matcher [ ]

U7_AAA(reverse7_out_aa(cons(nil))) → P6_IN_AAA
with rule U7_AAA(reverse7_out_aa(T6)) → P6_IN_AAA

Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence


All these steps are and every following step will be a correct step w.r.t to Q.



(81) NO

(82) Obligation:

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

REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)

The TRS R consists of the following rules:

query1_in_g(T6) → U9_g(T6, p6_in_gaa(T6, X19, X21))
p6_in_gaa(T6, X19, X21) → U5_gaa(T6, X19, X21, reverse7_in_ga(T6, X19))
reverse7_in_ga(nil, nil) → reverse7_out_ga(nil, nil)
reverse7_in_ga(cons(T12, nil), cons(T12, nil)) → reverse7_out_ga(cons(T12, nil), cons(T12, nil))
reverse7_in_ga(cons(T17, T18), X41) → U1_ga(T17, T18, X41, reverse7_in_ga(T18, X40))
reverse7_in_ga(cons(T17, T18), X41) → U2_ga(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_ga(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_ga(T17, T18, X41, append23_in_aaa(T19, T17, X41))
append23_in_aaa(nil, T26, cons(T26, nil)) → append23_out_aaa(nil, T26, cons(T26, nil))
append23_in_aaa(cons(T33, T34), T35, cons(T33, X67)) → U4_aaa(T33, T34, T35, X67, append23_in_aaa(T34, T35, X67))
U4_aaa(T33, T34, T35, X67, append23_out_aaa(T34, T35, X67)) → append23_out_aaa(cons(T33, T34), T35, cons(T33, X67))
U3_ga(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_ga(cons(T17, T18), X41)
U1_ga(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_ga(cons(T17, T18), X41)
U5_gaa(T6, X19, X21, reverse7_out_ga(T6, X19)) → p6_out_gaa(T6, X19, X21)
p6_in_gaa(T6, nil, nil) → U6_gaa(T6, reverse7_in_gg(T6, nil))
reverse7_in_gg(nil, nil) → reverse7_out_gg(nil, nil)
reverse7_in_gg(cons(T12, nil), cons(T12, nil)) → reverse7_out_gg(cons(T12, nil), cons(T12, nil))
reverse7_in_gg(cons(T17, T18), X41) → U1_gg(T17, T18, X41, reverse7_in_ga(T18, X40))
U1_gg(T17, T18, X41, reverse7_out_ga(T18, X40)) → reverse7_out_gg(cons(T17, T18), X41)
reverse7_in_gg(cons(T17, T18), X41) → U2_gg(T17, T18, X41, reverse7_in_ga(T18, T19))
U2_gg(T17, T18, X41, reverse7_out_ga(T18, T19)) → U3_gg(T17, T18, X41, append23_in_aag(T19, T17, X41))
append23_in_aag(nil, T26, cons(T26, nil)) → append23_out_aag(nil, T26, cons(T26, nil))
append23_in_aag(cons(T33, T34), T35, cons(T33, X67)) → U4_aag(T33, T34, T35, X67, append23_in_aag(T34, T35, X67))
U4_aag(T33, T34, T35, X67, append23_out_aag(T34, T35, X67)) → append23_out_aag(cons(T33, T34), T35, cons(T33, X67))
U3_gg(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_gg(cons(T17, T18), X41)
U6_gaa(T6, reverse7_out_gg(T6, nil)) → p6_out_gaa(T6, nil, nil)
p6_in_gaa(T6, cons(T42, T43), cons(T42, X87)) → U7_gaa(T6, T42, T43, X87, reverse7_in_ga(T6, cons(T42, T43)))
U7_gaa(T6, T42, T43, X87, reverse7_out_ga(T6, cons(T42, T43))) → U8_gaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
p6_in_aaa(T6, X19, X21) → U5_aaa(T6, X19, X21, reverse7_in_aa(T6, X19))
reverse7_in_aa(nil, nil) → reverse7_out_aa(nil, nil)
reverse7_in_aa(cons(T12, nil), cons(T12, nil)) → reverse7_out_aa(cons(T12, nil), cons(T12, nil))
reverse7_in_aa(cons(T17, T18), X41) → U1_aa(T17, T18, X41, reverse7_in_aa(T18, X40))
reverse7_in_aa(cons(T17, T18), X41) → U2_aa(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_aa(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_aa(T17, T18, X41, append23_in_aaa(T19, T17, X41))
U3_aa(T17, T18, X41, append23_out_aaa(T19, T17, X41)) → reverse7_out_aa(cons(T17, T18), X41)
U1_aa(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_aa(cons(T17, T18), X41)
U5_aaa(T6, X19, X21, reverse7_out_aa(T6, X19)) → p6_out_aaa(T6, X19, X21)
p6_in_aaa(T6, nil, nil) → U6_aaa(T6, reverse7_in_ag(T6, nil))
reverse7_in_ag(nil, nil) → reverse7_out_ag(nil, nil)
reverse7_in_ag(cons(T12, nil), cons(T12, nil)) → reverse7_out_ag(cons(T12, nil), cons(T12, nil))
reverse7_in_ag(cons(T17, T18), X41) → U1_ag(T17, T18, X41, reverse7_in_aa(T18, X40))
U1_ag(T17, T18, X41, reverse7_out_aa(T18, X40)) → reverse7_out_ag(cons(T17, T18), X41)
reverse7_in_ag(cons(T17, T18), X41) → U2_ag(T17, T18, X41, reverse7_in_aa(T18, T19))
U2_ag(T17, T18, X41, reverse7_out_aa(T18, T19)) → U3_ag(T17, T18, X41, append23_in_aag(T19, T17, X41))
U3_ag(T17, T18, X41, append23_out_aag(T19, T17, X41)) → reverse7_out_ag(cons(T17, T18), X41)
U6_aaa(T6, reverse7_out_ag(T6, nil)) → p6_out_aaa(T6, nil, nil)
p6_in_aaa(T6, cons(T42, T43), cons(T42, X87)) → U7_aaa(T6, T42, T43, X87, reverse7_in_aa(T6, cons(T42, T43)))
U7_aaa(T6, T42, T43, X87, reverse7_out_aa(T6, cons(T42, T43))) → U8_aaa(T6, T42, T43, X87, p6_in_aaa(T43, X86, X87))
U8_aaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_aaa(T6, cons(T42, T43), cons(T42, X87))
U8_gaa(T6, T42, T43, X87, p6_out_aaa(T43, X86, X87)) → p6_out_gaa(T6, cons(T42, T43), cons(T42, X87))
U9_g(T6, p6_out_gaa(T6, X19, X21)) → query1_out_g(T6)

The argument filtering Pi contains the following mapping:
query1_in_g(x1)  =  query1_in_g(x1)
U9_g(x1, x2)  =  U9_g(x2)
p6_in_gaa(x1, x2, x3)  =  p6_in_gaa(x1)
U5_gaa(x1, x2, x3, x4)  =  U5_gaa(x4)
reverse7_in_ga(x1, x2)  =  reverse7_in_ga(x1)
nil  =  nil
reverse7_out_ga(x1, x2)  =  reverse7_out_ga
cons(x1, x2)  =  cons(x2)
U1_ga(x1, x2, x3, x4)  =  U1_ga(x4)
U2_ga(x1, x2, x3, x4)  =  U2_ga(x4)
U3_ga(x1, x2, x3, x4)  =  U3_ga(x4)
append23_in_aaa(x1, x2, x3)  =  append23_in_aaa
append23_out_aaa(x1, x2, x3)  =  append23_out_aaa(x1, x3)
U4_aaa(x1, x2, x3, x4, x5)  =  U4_aaa(x5)
p6_out_gaa(x1, x2, x3)  =  p6_out_gaa
U6_gaa(x1, x2)  =  U6_gaa(x2)
reverse7_in_gg(x1, x2)  =  reverse7_in_gg(x1, x2)
reverse7_out_gg(x1, x2)  =  reverse7_out_gg
U1_gg(x1, x2, x3, x4)  =  U1_gg(x4)
U2_gg(x1, x2, x3, x4)  =  U2_gg(x3, x4)
U3_gg(x1, x2, x3, x4)  =  U3_gg(x4)
append23_in_aag(x1, x2, x3)  =  append23_in_aag(x3)
append23_out_aag(x1, x2, x3)  =  append23_out_aag(x1)
U4_aag(x1, x2, x3, x4, x5)  =  U4_aag(x5)
U7_gaa(x1, x2, x3, x4, x5)  =  U7_gaa(x5)
U8_gaa(x1, x2, x3, x4, x5)  =  U8_gaa(x5)
p6_in_aaa(x1, x2, x3)  =  p6_in_aaa
U5_aaa(x1, x2, x3, x4)  =  U5_aaa(x4)
reverse7_in_aa(x1, x2)  =  reverse7_in_aa
reverse7_out_aa(x1, x2)  =  reverse7_out_aa(x1)
U1_aa(x1, x2, x3, x4)  =  U1_aa(x4)
U2_aa(x1, x2, x3, x4)  =  U2_aa(x4)
U3_aa(x1, x2, x3, x4)  =  U3_aa(x2, x4)
p6_out_aaa(x1, x2, x3)  =  p6_out_aaa(x1)
U6_aaa(x1, x2)  =  U6_aaa(x2)
reverse7_in_ag(x1, x2)  =  reverse7_in_ag(x2)
reverse7_out_ag(x1, x2)  =  reverse7_out_ag(x1)
U1_ag(x1, x2, x3, x4)  =  U1_ag(x4)
U2_ag(x1, x2, x3, x4)  =  U2_ag(x3, x4)
U3_ag(x1, x2, x3, x4)  =  U3_ag(x2, x4)
U7_aaa(x1, x2, x3, x4, x5)  =  U7_aaa(x5)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x1, x5)
query1_out_g(x1)  =  query1_out_g
REVERSE7_IN_GA(x1, x2)  =  REVERSE7_IN_GA(x1)

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

(83) UsableRulesProof (EQUIVALENT transformation)

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

(84) Obligation:

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

REVERSE7_IN_GA(cons(T17, T18), X41) → REVERSE7_IN_GA(T18, X40)

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

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

(85) PiDPToQDPProof (SOUND transformation)

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

(86) Obligation:

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

REVERSE7_IN_GA(cons(T18)) → REVERSE7_IN_GA(T18)

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

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

  • REVERSE7_IN_GA(cons(T18)) → REVERSE7_IN_GA(T18)
    The graph contains the following edges 1 > 1

(88) YES