(0) Obligation:

Clauses:

in_order(void, []).
in_order(tree(X, Left, Right), Xs) :- ','(in_order(Left, Ls), ','(in_order(Right, Rs), app(Ls, .(X, Rs), Xs))).
app([], X, X).
app(.(X, Xs), Ys, .(X, Zs)) :- app(Xs, Ys, Zs).

Queries:

in_order(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

in_order14(tree(T19, T20, T21), X37) :- in_order14(T20, X35).
in_order14(tree(T19, T20, T21), X37) :- ','(in_orderc14(T20, T22), in_order14(T21, X36)).
in_order14(tree(T19, T20, T21), X37) :- ','(in_orderc14(T20, T22), ','(in_orderc14(T21, T23), app27(T22, T19, T23, X37))).
app27(.(T46, T47), T48, T49, .(T46, X64)) :- app27(T47, T48, T49, X64).
app52(.(T113, T114), T115, T116, .(T113, T118)) :- app52(T114, T115, T116, T118).
in_order1(tree(T7, void, T9), T11) :- in_order14(T9, X14).
in_order1(tree(T7, tree(T74, T75, T76), T9), T11) :- in_order14(T75, X99).
in_order1(tree(T7, tree(T74, T75, T76), T9), T11) :- ','(in_orderc14(T75, T77), in_order14(T76, X100)).
in_order1(tree(T7, tree(T74, T75, T76), T9), T11) :- ','(in_orderc14(T75, T77), ','(in_orderc14(T76, T78), app27(T77, T74, T78, X101))).
in_order1(tree(T7, tree(T74, T75, T76), T9), T11) :- ','(in_orderc14(T75, T77), ','(in_orderc14(T76, T78), ','(appc27(T77, T74, T78, T83), in_order14(T9, X14)))).
in_order1(tree(T7, tree(T74, T75, T76), T9), T11) :- ','(in_orderc14(T75, T77), ','(in_orderc14(T76, T78), ','(appc27(T77, T74, T78, T83), ','(in_orderc14(T9, T88), app52(T83, T7, T88, T11))))).

Clauses:

in_orderc14(void, []).
in_orderc14(tree(T19, T20, T21), X37) :- ','(in_orderc14(T20, T22), ','(in_orderc14(T21, T23), appc27(T22, T19, T23, X37))).
appc27([], T36, T37, .(T36, T37)).
appc27(.(T46, T47), T48, T49, .(T46, X64)) :- appc27(T47, T48, T49, X64).
appc52([], T101, T102, .(T101, T102)).
appc52(.(T113, T114), T115, T116, .(T113, T118)) :- appc52(T114, T115, T116, T118).

Afs:

in_order1(x1, x2)  =  in_order1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
in_order1_in: (b,f)
in_order14_in: (b,f)
in_orderc14_in: (b,f)
appc27_in: (b,b,b,f)
app27_in: (b,b,b,f)
app52_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

IN_ORDER1_IN_GA(tree(T7, void, T9), T11) → U8_GA(T7, T9, T11, in_order14_in_ga(T9, X14))
IN_ORDER1_IN_GA(tree(T7, void, T9), T11) → IN_ORDER14_IN_GA(T9, X14)
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → U1_GA(T19, T20, T21, X37, in_order14_in_ga(T20, X35))
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → IN_ORDER14_IN_GA(T20, X35)
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → U2_GA(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U3_GA(T19, T20, T21, X37, in_order14_in_ga(T21, X36))
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → IN_ORDER14_IN_GA(T21, X36)
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U4_GA(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U4_GA(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U5_GA(T19, T20, T21, X37, app27_in_ggga(T22, T19, T23, X37))
U4_GA(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → APP27_IN_GGGA(T22, T19, T23, X37)
APP27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → U6_GGGA(T46, T47, T48, T49, X64, app27_in_ggga(T47, T48, T49, X64))
APP27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → APP27_IN_GGGA(T47, T48, T49, X64)
IN_ORDER1_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → U9_GA(T7, T74, T75, T76, T9, T11, in_order14_in_ga(T75, X99))
IN_ORDER1_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → IN_ORDER14_IN_GA(T75, X99)
IN_ORDER1_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_in_ga(T75, T77))
U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_out_ga(T75, T77)) → U11_GA(T7, T74, T75, T76, T9, T11, in_order14_in_ga(T76, X100))
U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_out_ga(T75, T77)) → IN_ORDER14_IN_GA(T76, X100)
U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_out_ga(T75, T77)) → U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_in_ga(T76, T78))
U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_out_ga(T76, T78)) → U13_GA(T7, T74, T75, T76, T9, T11, app27_in_ggga(T77, T74, T78, X101))
U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_out_ga(T76, T78)) → APP27_IN_GGGA(T77, T74, T78, X101)
U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_out_ga(T76, T78)) → U14_GA(T7, T74, T75, T76, T9, T11, appc27_in_ggga(T77, T74, T78, T83))
U14_GA(T7, T74, T75, T76, T9, T11, appc27_out_ggga(T77, T74, T78, T83)) → U15_GA(T7, T74, T75, T76, T9, T11, in_order14_in_ga(T9, X14))
U14_GA(T7, T74, T75, T76, T9, T11, appc27_out_ggga(T77, T74, T78, T83)) → IN_ORDER14_IN_GA(T9, X14)
U14_GA(T7, T74, T75, T76, T9, T11, appc27_out_ggga(T77, T74, T78, T83)) → U16_GA(T7, T74, T75, T76, T9, T11, T83, in_orderc14_in_ga(T9, T88))
U16_GA(T7, T74, T75, T76, T9, T11, T83, in_orderc14_out_ga(T9, T88)) → U17_GA(T7, T74, T75, T76, T9, T11, app52_in_ggga(T83, T7, T88, T11))
U16_GA(T7, T74, T75, T76, T9, T11, T83, in_orderc14_out_ga(T9, T88)) → APP52_IN_GGGA(T83, T7, T88, T11)
APP52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U7_GGGA(T113, T114, T115, T116, T118, app52_in_ggga(T114, T115, T116, T118))
APP52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APP52_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

in_orderc14_in_ga(void, []) → in_orderc14_out_ga(void, [])
in_orderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U19_ga(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U20_ga(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appc27_in_ggga(T22, T19, T23, X37))
appc27_in_ggga([], T36, T37, .(T36, T37)) → appc27_out_ggga([], T36, T37, .(T36, T37))
appc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appc27_out_ggga(T47, T48, T49, X64)) → appc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appc27_out_ggga(T22, T19, T23, X37)) → in_orderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
in_order14_in_ga(x1, x2)  =  in_order14_in_ga(x1)
in_orderc14_in_ga(x1, x2)  =  in_orderc14_in_ga(x1)
in_orderc14_out_ga(x1, x2)  =  in_orderc14_out_ga(x1, x2)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6)  =  U20_ga(x1, x2, x3, x5, x6)
U21_ga(x1, x2, x3, x4, x5)  =  U21_ga(x1, x2, x3, x5)
appc27_in_ggga(x1, x2, x3, x4)  =  appc27_in_ggga(x1, x2, x3)
[]  =  []
appc27_out_ggga(x1, x2, x3, x4)  =  appc27_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U22_ggga(x1, x2, x3, x4, x5, x6)  =  U22_ggga(x1, x2, x3, x4, x6)
app27_in_ggga(x1, x2, x3, x4)  =  app27_in_ggga(x1, x2, x3)
app52_in_ggga(x1, x2, x3, x4)  =  app52_in_ggga(x1, x2, x3)
IN_ORDER1_IN_GA(x1, x2)  =  IN_ORDER1_IN_GA(x1)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
IN_ORDER14_IN_GA(x1, x2)  =  IN_ORDER14_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x3, x5)
U4_GA(x1, x2, x3, x4, x5, x6)  =  U4_GA(x1, x2, x3, x5, x6)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x3, x5)
APP27_IN_GGGA(x1, x2, x3, x4)  =  APP27_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5, x6)  =  U6_GGGA(x1, x2, x3, x4, x6)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x1, x2, x3, x4, x5, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x4, x5, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x4, x5, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GA(x1, x2, x3, x4, x5, x7, x8)
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)  =  U15_GA(x1, x2, x3, x4, x5, x7)
U16_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_GA(x1, x2, x3, x4, x5, x7, x8)
U17_GA(x1, x2, x3, x4, x5, x6, x7)  =  U17_GA(x1, x2, x3, x4, x5, x7)
APP52_IN_GGGA(x1, x2, x3, x4)  =  APP52_IN_GGGA(x1, x2, x3)
U7_GGGA(x1, x2, x3, x4, x5, x6)  =  U7_GGGA(x1, x2, x3, x4, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

IN_ORDER1_IN_GA(tree(T7, void, T9), T11) → U8_GA(T7, T9, T11, in_order14_in_ga(T9, X14))
IN_ORDER1_IN_GA(tree(T7, void, T9), T11) → IN_ORDER14_IN_GA(T9, X14)
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → U1_GA(T19, T20, T21, X37, in_order14_in_ga(T20, X35))
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → IN_ORDER14_IN_GA(T20, X35)
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → U2_GA(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U3_GA(T19, T20, T21, X37, in_order14_in_ga(T21, X36))
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → IN_ORDER14_IN_GA(T21, X36)
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U4_GA(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U4_GA(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U5_GA(T19, T20, T21, X37, app27_in_ggga(T22, T19, T23, X37))
U4_GA(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → APP27_IN_GGGA(T22, T19, T23, X37)
APP27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → U6_GGGA(T46, T47, T48, T49, X64, app27_in_ggga(T47, T48, T49, X64))
APP27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → APP27_IN_GGGA(T47, T48, T49, X64)
IN_ORDER1_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → U9_GA(T7, T74, T75, T76, T9, T11, in_order14_in_ga(T75, X99))
IN_ORDER1_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → IN_ORDER14_IN_GA(T75, X99)
IN_ORDER1_IN_GA(tree(T7, tree(T74, T75, T76), T9), T11) → U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_in_ga(T75, T77))
U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_out_ga(T75, T77)) → U11_GA(T7, T74, T75, T76, T9, T11, in_order14_in_ga(T76, X100))
U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_out_ga(T75, T77)) → IN_ORDER14_IN_GA(T76, X100)
U10_GA(T7, T74, T75, T76, T9, T11, in_orderc14_out_ga(T75, T77)) → U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_in_ga(T76, T78))
U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_out_ga(T76, T78)) → U13_GA(T7, T74, T75, T76, T9, T11, app27_in_ggga(T77, T74, T78, X101))
U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_out_ga(T76, T78)) → APP27_IN_GGGA(T77, T74, T78, X101)
U12_GA(T7, T74, T75, T76, T9, T11, T77, in_orderc14_out_ga(T76, T78)) → U14_GA(T7, T74, T75, T76, T9, T11, appc27_in_ggga(T77, T74, T78, T83))
U14_GA(T7, T74, T75, T76, T9, T11, appc27_out_ggga(T77, T74, T78, T83)) → U15_GA(T7, T74, T75, T76, T9, T11, in_order14_in_ga(T9, X14))
U14_GA(T7, T74, T75, T76, T9, T11, appc27_out_ggga(T77, T74, T78, T83)) → IN_ORDER14_IN_GA(T9, X14)
U14_GA(T7, T74, T75, T76, T9, T11, appc27_out_ggga(T77, T74, T78, T83)) → U16_GA(T7, T74, T75, T76, T9, T11, T83, in_orderc14_in_ga(T9, T88))
U16_GA(T7, T74, T75, T76, T9, T11, T83, in_orderc14_out_ga(T9, T88)) → U17_GA(T7, T74, T75, T76, T9, T11, app52_in_ggga(T83, T7, T88, T11))
U16_GA(T7, T74, T75, T76, T9, T11, T83, in_orderc14_out_ga(T9, T88)) → APP52_IN_GGGA(T83, T7, T88, T11)
APP52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U7_GGGA(T113, T114, T115, T116, T118, app52_in_ggga(T114, T115, T116, T118))
APP52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APP52_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

in_orderc14_in_ga(void, []) → in_orderc14_out_ga(void, [])
in_orderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U19_ga(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U20_ga(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appc27_in_ggga(T22, T19, T23, X37))
appc27_in_ggga([], T36, T37, .(T36, T37)) → appc27_out_ggga([], T36, T37, .(T36, T37))
appc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appc27_out_ggga(T47, T48, T49, X64)) → appc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appc27_out_ggga(T22, T19, T23, X37)) → in_orderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
in_order14_in_ga(x1, x2)  =  in_order14_in_ga(x1)
in_orderc14_in_ga(x1, x2)  =  in_orderc14_in_ga(x1)
in_orderc14_out_ga(x1, x2)  =  in_orderc14_out_ga(x1, x2)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6)  =  U20_ga(x1, x2, x3, x5, x6)
U21_ga(x1, x2, x3, x4, x5)  =  U21_ga(x1, x2, x3, x5)
appc27_in_ggga(x1, x2, x3, x4)  =  appc27_in_ggga(x1, x2, x3)
[]  =  []
appc27_out_ggga(x1, x2, x3, x4)  =  appc27_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U22_ggga(x1, x2, x3, x4, x5, x6)  =  U22_ggga(x1, x2, x3, x4, x6)
app27_in_ggga(x1, x2, x3, x4)  =  app27_in_ggga(x1, x2, x3)
app52_in_ggga(x1, x2, x3, x4)  =  app52_in_ggga(x1, x2, x3)
IN_ORDER1_IN_GA(x1, x2)  =  IN_ORDER1_IN_GA(x1)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
IN_ORDER14_IN_GA(x1, x2)  =  IN_ORDER14_IN_GA(x1)
U1_GA(x1, x2, x3, x4, x5)  =  U1_GA(x1, x2, x3, x5)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)
U3_GA(x1, x2, x3, x4, x5)  =  U3_GA(x1, x2, x3, x5)
U4_GA(x1, x2, x3, x4, x5, x6)  =  U4_GA(x1, x2, x3, x5, x6)
U5_GA(x1, x2, x3, x4, x5)  =  U5_GA(x1, x2, x3, x5)
APP27_IN_GGGA(x1, x2, x3, x4)  =  APP27_IN_GGGA(x1, x2, x3)
U6_GGGA(x1, x2, x3, x4, x5, x6)  =  U6_GGGA(x1, x2, x3, x4, x6)
U9_GA(x1, x2, x3, x4, x5, x6, x7)  =  U9_GA(x1, x2, x3, x4, x5, x7)
U10_GA(x1, x2, x3, x4, x5, x6, x7)  =  U10_GA(x1, x2, x3, x4, x5, x7)
U11_GA(x1, x2, x3, x4, x5, x6, x7)  =  U11_GA(x1, x2, x3, x4, x5, x7)
U12_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U12_GA(x1, x2, x3, x4, x5, x7, x8)
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)  =  U15_GA(x1, x2, x3, x4, x5, x7)
U16_GA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U16_GA(x1, x2, x3, x4, x5, x7, x8)
U17_GA(x1, x2, x3, x4, x5, x6, x7)  =  U17_GA(x1, x2, x3, x4, x5, x7)
APP52_IN_GGGA(x1, x2, x3, x4)  =  APP52_IN_GGGA(x1, x2, x3)
U7_GGGA(x1, x2, x3, x4, x5, x6)  =  U7_GGGA(x1, x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

APP52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APP52_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

in_orderc14_in_ga(void, []) → in_orderc14_out_ga(void, [])
in_orderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U19_ga(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U20_ga(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appc27_in_ggga(T22, T19, T23, X37))
appc27_in_ggga([], T36, T37, .(T36, T37)) → appc27_out_ggga([], T36, T37, .(T36, T37))
appc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appc27_out_ggga(T47, T48, T49, X64)) → appc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appc27_out_ggga(T22, T19, T23, X37)) → in_orderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
in_orderc14_in_ga(x1, x2)  =  in_orderc14_in_ga(x1)
in_orderc14_out_ga(x1, x2)  =  in_orderc14_out_ga(x1, x2)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6)  =  U20_ga(x1, x2, x3, x5, x6)
U21_ga(x1, x2, x3, x4, x5)  =  U21_ga(x1, x2, x3, x5)
appc27_in_ggga(x1, x2, x3, x4)  =  appc27_in_ggga(x1, x2, x3)
[]  =  []
appc27_out_ggga(x1, x2, x3, x4)  =  appc27_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U22_ggga(x1, x2, x3, x4, x5, x6)  =  U22_ggga(x1, x2, x3, x4, x6)
APP52_IN_GGGA(x1, x2, x3, x4)  =  APP52_IN_GGGA(x1, x2, x3)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

APP52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APP52_IN_GGGA(T114, T115, T116, T118)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

APP52_IN_GGGA(.(T113, T114), T115, T116) → APP52_IN_GGGA(T114, T115, T116)

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

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

  • APP52_IN_GGGA(.(T113, T114), T115, T116) → APP52_IN_GGGA(T114, T115, T116)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(13) YES

(14) Obligation:

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

APP27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → APP27_IN_GGGA(T47, T48, T49, X64)

The TRS R consists of the following rules:

in_orderc14_in_ga(void, []) → in_orderc14_out_ga(void, [])
in_orderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U19_ga(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U20_ga(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appc27_in_ggga(T22, T19, T23, X37))
appc27_in_ggga([], T36, T37, .(T36, T37)) → appc27_out_ggga([], T36, T37, .(T36, T37))
appc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appc27_out_ggga(T47, T48, T49, X64)) → appc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appc27_out_ggga(T22, T19, T23, X37)) → in_orderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
in_orderc14_in_ga(x1, x2)  =  in_orderc14_in_ga(x1)
in_orderc14_out_ga(x1, x2)  =  in_orderc14_out_ga(x1, x2)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6)  =  U20_ga(x1, x2, x3, x5, x6)
U21_ga(x1, x2, x3, x4, x5)  =  U21_ga(x1, x2, x3, x5)
appc27_in_ggga(x1, x2, x3, x4)  =  appc27_in_ggga(x1, x2, x3)
[]  =  []
appc27_out_ggga(x1, x2, x3, x4)  =  appc27_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U22_ggga(x1, x2, x3, x4, x5, x6)  =  U22_ggga(x1, x2, x3, x4, x6)
APP27_IN_GGGA(x1, x2, x3, x4)  =  APP27_IN_GGGA(x1, x2, x3)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

APP27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → APP27_IN_GGGA(T47, T48, T49, X64)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

APP27_IN_GGGA(.(T46, T47), T48, T49) → APP27_IN_GGGA(T47, T48, T49)

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

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

  • APP27_IN_GGGA(.(T46, T47), T48, T49) → APP27_IN_GGGA(T47, T48, T49)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3

(20) YES

(21) Obligation:

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

IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → U2_GA(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U2_GA(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → IN_ORDER14_IN_GA(T21, X36)
IN_ORDER14_IN_GA(tree(T19, T20, T21), X37) → IN_ORDER14_IN_GA(T20, X35)

The TRS R consists of the following rules:

in_orderc14_in_ga(void, []) → in_orderc14_out_ga(void, [])
in_orderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, in_orderc14_in_ga(T20, T22))
U19_ga(T19, T20, T21, X37, in_orderc14_out_ga(T20, T22)) → U20_ga(T19, T20, T21, X37, T22, in_orderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, in_orderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appc27_in_ggga(T22, T19, T23, X37))
appc27_in_ggga([], T36, T37, .(T36, T37)) → appc27_out_ggga([], T36, T37, .(T36, T37))
appc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appc27_out_ggga(T47, T48, T49, X64)) → appc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appc27_out_ggga(T22, T19, T23, X37)) → in_orderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
in_orderc14_in_ga(x1, x2)  =  in_orderc14_in_ga(x1)
in_orderc14_out_ga(x1, x2)  =  in_orderc14_out_ga(x1, x2)
U19_ga(x1, x2, x3, x4, x5)  =  U19_ga(x1, x2, x3, x5)
U20_ga(x1, x2, x3, x4, x5, x6)  =  U20_ga(x1, x2, x3, x5, x6)
U21_ga(x1, x2, x3, x4, x5)  =  U21_ga(x1, x2, x3, x5)
appc27_in_ggga(x1, x2, x3, x4)  =  appc27_in_ggga(x1, x2, x3)
[]  =  []
appc27_out_ggga(x1, x2, x3, x4)  =  appc27_out_ggga(x1, x2, x3, x4)
.(x1, x2)  =  .(x1, x2)
U22_ggga(x1, x2, x3, x4, x5, x6)  =  U22_ggga(x1, x2, x3, x4, x6)
IN_ORDER14_IN_GA(x1, x2)  =  IN_ORDER14_IN_GA(x1)
U2_GA(x1, x2, x3, x4, x5)  =  U2_GA(x1, x2, x3, x5)

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

(22) PiDPToQDPProof (SOUND transformation)

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

(23) Obligation:

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

IN_ORDER14_IN_GA(tree(T19, T20, T21)) → U2_GA(T19, T20, T21, in_orderc14_in_ga(T20))
U2_GA(T19, T20, T21, in_orderc14_out_ga(T20, T22)) → IN_ORDER14_IN_GA(T21)
IN_ORDER14_IN_GA(tree(T19, T20, T21)) → IN_ORDER14_IN_GA(T20)

The TRS R consists of the following rules:

in_orderc14_in_ga(void) → in_orderc14_out_ga(void, [])
in_orderc14_in_ga(tree(T19, T20, T21)) → U19_ga(T19, T20, T21, in_orderc14_in_ga(T20))
U19_ga(T19, T20, T21, in_orderc14_out_ga(T20, T22)) → U20_ga(T19, T20, T21, T22, in_orderc14_in_ga(T21))
U20_ga(T19, T20, T21, T22, in_orderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, appc27_in_ggga(T22, T19, T23))
appc27_in_ggga([], T36, T37) → appc27_out_ggga([], T36, T37, .(T36, T37))
appc27_in_ggga(.(T46, T47), T48, T49) → U22_ggga(T46, T47, T48, T49, appc27_in_ggga(T47, T48, T49))
U22_ggga(T46, T47, T48, T49, appc27_out_ggga(T47, T48, T49, X64)) → appc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, appc27_out_ggga(T22, T19, T23, X37)) → in_orderc14_out_ga(tree(T19, T20, T21), X37)

The set Q consists of the following terms:

in_orderc14_in_ga(x0)
U19_ga(x0, x1, x2, x3)
U20_ga(x0, x1, x2, x3, x4)
appc27_in_ggga(x0, x1, x2)
U22_ggga(x0, x1, x2, x3, x4)
U21_ga(x0, x1, x2, x3)

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

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

  • U2_GA(T19, T20, T21, in_orderc14_out_ga(T20, T22)) → IN_ORDER14_IN_GA(T21)
    The graph contains the following edges 3 >= 1

  • IN_ORDER14_IN_GA(tree(T19, T20, T21)) → IN_ORDER14_IN_GA(T20)
    The graph contains the following edges 1 > 1

  • IN_ORDER14_IN_GA(tree(T19, T20, T21)) → U2_GA(T19, T20, T21, in_orderc14_in_ga(T20))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

(25) YES