(0) Obligation:

Clauses:

inorder(nil, []).
inorder(tree(L, V, R), I) :- ','(inorder(L, LI), ','(inorder(R, RI), append(LI, .(V, RI), I))).
append([], X, X).
append(.(X, Xs), Ys, .(X, Zs)) :- append(Xs, Ys, Zs).

Queries:

inorder(g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

inorder14(tree(T19, T20, T21), X37) :- inorder14(T19, X35).
inorder14(tree(T19, T20, T21), X37) :- ','(inorderc14(T19, T22), inorder14(T21, X36)).
inorder14(tree(T19, T20, T21), X37) :- ','(inorderc14(T19, T22), ','(inorderc14(T21, T23), append27(T22, T20, T23, X37))).
append27(.(T46, T47), T48, T49, .(T46, X64)) :- append27(T47, T48, T49, X64).
append52(.(T113, T114), T115, T116, .(T113, T118)) :- append52(T114, T115, T116, T118).
inorder1(tree(nil, T8, T9), T11) :- inorder14(T9, X14).
inorder1(tree(tree(T74, T75, T76), T8, T9), T11) :- inorder14(T74, X99).
inorder1(tree(tree(T74, T75, T76), T8, T9), T11) :- ','(inorderc14(T74, T77), inorder14(T76, X100)).
inorder1(tree(tree(T74, T75, T76), T8, T9), T11) :- ','(inorderc14(T74, T77), ','(inorderc14(T76, T78), append27(T77, T75, T78, X101))).
inorder1(tree(tree(T74, T75, T76), T8, T9), T11) :- ','(inorderc14(T74, T77), ','(inorderc14(T76, T78), ','(appendc27(T77, T75, T78, T83), inorder14(T9, X14)))).
inorder1(tree(tree(T74, T75, T76), T8, T9), T11) :- ','(inorderc14(T74, T77), ','(inorderc14(T76, T78), ','(appendc27(T77, T75, T78, T83), ','(inorderc14(T9, T88), append52(T83, T8, T88, T11))))).

Clauses:

inorderc14(nil, []).
inorderc14(tree(T19, T20, T21), X37) :- ','(inorderc14(T19, T22), ','(inorderc14(T21, T23), appendc27(T22, T20, T23, X37))).
appendc27([], T36, T37, .(T36, T37)).
appendc27(.(T46, T47), T48, T49, .(T46, X64)) :- appendc27(T47, T48, T49, X64).
appendc52([], T101, T102, .(T101, T102)).
appendc52(.(T113, T114), T115, T116, .(T113, T118)) :- appendc52(T114, T115, T116, T118).

Afs:

inorder1(x1, x2)  =  inorder1(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:
inorder1_in: (b,f)
inorder14_in: (b,f)
inorderc14_in: (b,f)
appendc27_in: (b,b,b,f)
append27_in: (b,b,b,f)
append52_in: (b,b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

INORDER1_IN_GA(tree(nil, T8, T9), T11) → U8_GA(T8, T9, T11, inorder14_in_ga(T9, X14))
INORDER1_IN_GA(tree(nil, T8, T9), T11) → INORDER14_IN_GA(T9, X14)
INORDER14_IN_GA(tree(T19, T20, T21), X37) → U1_GA(T19, T20, T21, X37, inorder14_in_ga(T19, X35))
INORDER14_IN_GA(tree(T19, T20, T21), X37) → INORDER14_IN_GA(T19, X35)
INORDER14_IN_GA(tree(T19, T20, T21), X37) → U2_GA(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U3_GA(T19, T20, T21, X37, inorder14_in_ga(T21, X36))
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → INORDER14_IN_GA(T21, X36)
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U4_GA(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U4_GA(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U5_GA(T19, T20, T21, X37, append27_in_ggga(T22, T20, T23, X37))
U4_GA(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → APPEND27_IN_GGGA(T22, T20, T23, X37)
APPEND27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → U6_GGGA(T46, T47, T48, T49, X64, append27_in_ggga(T47, T48, T49, X64))
APPEND27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → APPEND27_IN_GGGA(T47, T48, T49, X64)
INORDER1_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → U9_GA(T74, T75, T76, T8, T9, T11, inorder14_in_ga(T74, X99))
INORDER1_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → INORDER14_IN_GA(T74, X99)
INORDER1_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_in_ga(T74, T77))
U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_out_ga(T74, T77)) → U11_GA(T74, T75, T76, T8, T9, T11, inorder14_in_ga(T76, X100))
U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_out_ga(T74, T77)) → INORDER14_IN_GA(T76, X100)
U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_out_ga(T74, T77)) → U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_in_ga(T76, T78))
U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_out_ga(T76, T78)) → U13_GA(T74, T75, T76, T8, T9, T11, append27_in_ggga(T77, T75, T78, X101))
U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_out_ga(T76, T78)) → APPEND27_IN_GGGA(T77, T75, T78, X101)
U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_out_ga(T76, T78)) → U14_GA(T74, T75, T76, T8, T9, T11, appendc27_in_ggga(T77, T75, T78, T83))
U14_GA(T74, T75, T76, T8, T9, T11, appendc27_out_ggga(T77, T75, T78, T83)) → U15_GA(T74, T75, T76, T8, T9, T11, inorder14_in_ga(T9, X14))
U14_GA(T74, T75, T76, T8, T9, T11, appendc27_out_ggga(T77, T75, T78, T83)) → INORDER14_IN_GA(T9, X14)
U14_GA(T74, T75, T76, T8, T9, T11, appendc27_out_ggga(T77, T75, T78, T83)) → U16_GA(T74, T75, T76, T8, T9, T11, T83, inorderc14_in_ga(T9, T88))
U16_GA(T74, T75, T76, T8, T9, T11, T83, inorderc14_out_ga(T9, T88)) → U17_GA(T74, T75, T76, T8, T9, T11, append52_in_ggga(T83, T8, T88, T11))
U16_GA(T74, T75, T76, T8, T9, T11, T83, inorderc14_out_ga(T9, T88)) → APPEND52_IN_GGGA(T83, T8, T88, T11)
APPEND52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U7_GGGA(T113, T114, T115, T116, T118, append52_in_ggga(T114, T115, T116, T118))
APPEND52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPEND52_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

inorderc14_in_ga(nil, []) → inorderc14_out_ga(nil, [])
inorderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U19_ga(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U20_ga(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appendc27_in_ggga(T22, T20, T23, X37))
appendc27_in_ggga([], T36, T37, .(T36, T37)) → appendc27_out_ggga([], T36, T37, .(T36, T37))
appendc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appendc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appendc27_out_ggga(T47, T48, T49, X64)) → appendc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appendc27_out_ggga(T22, T20, T23, X37)) → inorderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
nil  =  nil
inorder14_in_ga(x1, x2)  =  inorder14_in_ga(x1)
inorderc14_in_ga(x1, x2)  =  inorderc14_in_ga(x1)
inorderc14_out_ga(x1, x2)  =  inorderc14_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)
appendc27_in_ggga(x1, x2, x3, x4)  =  appendc27_in_ggga(x1, x2, x3)
[]  =  []
appendc27_out_ggga(x1, x2, x3, x4)  =  appendc27_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)
append27_in_ggga(x1, x2, x3, x4)  =  append27_in_ggga(x1, x2, x3)
append52_in_ggga(x1, x2, x3, x4)  =  append52_in_ggga(x1, x2, x3)
INORDER1_IN_GA(x1, x2)  =  INORDER1_IN_GA(x1)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
INORDER14_IN_GA(x1, x2)  =  INORDER14_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)
APPEND27_IN_GGGA(x1, x2, x3, x4)  =  APPEND27_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)
APPEND52_IN_GGGA(x1, x2, x3, x4)  =  APPEND52_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:

INORDER1_IN_GA(tree(nil, T8, T9), T11) → U8_GA(T8, T9, T11, inorder14_in_ga(T9, X14))
INORDER1_IN_GA(tree(nil, T8, T9), T11) → INORDER14_IN_GA(T9, X14)
INORDER14_IN_GA(tree(T19, T20, T21), X37) → U1_GA(T19, T20, T21, X37, inorder14_in_ga(T19, X35))
INORDER14_IN_GA(tree(T19, T20, T21), X37) → INORDER14_IN_GA(T19, X35)
INORDER14_IN_GA(tree(T19, T20, T21), X37) → U2_GA(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U3_GA(T19, T20, T21, X37, inorder14_in_ga(T21, X36))
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → INORDER14_IN_GA(T21, X36)
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U4_GA(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U4_GA(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U5_GA(T19, T20, T21, X37, append27_in_ggga(T22, T20, T23, X37))
U4_GA(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → APPEND27_IN_GGGA(T22, T20, T23, X37)
APPEND27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → U6_GGGA(T46, T47, T48, T49, X64, append27_in_ggga(T47, T48, T49, X64))
APPEND27_IN_GGGA(.(T46, T47), T48, T49, .(T46, X64)) → APPEND27_IN_GGGA(T47, T48, T49, X64)
INORDER1_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → U9_GA(T74, T75, T76, T8, T9, T11, inorder14_in_ga(T74, X99))
INORDER1_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → INORDER14_IN_GA(T74, X99)
INORDER1_IN_GA(tree(tree(T74, T75, T76), T8, T9), T11) → U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_in_ga(T74, T77))
U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_out_ga(T74, T77)) → U11_GA(T74, T75, T76, T8, T9, T11, inorder14_in_ga(T76, X100))
U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_out_ga(T74, T77)) → INORDER14_IN_GA(T76, X100)
U10_GA(T74, T75, T76, T8, T9, T11, inorderc14_out_ga(T74, T77)) → U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_in_ga(T76, T78))
U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_out_ga(T76, T78)) → U13_GA(T74, T75, T76, T8, T9, T11, append27_in_ggga(T77, T75, T78, X101))
U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_out_ga(T76, T78)) → APPEND27_IN_GGGA(T77, T75, T78, X101)
U12_GA(T74, T75, T76, T8, T9, T11, T77, inorderc14_out_ga(T76, T78)) → U14_GA(T74, T75, T76, T8, T9, T11, appendc27_in_ggga(T77, T75, T78, T83))
U14_GA(T74, T75, T76, T8, T9, T11, appendc27_out_ggga(T77, T75, T78, T83)) → U15_GA(T74, T75, T76, T8, T9, T11, inorder14_in_ga(T9, X14))
U14_GA(T74, T75, T76, T8, T9, T11, appendc27_out_ggga(T77, T75, T78, T83)) → INORDER14_IN_GA(T9, X14)
U14_GA(T74, T75, T76, T8, T9, T11, appendc27_out_ggga(T77, T75, T78, T83)) → U16_GA(T74, T75, T76, T8, T9, T11, T83, inorderc14_in_ga(T9, T88))
U16_GA(T74, T75, T76, T8, T9, T11, T83, inorderc14_out_ga(T9, T88)) → U17_GA(T74, T75, T76, T8, T9, T11, append52_in_ggga(T83, T8, T88, T11))
U16_GA(T74, T75, T76, T8, T9, T11, T83, inorderc14_out_ga(T9, T88)) → APPEND52_IN_GGGA(T83, T8, T88, T11)
APPEND52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → U7_GGGA(T113, T114, T115, T116, T118, append52_in_ggga(T114, T115, T116, T118))
APPEND52_IN_GGGA(.(T113, T114), T115, T116, .(T113, T118)) → APPEND52_IN_GGGA(T114, T115, T116, T118)

The TRS R consists of the following rules:

inorderc14_in_ga(nil, []) → inorderc14_out_ga(nil, [])
inorderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U19_ga(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U20_ga(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appendc27_in_ggga(T22, T20, T23, X37))
appendc27_in_ggga([], T36, T37, .(T36, T37)) → appendc27_out_ggga([], T36, T37, .(T36, T37))
appendc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appendc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appendc27_out_ggga(T47, T48, T49, X64)) → appendc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appendc27_out_ggga(T22, T20, T23, X37)) → inorderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
nil  =  nil
inorder14_in_ga(x1, x2)  =  inorder14_in_ga(x1)
inorderc14_in_ga(x1, x2)  =  inorderc14_in_ga(x1)
inorderc14_out_ga(x1, x2)  =  inorderc14_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)
appendc27_in_ggga(x1, x2, x3, x4)  =  appendc27_in_ggga(x1, x2, x3)
[]  =  []
appendc27_out_ggga(x1, x2, x3, x4)  =  appendc27_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)
append27_in_ggga(x1, x2, x3, x4)  =  append27_in_ggga(x1, x2, x3)
append52_in_ggga(x1, x2, x3, x4)  =  append52_in_ggga(x1, x2, x3)
INORDER1_IN_GA(x1, x2)  =  INORDER1_IN_GA(x1)
U8_GA(x1, x2, x3, x4)  =  U8_GA(x1, x2, x4)
INORDER14_IN_GA(x1, x2)  =  INORDER14_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)
APPEND27_IN_GGGA(x1, x2, x3, x4)  =  APPEND27_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)
APPEND52_IN_GGGA(x1, x2, x3, x4)  =  APPEND52_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:

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

The TRS R consists of the following rules:

inorderc14_in_ga(nil, []) → inorderc14_out_ga(nil, [])
inorderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U19_ga(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U20_ga(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appendc27_in_ggga(T22, T20, T23, X37))
appendc27_in_ggga([], T36, T37, .(T36, T37)) → appendc27_out_ggga([], T36, T37, .(T36, T37))
appendc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appendc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appendc27_out_ggga(T47, T48, T49, X64)) → appendc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appendc27_out_ggga(T22, T20, T23, X37)) → inorderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
nil  =  nil
inorderc14_in_ga(x1, x2)  =  inorderc14_in_ga(x1)
inorderc14_out_ga(x1, x2)  =  inorderc14_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)
appendc27_in_ggga(x1, x2, x3, x4)  =  appendc27_in_ggga(x1, x2, x3)
[]  =  []
appendc27_out_ggga(x1, x2, x3, x4)  =  appendc27_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)
APPEND52_IN_GGGA(x1, x2, x3, x4)  =  APPEND52_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:

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

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

APPEND52_IN_GGGA(.(T113, T114), T115, T116) → APPEND52_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:

  • APPEND52_IN_GGGA(.(T113, T114), T115, T116) → APPEND52_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:

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

The TRS R consists of the following rules:

inorderc14_in_ga(nil, []) → inorderc14_out_ga(nil, [])
inorderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U19_ga(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U20_ga(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appendc27_in_ggga(T22, T20, T23, X37))
appendc27_in_ggga([], T36, T37, .(T36, T37)) → appendc27_out_ggga([], T36, T37, .(T36, T37))
appendc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appendc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appendc27_out_ggga(T47, T48, T49, X64)) → appendc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appendc27_out_ggga(T22, T20, T23, X37)) → inorderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
nil  =  nil
inorderc14_in_ga(x1, x2)  =  inorderc14_in_ga(x1)
inorderc14_out_ga(x1, x2)  =  inorderc14_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)
appendc27_in_ggga(x1, x2, x3, x4)  =  appendc27_in_ggga(x1, x2, x3)
[]  =  []
appendc27_out_ggga(x1, x2, x3, x4)  =  appendc27_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)
APPEND27_IN_GGGA(x1, x2, x3, x4)  =  APPEND27_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:

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

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

APPEND27_IN_GGGA(.(T46, T47), T48, T49) → APPEND27_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:

  • APPEND27_IN_GGGA(.(T46, T47), T48, T49) → APPEND27_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:

INORDER14_IN_GA(tree(T19, T20, T21), X37) → U2_GA(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U2_GA(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → INORDER14_IN_GA(T21, X36)
INORDER14_IN_GA(tree(T19, T20, T21), X37) → INORDER14_IN_GA(T19, X35)

The TRS R consists of the following rules:

inorderc14_in_ga(nil, []) → inorderc14_out_ga(nil, [])
inorderc14_in_ga(tree(T19, T20, T21), X37) → U19_ga(T19, T20, T21, X37, inorderc14_in_ga(T19, T22))
U19_ga(T19, T20, T21, X37, inorderc14_out_ga(T19, T22)) → U20_ga(T19, T20, T21, X37, T22, inorderc14_in_ga(T21, T23))
U20_ga(T19, T20, T21, X37, T22, inorderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, X37, appendc27_in_ggga(T22, T20, T23, X37))
appendc27_in_ggga([], T36, T37, .(T36, T37)) → appendc27_out_ggga([], T36, T37, .(T36, T37))
appendc27_in_ggga(.(T46, T47), T48, T49, .(T46, X64)) → U22_ggga(T46, T47, T48, T49, X64, appendc27_in_ggga(T47, T48, T49, X64))
U22_ggga(T46, T47, T48, T49, X64, appendc27_out_ggga(T47, T48, T49, X64)) → appendc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, X37, appendc27_out_ggga(T22, T20, T23, X37)) → inorderc14_out_ga(tree(T19, T20, T21), X37)

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
nil  =  nil
inorderc14_in_ga(x1, x2)  =  inorderc14_in_ga(x1)
inorderc14_out_ga(x1, x2)  =  inorderc14_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)
appendc27_in_ggga(x1, x2, x3, x4)  =  appendc27_in_ggga(x1, x2, x3)
[]  =  []
appendc27_out_ggga(x1, x2, x3, x4)  =  appendc27_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)
INORDER14_IN_GA(x1, x2)  =  INORDER14_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:

INORDER14_IN_GA(tree(T19, T20, T21)) → U2_GA(T19, T20, T21, inorderc14_in_ga(T19))
U2_GA(T19, T20, T21, inorderc14_out_ga(T19, T22)) → INORDER14_IN_GA(T21)
INORDER14_IN_GA(tree(T19, T20, T21)) → INORDER14_IN_GA(T19)

The TRS R consists of the following rules:

inorderc14_in_ga(nil) → inorderc14_out_ga(nil, [])
inorderc14_in_ga(tree(T19, T20, T21)) → U19_ga(T19, T20, T21, inorderc14_in_ga(T19))
U19_ga(T19, T20, T21, inorderc14_out_ga(T19, T22)) → U20_ga(T19, T20, T21, T22, inorderc14_in_ga(T21))
U20_ga(T19, T20, T21, T22, inorderc14_out_ga(T21, T23)) → U21_ga(T19, T20, T21, appendc27_in_ggga(T22, T20, T23))
appendc27_in_ggga([], T36, T37) → appendc27_out_ggga([], T36, T37, .(T36, T37))
appendc27_in_ggga(.(T46, T47), T48, T49) → U22_ggga(T46, T47, T48, T49, appendc27_in_ggga(T47, T48, T49))
U22_ggga(T46, T47, T48, T49, appendc27_out_ggga(T47, T48, T49, X64)) → appendc27_out_ggga(.(T46, T47), T48, T49, .(T46, X64))
U21_ga(T19, T20, T21, appendc27_out_ggga(T22, T20, T23, X37)) → inorderc14_out_ga(tree(T19, T20, T21), X37)

The set Q consists of the following terms:

inorderc14_in_ga(x0)
U19_ga(x0, x1, x2, x3)
U20_ga(x0, x1, x2, x3, x4)
appendc27_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, inorderc14_out_ga(T19, T22)) → INORDER14_IN_GA(T21)
    The graph contains the following edges 3 >= 1

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

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

(25) YES