(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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

p54(T43, X84, T44, X85, X86) :- front56(T43, X84).
p54(T43, T45, T44, X85, X86) :- ','(frontc56(T43, T45), front56(T44, X85)).
p54(T43, T45, T44, T60, X86) :- ','(frontc56(T43, T45), ','(frontc56(T44, T60), app72(T45, T60, X86))).
front56(tree(T57, T58, T59), X115) :- p54(T58, X113, T59, X114, X115).
app72(.(T74, T75), T76, .(T74, X142)) :- app72(T75, T76, X142).
app100(.(T134, T135), T136, .(T134, T138)) :- app100(T135, T136, T138).
front1(tree(T7, void, void), T9) :- ','(frontc16(T13), app17(T13, T9)).
front1(tree(T25, void, tree(T42, T43, T44)), T29) :- p54(T43, X84, T44, X85, X86).
front1(tree(T25, void, T27), T29) :- ','(frontc41(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)) :- ','(frontc56(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) :- ','(frontc56(T109, T111), front56(T110, X199)).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), ','(frontc56(T110, T112), app72(T111, T112, X200))).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), ','(frontc56(T110, T112), ','(appc72(T111, T112, T115), front56(T27, X57)))).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), ','(frontc56(T110, T112), ','(appc72(T111, T112, T115), ','(frontc56(T27, T118), app100(T115, T118, T29))))).

Clauses:

appc17(T20, T20).
qc54(T43, T45, T44, T60, X86) :- ','(frontc56(T43, T45), ','(frontc56(T44, T60), appc72(T45, T60, X86))).
frontc56(void, []).
frontc56(tree(T50, void, void), .(T50, [])).
frontc56(tree(T57, T58, T59), X115) :- qc54(T58, X113, T59, X114, X115).
appc72([], T67, T67).
appc72(.(T74, T75), T76, .(T74, X142)) :- appc72(T75, T76, X142).
appc100([], T125, T125).
appc100(.(T134, T135), T136, .(T134, T138)) :- appc100(T135, T136, T138).
frontc16([]).
frontc41(void, []).
frontc41(tree(T35, void, void), .(T35, [])).
frontc41(tree(T42, T43, T44), X86) :- qc54(T43, X84, T44, X85, X86).

Afs:

front1(x1, x2)  =  front1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

p54(T43, X84, T44, X85, X86) :- front56(T43, X84).
p54(T43, T45, T44, X85, X86) :- ','(frontc56(T43, T45), front56(T44, X85)).
p54(T43, T45, T44, T60, X86) :- ','(frontc56(T43, T45), ','(frontc56(T44, T60), app72(T45, T60, X86))).
front56(tree(T57, T58, T59), X115) :- p54(T58, X113, T59, X114, X115).
app72(.(T74, T75), T76, .(T74, X142)) :- app72(T75, T76, X142).
app100(.(T134, T135), T136, .(T134, T138)) :- app100(T135, T136, T138).
front1(tree(T25, void, tree(T42, T43, T44)), T29) :- p54(T43, X84, T44, X85, X86).
front1(tree(T25, tree(T85, void, void), T27), T29) :- front56(T27, X57).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- front56(T109, X198).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), front56(T110, X199)).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), ','(frontc56(T110, T112), app72(T111, T112, X200))).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), ','(frontc56(T110, T112), ','(appc72(T111, T112, T115), front56(T27, X57)))).
front1(tree(T25, tree(T108, T109, T110), T27), T29) :- ','(frontc56(T109, T111), ','(frontc56(T110, T112), ','(appc72(T111, T112, T115), ','(frontc56(T27, T118), app100(T115, T118, T29))))).

Clauses:

appc17(T20, T20).
qc54(T43, T45, T44, T60, X86) :- ','(frontc56(T43, T45), ','(frontc56(T44, T60), appc72(T45, T60, X86))).
frontc56(void, []).
frontc56(tree(T50, void, void), .(T50, [])).
frontc56(tree(T57, T58, T59), X115) :- qc54(T58, X113, T59, X114, X115).
appc72([], T67, T67).
appc72(.(T74, T75), T76, .(T74, X142)) :- appc72(T75, T76, X142).
appc100([], T125, T125).
appc100(.(T134, T135), T136, .(T134, T138)) :- appc100(T135, T136, T138).
frontc16([]).
frontc41(void, []).
frontc41(tree(T35, void, void), .(T35, [])).
frontc41(tree(T42, T43, T44), X86) :- qc54(T43, X84, T44, X85, X86).

Afs:

front1(x1, x2)  =  front1(x1)

(5) TriplesToPiDPProof (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)
p54_in: (b,f,b,f,f)
front56_in: (b,f)
frontc56_in: (b,f)
qc54_in: (b,f,b,f,f)
appc72_in: (b,b,f)
app72_in: (b,b,f)
app100_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FRONT1_IN_GA(tree(T25, void, tree(T42, T43, T44)), T29) → U10_GA(T25, T42, T43, T44, T29, p54_in_gagaa(T43, X84, T44, X85, X86))
FRONT1_IN_GA(tree(T25, void, tree(T42, T43, T44)), T29) → 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, frontc56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, frontc56_out_ga(T43, T45)) → U3_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U2_GAGAA(T43, T45, T44, X85, X86, frontc56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U5_GAGAA(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U5_GAGAA(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U6_GAGAA(T43, T45, T44, T60, X86, app72_in_gga(T45, T60, X86))
U5_GAGAA(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → APP72_IN_GGA(T45, T60, X86)
APP72_IN_GGA(.(T74, T75), T76, .(T74, X142)) → U8_GGA(T74, T75, T76, X142, app72_in_gga(T75, T76, X142))
APP72_IN_GGA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_GGA(T75, T76, X142)
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U11_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(T108, T109, T110), T27), T29) → U12_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) → U13_GA(T25, T108, T109, T110, T27, T29, frontc56_in_ga(T109, T111))
U13_GA(T25, T108, T109, T110, T27, T29, frontc56_out_ga(T109, T111)) → U14_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U13_GA(T25, T108, T109, T110, T27, T29, frontc56_out_ga(T109, T111)) → FRONT56_IN_GA(T110, X199)
U13_GA(T25, T108, T109, T110, T27, T29, frontc56_out_ga(T109, T111)) → U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_in_ga(T110, T112))
U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_out_ga(T110, T112)) → U16_GA(T25, T108, T109, T110, T27, T29, app72_in_gga(T111, T112, X200))
U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_out_ga(T110, T112)) → APP72_IN_GGA(T111, T112, X200)
U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_out_ga(T110, T112)) → U17_GA(T25, T108, T109, T110, T27, T29, appc72_in_gga(T111, T112, T115))
U17_GA(T25, T108, T109, T110, T27, T29, appc72_out_gga(T111, T112, T115)) → U18_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U17_GA(T25, T108, T109, T110, T27, T29, appc72_out_gga(T111, T112, T115)) → FRONT56_IN_GA(T27, X57)
U17_GA(T25, T108, T109, T110, T27, T29, appc72_out_gga(T111, T112, T115)) → U19_GA(T25, T108, T109, T110, T27, T29, T115, frontc56_in_ga(T27, T118))
U19_GA(T25, T108, T109, T110, T27, T29, T115, frontc56_out_ga(T27, T118)) → U20_GA(T25, T108, T109, T110, T27, T29, app100_in_gga(T115, T118, T29))
U19_GA(T25, T108, T109, T110, T27, T29, T115, frontc56_out_ga(T27, T118)) → APP100_IN_GGA(T115, T118, T29)
APP100_IN_GGA(.(T134, T135), T136, .(T134, T138)) → U9_GGA(T134, T135, T136, T138, app100_in_gga(T135, T136, T138))
APP100_IN_GGA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_GGA(T135, T136, T138)

The TRS R consists of the following rules:

frontc56_in_ga(void, []) → frontc56_out_ga(void, [])
frontc56_in_ga(tree(T50, void, void), .(T50, [])) → frontc56_out_ga(tree(T50, void, void), .(T50, []))
frontc56_in_ga(tree(T57, T58, T59), X115) → U25_ga(T57, T58, T59, X115, qc54_in_gagaa(T58, X113, T59, X114, X115))
qc54_in_gagaa(T43, T45, T44, T60, X86) → U22_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U22_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U23_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U23_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U24_gagaa(T43, T45, T44, T60, X86, appc72_in_gga(T45, T60, X86))
appc72_in_gga([], T67, T67) → appc72_out_gga([], T67, T67)
appc72_in_gga(.(T74, T75), T76, .(T74, X142)) → U26_gga(T74, T75, T76, X142, appc72_in_gga(T75, T76, X142))
U26_gga(T74, T75, T76, X142, appc72_out_gga(T75, T76, X142)) → appc72_out_gga(.(T74, T75), T76, .(T74, X142))
U24_gagaa(T43, T45, T44, T60, X86, appc72_out_gga(T45, T60, X86)) → qc54_out_gagaa(T43, T45, T44, T60, X86)
U25_ga(T57, T58, T59, X115, qc54_out_gagaa(T58, X113, T59, X114, X115)) → frontc56_out_ga(tree(T57, T58, T59), X115)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
frontc56_in_ga(x1, x2)  =  frontc56_in_ga(x1)
frontc56_out_ga(x1, x2)  =  frontc56_out_ga(x1, x2)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x1, x2, x3, x5)
qc54_in_gagaa(x1, x2, x3, x4, x5)  =  qc54_in_gagaa(x1, x3)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x6)
U24_gagaa(x1, x2, x3, x4, x5, x6)  =  U24_gagaa(x1, x2, x3, x4, x6)
appc72_in_gga(x1, x2, x3)  =  appc72_in_gga(x1, x2)
[]  =  []
appc72_out_gga(x1, x2, x3)  =  appc72_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
qc54_out_gagaa(x1, x2, x3, x4, x5)  =  qc54_out_gagaa(x1, x2, x3, x4, x5)
app72_in_gga(x1, x2, x3)  =  app72_in_gga(x1, x2)
app100_in_gga(x1, x2, x3)  =  app100_in_gga(x1, x2)
FRONT1_IN_GA(x1, x2)  =  FRONT1_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5, x6)  =  U10_GA(x1, x2, x3, x4, x6)
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, x2, x3, x6)
U6_GAGAA(x1, x2, x3, x4, x5, x6)  =  U6_GAGAA(x1, x3, x6)
APP72_IN_GGA(x1, x2, x3)  =  APP72_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5)  =  U8_GGA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x3, x5)
U12_GA(x1, x2, x3, x4, x5, x6, x7)  =  U12_GA(x1, x2, x3, x4, x5, x7)
U13_GA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GA(x1, x2, x3, x4, x5, x7)
U14_GA(x1, x2, x3, x4, x5, x6, x7)  =  U14_GA(x1, x2, x3, x4, x5, x7)
U15_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_GA(x1, x2, x3, x4, x5, x7, x8)
U16_GA(x1, x2, x3, x4, x5, x6, x7)  =  U16_GA(x1, x2, x3, x4, x5, x7)
U17_GA(x1, x2, x3, x4, x5, x6, x7)  =  U17_GA(x1, x2, x3, x4, x5, x7)
U18_GA(x1, x2, x3, x4, x5, x6, x7)  =  U18_GA(x1, x2, x3, x4, x5, x7)
U19_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_GA(x1, x2, x3, x4, x5, x7, x8)
U20_GA(x1, x2, x3, x4, x5, x6, x7)  =  U20_GA(x1, x2, x3, x4, x5, x7)
APP100_IN_GGA(x1, x2, x3)  =  APP100_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5)  =  U9_GGA(x1, x2, x3, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

FRONT1_IN_GA(tree(T25, void, tree(T42, T43, T44)), T29) → U10_GA(T25, T42, T43, T44, T29, p54_in_gagaa(T43, X84, T44, X85, X86))
FRONT1_IN_GA(tree(T25, void, tree(T42, T43, T44)), T29) → 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, frontc56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, frontc56_out_ga(T43, T45)) → U3_GAGAA(T43, T45, T44, X85, X86, front56_in_ga(T44, X85))
U2_GAGAA(T43, T45, T44, X85, X86, frontc56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)
P54_IN_GAGAA(T43, T45, T44, T60, X86) → U4_GAGAA(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U4_GAGAA(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U5_GAGAA(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U5_GAGAA(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U6_GAGAA(T43, T45, T44, T60, X86, app72_in_gga(T45, T60, X86))
U5_GAGAA(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → APP72_IN_GGA(T45, T60, X86)
APP72_IN_GGA(.(T74, T75), T76, .(T74, X142)) → U8_GGA(T74, T75, T76, X142, app72_in_gga(T75, T76, X142))
APP72_IN_GGA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_GGA(T75, T76, X142)
FRONT1_IN_GA(tree(T25, tree(T85, void, void), T27), T29) → U11_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(T108, T109, T110), T27), T29) → U12_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) → U13_GA(T25, T108, T109, T110, T27, T29, frontc56_in_ga(T109, T111))
U13_GA(T25, T108, T109, T110, T27, T29, frontc56_out_ga(T109, T111)) → U14_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T110, X199))
U13_GA(T25, T108, T109, T110, T27, T29, frontc56_out_ga(T109, T111)) → FRONT56_IN_GA(T110, X199)
U13_GA(T25, T108, T109, T110, T27, T29, frontc56_out_ga(T109, T111)) → U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_in_ga(T110, T112))
U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_out_ga(T110, T112)) → U16_GA(T25, T108, T109, T110, T27, T29, app72_in_gga(T111, T112, X200))
U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_out_ga(T110, T112)) → APP72_IN_GGA(T111, T112, X200)
U15_GA(T25, T108, T109, T110, T27, T29, T111, frontc56_out_ga(T110, T112)) → U17_GA(T25, T108, T109, T110, T27, T29, appc72_in_gga(T111, T112, T115))
U17_GA(T25, T108, T109, T110, T27, T29, appc72_out_gga(T111, T112, T115)) → U18_GA(T25, T108, T109, T110, T27, T29, front56_in_ga(T27, X57))
U17_GA(T25, T108, T109, T110, T27, T29, appc72_out_gga(T111, T112, T115)) → FRONT56_IN_GA(T27, X57)
U17_GA(T25, T108, T109, T110, T27, T29, appc72_out_gga(T111, T112, T115)) → U19_GA(T25, T108, T109, T110, T27, T29, T115, frontc56_in_ga(T27, T118))
U19_GA(T25, T108, T109, T110, T27, T29, T115, frontc56_out_ga(T27, T118)) → U20_GA(T25, T108, T109, T110, T27, T29, app100_in_gga(T115, T118, T29))
U19_GA(T25, T108, T109, T110, T27, T29, T115, frontc56_out_ga(T27, T118)) → APP100_IN_GGA(T115, T118, T29)
APP100_IN_GGA(.(T134, T135), T136, .(T134, T138)) → U9_GGA(T134, T135, T136, T138, app100_in_gga(T135, T136, T138))
APP100_IN_GGA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_GGA(T135, T136, T138)

The TRS R consists of the following rules:

frontc56_in_ga(void, []) → frontc56_out_ga(void, [])
frontc56_in_ga(tree(T50, void, void), .(T50, [])) → frontc56_out_ga(tree(T50, void, void), .(T50, []))
frontc56_in_ga(tree(T57, T58, T59), X115) → U25_ga(T57, T58, T59, X115, qc54_in_gagaa(T58, X113, T59, X114, X115))
qc54_in_gagaa(T43, T45, T44, T60, X86) → U22_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U22_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U23_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U23_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U24_gagaa(T43, T45, T44, T60, X86, appc72_in_gga(T45, T60, X86))
appc72_in_gga([], T67, T67) → appc72_out_gga([], T67, T67)
appc72_in_gga(.(T74, T75), T76, .(T74, X142)) → U26_gga(T74, T75, T76, X142, appc72_in_gga(T75, T76, X142))
U26_gga(T74, T75, T76, X142, appc72_out_gga(T75, T76, X142)) → appc72_out_gga(.(T74, T75), T76, .(T74, X142))
U24_gagaa(T43, T45, T44, T60, X86, appc72_out_gga(T45, T60, X86)) → qc54_out_gagaa(T43, T45, T44, T60, X86)
U25_ga(T57, T58, T59, X115, qc54_out_gagaa(T58, X113, T59, X114, X115)) → frontc56_out_ga(tree(T57, T58, T59), X115)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
p54_in_gagaa(x1, x2, x3, x4, x5)  =  p54_in_gagaa(x1, x3)
front56_in_ga(x1, x2)  =  front56_in_ga(x1)
frontc56_in_ga(x1, x2)  =  frontc56_in_ga(x1)
frontc56_out_ga(x1, x2)  =  frontc56_out_ga(x1, x2)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x1, x2, x3, x5)
qc54_in_gagaa(x1, x2, x3, x4, x5)  =  qc54_in_gagaa(x1, x3)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x6)
U24_gagaa(x1, x2, x3, x4, x5, x6)  =  U24_gagaa(x1, x2, x3, x4, x6)
appc72_in_gga(x1, x2, x3)  =  appc72_in_gga(x1, x2)
[]  =  []
appc72_out_gga(x1, x2, x3)  =  appc72_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
qc54_out_gagaa(x1, x2, x3, x4, x5)  =  qc54_out_gagaa(x1, x2, x3, x4, x5)
app72_in_gga(x1, x2, x3)  =  app72_in_gga(x1, x2)
app100_in_gga(x1, x2, x3)  =  app100_in_gga(x1, x2)
FRONT1_IN_GA(x1, x2)  =  FRONT1_IN_GA(x1)
U10_GA(x1, x2, x3, x4, x5, x6)  =  U10_GA(x1, x2, x3, x4, x6)
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, x2, x3, x6)
U6_GAGAA(x1, x2, x3, x4, x5, x6)  =  U6_GAGAA(x1, x3, x6)
APP72_IN_GGA(x1, x2, x3)  =  APP72_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4, x5)  =  U8_GGA(x1, x2, x3, x5)
U11_GA(x1, x2, x3, x4, x5)  =  U11_GA(x1, x2, x3, x5)
U12_GA(x1, x2, x3, x4, x5, x6, x7)  =  U12_GA(x1, x2, x3, x4, x5, x7)
U13_GA(x1, x2, x3, x4, x5, x6, x7)  =  U13_GA(x1, x2, x3, x4, x5, x7)
U14_GA(x1, x2, x3, x4, x5, x6, x7)  =  U14_GA(x1, x2, x3, x4, x5, x7)
U15_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U15_GA(x1, x2, x3, x4, x5, x7, x8)
U16_GA(x1, x2, x3, x4, x5, x6, x7)  =  U16_GA(x1, x2, x3, x4, x5, x7)
U17_GA(x1, x2, x3, x4, x5, x6, x7)  =  U17_GA(x1, x2, x3, x4, x5, x7)
U18_GA(x1, x2, x3, x4, x5, x6, x7)  =  U18_GA(x1, x2, x3, x4, x5, x7)
U19_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U19_GA(x1, x2, x3, x4, x5, x7, x8)
U20_GA(x1, x2, x3, x4, x5, x6, x7)  =  U20_GA(x1, x2, x3, x4, x5, x7)
APP100_IN_GGA(x1, x2, x3)  =  APP100_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3, x4, x5)  =  U9_GGA(x1, x2, x3, 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 27 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

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

The TRS R consists of the following rules:

frontc56_in_ga(void, []) → frontc56_out_ga(void, [])
frontc56_in_ga(tree(T50, void, void), .(T50, [])) → frontc56_out_ga(tree(T50, void, void), .(T50, []))
frontc56_in_ga(tree(T57, T58, T59), X115) → U25_ga(T57, T58, T59, X115, qc54_in_gagaa(T58, X113, T59, X114, X115))
qc54_in_gagaa(T43, T45, T44, T60, X86) → U22_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U22_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U23_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U23_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U24_gagaa(T43, T45, T44, T60, X86, appc72_in_gga(T45, T60, X86))
appc72_in_gga([], T67, T67) → appc72_out_gga([], T67, T67)
appc72_in_gga(.(T74, T75), T76, .(T74, X142)) → U26_gga(T74, T75, T76, X142, appc72_in_gga(T75, T76, X142))
U26_gga(T74, T75, T76, X142, appc72_out_gga(T75, T76, X142)) → appc72_out_gga(.(T74, T75), T76, .(T74, X142))
U24_gagaa(T43, T45, T44, T60, X86, appc72_out_gga(T45, T60, X86)) → qc54_out_gagaa(T43, T45, T44, T60, X86)
U25_ga(T57, T58, T59, X115, qc54_out_gagaa(T58, X113, T59, X114, X115)) → frontc56_out_ga(tree(T57, T58, T59), X115)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
frontc56_in_ga(x1, x2)  =  frontc56_in_ga(x1)
frontc56_out_ga(x1, x2)  =  frontc56_out_ga(x1, x2)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x1, x2, x3, x5)
qc54_in_gagaa(x1, x2, x3, x4, x5)  =  qc54_in_gagaa(x1, x3)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x6)
U24_gagaa(x1, x2, x3, x4, x5, x6)  =  U24_gagaa(x1, x2, x3, x4, x6)
appc72_in_gga(x1, x2, x3)  =  appc72_in_gga(x1, x2)
[]  =  []
appc72_out_gga(x1, x2, x3)  =  appc72_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
qc54_out_gagaa(x1, x2, x3, x4, x5)  =  qc54_out_gagaa(x1, x2, x3, x4, x5)
APP100_IN_GGA(x1, x2, x3)  =  APP100_IN_GGA(x1, x2)

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_GGA(.(T134, T135), T136, .(T134, T138)) → APP100_IN_GGA(T135, T136, T138)

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

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_GGA(.(T134, T135), T136) → APP100_IN_GGA(T135, T136)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • APP100_IN_GGA(.(T134, T135), T136) → APP100_IN_GGA(T135, T136)
    The graph contains the following edges 1 > 1, 2 >= 2

(15) YES

(16) Obligation:

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

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

The TRS R consists of the following rules:

frontc56_in_ga(void, []) → frontc56_out_ga(void, [])
frontc56_in_ga(tree(T50, void, void), .(T50, [])) → frontc56_out_ga(tree(T50, void, void), .(T50, []))
frontc56_in_ga(tree(T57, T58, T59), X115) → U25_ga(T57, T58, T59, X115, qc54_in_gagaa(T58, X113, T59, X114, X115))
qc54_in_gagaa(T43, T45, T44, T60, X86) → U22_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U22_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U23_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U23_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U24_gagaa(T43, T45, T44, T60, X86, appc72_in_gga(T45, T60, X86))
appc72_in_gga([], T67, T67) → appc72_out_gga([], T67, T67)
appc72_in_gga(.(T74, T75), T76, .(T74, X142)) → U26_gga(T74, T75, T76, X142, appc72_in_gga(T75, T76, X142))
U26_gga(T74, T75, T76, X142, appc72_out_gga(T75, T76, X142)) → appc72_out_gga(.(T74, T75), T76, .(T74, X142))
U24_gagaa(T43, T45, T44, T60, X86, appc72_out_gga(T45, T60, X86)) → qc54_out_gagaa(T43, T45, T44, T60, X86)
U25_ga(T57, T58, T59, X115, qc54_out_gagaa(T58, X113, T59, X114, X115)) → frontc56_out_ga(tree(T57, T58, T59), X115)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
frontc56_in_ga(x1, x2)  =  frontc56_in_ga(x1)
frontc56_out_ga(x1, x2)  =  frontc56_out_ga(x1, x2)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x1, x2, x3, x5)
qc54_in_gagaa(x1, x2, x3, x4, x5)  =  qc54_in_gagaa(x1, x3)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x6)
U24_gagaa(x1, x2, x3, x4, x5, x6)  =  U24_gagaa(x1, x2, x3, x4, x6)
appc72_in_gga(x1, x2, x3)  =  appc72_in_gga(x1, x2)
[]  =  []
appc72_out_gga(x1, x2, x3)  =  appc72_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
qc54_out_gagaa(x1, x2, x3, x4, x5)  =  qc54_out_gagaa(x1, x2, x3, x4, x5)
APP72_IN_GGA(x1, x2, x3)  =  APP72_IN_GGA(x1, x2)

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_GGA(.(T74, T75), T76, .(T74, X142)) → APP72_IN_GGA(T75, T76, X142)

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

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_GGA(.(T74, T75), T76) → APP72_IN_GGA(T75, T76)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • APP72_IN_GGA(.(T74, T75), T76) → APP72_IN_GGA(T75, T76)
    The graph contains the following edges 1 > 1, 2 >= 2

(22) YES

(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, frontc56_in_ga(T43, T45))
U2_GAGAA(T43, T45, T44, X85, X86, frontc56_out_ga(T43, T45)) → FRONT56_IN_GA(T44, X85)

The TRS R consists of the following rules:

frontc56_in_ga(void, []) → frontc56_out_ga(void, [])
frontc56_in_ga(tree(T50, void, void), .(T50, [])) → frontc56_out_ga(tree(T50, void, void), .(T50, []))
frontc56_in_ga(tree(T57, T58, T59), X115) → U25_ga(T57, T58, T59, X115, qc54_in_gagaa(T58, X113, T59, X114, X115))
qc54_in_gagaa(T43, T45, T44, T60, X86) → U22_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T43, T45))
U22_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T43, T45)) → U23_gagaa(T43, T45, T44, T60, X86, frontc56_in_ga(T44, T60))
U23_gagaa(T43, T45, T44, T60, X86, frontc56_out_ga(T44, T60)) → U24_gagaa(T43, T45, T44, T60, X86, appc72_in_gga(T45, T60, X86))
appc72_in_gga([], T67, T67) → appc72_out_gga([], T67, T67)
appc72_in_gga(.(T74, T75), T76, .(T74, X142)) → U26_gga(T74, T75, T76, X142, appc72_in_gga(T75, T76, X142))
U26_gga(T74, T75, T76, X142, appc72_out_gga(T75, T76, X142)) → appc72_out_gga(.(T74, T75), T76, .(T74, X142))
U24_gagaa(T43, T45, T44, T60, X86, appc72_out_gga(T45, T60, X86)) → qc54_out_gagaa(T43, T45, T44, T60, X86)
U25_ga(T57, T58, T59, X115, qc54_out_gagaa(T58, X113, T59, X114, X115)) → frontc56_out_ga(tree(T57, T58, T59), X115)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
frontc56_in_ga(x1, x2)  =  frontc56_in_ga(x1)
frontc56_out_ga(x1, x2)  =  frontc56_out_ga(x1, x2)
U25_ga(x1, x2, x3, x4, x5)  =  U25_ga(x1, x2, x3, x5)
qc54_in_gagaa(x1, x2, x3, x4, x5)  =  qc54_in_gagaa(x1, x3)
U22_gagaa(x1, x2, x3, x4, x5, x6)  =  U22_gagaa(x1, x3, x6)
U23_gagaa(x1, x2, x3, x4, x5, x6)  =  U23_gagaa(x1, x2, x3, x6)
U24_gagaa(x1, x2, x3, x4, x5, x6)  =  U24_gagaa(x1, x2, x3, x4, x6)
appc72_in_gga(x1, x2, x3)  =  appc72_in_gga(x1, x2)
[]  =  []
appc72_out_gga(x1, x2, x3)  =  appc72_out_gga(x1, x2, x3)
.(x1, x2)  =  .(x1, x2)
U26_gga(x1, x2, x3, x4, x5)  =  U26_gga(x1, x2, x3, x5)
qc54_out_gagaa(x1, x2, x3, x4, x5)  =  qc54_out_gagaa(x1, x2, x3, x4, 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)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

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, frontc56_in_ga(T43))
U2_GAGAA(T43, T44, frontc56_out_ga(T43, T45)) → FRONT56_IN_GA(T44)

The TRS R consists of the following rules:

frontc56_in_ga(void) → frontc56_out_ga(void, [])
frontc56_in_ga(tree(T50, void, void)) → frontc56_out_ga(tree(T50, void, void), .(T50, []))
frontc56_in_ga(tree(T57, T58, T59)) → U25_ga(T57, T58, T59, qc54_in_gagaa(T58, T59))
qc54_in_gagaa(T43, T44) → U22_gagaa(T43, T44, frontc56_in_ga(T43))
U22_gagaa(T43, T44, frontc56_out_ga(T43, T45)) → U23_gagaa(T43, T45, T44, frontc56_in_ga(T44))
U23_gagaa(T43, T45, T44, frontc56_out_ga(T44, T60)) → U24_gagaa(T43, T45, T44, T60, appc72_in_gga(T45, T60))
appc72_in_gga([], T67) → appc72_out_gga([], T67, T67)
appc72_in_gga(.(T74, T75), T76) → U26_gga(T74, T75, T76, appc72_in_gga(T75, T76))
U26_gga(T74, T75, T76, appc72_out_gga(T75, T76, X142)) → appc72_out_gga(.(T74, T75), T76, .(T74, X142))
U24_gagaa(T43, T45, T44, T60, appc72_out_gga(T45, T60, X86)) → qc54_out_gagaa(T43, T45, T44, T60, X86)
U25_ga(T57, T58, T59, qc54_out_gagaa(T58, X113, T59, X114, X115)) → frontc56_out_ga(tree(T57, T58, T59), X115)

The set Q consists of the following terms:

frontc56_in_ga(x0)
qc54_in_gagaa(x0, x1)
U22_gagaa(x0, x1, x2)
U23_gagaa(x0, x1, x2, x3)
appc72_in_gga(x0, x1)
U26_gga(x0, x1, x2, x3)
U24_gagaa(x0, x1, x2, x3, x4)
U25_ga(x0, x1, x2, x3)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • 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

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

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

(27) YES