(0) Obligation:

Clauses:

goal(A, B, C) :- ','(s2t(A, T), tapplast(T, B, C)).
tapplast(L, X, Last) :- ','(tappend(L, node(nil, X, nil), LX), tlast(Last, LX)).
tlast(X, node(nil, X, nil)).
tlast(X, node(L, X1, X2)) :- tlast(X, L).
tlast(X, node(X3, X4, R)) :- tlast(X, R).
tappend(nil, Y, Z) :- ','(!, eq(Y, Z)).
tappend(T, T1, node(T1, X, T2)) :- ','(left(T, nil), ','(right(T, T2), value(T, X))).
tappend(T, T2, node(T1, X, T2)) :- ','(left(T, T1), ','(right(T, nil), value(T, X))).
tappend(T, T3, node(U, X, T2)) :- ','(left(T, T1), ','(right(T, T2), ','(value(T, X), tappend(T1, T3, U)))).
tappend(T, T1, node(T1, X, U)) :- ','(left(T, T1), ','(right(T, T2), ','(value(T, X), tappend(T2, T3, U)))).
s2t(0, L) :- ','(!, eq(L, nil)).
s2t(X, node(T, X5, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X6, T)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(T, X7, nil)) :- ','(p(X, P), s2t(P, T)).
s2t(X, node(nil, X8, nil)).
left(nil, nil).
left(node(L, X9, X10), L).
right(nil, nil).
right(node(X11, X12, R), R).
value(nil, nil).
value(node(X13, X, X14), X).
p(0, 0).
p(s(X), X).
eq(X, X).

Queries:

goal(g,a,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

tlast13(T71, node(T72, T69, T70)) :- tlast13(T71, T72).
tlast13(T87, node(T84, T85, T88)) :- tlast13(T87, T88).
s2t39(s(T107), node(X217, X218, X217)) :- s2t39(T107, X217).
s2t39(s(T115), node(nil, X257, X258)) :- s2t39(T115, X258).
s2t39(s(T123), node(X297, X298, nil)) :- s2t39(T123, X297).
tappend116(nil, T345, node(X818, nil, nil)) :- tappend12(T345, X818).
tappend116(node(T398, T396, T397), T399, node(X818, T396, T397)) :- tappend116(T398, T399, X818).
tappend116(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) :- tappend217(T451, X919, X921).
tappend217(nil, X1193, node(X1194, nil, nil)) :- tappend217(nil, X1193, X1194).
tappend217(node(T569, T567, T568), X1193, node(X1194, T567, T568)) :- tappend217(T569, X1193, X1194).
tappend217(nil, nil, node(nil, nil, X1313)) :- tappend217(nil, X1310, X1313).
tappend217(node(T609, T610, T612), T609, node(T609, T610, X1313)) :- tappend217(T612, X1310, X1313).
p72(T234, X619, T235, node(X563, X619, T234), T146) :- tappend116(T234, T235, X563).
p72(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) :- tappend217(node(nil, T642, nil), X1427, X1430).
p72(T144, T149, T145, T150, T151) :- ','(tappendc73(T144, T149, T145, T150), tlast13(T151, T150)).
goal1(0, T30, T31) :- tappend12(T30, X61).
goal1(0, T30, T34) :- ','(tappendc12(T30, T33), tlast13(T34, T33)).
goal1(s(T98), T13, T14) :- s2t39(T98, X162).
goal1(s(T98), T145, T146) :- ','(s2tc39(T98, T144), p72(T144, X343, T145, X342, T146)).
goal1(s(T653), T13, T14) :- s2t39(T653, X1547).
goal1(s(T653), T673, T674) :- ','(s2tc39(T653, T672), tappend116(node(nil, X1585, T672), T673, X1584)).
goal1(s(T653), T673, T679) :- ','(s2tc39(T653, T672), ','(tappendc116(node(nil, T677, T672), T673, T678), tlast13(T679, T678))).
goal1(s(T691), T13, T14) :- s2t39(T691, X1636).
goal1(s(T691), T711, T712) :- ','(s2tc39(T691, T710), tappend116(node(T710, X1675, nil), T711, X1674)).
goal1(s(T691), T711, T717) :- ','(s2tc39(T691, T710), ','(tappendc116(node(T710, T715, nil), T711, T716), tlast13(T717, T716))).
goal1(T726, T738, T739) :- p72(nil, X1737, T738, X1736, T739).

Clauses:

tlastc13(T50, node(nil, T50, nil)).
tlastc13(T71, node(T72, T69, T70)) :- tlastc13(T71, T72).
tlastc13(T87, node(T84, T85, T88)) :- tlastc13(T87, T88).
s2tc39(0, nil).
s2tc39(s(T107), node(X217, X218, X217)) :- s2tc39(T107, X217).
s2tc39(s(T115), node(nil, X257, X258)) :- s2tc39(T115, X258).
s2tc39(s(T123), node(X297, X298, nil)) :- s2tc39(T123, X297).
s2tc39(T126, node(nil, X315, nil)).
tappendc12(T43, node(nil, T43, nil)).
tappendc116(nil, T243, node(nil, T243, nil)).
tappendc116(nil, T255, node(node(nil, T255, nil), nil, nil)).
tappendc116(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)).
tappendc116(nil, T295, node(nil, nil, node(nil, T295, nil))).
tappendc116(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))).
tappendc116(nil, T345, node(X818, nil, nil)) :- tappendc12(T345, X818).
tappendc116(node(T398, T396, T397), T399, node(X818, T396, T397)) :- tappendc116(T398, T399, X818).
tappendc116(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) :- tappendc217(T451, X919, X921).
tappendc217(nil, X995, X995).
tappendc217(nil, X1028, node(X1028, nil, nil)).
tappendc217(node(nil, T485, T486), X1028, node(X1028, T485, T486)).
tappendc217(nil, X1099, node(nil, nil, X1099)).
tappendc217(node(T522, T523, nil), X1099, node(T522, T523, X1099)).
tappendc217(nil, X1193, node(X1194, nil, nil)) :- tappendc217(nil, X1193, X1194).
tappendc217(node(T569, T567, T568), X1193, node(X1194, T567, T568)) :- tappendc217(T569, X1193, X1194).
tappendc217(nil, nil, node(nil, nil, X1313)) :- tappendc217(nil, X1310, X1313).
tappendc217(node(T609, T610, T612), T609, node(T609, T610, X1313)) :- tappendc217(T612, X1310, X1313).
qc72(T144, T149, T145, T150, T151) :- ','(tappendc73(T144, T149, T145, T150), tlastc13(T151, T150)).
tappendc73(nil, X437, T165, node(node(nil, T165, nil), X437, nil)).
tappendc73(nil, X511, T181, node(nil, X511, node(nil, T181, nil))).
tappendc73(T234, X619, T235, node(X563, X619, T234)) :- tappendc116(T234, T235, X563).
tappendc73(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) :- tappendc217(node(nil, T642, nil), X1427, X1430).

Afs:

goal1(x1, x2, x3)  =  goal1(x1)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

tlast13(T71, node(T72, T69, T70)) :- tlast13(T71, T72).
tlast13(T87, node(T84, T85, T88)) :- tlast13(T87, T88).
s2t39(s(T107), node(X217, X218, X217)) :- s2t39(T107, X217).
s2t39(s(T115), node(nil, X257, X258)) :- s2t39(T115, X258).
s2t39(s(T123), node(X297, X298, nil)) :- s2t39(T123, X297).
tappend116(node(T398, T396, T397), T399, node(X818, T396, T397)) :- tappend116(T398, T399, X818).
tappend116(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) :- tappend217(T451, X919, X921).
tappend217(nil, X1193, node(X1194, nil, nil)) :- tappend217(nil, X1193, X1194).
tappend217(node(T569, T567, T568), X1193, node(X1194, T567, T568)) :- tappend217(T569, X1193, X1194).
tappend217(nil, nil, node(nil, nil, X1313)) :- tappend217(nil, X1310, X1313).
tappend217(node(T609, T610, T612), T609, node(T609, T610, X1313)) :- tappend217(T612, X1310, X1313).
p72(T234, X619, T235, node(X563, X619, T234), T146) :- tappend116(T234, T235, X563).
p72(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) :- tappend217(node(nil, T642, nil), X1427, X1430).
p72(T144, T149, T145, T150, T151) :- ','(tappendc73(T144, T149, T145, T150), tlast13(T151, T150)).
goal1(0, T30, T34) :- ','(tappendc12(T30, T33), tlast13(T34, T33)).
goal1(s(T98), T13, T14) :- s2t39(T98, X162).
goal1(s(T98), T145, T146) :- ','(s2tc39(T98, T144), p72(T144, X343, T145, X342, T146)).
goal1(s(T653), T13, T14) :- s2t39(T653, X1547).
goal1(s(T653), T673, T674) :- ','(s2tc39(T653, T672), tappend116(node(nil, X1585, T672), T673, X1584)).
goal1(s(T653), T673, T679) :- ','(s2tc39(T653, T672), ','(tappendc116(node(nil, T677, T672), T673, T678), tlast13(T679, T678))).
goal1(s(T691), T13, T14) :- s2t39(T691, X1636).
goal1(s(T691), T711, T712) :- ','(s2tc39(T691, T710), tappend116(node(T710, X1675, nil), T711, X1674)).
goal1(s(T691), T711, T717) :- ','(s2tc39(T691, T710), ','(tappendc116(node(T710, T715, nil), T711, T716), tlast13(T717, T716))).
goal1(T726, T738, T739) :- p72(nil, X1737, T738, X1736, T739).

Clauses:

tlastc13(T50, node(nil, T50, nil)).
tlastc13(T71, node(T72, T69, T70)) :- tlastc13(T71, T72).
tlastc13(T87, node(T84, T85, T88)) :- tlastc13(T87, T88).
s2tc39(0, nil).
s2tc39(s(T107), node(X217, X218, X217)) :- s2tc39(T107, X217).
s2tc39(s(T115), node(nil, X257, X258)) :- s2tc39(T115, X258).
s2tc39(s(T123), node(X297, X298, nil)) :- s2tc39(T123, X297).
s2tc39(T126, node(nil, X315, nil)).
tappendc12(T43, node(nil, T43, nil)).
tappendc116(nil, T243, node(nil, T243, nil)).
tappendc116(nil, T255, node(node(nil, T255, nil), nil, nil)).
tappendc116(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)).
tappendc116(nil, T295, node(nil, nil, node(nil, T295, nil))).
tappendc116(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))).
tappendc116(nil, T345, node(X818, nil, nil)) :- tappendc12(T345, X818).
tappendc116(node(T398, T396, T397), T399, node(X818, T396, T397)) :- tappendc116(T398, T399, X818).
tappendc116(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) :- tappendc217(T451, X919, X921).
tappendc217(nil, X995, X995).
tappendc217(nil, X1028, node(X1028, nil, nil)).
tappendc217(node(nil, T485, T486), X1028, node(X1028, T485, T486)).
tappendc217(nil, X1099, node(nil, nil, X1099)).
tappendc217(node(T522, T523, nil), X1099, node(T522, T523, X1099)).
tappendc217(nil, X1193, node(X1194, nil, nil)) :- tappendc217(nil, X1193, X1194).
tappendc217(node(T569, T567, T568), X1193, node(X1194, T567, T568)) :- tappendc217(T569, X1193, X1194).
tappendc217(nil, nil, node(nil, nil, X1313)) :- tappendc217(nil, X1310, X1313).
tappendc217(node(T609, T610, T612), T609, node(T609, T610, X1313)) :- tappendc217(T612, X1310, X1313).
qc72(T144, T149, T145, T150, T151) :- ','(tappendc73(T144, T149, T145, T150), tlastc13(T151, T150)).
tappendc73(nil, X437, T165, node(node(nil, T165, nil), X437, nil)).
tappendc73(nil, X511, T181, node(nil, X511, node(nil, T181, nil))).
tappendc73(T234, X619, T235, node(X563, X619, T234)) :- tappendc116(T234, T235, X563).
tappendc73(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) :- tappendc217(node(nil, T642, nil), X1427, X1430).

Afs:

goal1(x1, x2, x3)  =  goal1(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:
goal1_in: (b,f,f)
tlast13_in: (f,f)
s2t39_in: (b,f)
s2tc39_in: (b,f)
p72_in: (f,f,f,f,f) (b,f,f,f,f)
tappend116_in: (f,f,f) (b,f,f)
tappend217_in: (f,f,f) (b,f,f)
tappendc73_in: (f,f,f,f) (b,f,f,f)
tappendc116_in: (f,f,f) (b,f,f)
tappendc217_in: (f,f,f) (b,f,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

GOAL1_IN_GAA(0, T30, T34) → U16_GAA(T30, T34, tappendc12_in_aa(T30, T33))
U16_GAA(T30, T34, tappendc12_out_aa(T30, T33)) → U17_GAA(T30, T34, tlast13_in_aa(T34, T33))
U16_GAA(T30, T34, tappendc12_out_aa(T30, T33)) → TLAST13_IN_AA(T34, T33)
TLAST13_IN_AA(T71, node(T72, T69, T70)) → U1_AA(T71, T72, T69, T70, tlast13_in_aa(T71, T72))
TLAST13_IN_AA(T71, node(T72, T69, T70)) → TLAST13_IN_AA(T71, T72)
TLAST13_IN_AA(T87, node(T84, T85, T88)) → U2_AA(T87, T84, T85, T88, tlast13_in_aa(T87, T88))
TLAST13_IN_AA(T87, node(T84, T85, T88)) → TLAST13_IN_AA(T87, T88)
GOAL1_IN_GAA(s(T98), T13, T14) → U18_GAA(T98, T13, T14, s2t39_in_ga(T98, X162))
GOAL1_IN_GAA(s(T98), T13, T14) → S2T39_IN_GA(T98, X162)
S2T39_IN_GA(s(T107), node(X217, X218, X217)) → U3_GA(T107, X217, X218, s2t39_in_ga(T107, X217))
S2T39_IN_GA(s(T107), node(X217, X218, X217)) → S2T39_IN_GA(T107, X217)
S2T39_IN_GA(s(T115), node(nil, X257, X258)) → U4_GA(T115, X257, X258, s2t39_in_ga(T115, X258))
S2T39_IN_GA(s(T115), node(nil, X257, X258)) → S2T39_IN_GA(T115, X258)
S2T39_IN_GA(s(T123), node(X297, X298, nil)) → U5_GA(T123, X297, X298, s2t39_in_ga(T123, X297))
S2T39_IN_GA(s(T123), node(X297, X298, nil)) → S2T39_IN_GA(T123, X297)
GOAL1_IN_GAA(s(T98), T145, T146) → U19_GAA(T98, T145, T146, s2tc39_in_ga(T98, T144))
U19_GAA(T98, T145, T146, s2tc39_out_ga(T98, T144)) → U20_GAA(T98, T145, T146, p72_in_aaaaa(T144, X343, T145, X342, T146))
U19_GAA(T98, T145, T146, s2tc39_out_ga(T98, T144)) → P72_IN_AAAAA(T144, X343, T145, X342, T146)
P72_IN_AAAAA(T234, X619, T235, node(X563, X619, T234), T146) → U12_AAAAA(T234, X619, T235, X563, T146, tappend116_in_aaa(T234, T235, X563))
P72_IN_AAAAA(T234, X619, T235, node(X563, X619, T234), T146) → TAPPEND116_IN_AAA(T234, T235, X563)
TAPPEND116_IN_AAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → U6_AAA(T398, T396, T397, T399, X818, tappend116_in_aaa(T398, T399, X818))
TAPPEND116_IN_AAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_AAA(T398, T399, X818)
TAPPEND116_IN_AAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U7_AAA(T448, T449, T451, X921, tappend217_in_aaa(T451, X919, X921))
TAPPEND116_IN_AAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → TAPPEND217_IN_AAA(T451, X919, X921)
TAPPEND217_IN_AAA(nil, X1193, node(X1194, nil, nil)) → U8_AAA(X1193, X1194, tappend217_in_gaa(nil, X1193, X1194))
TAPPEND217_IN_AAA(nil, X1193, node(X1194, nil, nil)) → TAPPEND217_IN_GAA(nil, X1193, X1194)
TAPPEND217_IN_GAA(nil, X1193, node(X1194, nil, nil)) → U8_GAA(X1193, X1194, tappend217_in_gaa(nil, X1193, X1194))
TAPPEND217_IN_GAA(nil, X1193, node(X1194, nil, nil)) → TAPPEND217_IN_GAA(nil, X1193, X1194)
TAPPEND217_IN_GAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U9_GAA(T569, T567, T568, X1193, X1194, tappend217_in_gaa(T569, X1193, X1194))
TAPPEND217_IN_GAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_GAA(T569, X1193, X1194)
TAPPEND217_IN_GAA(nil, nil, node(nil, nil, X1313)) → U10_GAA(X1313, tappend217_in_gaa(nil, X1310, X1313))
TAPPEND217_IN_GAA(nil, nil, node(nil, nil, X1313)) → TAPPEND217_IN_GAA(nil, X1310, X1313)
TAPPEND217_IN_GAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U11_GAA(T609, T610, T612, X1313, tappend217_in_gaa(T612, X1310, X1313))
TAPPEND217_IN_GAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_GAA(T612, X1310, X1313)
TAPPEND217_IN_AAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U9_AAA(T569, T567, T568, X1193, X1194, tappend217_in_aaa(T569, X1193, X1194))
TAPPEND217_IN_AAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_AAA(T569, X1193, X1194)
TAPPEND217_IN_AAA(nil, nil, node(nil, nil, X1313)) → U10_AAA(X1313, tappend217_in_gaa(nil, X1310, X1313))
TAPPEND217_IN_AAA(nil, nil, node(nil, nil, X1313)) → TAPPEND217_IN_GAA(nil, X1310, X1313)
TAPPEND217_IN_AAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U11_AAA(T609, T610, T612, X1313, tappend217_in_aaa(T612, X1310, X1313))
TAPPEND217_IN_AAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_AAA(T612, X1310, X1313)
P72_IN_AAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → U13_AAAAA(T642, X1504, X1430, T146, tappend217_in_aaa(node(nil, T642, nil), X1427, X1430))
P72_IN_AAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → TAPPEND217_IN_AAA(node(nil, T642, nil), X1427, X1430)
P72_IN_AAAAA(T144, T149, T145, T150, T151) → U14_AAAAA(T144, T149, T145, T150, T151, tappendc73_in_aaaa(T144, T149, T145, T150))
U14_AAAAA(T144, T149, T145, T150, T151, tappendc73_out_aaaa(T144, T149, T145, T150)) → U15_AAAAA(T144, T149, T145, T150, T151, tlast13_in_aa(T151, T150))
U14_AAAAA(T144, T149, T145, T150, T151, tappendc73_out_aaaa(T144, T149, T145, T150)) → TLAST13_IN_AA(T151, T150)
GOAL1_IN_GAA(s(T653), T13, T14) → U21_GAA(T653, T13, T14, s2t39_in_ga(T653, X1547))
GOAL1_IN_GAA(s(T653), T673, T674) → U22_GAA(T653, T673, T674, s2tc39_in_ga(T653, T672))
U22_GAA(T653, T673, T674, s2tc39_out_ga(T653, T672)) → U23_GAA(T653, T673, T674, tappend116_in_aaa(node(nil, X1585, T672), T673, X1584))
U22_GAA(T653, T673, T674, s2tc39_out_ga(T653, T672)) → TAPPEND116_IN_AAA(node(nil, X1585, T672), T673, X1584)
GOAL1_IN_GAA(s(T653), T673, T679) → U24_GAA(T653, T673, T679, s2tc39_in_ga(T653, T672))
U24_GAA(T653, T673, T679, s2tc39_out_ga(T653, T672)) → U25_GAA(T653, T673, T679, tappendc116_in_aaa(node(nil, T677, T672), T673, T678))
U25_GAA(T653, T673, T679, tappendc116_out_aaa(node(nil, T677, T672), T673, T678)) → U26_GAA(T653, T673, T679, tlast13_in_aa(T679, T678))
U25_GAA(T653, T673, T679, tappendc116_out_aaa(node(nil, T677, T672), T673, T678)) → TLAST13_IN_AA(T679, T678)
GOAL1_IN_GAA(s(T691), T13, T14) → U27_GAA(T691, T13, T14, s2t39_in_ga(T691, X1636))
GOAL1_IN_GAA(s(T691), T711, T712) → U28_GAA(T691, T711, T712, s2tc39_in_ga(T691, T710))
U28_GAA(T691, T711, T712, s2tc39_out_ga(T691, T710)) → U29_GAA(T691, T711, T712, tappend116_in_aaa(node(T710, X1675, nil), T711, X1674))
U28_GAA(T691, T711, T712, s2tc39_out_ga(T691, T710)) → TAPPEND116_IN_AAA(node(T710, X1675, nil), T711, X1674)
GOAL1_IN_GAA(s(T691), T711, T717) → U30_GAA(T691, T711, T717, s2tc39_in_ga(T691, T710))
U30_GAA(T691, T711, T717, s2tc39_out_ga(T691, T710)) → U31_GAA(T691, T711, T717, tappendc116_in_aaa(node(T710, T715, nil), T711, T716))
U31_GAA(T691, T711, T717, tappendc116_out_aaa(node(T710, T715, nil), T711, T716)) → U32_GAA(T691, T711, T717, tlast13_in_aa(T717, T716))
U31_GAA(T691, T711, T717, tappendc116_out_aaa(node(T710, T715, nil), T711, T716)) → TLAST13_IN_AA(T717, T716)
GOAL1_IN_GAA(T726, T738, T739) → U33_GAA(T726, T738, T739, p72_in_gaaaa(nil, X1737, T738, X1736, T739))
GOAL1_IN_GAA(T726, T738, T739) → P72_IN_GAAAA(nil, X1737, T738, X1736, T739)
P72_IN_GAAAA(T234, X619, T235, node(X563, X619, T234), T146) → U12_GAAAA(T234, X619, T235, X563, T146, tappend116_in_gaa(T234, T235, X563))
P72_IN_GAAAA(T234, X619, T235, node(X563, X619, T234), T146) → TAPPEND116_IN_GAA(T234, T235, X563)
TAPPEND116_IN_GAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → U6_GAA(T398, T396, T397, T399, X818, tappend116_in_gaa(T398, T399, X818))
TAPPEND116_IN_GAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_GAA(T398, T399, X818)
TAPPEND116_IN_GAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U7_GAA(T448, T449, T451, X921, tappend217_in_gaa(T451, X919, X921))
TAPPEND116_IN_GAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → TAPPEND217_IN_GAA(T451, X919, X921)
P72_IN_GAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → U13_GAAAA(T642, X1504, X1430, T146, tappend217_in_gaa(node(nil, T642, nil), X1427, X1430))
P72_IN_GAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → TAPPEND217_IN_GAA(node(nil, T642, nil), X1427, X1430)
P72_IN_GAAAA(T144, T149, T145, T150, T151) → U14_GAAAA(T144, T149, T145, T150, T151, tappendc73_in_gaaa(T144, T149, T145, T150))
U14_GAAAA(T144, T149, T145, T150, T151, tappendc73_out_gaaa(T144, T149, T145, T150)) → U15_GAAAA(T144, T149, T145, T150, T151, tlast13_in_aa(T151, T150))
U14_GAAAA(T144, T149, T145, T150, T151, tappendc73_out_gaaa(T144, T149, T145, T150)) → TLAST13_IN_AA(T151, T150)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
tlast13_in_aa(x1, x2)  =  tlast13_in_aa
s(x1)  =  s(x1)
s2t39_in_ga(x1, x2)  =  s2t39_in_ga(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
p72_in_aaaaa(x1, x2, x3, x4, x5)  =  p72_in_aaaaa
tappend116_in_aaa(x1, x2, x3)  =  tappend116_in_aaa
tappend217_in_aaa(x1, x2, x3)  =  tappend217_in_aaa
tappend217_in_gaa(x1, x2, x3)  =  tappend217_in_gaa(x1)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
p72_in_gaaaa(x1, x2, x3, x4, x5)  =  p72_in_gaaaa(x1)
tappend116_in_gaa(x1, x2, x3)  =  tappend116_in_gaa(x1)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
GOAL1_IN_GAA(x1, x2, x3)  =  GOAL1_IN_GAA(x1)
U16_GAA(x1, x2, x3)  =  U16_GAA(x3)
U17_GAA(x1, x2, x3)  =  U17_GAA(x3)
TLAST13_IN_AA(x1, x2)  =  TLAST13_IN_AA
U1_AA(x1, x2, x3, x4, x5)  =  U1_AA(x5)
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
S2T39_IN_GA(x1, x2)  =  S2T39_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x4)
P72_IN_AAAAA(x1, x2, x3, x4, x5)  =  P72_IN_AAAAA
U12_AAAAA(x1, x2, x3, x4, x5, x6)  =  U12_AAAAA(x6)
TAPPEND116_IN_AAA(x1, x2, x3)  =  TAPPEND116_IN_AAA
U6_AAA(x1, x2, x3, x4, x5, x6)  =  U6_AAA(x6)
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)
TAPPEND217_IN_AAA(x1, x2, x3)  =  TAPPEND217_IN_AAA
U8_AAA(x1, x2, x3)  =  U8_AAA(x3)
TAPPEND217_IN_GAA(x1, x2, x3)  =  TAPPEND217_IN_GAA(x1)
U8_GAA(x1, x2, x3)  =  U8_GAA(x3)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x3, x6)
U10_GAA(x1, x2)  =  U10_GAA(x2)
U11_GAA(x1, x2, x3, x4, x5)  =  U11_GAA(x1, x2, x3, x5)
U9_AAA(x1, x2, x3, x4, x5, x6)  =  U9_AAA(x6)
U10_AAA(x1, x2)  =  U10_AAA(x2)
U11_AAA(x1, x2, x3, x4, x5)  =  U11_AAA(x5)
U13_AAAAA(x1, x2, x3, x4, x5)  =  U13_AAAAA(x5)
U14_AAAAA(x1, x2, x3, x4, x5, x6)  =  U14_AAAAA(x6)
U15_AAAAA(x1, x2, x3, x4, x5, x6)  =  U15_AAAAA(x6)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x4)
U22_GAA(x1, x2, x3, x4)  =  U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4)  =  U23_GAA(x1, x4)
U24_GAA(x1, x2, x3, x4)  =  U24_GAA(x1, x4)
U25_GAA(x1, x2, x3, x4)  =  U25_GAA(x1, x4)
U26_GAA(x1, x2, x3, x4)  =  U26_GAA(x1, x4)
U27_GAA(x1, x2, x3, x4)  =  U27_GAA(x1, x4)
U28_GAA(x1, x2, x3, x4)  =  U28_GAA(x1, x4)
U29_GAA(x1, x2, x3, x4)  =  U29_GAA(x1, x4)
U30_GAA(x1, x2, x3, x4)  =  U30_GAA(x1, x4)
U31_GAA(x1, x2, x3, x4)  =  U31_GAA(x1, x4)
U32_GAA(x1, x2, x3, x4)  =  U32_GAA(x1, x4)
U33_GAA(x1, x2, x3, x4)  =  U33_GAA(x1, x4)
P72_IN_GAAAA(x1, x2, x3, x4, x5)  =  P72_IN_GAAAA(x1)
U12_GAAAA(x1, x2, x3, x4, x5, x6)  =  U12_GAAAA(x1, x6)
TAPPEND116_IN_GAA(x1, x2, x3)  =  TAPPEND116_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x1, x2, x3, x6)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x1, x2, x3, x5)
U13_GAAAA(x1, x2, x3, x4, x5)  =  U13_GAAAA(x1, x5)
U14_GAAAA(x1, x2, x3, x4, x5, x6)  =  U14_GAAAA(x1, x6)
U15_GAAAA(x1, x2, x3, x4, x5, x6)  =  U15_GAAAA(x1, x6)

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:

GOAL1_IN_GAA(0, T30, T34) → U16_GAA(T30, T34, tappendc12_in_aa(T30, T33))
U16_GAA(T30, T34, tappendc12_out_aa(T30, T33)) → U17_GAA(T30, T34, tlast13_in_aa(T34, T33))
U16_GAA(T30, T34, tappendc12_out_aa(T30, T33)) → TLAST13_IN_AA(T34, T33)
TLAST13_IN_AA(T71, node(T72, T69, T70)) → U1_AA(T71, T72, T69, T70, tlast13_in_aa(T71, T72))
TLAST13_IN_AA(T71, node(T72, T69, T70)) → TLAST13_IN_AA(T71, T72)
TLAST13_IN_AA(T87, node(T84, T85, T88)) → U2_AA(T87, T84, T85, T88, tlast13_in_aa(T87, T88))
TLAST13_IN_AA(T87, node(T84, T85, T88)) → TLAST13_IN_AA(T87, T88)
GOAL1_IN_GAA(s(T98), T13, T14) → U18_GAA(T98, T13, T14, s2t39_in_ga(T98, X162))
GOAL1_IN_GAA(s(T98), T13, T14) → S2T39_IN_GA(T98, X162)
S2T39_IN_GA(s(T107), node(X217, X218, X217)) → U3_GA(T107, X217, X218, s2t39_in_ga(T107, X217))
S2T39_IN_GA(s(T107), node(X217, X218, X217)) → S2T39_IN_GA(T107, X217)
S2T39_IN_GA(s(T115), node(nil, X257, X258)) → U4_GA(T115, X257, X258, s2t39_in_ga(T115, X258))
S2T39_IN_GA(s(T115), node(nil, X257, X258)) → S2T39_IN_GA(T115, X258)
S2T39_IN_GA(s(T123), node(X297, X298, nil)) → U5_GA(T123, X297, X298, s2t39_in_ga(T123, X297))
S2T39_IN_GA(s(T123), node(X297, X298, nil)) → S2T39_IN_GA(T123, X297)
GOAL1_IN_GAA(s(T98), T145, T146) → U19_GAA(T98, T145, T146, s2tc39_in_ga(T98, T144))
U19_GAA(T98, T145, T146, s2tc39_out_ga(T98, T144)) → U20_GAA(T98, T145, T146, p72_in_aaaaa(T144, X343, T145, X342, T146))
U19_GAA(T98, T145, T146, s2tc39_out_ga(T98, T144)) → P72_IN_AAAAA(T144, X343, T145, X342, T146)
P72_IN_AAAAA(T234, X619, T235, node(X563, X619, T234), T146) → U12_AAAAA(T234, X619, T235, X563, T146, tappend116_in_aaa(T234, T235, X563))
P72_IN_AAAAA(T234, X619, T235, node(X563, X619, T234), T146) → TAPPEND116_IN_AAA(T234, T235, X563)
TAPPEND116_IN_AAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → U6_AAA(T398, T396, T397, T399, X818, tappend116_in_aaa(T398, T399, X818))
TAPPEND116_IN_AAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_AAA(T398, T399, X818)
TAPPEND116_IN_AAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U7_AAA(T448, T449, T451, X921, tappend217_in_aaa(T451, X919, X921))
TAPPEND116_IN_AAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → TAPPEND217_IN_AAA(T451, X919, X921)
TAPPEND217_IN_AAA(nil, X1193, node(X1194, nil, nil)) → U8_AAA(X1193, X1194, tappend217_in_gaa(nil, X1193, X1194))
TAPPEND217_IN_AAA(nil, X1193, node(X1194, nil, nil)) → TAPPEND217_IN_GAA(nil, X1193, X1194)
TAPPEND217_IN_GAA(nil, X1193, node(X1194, nil, nil)) → U8_GAA(X1193, X1194, tappend217_in_gaa(nil, X1193, X1194))
TAPPEND217_IN_GAA(nil, X1193, node(X1194, nil, nil)) → TAPPEND217_IN_GAA(nil, X1193, X1194)
TAPPEND217_IN_GAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U9_GAA(T569, T567, T568, X1193, X1194, tappend217_in_gaa(T569, X1193, X1194))
TAPPEND217_IN_GAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_GAA(T569, X1193, X1194)
TAPPEND217_IN_GAA(nil, nil, node(nil, nil, X1313)) → U10_GAA(X1313, tappend217_in_gaa(nil, X1310, X1313))
TAPPEND217_IN_GAA(nil, nil, node(nil, nil, X1313)) → TAPPEND217_IN_GAA(nil, X1310, X1313)
TAPPEND217_IN_GAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U11_GAA(T609, T610, T612, X1313, tappend217_in_gaa(T612, X1310, X1313))
TAPPEND217_IN_GAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_GAA(T612, X1310, X1313)
TAPPEND217_IN_AAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U9_AAA(T569, T567, T568, X1193, X1194, tappend217_in_aaa(T569, X1193, X1194))
TAPPEND217_IN_AAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_AAA(T569, X1193, X1194)
TAPPEND217_IN_AAA(nil, nil, node(nil, nil, X1313)) → U10_AAA(X1313, tappend217_in_gaa(nil, X1310, X1313))
TAPPEND217_IN_AAA(nil, nil, node(nil, nil, X1313)) → TAPPEND217_IN_GAA(nil, X1310, X1313)
TAPPEND217_IN_AAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U11_AAA(T609, T610, T612, X1313, tappend217_in_aaa(T612, X1310, X1313))
TAPPEND217_IN_AAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_AAA(T612, X1310, X1313)
P72_IN_AAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → U13_AAAAA(T642, X1504, X1430, T146, tappend217_in_aaa(node(nil, T642, nil), X1427, X1430))
P72_IN_AAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → TAPPEND217_IN_AAA(node(nil, T642, nil), X1427, X1430)
P72_IN_AAAAA(T144, T149, T145, T150, T151) → U14_AAAAA(T144, T149, T145, T150, T151, tappendc73_in_aaaa(T144, T149, T145, T150))
U14_AAAAA(T144, T149, T145, T150, T151, tappendc73_out_aaaa(T144, T149, T145, T150)) → U15_AAAAA(T144, T149, T145, T150, T151, tlast13_in_aa(T151, T150))
U14_AAAAA(T144, T149, T145, T150, T151, tappendc73_out_aaaa(T144, T149, T145, T150)) → TLAST13_IN_AA(T151, T150)
GOAL1_IN_GAA(s(T653), T13, T14) → U21_GAA(T653, T13, T14, s2t39_in_ga(T653, X1547))
GOAL1_IN_GAA(s(T653), T673, T674) → U22_GAA(T653, T673, T674, s2tc39_in_ga(T653, T672))
U22_GAA(T653, T673, T674, s2tc39_out_ga(T653, T672)) → U23_GAA(T653, T673, T674, tappend116_in_aaa(node(nil, X1585, T672), T673, X1584))
U22_GAA(T653, T673, T674, s2tc39_out_ga(T653, T672)) → TAPPEND116_IN_AAA(node(nil, X1585, T672), T673, X1584)
GOAL1_IN_GAA(s(T653), T673, T679) → U24_GAA(T653, T673, T679, s2tc39_in_ga(T653, T672))
U24_GAA(T653, T673, T679, s2tc39_out_ga(T653, T672)) → U25_GAA(T653, T673, T679, tappendc116_in_aaa(node(nil, T677, T672), T673, T678))
U25_GAA(T653, T673, T679, tappendc116_out_aaa(node(nil, T677, T672), T673, T678)) → U26_GAA(T653, T673, T679, tlast13_in_aa(T679, T678))
U25_GAA(T653, T673, T679, tappendc116_out_aaa(node(nil, T677, T672), T673, T678)) → TLAST13_IN_AA(T679, T678)
GOAL1_IN_GAA(s(T691), T13, T14) → U27_GAA(T691, T13, T14, s2t39_in_ga(T691, X1636))
GOAL1_IN_GAA(s(T691), T711, T712) → U28_GAA(T691, T711, T712, s2tc39_in_ga(T691, T710))
U28_GAA(T691, T711, T712, s2tc39_out_ga(T691, T710)) → U29_GAA(T691, T711, T712, tappend116_in_aaa(node(T710, X1675, nil), T711, X1674))
U28_GAA(T691, T711, T712, s2tc39_out_ga(T691, T710)) → TAPPEND116_IN_AAA(node(T710, X1675, nil), T711, X1674)
GOAL1_IN_GAA(s(T691), T711, T717) → U30_GAA(T691, T711, T717, s2tc39_in_ga(T691, T710))
U30_GAA(T691, T711, T717, s2tc39_out_ga(T691, T710)) → U31_GAA(T691, T711, T717, tappendc116_in_aaa(node(T710, T715, nil), T711, T716))
U31_GAA(T691, T711, T717, tappendc116_out_aaa(node(T710, T715, nil), T711, T716)) → U32_GAA(T691, T711, T717, tlast13_in_aa(T717, T716))
U31_GAA(T691, T711, T717, tappendc116_out_aaa(node(T710, T715, nil), T711, T716)) → TLAST13_IN_AA(T717, T716)
GOAL1_IN_GAA(T726, T738, T739) → U33_GAA(T726, T738, T739, p72_in_gaaaa(nil, X1737, T738, X1736, T739))
GOAL1_IN_GAA(T726, T738, T739) → P72_IN_GAAAA(nil, X1737, T738, X1736, T739)
P72_IN_GAAAA(T234, X619, T235, node(X563, X619, T234), T146) → U12_GAAAA(T234, X619, T235, X563, T146, tappend116_in_gaa(T234, T235, X563))
P72_IN_GAAAA(T234, X619, T235, node(X563, X619, T234), T146) → TAPPEND116_IN_GAA(T234, T235, X563)
TAPPEND116_IN_GAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → U6_GAA(T398, T396, T397, T399, X818, tappend116_in_gaa(T398, T399, X818))
TAPPEND116_IN_GAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_GAA(T398, T399, X818)
TAPPEND116_IN_GAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U7_GAA(T448, T449, T451, X921, tappend217_in_gaa(T451, X919, X921))
TAPPEND116_IN_GAA(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → TAPPEND217_IN_GAA(T451, X919, X921)
P72_IN_GAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → U13_GAAAA(T642, X1504, X1430, T146, tappend217_in_gaa(node(nil, T642, nil), X1427, X1430))
P72_IN_GAAAA(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430), T146) → TAPPEND217_IN_GAA(node(nil, T642, nil), X1427, X1430)
P72_IN_GAAAA(T144, T149, T145, T150, T151) → U14_GAAAA(T144, T149, T145, T150, T151, tappendc73_in_gaaa(T144, T149, T145, T150))
U14_GAAAA(T144, T149, T145, T150, T151, tappendc73_out_gaaa(T144, T149, T145, T150)) → U15_GAAAA(T144, T149, T145, T150, T151, tlast13_in_aa(T151, T150))
U14_GAAAA(T144, T149, T145, T150, T151, tappendc73_out_gaaa(T144, T149, T145, T150)) → TLAST13_IN_AA(T151, T150)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
tlast13_in_aa(x1, x2)  =  tlast13_in_aa
s(x1)  =  s(x1)
s2t39_in_ga(x1, x2)  =  s2t39_in_ga(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
p72_in_aaaaa(x1, x2, x3, x4, x5)  =  p72_in_aaaaa
tappend116_in_aaa(x1, x2, x3)  =  tappend116_in_aaa
tappend217_in_aaa(x1, x2, x3)  =  tappend217_in_aaa
tappend217_in_gaa(x1, x2, x3)  =  tappend217_in_gaa(x1)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
p72_in_gaaaa(x1, x2, x3, x4, x5)  =  p72_in_gaaaa(x1)
tappend116_in_gaa(x1, x2, x3)  =  tappend116_in_gaa(x1)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
GOAL1_IN_GAA(x1, x2, x3)  =  GOAL1_IN_GAA(x1)
U16_GAA(x1, x2, x3)  =  U16_GAA(x3)
U17_GAA(x1, x2, x3)  =  U17_GAA(x3)
TLAST13_IN_AA(x1, x2)  =  TLAST13_IN_AA
U1_AA(x1, x2, x3, x4, x5)  =  U1_AA(x5)
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
S2T39_IN_GA(x1, x2)  =  S2T39_IN_GA(x1)
U3_GA(x1, x2, x3, x4)  =  U3_GA(x1, x4)
U4_GA(x1, x2, x3, x4)  =  U4_GA(x1, x4)
U5_GA(x1, x2, x3, x4)  =  U5_GA(x1, x4)
U19_GAA(x1, x2, x3, x4)  =  U19_GAA(x1, x4)
U20_GAA(x1, x2, x3, x4)  =  U20_GAA(x1, x4)
P72_IN_AAAAA(x1, x2, x3, x4, x5)  =  P72_IN_AAAAA
U12_AAAAA(x1, x2, x3, x4, x5, x6)  =  U12_AAAAA(x6)
TAPPEND116_IN_AAA(x1, x2, x3)  =  TAPPEND116_IN_AAA
U6_AAA(x1, x2, x3, x4, x5, x6)  =  U6_AAA(x6)
U7_AAA(x1, x2, x3, x4, x5)  =  U7_AAA(x5)
TAPPEND217_IN_AAA(x1, x2, x3)  =  TAPPEND217_IN_AAA
U8_AAA(x1, x2, x3)  =  U8_AAA(x3)
TAPPEND217_IN_GAA(x1, x2, x3)  =  TAPPEND217_IN_GAA(x1)
U8_GAA(x1, x2, x3)  =  U8_GAA(x3)
U9_GAA(x1, x2, x3, x4, x5, x6)  =  U9_GAA(x1, x2, x3, x6)
U10_GAA(x1, x2)  =  U10_GAA(x2)
U11_GAA(x1, x2, x3, x4, x5)  =  U11_GAA(x1, x2, x3, x5)
U9_AAA(x1, x2, x3, x4, x5, x6)  =  U9_AAA(x6)
U10_AAA(x1, x2)  =  U10_AAA(x2)
U11_AAA(x1, x2, x3, x4, x5)  =  U11_AAA(x5)
U13_AAAAA(x1, x2, x3, x4, x5)  =  U13_AAAAA(x5)
U14_AAAAA(x1, x2, x3, x4, x5, x6)  =  U14_AAAAA(x6)
U15_AAAAA(x1, x2, x3, x4, x5, x6)  =  U15_AAAAA(x6)
U21_GAA(x1, x2, x3, x4)  =  U21_GAA(x1, x4)
U22_GAA(x1, x2, x3, x4)  =  U22_GAA(x1, x4)
U23_GAA(x1, x2, x3, x4)  =  U23_GAA(x1, x4)
U24_GAA(x1, x2, x3, x4)  =  U24_GAA(x1, x4)
U25_GAA(x1, x2, x3, x4)  =  U25_GAA(x1, x4)
U26_GAA(x1, x2, x3, x4)  =  U26_GAA(x1, x4)
U27_GAA(x1, x2, x3, x4)  =  U27_GAA(x1, x4)
U28_GAA(x1, x2, x3, x4)  =  U28_GAA(x1, x4)
U29_GAA(x1, x2, x3, x4)  =  U29_GAA(x1, x4)
U30_GAA(x1, x2, x3, x4)  =  U30_GAA(x1, x4)
U31_GAA(x1, x2, x3, x4)  =  U31_GAA(x1, x4)
U32_GAA(x1, x2, x3, x4)  =  U32_GAA(x1, x4)
U33_GAA(x1, x2, x3, x4)  =  U33_GAA(x1, x4)
P72_IN_GAAAA(x1, x2, x3, x4, x5)  =  P72_IN_GAAAA(x1)
U12_GAAAA(x1, x2, x3, x4, x5, x6)  =  U12_GAAAA(x1, x6)
TAPPEND116_IN_GAA(x1, x2, x3)  =  TAPPEND116_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6)  =  U6_GAA(x1, x2, x3, x6)
U7_GAA(x1, x2, x3, x4, x5)  =  U7_GAA(x1, x2, x3, x5)
U13_GAAAA(x1, x2, x3, x4, x5)  =  U13_GAAAA(x1, x5)
U14_GAAAA(x1, x2, x3, x4, x5, x6)  =  U14_GAAAA(x1, x6)
U15_GAAAA(x1, x2, x3, x4, x5, x6)  =  U15_GAAAA(x1, x6)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 7 SCCs with 61 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

TAPPEND217_IN_GAA(nil, nil, node(nil, nil, X1313)) → TAPPEND217_IN_GAA(nil, X1310, X1313)
TAPPEND217_IN_GAA(nil, X1193, node(X1194, nil, nil)) → TAPPEND217_IN_GAA(nil, X1193, X1194)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
TAPPEND217_IN_GAA(x1, x2, x3)  =  TAPPEND217_IN_GAA(x1)

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:

TAPPEND217_IN_GAA(nil, nil, node(nil, nil, X1313)) → TAPPEND217_IN_GAA(nil, X1310, X1313)
TAPPEND217_IN_GAA(nil, X1193, node(X1194, nil, nil)) → TAPPEND217_IN_GAA(nil, X1193, X1194)

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

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:

TAPPEND217_IN_GAA(nil) → TAPPEND217_IN_GAA(nil)

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 = TAPPEND217_IN_GAA(nil) evaluates to t =TAPPEND217_IN_GAA(nil)

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




Rewriting sequence

The DP semiunifies directly so there is only one rewrite step from TAPPEND217_IN_GAA(nil) to TAPPEND217_IN_GAA(nil).



(15) NO

(16) Obligation:

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

TAPPEND217_IN_GAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_GAA(T612, X1310, X1313)
TAPPEND217_IN_GAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_GAA(T569, X1193, X1194)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
TAPPEND217_IN_GAA(x1, x2, x3)  =  TAPPEND217_IN_GAA(x1)

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:

TAPPEND217_IN_GAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_GAA(T612, X1310, X1313)
TAPPEND217_IN_GAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_GAA(T569, X1193, X1194)

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

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:

TAPPEND217_IN_GAA(node(T609, T610, T612)) → TAPPEND217_IN_GAA(T612)
TAPPEND217_IN_GAA(node(T569, T567, T568)) → TAPPEND217_IN_GAA(T569)

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:

  • TAPPEND217_IN_GAA(node(T609, T610, T612)) → TAPPEND217_IN_GAA(T612)
    The graph contains the following edges 1 > 1

  • TAPPEND217_IN_GAA(node(T569, T567, T568)) → TAPPEND217_IN_GAA(T569)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

TAPPEND116_IN_GAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_GAA(T398, T399, X818)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
TAPPEND116_IN_GAA(x1, x2, x3)  =  TAPPEND116_IN_GAA(x1)

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:

TAPPEND116_IN_GAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_GAA(T398, T399, X818)

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

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:

TAPPEND116_IN_GAA(node(T398, T396, T397)) → TAPPEND116_IN_GAA(T398)

R is empty.
Q is empty.
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:

  • TAPPEND116_IN_GAA(node(T398, T396, T397)) → TAPPEND116_IN_GAA(T398)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

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

TAPPEND217_IN_AAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_AAA(T612, X1310, X1313)
TAPPEND217_IN_AAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_AAA(T569, X1193, X1194)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
TAPPEND217_IN_AAA(x1, x2, x3)  =  TAPPEND217_IN_AAA

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

TAPPEND217_IN_AAA(node(T609, T610, T612), T609, node(T609, T610, X1313)) → TAPPEND217_IN_AAA(T612, X1310, X1313)
TAPPEND217_IN_AAA(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → TAPPEND217_IN_AAA(T569, X1193, X1194)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

TAPPEND217_IN_AAATAPPEND217_IN_AAA

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

(35) 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 = TAPPEND217_IN_AAA evaluates to t =TAPPEND217_IN_AAA

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




Rewriting sequence

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



(36) NO

(37) Obligation:

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

TAPPEND116_IN_AAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_AAA(T398, T399, X818)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
TAPPEND116_IN_AAA(x1, x2, x3)  =  TAPPEND116_IN_AAA

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

TAPPEND116_IN_AAA(node(T398, T396, T397), T399, node(X818, T396, T397)) → TAPPEND116_IN_AAA(T398, T399, X818)

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

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

TAPPEND116_IN_AAATAPPEND116_IN_AAA

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

(42) 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 = TAPPEND116_IN_AAA evaluates to t =TAPPEND116_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 TAPPEND116_IN_AAA to TAPPEND116_IN_AAA.



(43) NO

(44) Obligation:

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

S2T39_IN_GA(s(T115), node(nil, X257, X258)) → S2T39_IN_GA(T115, X258)
S2T39_IN_GA(s(T107), node(X217, X218, X217)) → S2T39_IN_GA(T107, X217)
S2T39_IN_GA(s(T123), node(X297, X298, nil)) → S2T39_IN_GA(T123, X297)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
S2T39_IN_GA(x1, x2)  =  S2T39_IN_GA(x1)

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

(45) UsableRulesProof (EQUIVALENT transformation)

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

(46) Obligation:

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

S2T39_IN_GA(s(T115), node(nil, X257, X258)) → S2T39_IN_GA(T115, X258)
S2T39_IN_GA(s(T107), node(X217, X218, X217)) → S2T39_IN_GA(T107, X217)
S2T39_IN_GA(s(T123), node(X297, X298, nil)) → S2T39_IN_GA(T123, X297)

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

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

(47) PiDPToQDPProof (SOUND transformation)

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

(48) Obligation:

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

S2T39_IN_GA(s(T115)) → S2T39_IN_GA(T115)

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

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

  • S2T39_IN_GA(s(T115)) → S2T39_IN_GA(T115)
    The graph contains the following edges 1 > 1

(50) YES

(51) Obligation:

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

TLAST13_IN_AA(T87, node(T84, T85, T88)) → TLAST13_IN_AA(T87, T88)
TLAST13_IN_AA(T71, node(T72, T69, T70)) → TLAST13_IN_AA(T71, T72)

The TRS R consists of the following rules:

tappendc12_in_aa(T43, node(nil, T43, nil)) → tappendc12_out_aa(T43, node(nil, T43, nil))
s2tc39_in_ga(0, nil) → s2tc39_out_ga(0, nil)
s2tc39_in_ga(s(T107), node(X217, X218, X217)) → U37_ga(T107, X217, X218, s2tc39_in_ga(T107, X217))
s2tc39_in_ga(s(T115), node(nil, X257, X258)) → U38_ga(T115, X257, X258, s2tc39_in_ga(T115, X258))
s2tc39_in_ga(s(T123), node(X297, X298, nil)) → U39_ga(T123, X297, X298, s2tc39_in_ga(T123, X297))
s2tc39_in_ga(T126, node(nil, X315, nil)) → s2tc39_out_ga(T126, node(nil, X315, nil))
U39_ga(T123, X297, X298, s2tc39_out_ga(T123, X297)) → s2tc39_out_ga(s(T123), node(X297, X298, nil))
U38_ga(T115, X257, X258, s2tc39_out_ga(T115, X258)) → s2tc39_out_ga(s(T115), node(nil, X257, X258))
U37_ga(T107, X217, X218, s2tc39_out_ga(T107, X217)) → s2tc39_out_ga(s(T107), node(X217, X218, X217))
tappendc73_in_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_aaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_aaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_aaaa(T234, X619, T235, node(X563, X619, T234)) → U49_aaaa(T234, X619, T235, X563, tappendc116_in_aaa(T234, T235, X563))
tappendc116_in_aaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_aaa(nil, T243, node(nil, T243, nil))
tappendc116_in_aaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_aaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_aaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_aaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_aaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_aaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_aaa(nil, T345, node(X818, nil, nil)) → U40_aaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_aaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_aaa(nil, T345, node(X818, nil, nil))
tappendc116_in_aaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_aaa(T398, T396, T397, T399, X818, tappendc116_in_aaa(T398, T399, X818))
tappendc116_in_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_aaa(T448, T449, T451, X921, tappendc217_in_aaa(T451, X919, X921))
tappendc217_in_aaa(nil, X995, X995) → tappendc217_out_aaa(nil, X995, X995)
tappendc217_in_aaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_aaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_aaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_aaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_aaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_aaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_aaa(nil, X1193, node(X1194, nil, nil)) → U43_aaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(nil, X995, X995) → tappendc217_out_gaa(nil, X995, X995)
tappendc217_in_gaa(nil, X1028, node(X1028, nil, nil)) → tappendc217_out_gaa(nil, X1028, node(X1028, nil, nil))
tappendc217_in_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486)) → tappendc217_out_gaa(node(nil, T485, T486), X1028, node(X1028, T485, T486))
tappendc217_in_gaa(nil, X1099, node(nil, nil, X1099)) → tappendc217_out_gaa(nil, X1099, node(nil, nil, X1099))
tappendc217_in_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099)) → tappendc217_out_gaa(node(T522, T523, nil), X1099, node(T522, T523, X1099))
tappendc217_in_gaa(nil, X1193, node(X1194, nil, nil)) → U43_gaa(X1193, X1194, tappendc217_in_gaa(nil, X1193, X1194))
tappendc217_in_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_in_gaa(T569, X1193, X1194))
tappendc217_in_gaa(nil, nil, node(nil, nil, X1313)) → U45_gaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
tappendc217_in_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_gaa(T609, T610, T612, X1313, tappendc217_in_gaa(T612, X1310, X1313))
U46_gaa(T609, T610, T612, X1313, tappendc217_out_gaa(T612, X1310, X1313)) → tappendc217_out_gaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U45_gaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_gaa(nil, nil, node(nil, nil, X1313))
U44_gaa(T569, T567, T568, X1193, X1194, tappendc217_out_gaa(T569, X1193, X1194)) → tappendc217_out_gaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U43_gaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_gaa(nil, X1193, node(X1194, nil, nil))
U43_aaa(X1193, X1194, tappendc217_out_gaa(nil, X1193, X1194)) → tappendc217_out_aaa(nil, X1193, node(X1194, nil, nil))
tappendc217_in_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568)) → U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_in_aaa(T569, X1193, X1194))
tappendc217_in_aaa(nil, nil, node(nil, nil, X1313)) → U45_aaa(X1313, tappendc217_in_gaa(nil, X1310, X1313))
U45_aaa(X1313, tappendc217_out_gaa(nil, X1310, X1313)) → tappendc217_out_aaa(nil, nil, node(nil, nil, X1313))
tappendc217_in_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313)) → U46_aaa(T609, T610, T612, X1313, tappendc217_in_aaa(T612, X1310, X1313))
U46_aaa(T609, T610, T612, X1313, tappendc217_out_aaa(T612, X1310, X1313)) → tappendc217_out_aaa(node(T609, T610, T612), T609, node(T609, T610, X1313))
U44_aaa(T569, T567, T568, X1193, X1194, tappendc217_out_aaa(T569, X1193, X1194)) → tappendc217_out_aaa(node(T569, T567, T568), X1193, node(X1194, T567, T568))
U42_aaa(T448, T449, T451, X921, tappendc217_out_aaa(T451, X919, X921)) → tappendc116_out_aaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_aaa(T398, T396, T397, T399, X818, tappendc116_out_aaa(T398, T399, X818)) → tappendc116_out_aaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_aaaa(T234, X619, T235, X563, tappendc116_out_aaa(T234, T235, X563)) → tappendc73_out_aaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_aaaa(T642, X1504, X1430, tappendc217_in_aaa(node(nil, T642, nil), X1427, X1430))
U50_aaaa(T642, X1504, X1430, tappendc217_out_aaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_aaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))
tappendc73_in_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil)) → tappendc73_out_gaaa(nil, X437, T165, node(node(nil, T165, nil), X437, nil))
tappendc73_in_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil))) → tappendc73_out_gaaa(nil, X511, T181, node(nil, X511, node(nil, T181, nil)))
tappendc73_in_gaaa(T234, X619, T235, node(X563, X619, T234)) → U49_gaaa(T234, X619, T235, X563, tappendc116_in_gaa(T234, T235, X563))
tappendc116_in_gaa(nil, T243, node(nil, T243, nil)) → tappendc116_out_gaa(nil, T243, node(nil, T243, nil))
tappendc116_in_gaa(nil, T255, node(node(nil, T255, nil), nil, nil)) → tappendc116_out_gaa(nil, T255, node(node(nil, T255, nil), nil, nil))
tappendc116_in_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283)) → tappendc116_out_gaa(node(nil, T282, T283), T255, node(node(nil, T255, nil), T282, T283))
tappendc116_in_gaa(nil, T295, node(nil, nil, node(nil, T295, nil))) → tappendc116_out_gaa(nil, T295, node(nil, nil, node(nil, T295, nil)))
tappendc116_in_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil))) → tappendc116_out_gaa(node(T324, T325, nil), T295, node(T324, T325, node(nil, T295, nil)))
tappendc116_in_gaa(nil, T345, node(X818, nil, nil)) → U40_gaa(T345, X818, tappendc12_in_aa(T345, X818))
U40_gaa(T345, X818, tappendc12_out_aa(T345, X818)) → tappendc116_out_gaa(nil, T345, node(X818, nil, nil))
tappendc116_in_gaa(node(T398, T396, T397), T399, node(X818, T396, T397)) → U41_gaa(T398, T396, T397, T399, X818, tappendc116_in_gaa(T398, T399, X818))
tappendc116_in_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921)) → U42_gaa(T448, T449, T451, X921, tappendc217_in_gaa(T451, X919, X921))
U42_gaa(T448, T449, T451, X921, tappendc217_out_gaa(T451, X919, X921)) → tappendc116_out_gaa(node(node(nil, T448, nil), T449, T451), T448, node(node(nil, T448, nil), T449, X921))
U41_gaa(T398, T396, T397, T399, X818, tappendc116_out_gaa(T398, T399, X818)) → tappendc116_out_gaa(node(T398, T396, T397), T399, node(X818, T396, T397))
U49_gaaa(T234, X619, T235, X563, tappendc116_out_gaa(T234, T235, X563)) → tappendc73_out_gaaa(T234, X619, T235, node(X563, X619, T234))
tappendc73_in_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430)) → U50_gaaa(T642, X1504, X1430, tappendc217_in_gaa(node(nil, T642, nil), X1427, X1430))
U50_gaaa(T642, X1504, X1430, tappendc217_out_gaa(node(nil, T642, nil), X1427, X1430)) → tappendc73_out_gaaa(node(nil, T642, nil), X1504, T642, node(node(nil, T642, nil), X1504, X1430))

The argument filtering Pi contains the following mapping:
0  =  0
tappendc12_in_aa(x1, x2)  =  tappendc12_in_aa
tappendc12_out_aa(x1, x2)  =  tappendc12_out_aa
s(x1)  =  s(x1)
s2tc39_in_ga(x1, x2)  =  s2tc39_in_ga(x1)
s2tc39_out_ga(x1, x2)  =  s2tc39_out_ga(x1)
U37_ga(x1, x2, x3, x4)  =  U37_ga(x1, x4)
U38_ga(x1, x2, x3, x4)  =  U38_ga(x1, x4)
U39_ga(x1, x2, x3, x4)  =  U39_ga(x1, x4)
nil  =  nil
node(x1, x2, x3)  =  node(x1, x2, x3)
tappendc73_in_aaaa(x1, x2, x3, x4)  =  tappendc73_in_aaaa
tappendc73_out_aaaa(x1, x2, x3, x4)  =  tappendc73_out_aaaa
U49_aaaa(x1, x2, x3, x4, x5)  =  U49_aaaa(x5)
tappendc116_in_aaa(x1, x2, x3)  =  tappendc116_in_aaa
tappendc116_out_aaa(x1, x2, x3)  =  tappendc116_out_aaa
U40_aaa(x1, x2, x3)  =  U40_aaa(x3)
U41_aaa(x1, x2, x3, x4, x5, x6)  =  U41_aaa(x6)
U42_aaa(x1, x2, x3, x4, x5)  =  U42_aaa(x5)
tappendc217_in_aaa(x1, x2, x3)  =  tappendc217_in_aaa
tappendc217_out_aaa(x1, x2, x3)  =  tappendc217_out_aaa
U43_aaa(x1, x2, x3)  =  U43_aaa(x3)
tappendc217_in_gaa(x1, x2, x3)  =  tappendc217_in_gaa(x1)
tappendc217_out_gaa(x1, x2, x3)  =  tappendc217_out_gaa(x1)
U43_gaa(x1, x2, x3)  =  U43_gaa(x3)
U44_gaa(x1, x2, x3, x4, x5, x6)  =  U44_gaa(x1, x2, x3, x6)
U45_gaa(x1, x2)  =  U45_gaa(x2)
U46_gaa(x1, x2, x3, x4, x5)  =  U46_gaa(x1, x2, x3, x5)
U44_aaa(x1, x2, x3, x4, x5, x6)  =  U44_aaa(x6)
U45_aaa(x1, x2)  =  U45_aaa(x2)
U46_aaa(x1, x2, x3, x4, x5)  =  U46_aaa(x5)
U50_aaaa(x1, x2, x3, x4)  =  U50_aaaa(x4)
tappendc73_in_gaaa(x1, x2, x3, x4)  =  tappendc73_in_gaaa(x1)
tappendc73_out_gaaa(x1, x2, x3, x4)  =  tappendc73_out_gaaa(x1)
U49_gaaa(x1, x2, x3, x4, x5)  =  U49_gaaa(x1, x5)
tappendc116_in_gaa(x1, x2, x3)  =  tappendc116_in_gaa(x1)
tappendc116_out_gaa(x1, x2, x3)  =  tappendc116_out_gaa(x1)
U40_gaa(x1, x2, x3)  =  U40_gaa(x3)
U41_gaa(x1, x2, x3, x4, x5, x6)  =  U41_gaa(x1, x2, x3, x6)
U42_gaa(x1, x2, x3, x4, x5)  =  U42_gaa(x1, x2, x3, x5)
U50_gaaa(x1, x2, x3, x4)  =  U50_gaaa(x1, x4)
TLAST13_IN_AA(x1, x2)  =  TLAST13_IN_AA

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

(52) UsableRulesProof (EQUIVALENT transformation)

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

(53) Obligation:

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

TLAST13_IN_AA(T87, node(T84, T85, T88)) → TLAST13_IN_AA(T87, T88)
TLAST13_IN_AA(T71, node(T72, T69, T70)) → TLAST13_IN_AA(T71, T72)

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

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

(54) PiDPToQDPProof (SOUND transformation)

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

(55) Obligation:

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

TLAST13_IN_AATLAST13_IN_AA

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

(56) 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 = TLAST13_IN_AA evaluates to t =TLAST13_IN_AA

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




Rewriting sequence

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



(57) NO