(0) Obligation:

Clauses:

front(void, []).
front(tree(X, void, void), .(X, [])).
front(tree(X1, L, R), Xs) :- ','(front(L, Ls), ','(front(R, Rs), app(Ls, Rs, Xs))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Queries:

front(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

app17(T20, T20).
p54(T43, X84, T44, X85, X86) :- front56(T43, X84).
p54(T43, T45, T44, X85, X86) :- ','(front56(T43, T45), front56(T44, X85)).
p54(T43, T45, T44, T60, X86) :- ','(front56(T43, T45), ','(front56(T44, T60), app72(T45, T60, X86))).
front56(void, []).
front56(tree(T50, void, void), .(T50, [])).
front56(tree(T57, T58, T59), X115) :- p54(T58, X113, T59, X114, X115).
app72([], T67, T67).
app72(.(T74, T75), T76, .(T74, X142)) :- app72(T75, T76, X142).
app100([], T125, T125).
app100(.(T134, T135), T136, .(T134, T138)) :- app100(T135, T136, T138).
front16([]).
front41(void, []).
front41(tree(T35, void, void), .(T35, [])).
front41(tree(T42, T43, T44), X86) :- p54(T43, X84, T44, X85, X86).
front1(void, []).
front1(tree(T4, void, void), .(T4, [])).
front1(tree(T7, void, void), T9) :- front16(X19).
front1(tree(T7, void, void), T9) :- ','(front16(T13), app17(T13, T9)).
front1(tree(T25, void, T27), T29) :- front41(T27, X57).
front1(tree(T25, void, T27), T29) :- ','(front41(T27, T30), app17(T30, T29)).
front1(tree(T25, tree(T85, void, void), T27), T29) :- front56(T27, X57).
front1(tree(T25, tree(T96, void, void), T27), .(T96, T99)) :- ','(front56(T27, T97), app17(T97, T99)).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- front56(T109, X198).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(front56(T109, T111), front56(T110, X199)).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(front56(T109, T111), ','(front56(T110, T112), app72(T111, T112, X200))).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(front56(T109, T111), ','(front56(T110, T112), ','(app72(T111, T112, T115), front56(T27, X57)))).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(front56(T109, T111), ','(front56(T110, T112), ','(app72(T111, T112, T115), ','(front56(T27, T118), app100(T115, T118, T29))))).

Queries:

front1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

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

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)

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

FRONT1_IN_GA(tree(T7, void, void), T9) → U11_GA(T7, T9, front16_in_a(X19))
FRONT1_IN_GA(tree(T7, void, void), T9) → FRONT16_IN_A(X19)
FRONT1_IN_GA(tree(T7, void, void), T9) → U12_GA(T7, T9, front16_in_a(T13))
U12_GA(T7, T9, front16_out_a(T13)) → U13_GA(T7, T9, app17_in_ga(T13, T9))
U12_GA(T7, T9, front16_out_a(T13)) → APP17_IN_GA(T13, T9)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U14_GA(T25, T27, T29, front41_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, void, T27), T29) → FRONT41_IN_GA(T27, X57)
FRONT41_IN_GA(tree(T42, T43, T44), X86) → U10_GA(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
FRONT41_IN_GA(tree(T42, T43, T44), X86) → P54_IN_GAGAA(T43, X84, T44, X85, X86)
P54_IN_GAGAA(T43, X84, T44, X85, X86) → U1_GAGAA(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → U7_GA(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_GAGAA(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → APP72_IN_AAA(T45, T60, X86)
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → U8_AAA(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U15_GA(T25, T27, T29, front41_in_ga(T27, T30))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → U16_GA(T25, T27, T29, app17_in_aa(T30, T29))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → APP17_IN_AA(T30, T29)
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U17_GA(T25, T85, T27, T29, front56_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → FRONT56_IN_GA(T27, X57)
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_GA(T25, T96, T27, T99, front56_in_ga(T27, T97))
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → FRONT56_IN_GA(T27, T97)
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_GA(T25, T96, T27, T99, app17_in_aa(T97, T99))
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → APP17_IN_AA(T97, T99)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U20_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → FRONT56_IN_GA(T109, X198)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U21_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → FRONT56_IN_GA(T110, X199)
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → APP72_IN_AAA(T111, T112, X200)
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → FRONT56_IN_GA(T27, X57)
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_GA(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → APP100_IN_AAA(T115, T118, T29)
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → U9_AAA(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
FRONT1_IN_GA(x1, x2)  =  FRONT1_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
FRONT16_IN_A(x1)  =  FRONT16_IN_A
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
APP17_IN_GA(x1, x2)  =  APP17_IN_GA(x1)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x4)
FRONT41_IN_GA(x1, x2)  =  FRONT41_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
U1_GAGAA(x1, x2, x3, x4, x5, x6)  =  U1_GAGAA(x6)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x5)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x3, x6)
U3_GAGAA(x1, x2, x3, x4, x5, x6)  =  U3_GAGAA(x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x3, x6)
U5_GAGAA(x1, x2, x3, x4, x5, x6)  =  U5_GAGAA(x6)
U6_GAGAA(x1, x2, x3, x4, x5, x6)  =  U6_GAGAA(x6)
APP72_IN_AAA(x1, x2, x3)  =  APP72_IN_AAA
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x5)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x4)
APP17_IN_AA(x1, x2)  =  APP17_IN_AA
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x5)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x5)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x5)
U20_GA(x1, x2, x3, x4, x5, x6, x7)  =  U20_GA(x7)
U21_GA(x1, x2, x3, x4, x5, x6, x7)  =  U21_GA(x4, x5, x7)
U22_GA(x1, x2, x3, x4, x5, x6, x7)  =  U22_GA(x7)
U23_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_GA(x5, x8)
U24_GA(x1, x2, x3, x4, x5, x6, x7)  =  U24_GA(x7)
U25_GA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GA(x5, x7)
U26_GA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GA(x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_GA(x8)
U28_GA(x1, x2, x3, x4, x5, x6, x7)  =  U28_GA(x7)
APP100_IN_AAA(x1, x2, x3)  =  APP100_IN_AAA
U9_AAA(x1, x2, x3, x4, x5)  =  U9_AAA(x5)

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

(6) Obligation:

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

FRONT1_IN_GA(tree(T7, void, void), T9) → U11_GA(T7, T9, front16_in_a(X19))
FRONT1_IN_GA(tree(T7, void, void), T9) → FRONT16_IN_A(X19)
FRONT1_IN_GA(tree(T7, void, void), T9) → U12_GA(T7, T9, front16_in_a(T13))
U12_GA(T7, T9, front16_out_a(T13)) → U13_GA(T7, T9, app17_in_ga(T13, T9))
U12_GA(T7, T9, front16_out_a(T13)) → APP17_IN_GA(T13, T9)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U14_GA(T25, T27, T29, front41_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, void, T27), T29) → FRONT41_IN_GA(T27, X57)
FRONT41_IN_GA(tree(T42, T43, T44), X86) → U10_GA(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
FRONT41_IN_GA(tree(T42, T43, T44), X86) → P54_IN_GAGAA(T43, X84, T44, X85, X86)
P54_IN_GAGAA(T43, X84, T44, X85, X86) → U1_GAGAA(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → U7_GA(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_GAGAA(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → APP72_IN_AAA(T45, T60, X86)
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → U8_AAA(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U15_GA(T25, T27, T29, front41_in_ga(T27, T30))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → U16_GA(T25, T27, T29, app17_in_aa(T30, T29))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → APP17_IN_AA(T30, T29)
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U17_GA(T25, T85, T27, T29, front56_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → FRONT56_IN_GA(T27, X57)
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_GA(T25, T96, T27, T99, front56_in_ga(T27, T97))
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → FRONT56_IN_GA(T27, T97)
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_GA(T25, T96, T27, T99, app17_in_aa(T97, T99))
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → APP17_IN_AA(T97, T99)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U20_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → FRONT56_IN_GA(T109, X198)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U21_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → FRONT56_IN_GA(T110, X199)
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → APP72_IN_AAA(T111, T112, X200)
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → FRONT56_IN_GA(T27, X57)
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_GA(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → APP100_IN_AAA(T115, T118, T29)
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → U9_AAA(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
FRONT1_IN_GA(x1, x2)  =  FRONT1_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
FRONT16_IN_A(x1)  =  FRONT16_IN_A
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
APP17_IN_GA(x1, x2)  =  APP17_IN_GA(x1)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x4)
FRONT41_IN_GA(x1, x2)  =  FRONT41_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
U1_GAGAA(x1, x2, x3, x4, x5, x6)  =  U1_GAGAA(x6)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x5)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x3, x6)
U3_GAGAA(x1, x2, x3, x4, x5, x6)  =  U3_GAGAA(x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x3, x6)
U5_GAGAA(x1, x2, x3, x4, x5, x6)  =  U5_GAGAA(x6)
U6_GAGAA(x1, x2, x3, x4, x5, x6)  =  U6_GAGAA(x6)
APP72_IN_AAA(x1, x2, x3)  =  APP72_IN_AAA
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x5)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x4)
APP17_IN_AA(x1, x2)  =  APP17_IN_AA
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x5)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x5)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x5)
U20_GA(x1, x2, x3, x4, x5, x6, x7)  =  U20_GA(x7)
U21_GA(x1, x2, x3, x4, x5, x6, x7)  =  U21_GA(x4, x5, x7)
U22_GA(x1, x2, x3, x4, x5, x6, x7)  =  U22_GA(x7)
U23_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_GA(x5, x8)
U24_GA(x1, x2, x3, x4, x5, x6, x7)  =  U24_GA(x7)
U25_GA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GA(x5, x7)
U26_GA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GA(x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_GA(x8)
U28_GA(x1, x2, x3, x4, x5, x6, x7)  =  U28_GA(x7)
APP100_IN_AAA(x1, x2, x3)  =  APP100_IN_AAA
U9_AAA(x1, x2, x3, x4, x5)  =  U9_AAA(x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
APP100_IN_AAA(x1, x2, x3)  =  APP100_IN_AAA

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:

APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

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

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:

APP100_IN_AAAAPP100_IN_AAA

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

(14) 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 = APP100_IN_AAA evaluates to t =APP100_IN_AAA

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 APP100_IN_AAA to APP100_IN_AAA.



(15) NO

(16) Obligation:

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

APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
APP72_IN_AAA(x1, x2, x3)  =  APP72_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:

APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)

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

APP72_IN_AAAAPP72_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 = APP72_IN_AAA evaluates to t =APP72_IN_AAA

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 APP72_IN_AAA to APP72_IN_AAA.



(22) NO

(23) Obligation:

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

P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x3, x6)

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:

P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)

The TRS R consists of the following rules:

front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))

The argument filtering Pi contains the following mapping:
void  =  void
tree(x1, x2, x3)  =  tree(x1, x2, x3)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x3, x6)

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:

P54_IN_GAGAA(T43, T44) → FRONT56_IN_GA(T43)
FRONT56_IN_GA(tree(T57, T58, T59)) → P54_IN_GAGAA(T58, T59)
P54_IN_GAGAA(T43, T44) → U2_GAGAA(T44, front56_in_ga(T43))
U2_GAGAA(T44, front56_out_ga) → FRONT56_IN_GA(T44)
P54_IN_GAGAA(T43, T44) → U4_GAGAA(T44, front56_in_ga(T43))
U4_GAGAA(T44, front56_out_ga) → FRONT56_IN_GA(T44)

The TRS R consists of the following rules:

front56_in_ga(void) → front56_out_ga
front56_in_ga(tree(T50, void, void)) → front56_out_ga
front56_in_ga(tree(T57, T58, T59)) → U7_ga(p54_in_gagaa(T58, T59))
U7_ga(p54_out_gagaa) → front56_out_ga
p54_in_gagaa(T43, T44) → U1_gagaa(front56_in_ga(T43))
p54_in_gagaa(T43, T44) → U2_gagaa(T44, front56_in_ga(T43))
p54_in_gagaa(T43, T44) → U4_gagaa(T44, front56_in_ga(T43))
U1_gagaa(front56_out_ga) → p54_out_gagaa
U2_gagaa(T44, front56_out_ga) → U3_gagaa(front56_in_ga(T44))
U4_gagaa(T44, front56_out_ga) → U5_gagaa(front56_in_ga(T44))
U3_gagaa(front56_out_ga) → p54_out_gagaa
U5_gagaa(front56_out_ga) → U6_gagaa(app72_in_aaa)
U6_gagaa(app72_out_aaa(T45)) → p54_out_gagaa
app72_in_aaaapp72_out_aaa([])
app72_in_aaaU8_aaa(app72_in_aaa)
U8_aaa(app72_out_aaa(T75)) → app72_out_aaa(.(T75))

The set Q consists of the following terms:

front56_in_ga(x0)
U7_ga(x0)
p54_in_gagaa(x0, x1)
U1_gagaa(x0)
U2_gagaa(x0, x1)
U4_gagaa(x0, x1)
U3_gagaa(x0)
U5_gagaa(x0)
U6_gagaa(x0)
app72_in_aaa
U8_aaa(x0)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • FRONT56_IN_GA(tree(T57, T58, T59)) → P54_IN_GAGAA(T58, T59)
    The graph contains the following edges 1 > 1, 1 > 2

  • P54_IN_GAGAA(T43, T44) → FRONT56_IN_GA(T43)
    The graph contains the following edges 1 >= 1

  • U2_GAGAA(T44, front56_out_ga) → FRONT56_IN_GA(T44)
    The graph contains the following edges 1 >= 1

  • U4_GAGAA(T44, front56_out_ga) → FRONT56_IN_GA(T44)
    The graph contains the following edges 1 >= 1

  • P54_IN_GAGAA(T43, T44) → U2_GAGAA(T44, front56_in_ga(T43))
    The graph contains the following edges 2 >= 1

  • P54_IN_GAGAA(T43, T44) → U4_GAGAA(T44, front56_in_ga(T43))
    The graph contains the following edges 2 >= 1

(29) YES

(30) PrologToPiTRSProof (SOUND transformation)

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

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(31) Obligation:

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

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)

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

FRONT1_IN_GA(tree(T7, void, void), T9) → U11_GA(T7, T9, front16_in_a(X19))
FRONT1_IN_GA(tree(T7, void, void), T9) → FRONT16_IN_A(X19)
FRONT1_IN_GA(tree(T7, void, void), T9) → U12_GA(T7, T9, front16_in_a(T13))
U12_GA(T7, T9, front16_out_a(T13)) → U13_GA(T7, T9, app17_in_ga(T13, T9))
U12_GA(T7, T9, front16_out_a(T13)) → APP17_IN_GA(T13, T9)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U14_GA(T25, T27, T29, front41_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, void, T27), T29) → FRONT41_IN_GA(T27, X57)
FRONT41_IN_GA(tree(T42, T43, T44), X86) → U10_GA(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
FRONT41_IN_GA(tree(T42, T43, T44), X86) → P54_IN_GAGAA(T43, X84, T44, X85, X86)
P54_IN_GAGAA(T43, X84, T44, X85, X86) → U1_GAGAA(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → U7_GA(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_GAGAA(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → APP72_IN_AAA(T45, T60, X86)
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → U8_AAA(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U15_GA(T25, T27, T29, front41_in_ga(T27, T30))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → U16_GA(T25, T27, T29, app17_in_aa(T30, T29))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → APP17_IN_AA(T30, T29)
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U17_GA(T25, T85, T27, T29, front56_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → FRONT56_IN_GA(T27, X57)
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_GA(T25, T96, T27, T99, front56_in_ga(T27, T97))
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → FRONT56_IN_GA(T27, T97)
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_GA(T25, T96, T27, T99, app17_in_aa(T97, T99))
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → APP17_IN_AA(T97, T99)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U20_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → FRONT56_IN_GA(T109, X198)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U21_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → FRONT56_IN_GA(T110, X199)
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → APP72_IN_AAA(T111, T112, X200)
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → FRONT56_IN_GA(T27, X57)
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_GA(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → APP100_IN_AAA(T115, T118, T29)
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → U9_AAA(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
FRONT1_IN_GA(x1, x2)  =  FRONT1_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
FRONT16_IN_A(x1)  =  FRONT16_IN_A
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
APP17_IN_GA(x1, x2)  =  APP17_IN_GA(x1)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
FRONT41_IN_GA(x1, x2)  =  FRONT41_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
U1_GAGAA(x1, x2, x3, x4, x5, x6)  =  U1_GAGAA(x1, x3, x6)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)
U3_GAGAA(x1, x2, x3, x4, x5, x6)  =  U3_GAGAA(x1, x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x1, x3, x6)
U5_GAGAA(x1, x2, x3, x4, x5, x6)  =  U5_GAGAA(x1, x3, x6)
U6_GAGAA(x1, x2, x3, x4, x5, x6)  =  U6_GAGAA(x1, x3, x6)
APP72_IN_AAA(x1, x2, x3)  =  APP72_IN_AAA
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x5)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
APP17_IN_AA(x1, x2)  =  APP17_IN_AA
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x1, x2, x3, x5)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x1, x2, x3, x5)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U20_GA(x1, x2, x3, x4, x5, x6, x7)  =  U20_GA(x1, x2, x3, x4, x5, x7)
U21_GA(x1, x2, x3, x4, x5, x6, x7)  =  U21_GA(x1, x2, x3, x4, x5, x7)
U22_GA(x1, x2, x3, x4, x5, x6, x7)  =  U22_GA(x1, x2, x3, x4, x5, x7)
U23_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_GA(x1, x2, x3, x4, x5, x8)
U24_GA(x1, x2, x3, x4, x5, x6, x7)  =  U24_GA(x1, x2, x3, x4, x5, x7)
U25_GA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GA(x1, x2, x3, x4, x5, x7)
U26_GA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GA(x1, x2, x3, x4, x5, x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_GA(x1, x2, x3, x4, x5, x8)
U28_GA(x1, x2, x3, x4, x5, x6, x7)  =  U28_GA(x1, x2, x3, x4, x5, x7)
APP100_IN_AAA(x1, x2, x3)  =  APP100_IN_AAA
U9_AAA(x1, x2, x3, x4, x5)  =  U9_AAA(x5)

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

(33) Obligation:

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

FRONT1_IN_GA(tree(T7, void, void), T9) → U11_GA(T7, T9, front16_in_a(X19))
FRONT1_IN_GA(tree(T7, void, void), T9) → FRONT16_IN_A(X19)
FRONT1_IN_GA(tree(T7, void, void), T9) → U12_GA(T7, T9, front16_in_a(T13))
U12_GA(T7, T9, front16_out_a(T13)) → U13_GA(T7, T9, app17_in_ga(T13, T9))
U12_GA(T7, T9, front16_out_a(T13)) → APP17_IN_GA(T13, T9)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U14_GA(T25, T27, T29, front41_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, void, T27), T29) → FRONT41_IN_GA(T27, X57)
FRONT41_IN_GA(tree(T42, T43, T44), X86) → U10_GA(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
FRONT41_IN_GA(tree(T42, T43, T44), X86) → P54_IN_GAGAA(T43, X84, T44, X85, X86)
P54_IN_GAGAA(T43, X84, T44, X85, X86) → U1_GAGAA(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → U7_GA(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_GAGAA(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
U5_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → APP72_IN_AAA(T45, T60, X86)
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → U8_AAA(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)
FRONT1_IN_GA(tree(T25, void, T27), T29) → U15_GA(T25, T27, T29, front41_in_ga(T27, T30))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → U16_GA(T25, T27, T29, app17_in_aa(T30, T29))
U15_GA(T25, T27, T29, front41_out_ga(T27, T30)) → APP17_IN_AA(T30, T29)
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U17_GA(T25, T85, T27, T29, front56_in_ga(T27, X57))
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → FRONT56_IN_GA(T27, X57)
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_GA(T25, T96, T27, T99, front56_in_ga(T27, T97))
FRONT1_IN_GA(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → FRONT56_IN_GA(T27, T97)
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_GA(T25, T96, T27, T99, app17_in_aa(T97, T99))
U18_GA(T25, T96, T27, T99, front56_out_ga(T27, T97)) → APP17_IN_AA(T97, T99)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U20_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → FRONT56_IN_GA(T109, X198)
FRONT1_IN_GA(tree(T25, tree(T108, T109, T110), T27), T29) → U21_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → FRONT56_IN_GA(T110, X199)
U21_GA(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → APP72_IN_AAA(T111, T112, X200)
U23_GA(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_GA(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → FRONT56_IN_GA(T27, X57)
U25_GA(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_GA(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
U27_GA(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → APP100_IN_AAA(T115, T118, T29)
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → U9_AAA(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
FRONT1_IN_GA(x1, x2)  =  FRONT1_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
FRONT16_IN_A(x1)  =  FRONT16_IN_A
U12_GA(x1, x2, x3)  =  U12_GA(x1, x3)
U13_GA(x1, x2, x3)  =  U13_GA(x1, x3)
APP17_IN_GA(x1, x2)  =  APP17_IN_GA(x1)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x2, x4)
FRONT41_IN_GA(x1, x2)  =  FRONT41_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5)  =  U10_GA(x1, x2, x3, x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
U1_GAGAA(x1, x2, x3, x4, x5, x6)  =  U1_GAGAA(x1, x3, x6)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U7_GA(x1, x2, x3, x4, x5)  =  U7_GA(x1, x2, x3, x5)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)
U3_GAGAA(x1, x2, x3, x4, x5, x6)  =  U3_GAGAA(x1, x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x1, x3, x6)
U5_GAGAA(x1, x2, x3, x4, x5, x6)  =  U5_GAGAA(x1, x3, x6)
U6_GAGAA(x1, x2, x3, x4, x5, x6)  =  U6_GAGAA(x1, x3, x6)
APP72_IN_AAA(x1, x2, x3)  =  APP72_IN_AAA
U8_AAA(x1, x2, x3, x4, x5)  =  U8_AAA(x5)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x2, x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x1, x2, x4)
APP17_IN_AA(x1, x2)  =  APP17_IN_AA
U17_GA(x1, x2, x3, x4, x5)  =  U17_GA(x1, x2, x3, x5)
U18_GA(x1, x2, x3, x4, x5)  =  U18_GA(x1, x2, x3, x5)
U19_GA(x1, x2, x3, x4, x5)  =  U19_GA(x1, x2, x3, x5)
U20_GA(x1, x2, x3, x4, x5, x6, x7)  =  U20_GA(x1, x2, x3, x4, x5, x7)
U21_GA(x1, x2, x3, x4, x5, x6, x7)  =  U21_GA(x1, x2, x3, x4, x5, x7)
U22_GA(x1, x2, x3, x4, x5, x6, x7)  =  U22_GA(x1, x2, x3, x4, x5, x7)
U23_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_GA(x1, x2, x3, x4, x5, x8)
U24_GA(x1, x2, x3, x4, x5, x6, x7)  =  U24_GA(x1, x2, x3, x4, x5, x7)
U25_GA(x1, x2, x3, x4, x5, x6, x7)  =  U25_GA(x1, x2, x3, x4, x5, x7)
U26_GA(x1, x2, x3, x4, x5, x6, x7)  =  U26_GA(x1, x2, x3, x4, x5, x7)
U27_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_GA(x1, x2, x3, x4, x5, x8)
U28_GA(x1, x2, x3, x4, x5, x6, x7)  =  U28_GA(x1, x2, x3, x4, x5, x7)
APP100_IN_AAA(x1, x2, x3)  =  APP100_IN_AAA
U9_AAA(x1, x2, x3, x4, x5)  =  U9_AAA(x5)

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

(34) DependencyGraphProof (EQUIVALENT transformation)

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

(35) Complex Obligation (AND)

(36) Obligation:

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

APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
APP100_IN_AAA(x1, x2, x3)  =  APP100_IN_AAA

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

(37) UsableRulesProof (EQUIVALENT transformation)

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

(38) Obligation:

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

APP100_IN_AAA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_AAA(T135, T136, T138)

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

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

(39) PiDPToQDPProof (SOUND transformation)

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

(40) Obligation:

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

APP100_IN_AAAAPP100_IN_AAA

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

(41) 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 = APP100_IN_AAA evaluates to t =APP100_IN_AAA

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 APP100_IN_AAA to APP100_IN_AAA.



(42) NO

(43) Obligation:

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

APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
APP72_IN_AAA(x1, x2, x3)  =  APP72_IN_AAA

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

(44) UsableRulesProof (EQUIVALENT transformation)

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

(45) Obligation:

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

APP72_IN_AAA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_AAA(T75, T76, X142)

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

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

(46) PiDPToQDPProof (SOUND transformation)

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

(47) Obligation:

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

APP72_IN_AAAAPP72_IN_AAA

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

(48) 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 = APP72_IN_AAA evaluates to t =APP72_IN_AAA

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 APP72_IN_AAA to APP72_IN_AAA.



(49) NO

(50) Obligation:

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

P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)

The TRS R consists of the following rules:

front1_in_ga(void, []) → front1_out_ga(void, [])
front1_in_ga(tree(T4, void, void), .(T4, [])) → front1_out_ga(tree(T4, void, void), .(T4, []))
front1_in_ga(tree(T7, void, void), T9) → U11_ga(T7, T9, front16_in_a(X19))
front16_in_a([]) → front16_out_a([])
U11_ga(T7, T9, front16_out_a(X19)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T7, void, void), T9) → U12_ga(T7, T9, front16_in_a(T13))
U12_ga(T7, T9, front16_out_a(T13)) → U13_ga(T7, T9, app17_in_ga(T13, T9))
app17_in_ga(T20, T20) → app17_out_ga(T20, T20)
U13_ga(T7, T9, app17_out_ga(T13, T9)) → front1_out_ga(tree(T7, void, void), T9)
front1_in_ga(tree(T25, void, T27), T29) → U14_ga(T25, T27, T29, front41_in_ga(T27, X57))
front41_in_ga(void, []) → front41_out_ga(void, [])
front41_in_ga(tree(T35, void, void), .(T35, [])) → front41_out_ga(tree(T35, void, void), .(T35, []))
front41_in_ga(tree(T42, T43, T44), X86) → U10_ga(T42, T43, T44, X86, p54_in_gagaa(T43, X84, T44, X85, X86))
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U10_ga(T42, T43, T44, X86, p54_out_gagaa(T43, X84, T44, X85, X86)) → front41_out_ga(tree(T42, T43, T44), X86)
U14_ga(T25, T27, T29, front41_out_ga(T27, X57)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, void, T27), T29) → U15_ga(T25, T27, T29, front41_in_ga(T27, T30))
U15_ga(T25, T27, T29, front41_out_ga(T27, T30)) → U16_ga(T25, T27, T29, app17_in_aa(T30, T29))
app17_in_aa(T20, T20) → app17_out_aa(T20, T20)
U16_ga(T25, T27, T29, app17_out_aa(T30, T29)) → front1_out_ga(tree(T25, void, T27), T29)
front1_in_ga(tree(T25, tree(T85, void, void), T27), T29) → U17_ga(T25, T85, T27, T29, front56_in_ga(T27, X57))
U17_ga(T25, T85, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T85, void, void), T27), T29)
front1_in_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99)) → U18_ga(T25, T96, T27, T99, front56_in_ga(T27, T97))
U18_ga(T25, T96, T27, T99, front56_out_ga(T27, T97)) → U19_ga(T25, T96, T27, T99, app17_in_aa(T97, T99))
U19_ga(T25, T96, T27, T99, app17_out_aa(T97, T99)) → front1_out_ga(tree(T25, tree(T96, void, void), T27), .(T96, T99))
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U20_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, X198))
U20_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, X198)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
front1_in_ga(tree(T25, tree(T108, T109, T110), T27), T29) → U21_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T109, T111))
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U22_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U22_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T110, X199)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U21_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T109, T111)) → U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_in_ga(T110, T112))
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U24_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, X200))
U24_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, X200)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U23_ga(T25, T108, T109, T110, T27, T29, T111, front56_out_ga(T110, T112)) → U25_ga(T25, T108, T109, T110, T27, T29, app72_in_aaa(T111, T112, T115))
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U26_ga(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U26_ga(T25, T108, T109, T110, T27, T29, front56_out_ga(T27, X57)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)
U25_ga(T25, T108, T109, T110, T27, T29, app72_out_aaa(T111, T112, T115)) → U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_in_ga(T27, T118))
U27_ga(T25, T108, T109, T110, T27, T29, T115, front56_out_ga(T27, T118)) → U28_ga(T25, T108, T109, T110, T27, T29, app100_in_aaa(T115, T118, T29))
app100_in_aaa([], T125, T125) → app100_out_aaa([], T125, T125)
app100_in_aaa(.(T134, T135), T136, .(T134, T138)) → U9_aaa(T134, T135, T136, T138, app100_in_aaa(T135, T136, T138))
U9_aaa(T134, T135, T136, T138, app100_out_aaa(T135, T136, T138)) → app100_out_aaa(.(T134, T135), T136, .(T134, T138))
U28_ga(T25, T108, T109, T110, T27, T29, app100_out_aaa(T115, T118, T29)) → front1_out_ga(tree(T25, tree(T108, T109, T110), T27), T29)

The argument filtering Pi contains the following mapping:
front1_in_ga(x1, x2)  =  front1_in_ga(x1)
void  =  void
front1_out_ga(x1, x2)  =  front1_out_ga(x1)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U11_ga(x1, x2, x3)  =  U11_ga(x1, x3)
front16_in_a(x1)  =  front16_in_a
front16_out_a(x1)  =  front16_out_a(x1)
U12_ga(x1, x2, x3)  =  U12_ga(x1, x3)
U13_ga(x1, x2, x3)  =  U13_ga(x1, x3)
app17_in_ga(x1, x2)  =  app17_in_ga(x1)
app17_out_ga(x1, x2)  =  app17_out_ga(x1, x2)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x1, x2, x4)
front41_in_ga(x1, x2)  =  front41_in_ga(x1)
front41_out_ga(x1, x2)  =  front41_out_ga(x1)
U10_ga(x1, x2, x3, x4, x5)  =  U10_ga(x1, x2, x3, x5)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x2, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x1, x2, x4)
app17_in_aa(x1, x2)  =  app17_in_aa
app17_out_aa(x1, x2)  =  app17_out_aa
U17_ga(x1, x2, x3, x4, x5)  =  U17_ga(x1, x2, x3, x5)
U18_ga(x1, x2, x3, x4, x5)  =  U18_ga(x1, x2, x3, x5)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6, x7)  =  U20_ga(x1, x2, x3, x4, x5, x7)
U21_ga(x1, x2, x3, x4, x5, x6, x7)  =  U21_ga(x1, x2, x3, x4, x5, x7)
U22_ga(x1, x2, x3, x4, x5, x6, x7)  =  U22_ga(x1, x2, x3, x4, x5, x7)
U23_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U23_ga(x1, x2, x3, x4, x5, x8)
U24_ga(x1, x2, x3, x4, x5, x6, x7)  =  U24_ga(x1, x2, x3, x4, x5, x7)
U25_ga(x1, x2, x3, x4, x5, x6, x7)  =  U25_ga(x1, x2, x3, x4, x5, x7)
U26_ga(x1, x2, x3, x4, x5, x6, x7)  =  U26_ga(x1, x2, x3, x4, x5, x7)
U27_ga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_ga(x1, x2, x3, x4, x5, x8)
U28_ga(x1, x2, x3, x4, x5, x6, x7)  =  U28_ga(x1, x2, x3, x4, x5, x7)
app100_in_aaa(x1, x2, x3)  =  app100_in_aaa
app100_out_aaa(x1, x2, x3)  =  app100_out_aaa(x1)
U9_aaa(x1, x2, x3, x4, x5)  =  U9_aaa(x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x1, x3, x6)

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

(51) UsableRulesProof (EQUIVALENT transformation)

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

(52) Obligation:

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

P54_IN_GAGAA(T43, X84, T44, X85, X86) → FRONT56_IN_GA(T43, X84)
FRONT56_IN_GA(tree(T57, T58, T59), X115) → P54_IN_GAGAA(T58, X113, T59, X114, X115)
P54_IN_GAGAA(T43, T45, T44, X85, X86) → U2_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, T60)

The TRS R consists of the following rules:

front56_in_ga(void, []) → front56_out_ga(void, [])
front56_in_ga(tree(T50, void, void), .(T50, [])) → front56_out_ga(tree(T50, void, void), .(T50, []))
front56_in_ga(tree(T57, T58, T59), X115) → U7_ga(T57, T58, T59, X115, p54_in_gagaa(T58, X113, T59, X114, X115))
U7_ga(T57, T58, T59, X115, p54_out_gagaa(T58, X113, T59, X114, X115)) → front56_out_ga(tree(T57, T58, T59), X115)
p54_in_gagaa(T43, X84, T44, X85, X86) → U1_gagaa(T43, X84, T44, X85, X86, front56_in_ga(T43, X84))
p54_in_gagaa(T43, T45, T44, X85, X86) → U2_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T43, T45))
p54_in_gagaa(T43, T45, T44, T60, X86) → U4_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T43, T45))
U1_gagaa(T43, X84, T44, X85, X86, front56_out_ga(T43, X84)) → p54_out_gagaa(T43, X84, T44, X85, X86)
U2_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T43, T45)) → U3_gagaa(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U4_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T43, T45)) → U5_gagaa(T43, T45, T44, T60, X86, front56_in_ga(T44, T60))
U3_gagaa(T43, T45, T44, X85, X86, front56_out_ga(T44, X85)) → p54_out_gagaa(T43, T45, T44, X85, X86)
U5_gagaa(T43, T45, T44, T60, X86, front56_out_ga(T44, T60)) → U6_gagaa(T43, T45, T44, T60, X86, app72_in_aaa(T45, T60, X86))
U6_gagaa(T43, T45, T44, T60, X86, app72_out_aaa(T45, T60, X86)) → p54_out_gagaa(T43, T45, T44, T60, X86)
app72_in_aaa([], T67, T67) → app72_out_aaa([], T67, T67)
app72_in_aaa(.(T74, T75), T76, .(T74, X142)) → U8_aaa(T74, T75, T76, X142, app72_in_aaa(T75, T76, X142))
U8_aaa(T74, T75, T76, X142, app72_out_aaa(T75, T76, X142)) → app72_out_aaa(.(T74, T75), T76, .(T74, X142))

The argument filtering Pi contains the following mapping:
void  =  void
tree(x1, x2, x3)  =  tree(x1, x2, x3)
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
U1_gagaa(x1, x2, x3, x4, x5, x6)  =  U1_gagaa(x1, x3, x6)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
front56_out_ga(x1, x2)  =  front56_out_ga(x1)
U7_ga(x1, x2, x3, x4, x5)  =  U7_ga(x1, x2, x3, x5)
U2_gagaa(x1, x2, x3, x4, x5, x6)  =  U2_gagaa(x1, x3, x6)
U3_gagaa(x1, x2, x3, x4, x5, x6)  =  U3_gagaa(x1, x3, x6)
p54_out_gagaa(x1, x2, x3, x4, x5)  =  p54_out_gagaa(x1, x3)
U4_gagaa(x1, x2, x3, x4, x5, x6)  =  U4_gagaa(x1, x3, x6)
U5_gagaa(x1, x2, x3, x4, x5, x6)  =  U5_gagaa(x1, x3, x6)
U6_gagaa(x1, x2, x3, x4, x5, x6)  =  U6_gagaa(x1, x3, x6)
[]  =  []
.(x1, x2)  =  .(x2)
app72_in_aaa(x1, x2, x3)  =  app72_in_aaa
app72_out_aaa(x1, x2, x3)  =  app72_out_aaa(x1)
U8_aaa(x1, x2, x3, x4, x5)  =  U8_aaa(x5)
P54_IN_GAGAA(x1, x2, x3, x4, x5)  =  P54_IN_GAGAA(x1, x3)
FRONT56_IN_GA(x1, x2)  =  FRONT56_IN_GA(x1)
U2_GAGAA(x1, x2, x3, x4, x5, x6)  =  U2_GAGAA(x1, x3, x6)
U4_GAGAA(x1, x2, x3, x4, x5, x6)  =  U4_GAGAA(x1, x3, x6)

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

(53) PiDPToQDPProof (SOUND transformation)

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

(54) Obligation:

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

P54_IN_GAGAA(T43, T44) → FRONT56_IN_GA(T43)
FRONT56_IN_GA(tree(T57, T58, T59)) → P54_IN_GAGAA(T58, T59)
P54_IN_GAGAA(T43, T44) → U2_GAGAA(T43, T44, front56_in_ga(T43))
U2_GAGAA(T43, T44, front56_out_ga(T43)) → FRONT56_IN_GA(T44)
P54_IN_GAGAA(T43, T44) → U4_GAGAA(T43, T44, front56_in_ga(T43))
U4_GAGAA(T43, T44, front56_out_ga(T43)) → FRONT56_IN_GA(T44)

The TRS R consists of the following rules:

front56_in_ga(void) → front56_out_ga(void)
front56_in_ga(tree(T50, void, void)) → front56_out_ga(tree(T50, void, void))
front56_in_ga(tree(T57, T58, T59)) → U7_ga(T57, T58, T59, p54_in_gagaa(T58, T59))
U7_ga(T57, T58, T59, p54_out_gagaa(T58, T59)) → front56_out_ga(tree(T57, T58, T59))
p54_in_gagaa(T43, T44) → U1_gagaa(T43, T44, front56_in_ga(T43))
p54_in_gagaa(T43, T44) → U2_gagaa(T43, T44, front56_in_ga(T43))
p54_in_gagaa(T43, T44) → U4_gagaa(T43, T44, front56_in_ga(T43))
U1_gagaa(T43, T44, front56_out_ga(T43)) → p54_out_gagaa(T43, T44)
U2_gagaa(T43, T44, front56_out_ga(T43)) → U3_gagaa(T43, T44, front56_in_ga(T44))
U4_gagaa(T43, T44, front56_out_ga(T43)) → U5_gagaa(T43, T44, front56_in_ga(T44))
U3_gagaa(T43, T44, front56_out_ga(T44)) → p54_out_gagaa(T43, T44)
U5_gagaa(T43, T44, front56_out_ga(T44)) → U6_gagaa(T43, T44, app72_in_aaa)
U6_gagaa(T43, T44, app72_out_aaa(T45)) → p54_out_gagaa(T43, T44)
app72_in_aaaapp72_out_aaa([])
app72_in_aaaU8_aaa(app72_in_aaa)
U8_aaa(app72_out_aaa(T75)) → app72_out_aaa(.(T75))

The set Q consists of the following terms:

front56_in_ga(x0)
U7_ga(x0, x1, x2, x3)
p54_in_gagaa(x0, x1)
U1_gagaa(x0, x1, x2)
U2_gagaa(x0, x1, x2)
U4_gagaa(x0, x1, x2)
U3_gagaa(x0, x1, x2)
U5_gagaa(x0, x1, x2)
U6_gagaa(x0, x1, x2)
app72_in_aaa
U8_aaa(x0)

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

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

  • FRONT56_IN_GA(tree(T57, T58, T59)) → P54_IN_GAGAA(T58, T59)
    The graph contains the following edges 1 > 1, 1 > 2

  • P54_IN_GAGAA(T43, T44) → FRONT56_IN_GA(T43)
    The graph contains the following edges 1 >= 1

  • U2_GAGAA(T43, T44, front56_out_ga(T43)) → FRONT56_IN_GA(T44)
    The graph contains the following edges 2 >= 1

  • U4_GAGAA(T43, T44, front56_out_ga(T43)) → FRONT56_IN_GA(T44)
    The graph contains the following edges 2 >= 1

  • P54_IN_GAGAA(T43, T44) → U2_GAGAA(T43, T44, front56_in_ga(T43))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • P54_IN_GAGAA(T43, T44) → U4_GAGAA(T43, T44, front56_in_ga(T43))
    The graph contains the following edges 1 >= 1, 2 >= 2

(56) YES