(0) Obligation:

Clauses:

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

Queries:

front(a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

front14(tree(T25, T28, T29), X41) :- front14(T28, X39).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T30), front14(T31, X40)).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), app32(T33, T32, X41))).
app32(.(T47, T50), T51, .(T47, X68)) :- app32(T50, T51, X68).
app178(.(T354, T358), T359, .(T354, T357)) :- app178(T358, T359, T357).
front1(tree(T7, void, T12), []) :- front14(T12, X12).
front1(tree(T7, void, T12), []) :- ','(frontc14(T12, T13), app15(T13)).
front1(tree(T7, tree(T67, void, void), T66), []) :- front14(T66, X12).
front1(tree(T7, tree(T80, T83, T84), T85), []) :- front14(T83, X120).
front1(tree(T7, tree(T80, T83, T87), T88), []) :- ','(frontc14(T83, T86), front14(T87, X121)).
front1(tree(T7, tree(T80, T83, T87), T91), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), app32(T90, T89, X122))).
front1(tree(T7, tree(T80, T83, T87), T95), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), ','(appc32(T90, T89, T94), front14(T95, X12)))).
front1(tree(T7, tree(T80, T83, T87), T95), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), ','(appc32(T90, T89, T99), ','(frontc14(T95, T98), app66(T99, T98))))).
front1(tree(T116, void, T122), .(T119, [])) :- front14(T122, X155).
front1(tree(T116, tree(T144, void, void), T143), .(T119, [])) :- front14(T143, X155).
front1(tree(T116, tree(T153, void, void), T143), .(T153, [])) :- ','(frontc14(T143, T155), app15(T155)).
front1(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) :- front14(T167, X219).
front1(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) :- ','(frontc14(T167, T170), front14(T171, X220)).
front1(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), app32(T174, T173, X221))).
front1(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), ','(appc32(T174, T173, T178), front14(T179, X155)))).
front1(tree(T116, tree(T164, T167, T171), T179), .(T204, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), ','(appc32(T174, T173, .(T204, T207)), ','(frontc14(T179, T208), app66(T207, T208))))).
front1(tree(T215, void, T221), T218) :- front14(T221, X265).
front1(tree(T215, tree(T238, void, void), T237), T218) :- front14(T237, X265).
front1(tree(T215, tree(T269, T272, T273), T274), T218) :- front14(T272, X339).
front1(tree(T215, tree(T269, T272, T276), T277), T218) :- ','(frontc14(T272, T275), front14(T276, X340)).
front1(tree(T215, tree(T269, T272, T276), T282), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), app32(T281, T280, X341))).
front1(tree(T215, tree(T269, T272, T276), T288), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, T287), front14(T288, X265)))).
front1(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, .(T312, .(T333, T337))), ','(frontc14(T288, T338), app178(T337, T338, T336))))).

Clauses:

frontc14(void, []).
frontc14(tree(T18, void, void), .(T18, [])).
frontc14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), appc32(T33, T32, X41))).
appc32([], T40, T40).
appc32(.(T47, T50), T51, .(T47, X68)) :- appc32(T50, T51, X68).
appc15([]).
appc66([], []).
appc178([], T345, T345).
appc178(.(T354, T358), T359, .(T354, T357)) :- appc178(T358, T359, T357).

Afs:

front1(x1, x2)  =  front1(x2)

(3) UndefinedPredicateInTriplesTransformerProof (SOUND transformation)

Deleted triples and predicates having undefined goals [UNKNOWN].

(4) Obligation:

Triples:

front14(tree(T25, T28, T29), X41) :- front14(T28, X39).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T30), front14(T31, X40)).
front14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), app32(T33, T32, X41))).
app32(.(T47, T50), T51, .(T47, X68)) :- app32(T50, T51, X68).
app178(.(T354, T358), T359, .(T354, T357)) :- app178(T358, T359, T357).
front1(tree(T7, void, T12), []) :- front14(T12, X12).
front1(tree(T7, tree(T67, void, void), T66), []) :- front14(T66, X12).
front1(tree(T7, tree(T80, T83, T84), T85), []) :- front14(T83, X120).
front1(tree(T7, tree(T80, T83, T87), T88), []) :- ','(frontc14(T83, T86), front14(T87, X121)).
front1(tree(T7, tree(T80, T83, T87), T91), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), app32(T90, T89, X122))).
front1(tree(T7, tree(T80, T83, T87), T95), []) :- ','(frontc14(T83, T90), ','(frontc14(T87, T89), ','(appc32(T90, T89, T94), front14(T95, X12)))).
front1(tree(T116, void, T122), .(T119, [])) :- front14(T122, X155).
front1(tree(T116, tree(T144, void, void), T143), .(T119, [])) :- front14(T143, X155).
front1(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) :- front14(T167, X219).
front1(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) :- ','(frontc14(T167, T170), front14(T171, X220)).
front1(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), app32(T174, T173, X221))).
front1(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) :- ','(frontc14(T167, T174), ','(frontc14(T171, T173), ','(appc32(T174, T173, T178), front14(T179, X155)))).
front1(tree(T215, void, T221), T218) :- front14(T221, X265).
front1(tree(T215, tree(T238, void, void), T237), T218) :- front14(T237, X265).
front1(tree(T215, tree(T269, T272, T273), T274), T218) :- front14(T272, X339).
front1(tree(T215, tree(T269, T272, T276), T277), T218) :- ','(frontc14(T272, T275), front14(T276, X340)).
front1(tree(T215, tree(T269, T272, T276), T282), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), app32(T281, T280, X341))).
front1(tree(T215, tree(T269, T272, T276), T288), T218) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, T287), front14(T288, X265)))).
front1(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) :- ','(frontc14(T272, T281), ','(frontc14(T276, T280), ','(appc32(T281, T280, .(T312, .(T333, T337))), ','(frontc14(T288, T338), app178(T337, T338, T336))))).

Clauses:

frontc14(void, []).
frontc14(tree(T18, void, void), .(T18, [])).
frontc14(tree(T25, T28, T31), X41) :- ','(frontc14(T28, T33), ','(frontc14(T31, T32), appc32(T33, T32, X41))).
appc32([], T40, T40).
appc32(.(T47, T50), T51, .(T47, X68)) :- appc32(T50, T51, X68).
appc15([]).
appc66([], []).
appc178([], T345, T345).
appc178(.(T354, T358), T359, .(T354, T357)) :- appc178(T358, T359, T357).

Afs:

front1(x1, x2)  =  front1(x2)

(5) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
front1_in: (f,b)
front14_in: (f,f)
frontc14_in: (f,f)
appc32_in: (b,b,f)
app32_in: (b,b,f)
app178_in: (b,b,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

FRONT1_IN_AG(tree(T7, void, T12), []) → U9_AG(T7, T12, front14_in_aa(T12, X12))
FRONT1_IN_AG(tree(T7, void, T12), []) → FRONT14_IN_AA(T12, X12)
FRONT14_IN_AA(tree(T25, T28, T29), X41) → U1_AA(T25, T28, T29, X41, front14_in_aa(T28, X39))
FRONT14_IN_AA(tree(T25, T28, T29), X41) → FRONT14_IN_AA(T28, X39)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U2_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T30))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → U3_AA(T25, T28, T31, X41, front14_in_aa(T31, X40))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → FRONT14_IN_AA(T31, X40)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U4_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U4_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U5_AA(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U6_AA(T25, T28, T31, X41, app32_in_gga(T33, T32, X41))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → APP32_IN_GGA(T33, T32, X41)
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → U7_GGA(T47, T50, T51, X68, app32_in_gga(T50, T51, X68))
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → U10_AG(T7, T67, T66, front14_in_aa(T66, X12))
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → FRONT14_IN_AA(T66, X12)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → U11_AG(T7, T80, T83, T84, T85, front14_in_aa(T83, X120))
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → FRONT14_IN_AA(T83, X120)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T88), []) → U12_AG(T7, T80, T83, T87, T88, frontc14_in_aa(T83, T86))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → U13_AG(T7, T80, T83, T87, T88, front14_in_aa(T87, X121))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → FRONT14_IN_AA(T87, X121)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T91), []) → U14_AG(T7, T80, T83, T87, T91, frontc14_in_aa(T83, T90))
U14_AG(T7, T80, T83, T87, T91, frontc14_out_aa(T83, T90)) → U15_AG(T7, T80, T83, T87, T91, T90, frontc14_in_aa(T87, T89))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → U16_AG(T7, T80, T83, T87, T91, app32_in_gga(T90, T89, X122))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → APP32_IN_GGA(T90, T89, X122)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T95), []) → U17_AG(T7, T80, T83, T87, T95, frontc14_in_aa(T83, T90))
U17_AG(T7, T80, T83, T87, T95, frontc14_out_aa(T83, T90)) → U18_AG(T7, T80, T83, T87, T95, T90, frontc14_in_aa(T87, T89))
U18_AG(T7, T80, T83, T87, T95, T90, frontc14_out_aa(T87, T89)) → U19_AG(T7, T80, T83, T87, T95, appc32_in_gga(T90, T89, T94))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → U20_AG(T7, T80, T83, T87, T95, front14_in_aa(T95, X12))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → FRONT14_IN_AA(T95, X12)
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → U21_AG(T116, T122, T119, front14_in_aa(T122, X155))
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → FRONT14_IN_AA(T122, X155)
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → U22_AG(T116, T144, T143, T119, front14_in_aa(T143, X155))
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → FRONT14_IN_AA(T143, X155)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → U23_AG(T116, T164, T167, T168, T169, T119, front14_in_aa(T167, X219))
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → FRONT14_IN_AA(T167, X219)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) → U24_AG(T116, T164, T167, T171, T172, T119, frontc14_in_aa(T167, T170))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → U25_AG(T116, T164, T167, T171, T172, T119, front14_in_aa(T171, X220))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → FRONT14_IN_AA(T171, X220)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) → U26_AG(T116, T164, T167, T171, T175, T119, frontc14_in_aa(T167, T174))
U26_AG(T116, T164, T167, T171, T175, T119, frontc14_out_aa(T167, T174)) → U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_in_aa(T171, T173))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → U28_AG(T116, T164, T167, T171, T175, T119, app32_in_gga(T174, T173, X221))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → APP32_IN_GGA(T174, T173, X221)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) → U29_AG(T116, T164, T167, T171, T179, T119, frontc14_in_aa(T167, T174))
U29_AG(T116, T164, T167, T171, T179, T119, frontc14_out_aa(T167, T174)) → U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_in_aa(T171, T173))
U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_out_aa(T171, T173)) → U31_AG(T116, T164, T167, T171, T179, T119, appc32_in_gga(T174, T173, T178))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → U32_AG(T116, T164, T167, T171, T179, T119, front14_in_aa(T179, X155))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → FRONT14_IN_AA(T179, X155)
FRONT1_IN_AG(tree(T215, void, T221), T218) → U33_AG(T215, T221, T218, front14_in_aa(T221, X265))
FRONT1_IN_AG(tree(T215, void, T221), T218) → FRONT14_IN_AA(T221, X265)
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → U34_AG(T215, T238, T237, T218, front14_in_aa(T237, X265))
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → FRONT14_IN_AA(T237, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → U35_AG(T215, T269, T272, T273, T274, T218, front14_in_aa(T272, X339))
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → FRONT14_IN_AA(T272, X339)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T277), T218) → U36_AG(T215, T269, T272, T276, T277, T218, frontc14_in_aa(T272, T275))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → U37_AG(T215, T269, T272, T276, T277, T218, front14_in_aa(T276, X340))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → FRONT14_IN_AA(T276, X340)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T282), T218) → U38_AG(T215, T269, T272, T276, T282, T218, frontc14_in_aa(T272, T281))
U38_AG(T215, T269, T272, T276, T282, T218, frontc14_out_aa(T272, T281)) → U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_in_aa(T276, T280))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → U40_AG(T215, T269, T272, T276, T282, T218, app32_in_gga(T281, T280, X341))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → APP32_IN_GGA(T281, T280, X341)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), T218) → U41_AG(T215, T269, T272, T276, T288, T218, frontc14_in_aa(T272, T281))
U41_AG(T215, T269, T272, T276, T288, T218, frontc14_out_aa(T272, T281)) → U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_in_aa(T276, T280))
U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_out_aa(T276, T280)) → U43_AG(T215, T269, T272, T276, T288, T218, appc32_in_gga(T281, T280, T287))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → U44_AG(T215, T269, T272, T276, T288, T218, front14_in_aa(T288, X265))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → FRONT14_IN_AA(T288, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) → U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_in_aa(T272, T281))
U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_out_aa(T272, T281)) → U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_in_aa(T276, T280))
U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_out_aa(T276, T280)) → U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_in_gga(T281, T280, .(T312, .(T333, T337))))
U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_out_gga(T281, T280, .(T312, .(T333, T337)))) → U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_in_aa(T288, T338))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → U49_AG(T215, T269, T272, T276, T288, T312, T333, T336, app178_in_ggg(T337, T338, T336))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → APP178_IN_GGG(T337, T338, T336)
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → U8_GGG(T354, T358, T359, T357, app178_in_ggg(T358, T359, T357))
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
front14_in_aa(x1, x2)  =  front14_in_aa
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
app32_in_gga(x1, x2, x3)  =  app32_in_gga(x1, x2)
app178_in_ggg(x1, x2, x3)  =  app178_in_ggg(x1, x2, x3)
FRONT1_IN_AG(x1, x2)  =  FRONT1_IN_AG(x2)
U9_AG(x1, x2, x3)  =  U9_AG(x3)
FRONT14_IN_AA(x1, x2)  =  FRONT14_IN_AA
U1_AA(x1, x2, x3, x4, x5)  =  U1_AA(x5)
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)
U3_AA(x1, x2, x3, x4, x5)  =  U3_AA(x5)
U4_AA(x1, x2, x3, x4, x5)  =  U4_AA(x5)
U5_AA(x1, x2, x3, x4, x5, x6)  =  U5_AA(x5, x6)
U6_AA(x1, x2, x3, x4, x5)  =  U6_AA(x5)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5)  =  U7_GGA(x2, x3, x5)
U10_AG(x1, x2, x3, x4)  =  U10_AG(x4)
U11_AG(x1, x2, x3, x4, x5, x6)  =  U11_AG(x6)
U12_AG(x1, x2, x3, x4, x5, x6)  =  U12_AG(x6)
U13_AG(x1, x2, x3, x4, x5, x6)  =  U13_AG(x6)
U14_AG(x1, x2, x3, x4, x5, x6)  =  U14_AG(x6)
U15_AG(x1, x2, x3, x4, x5, x6, x7)  =  U15_AG(x6, x7)
U16_AG(x1, x2, x3, x4, x5, x6)  =  U16_AG(x6)
U17_AG(x1, x2, x3, x4, x5, x6)  =  U17_AG(x6)
U18_AG(x1, x2, x3, x4, x5, x6, x7)  =  U18_AG(x6, x7)
U19_AG(x1, x2, x3, x4, x5, x6)  =  U19_AG(x6)
U20_AG(x1, x2, x3, x4, x5, x6)  =  U20_AG(x6)
U21_AG(x1, x2, x3, x4)  =  U21_AG(x4)
U22_AG(x1, x2, x3, x4, x5)  =  U22_AG(x5)
U23_AG(x1, x2, x3, x4, x5, x6, x7)  =  U23_AG(x7)
U24_AG(x1, x2, x3, x4, x5, x6, x7)  =  U24_AG(x7)
U25_AG(x1, x2, x3, x4, x5, x6, x7)  =  U25_AG(x7)
U26_AG(x1, x2, x3, x4, x5, x6, x7)  =  U26_AG(x7)
U27_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_AG(x7, x8)
U28_AG(x1, x2, x3, x4, x5, x6, x7)  =  U28_AG(x7)
U29_AG(x1, x2, x3, x4, x5, x6, x7)  =  U29_AG(x7)
U30_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_AG(x7, x8)
U31_AG(x1, x2, x3, x4, x5, x6, x7)  =  U31_AG(x7)
U32_AG(x1, x2, x3, x4, x5, x6, x7)  =  U32_AG(x7)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x3, x4)
U34_AG(x1, x2, x3, x4, x5)  =  U34_AG(x4, x5)
U35_AG(x1, x2, x3, x4, x5, x6, x7)  =  U35_AG(x6, x7)
U36_AG(x1, x2, x3, x4, x5, x6, x7)  =  U36_AG(x6, x7)
U37_AG(x1, x2, x3, x4, x5, x6, x7)  =  U37_AG(x6, x7)
U38_AG(x1, x2, x3, x4, x5, x6, x7)  =  U38_AG(x6, x7)
U39_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_AG(x6, x7, x8)
U40_AG(x1, x2, x3, x4, x5, x6, x7)  =  U40_AG(x6, x7)
U41_AG(x1, x2, x3, x4, x5, x6, x7)  =  U41_AG(x6, x7)
U42_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_AG(x6, x7, x8)
U43_AG(x1, x2, x3, x4, x5, x6, x7)  =  U43_AG(x6, x7)
U44_AG(x1, x2, x3, x4, x5, x6, x7)  =  U44_AG(x6, x7)
U45_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U45_AG(x8, x9)
U46_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U46_AG(x8, x9, x10)
U47_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_AG(x8, x9)
U48_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U48_AG(x8, x9, x10)
U49_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_AG(x8, x9)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)
U8_GGG(x1, x2, x3, x4, x5)  =  U8_GGG(x2, x3, x4, x5)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(6) Obligation:

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

FRONT1_IN_AG(tree(T7, void, T12), []) → U9_AG(T7, T12, front14_in_aa(T12, X12))
FRONT1_IN_AG(tree(T7, void, T12), []) → FRONT14_IN_AA(T12, X12)
FRONT14_IN_AA(tree(T25, T28, T29), X41) → U1_AA(T25, T28, T29, X41, front14_in_aa(T28, X39))
FRONT14_IN_AA(tree(T25, T28, T29), X41) → FRONT14_IN_AA(T28, X39)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U2_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T30))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → U3_AA(T25, T28, T31, X41, front14_in_aa(T31, X40))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → FRONT14_IN_AA(T31, X40)
FRONT14_IN_AA(tree(T25, T28, T31), X41) → U4_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U4_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U5_AA(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U6_AA(T25, T28, T31, X41, app32_in_gga(T33, T32, X41))
U5_AA(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → APP32_IN_GGA(T33, T32, X41)
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → U7_GGA(T47, T50, T51, X68, app32_in_gga(T50, T51, X68))
APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → U10_AG(T7, T67, T66, front14_in_aa(T66, X12))
FRONT1_IN_AG(tree(T7, tree(T67, void, void), T66), []) → FRONT14_IN_AA(T66, X12)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → U11_AG(T7, T80, T83, T84, T85, front14_in_aa(T83, X120))
FRONT1_IN_AG(tree(T7, tree(T80, T83, T84), T85), []) → FRONT14_IN_AA(T83, X120)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T88), []) → U12_AG(T7, T80, T83, T87, T88, frontc14_in_aa(T83, T86))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → U13_AG(T7, T80, T83, T87, T88, front14_in_aa(T87, X121))
U12_AG(T7, T80, T83, T87, T88, frontc14_out_aa(T83, T86)) → FRONT14_IN_AA(T87, X121)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T91), []) → U14_AG(T7, T80, T83, T87, T91, frontc14_in_aa(T83, T90))
U14_AG(T7, T80, T83, T87, T91, frontc14_out_aa(T83, T90)) → U15_AG(T7, T80, T83, T87, T91, T90, frontc14_in_aa(T87, T89))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → U16_AG(T7, T80, T83, T87, T91, app32_in_gga(T90, T89, X122))
U15_AG(T7, T80, T83, T87, T91, T90, frontc14_out_aa(T87, T89)) → APP32_IN_GGA(T90, T89, X122)
FRONT1_IN_AG(tree(T7, tree(T80, T83, T87), T95), []) → U17_AG(T7, T80, T83, T87, T95, frontc14_in_aa(T83, T90))
U17_AG(T7, T80, T83, T87, T95, frontc14_out_aa(T83, T90)) → U18_AG(T7, T80, T83, T87, T95, T90, frontc14_in_aa(T87, T89))
U18_AG(T7, T80, T83, T87, T95, T90, frontc14_out_aa(T87, T89)) → U19_AG(T7, T80, T83, T87, T95, appc32_in_gga(T90, T89, T94))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → U20_AG(T7, T80, T83, T87, T95, front14_in_aa(T95, X12))
U19_AG(T7, T80, T83, T87, T95, appc32_out_gga(T90, T89, T94)) → FRONT14_IN_AA(T95, X12)
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → U21_AG(T116, T122, T119, front14_in_aa(T122, X155))
FRONT1_IN_AG(tree(T116, void, T122), .(T119, [])) → FRONT14_IN_AA(T122, X155)
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → U22_AG(T116, T144, T143, T119, front14_in_aa(T143, X155))
FRONT1_IN_AG(tree(T116, tree(T144, void, void), T143), .(T119, [])) → FRONT14_IN_AA(T143, X155)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → U23_AG(T116, T164, T167, T168, T169, T119, front14_in_aa(T167, X219))
FRONT1_IN_AG(tree(T116, tree(T164, T167, T168), T169), .(T119, [])) → FRONT14_IN_AA(T167, X219)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T172), .(T119, [])) → U24_AG(T116, T164, T167, T171, T172, T119, frontc14_in_aa(T167, T170))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → U25_AG(T116, T164, T167, T171, T172, T119, front14_in_aa(T171, X220))
U24_AG(T116, T164, T167, T171, T172, T119, frontc14_out_aa(T167, T170)) → FRONT14_IN_AA(T171, X220)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T175), .(T119, [])) → U26_AG(T116, T164, T167, T171, T175, T119, frontc14_in_aa(T167, T174))
U26_AG(T116, T164, T167, T171, T175, T119, frontc14_out_aa(T167, T174)) → U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_in_aa(T171, T173))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → U28_AG(T116, T164, T167, T171, T175, T119, app32_in_gga(T174, T173, X221))
U27_AG(T116, T164, T167, T171, T175, T119, T174, frontc14_out_aa(T171, T173)) → APP32_IN_GGA(T174, T173, X221)
FRONT1_IN_AG(tree(T116, tree(T164, T167, T171), T179), .(T119, [])) → U29_AG(T116, T164, T167, T171, T179, T119, frontc14_in_aa(T167, T174))
U29_AG(T116, T164, T167, T171, T179, T119, frontc14_out_aa(T167, T174)) → U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_in_aa(T171, T173))
U30_AG(T116, T164, T167, T171, T179, T119, T174, frontc14_out_aa(T171, T173)) → U31_AG(T116, T164, T167, T171, T179, T119, appc32_in_gga(T174, T173, T178))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → U32_AG(T116, T164, T167, T171, T179, T119, front14_in_aa(T179, X155))
U31_AG(T116, T164, T167, T171, T179, T119, appc32_out_gga(T174, T173, T178)) → FRONT14_IN_AA(T179, X155)
FRONT1_IN_AG(tree(T215, void, T221), T218) → U33_AG(T215, T221, T218, front14_in_aa(T221, X265))
FRONT1_IN_AG(tree(T215, void, T221), T218) → FRONT14_IN_AA(T221, X265)
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → U34_AG(T215, T238, T237, T218, front14_in_aa(T237, X265))
FRONT1_IN_AG(tree(T215, tree(T238, void, void), T237), T218) → FRONT14_IN_AA(T237, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → U35_AG(T215, T269, T272, T273, T274, T218, front14_in_aa(T272, X339))
FRONT1_IN_AG(tree(T215, tree(T269, T272, T273), T274), T218) → FRONT14_IN_AA(T272, X339)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T277), T218) → U36_AG(T215, T269, T272, T276, T277, T218, frontc14_in_aa(T272, T275))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → U37_AG(T215, T269, T272, T276, T277, T218, front14_in_aa(T276, X340))
U36_AG(T215, T269, T272, T276, T277, T218, frontc14_out_aa(T272, T275)) → FRONT14_IN_AA(T276, X340)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T282), T218) → U38_AG(T215, T269, T272, T276, T282, T218, frontc14_in_aa(T272, T281))
U38_AG(T215, T269, T272, T276, T282, T218, frontc14_out_aa(T272, T281)) → U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_in_aa(T276, T280))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → U40_AG(T215, T269, T272, T276, T282, T218, app32_in_gga(T281, T280, X341))
U39_AG(T215, T269, T272, T276, T282, T218, T281, frontc14_out_aa(T276, T280)) → APP32_IN_GGA(T281, T280, X341)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), T218) → U41_AG(T215, T269, T272, T276, T288, T218, frontc14_in_aa(T272, T281))
U41_AG(T215, T269, T272, T276, T288, T218, frontc14_out_aa(T272, T281)) → U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_in_aa(T276, T280))
U42_AG(T215, T269, T272, T276, T288, T218, T281, frontc14_out_aa(T276, T280)) → U43_AG(T215, T269, T272, T276, T288, T218, appc32_in_gga(T281, T280, T287))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → U44_AG(T215, T269, T272, T276, T288, T218, front14_in_aa(T288, X265))
U43_AG(T215, T269, T272, T276, T288, T218, appc32_out_gga(T281, T280, T287)) → FRONT14_IN_AA(T288, X265)
FRONT1_IN_AG(tree(T215, tree(T269, T272, T276), T288), .(T312, .(T333, T336))) → U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_in_aa(T272, T281))
U45_AG(T215, T269, T272, T276, T288, T312, T333, T336, frontc14_out_aa(T272, T281)) → U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_in_aa(T276, T280))
U46_AG(T215, T269, T272, T276, T288, T312, T333, T336, T281, frontc14_out_aa(T276, T280)) → U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_in_gga(T281, T280, .(T312, .(T333, T337))))
U47_AG(T215, T269, T272, T276, T288, T312, T333, T336, appc32_out_gga(T281, T280, .(T312, .(T333, T337)))) → U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_in_aa(T288, T338))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → U49_AG(T215, T269, T272, T276, T288, T312, T333, T336, app178_in_ggg(T337, T338, T336))
U48_AG(T215, T269, T272, T276, T288, T312, T333, T336, T337, frontc14_out_aa(T288, T338)) → APP178_IN_GGG(T337, T338, T336)
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → U8_GGG(T354, T358, T359, T357, app178_in_ggg(T358, T359, T357))
APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
front14_in_aa(x1, x2)  =  front14_in_aa
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
app32_in_gga(x1, x2, x3)  =  app32_in_gga(x1, x2)
app178_in_ggg(x1, x2, x3)  =  app178_in_ggg(x1, x2, x3)
FRONT1_IN_AG(x1, x2)  =  FRONT1_IN_AG(x2)
U9_AG(x1, x2, x3)  =  U9_AG(x3)
FRONT14_IN_AA(x1, x2)  =  FRONT14_IN_AA
U1_AA(x1, x2, x3, x4, x5)  =  U1_AA(x5)
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)
U3_AA(x1, x2, x3, x4, x5)  =  U3_AA(x5)
U4_AA(x1, x2, x3, x4, x5)  =  U4_AA(x5)
U5_AA(x1, x2, x3, x4, x5, x6)  =  U5_AA(x5, x6)
U6_AA(x1, x2, x3, x4, x5)  =  U6_AA(x5)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4, x5)  =  U7_GGA(x2, x3, x5)
U10_AG(x1, x2, x3, x4)  =  U10_AG(x4)
U11_AG(x1, x2, x3, x4, x5, x6)  =  U11_AG(x6)
U12_AG(x1, x2, x3, x4, x5, x6)  =  U12_AG(x6)
U13_AG(x1, x2, x3, x4, x5, x6)  =  U13_AG(x6)
U14_AG(x1, x2, x3, x4, x5, x6)  =  U14_AG(x6)
U15_AG(x1, x2, x3, x4, x5, x6, x7)  =  U15_AG(x6, x7)
U16_AG(x1, x2, x3, x4, x5, x6)  =  U16_AG(x6)
U17_AG(x1, x2, x3, x4, x5, x6)  =  U17_AG(x6)
U18_AG(x1, x2, x3, x4, x5, x6, x7)  =  U18_AG(x6, x7)
U19_AG(x1, x2, x3, x4, x5, x6)  =  U19_AG(x6)
U20_AG(x1, x2, x3, x4, x5, x6)  =  U20_AG(x6)
U21_AG(x1, x2, x3, x4)  =  U21_AG(x4)
U22_AG(x1, x2, x3, x4, x5)  =  U22_AG(x5)
U23_AG(x1, x2, x3, x4, x5, x6, x7)  =  U23_AG(x7)
U24_AG(x1, x2, x3, x4, x5, x6, x7)  =  U24_AG(x7)
U25_AG(x1, x2, x3, x4, x5, x6, x7)  =  U25_AG(x7)
U26_AG(x1, x2, x3, x4, x5, x6, x7)  =  U26_AG(x7)
U27_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U27_AG(x7, x8)
U28_AG(x1, x2, x3, x4, x5, x6, x7)  =  U28_AG(x7)
U29_AG(x1, x2, x3, x4, x5, x6, x7)  =  U29_AG(x7)
U30_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U30_AG(x7, x8)
U31_AG(x1, x2, x3, x4, x5, x6, x7)  =  U31_AG(x7)
U32_AG(x1, x2, x3, x4, x5, x6, x7)  =  U32_AG(x7)
U33_AG(x1, x2, x3, x4)  =  U33_AG(x3, x4)
U34_AG(x1, x2, x3, x4, x5)  =  U34_AG(x4, x5)
U35_AG(x1, x2, x3, x4, x5, x6, x7)  =  U35_AG(x6, x7)
U36_AG(x1, x2, x3, x4, x5, x6, x7)  =  U36_AG(x6, x7)
U37_AG(x1, x2, x3, x4, x5, x6, x7)  =  U37_AG(x6, x7)
U38_AG(x1, x2, x3, x4, x5, x6, x7)  =  U38_AG(x6, x7)
U39_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U39_AG(x6, x7, x8)
U40_AG(x1, x2, x3, x4, x5, x6, x7)  =  U40_AG(x6, x7)
U41_AG(x1, x2, x3, x4, x5, x6, x7)  =  U41_AG(x6, x7)
U42_AG(x1, x2, x3, x4, x5, x6, x7, x8)  =  U42_AG(x6, x7, x8)
U43_AG(x1, x2, x3, x4, x5, x6, x7)  =  U43_AG(x6, x7)
U44_AG(x1, x2, x3, x4, x5, x6, x7)  =  U44_AG(x6, x7)
U45_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U45_AG(x8, x9)
U46_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U46_AG(x8, x9, x10)
U47_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_AG(x8, x9)
U48_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9, x10)  =  U48_AG(x8, x9, x10)
U49_AG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U49_AG(x8, x9)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)
U8_GGG(x1, x2, x3, x4, x5)  =  U8_GGG(x2, x3, x4, x5)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
APP178_IN_GGG(x1, x2, x3)  =  APP178_IN_GGG(x1, x2, x3)

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:

APP178_IN_GGG(.(T354, T358), T359, .(T354, T357)) → APP178_IN_GGG(T358, T359, T357)

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

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:

APP178_IN_GGG(.(T358), T359, .(T357)) → APP178_IN_GGG(T358, T359, T357)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • APP178_IN_GGG(.(T358), T359, .(T357)) → APP178_IN_GGG(T358, T359, T357)
    The graph contains the following edges 1 > 1, 2 >= 2, 3 > 3

(15) YES

(16) Obligation:

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

APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
APP32_IN_GGA(x1, x2, x3)  =  APP32_IN_GGA(x1, x2)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

APP32_IN_GGA(.(T47, T50), T51, .(T47, X68)) → APP32_IN_GGA(T50, T51, X68)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

APP32_IN_GGA(.(T50), T51) → APP32_IN_GGA(T50, T51)

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:

  • APP32_IN_GGA(.(T50), T51) → APP32_IN_GGA(T50, T51)
    The graph contains the following edges 1 > 1, 2 >= 2

(22) YES

(23) Obligation:

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

FRONT14_IN_AA(tree(T25, T28, T31), X41) → U2_AA(T25, T28, T31, X41, frontc14_in_aa(T28, T30))
U2_AA(T25, T28, T31, X41, frontc14_out_aa(T28, T30)) → FRONT14_IN_AA(T31, X40)
FRONT14_IN_AA(tree(T25, T28, T29), X41) → FRONT14_IN_AA(T28, X39)

The TRS R consists of the following rules:

frontc14_in_aa(void, []) → frontc14_out_aa(void, [])
frontc14_in_aa(tree(T18, void, void), .(T18, [])) → frontc14_out_aa(tree(T18, void, void), .(T18, []))
frontc14_in_aa(tree(T25, T28, T31), X41) → U51_aa(T25, T28, T31, X41, frontc14_in_aa(T28, T33))
U51_aa(T25, T28, T31, X41, frontc14_out_aa(T28, T33)) → U52_aa(T25, T28, T31, X41, T33, frontc14_in_aa(T31, T32))
U52_aa(T25, T28, T31, X41, T33, frontc14_out_aa(T31, T32)) → U53_aa(T25, T28, T31, X41, appc32_in_gga(T33, T32, X41))
appc32_in_gga([], T40, T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T47, T50), T51, .(T47, X68)) → U54_gga(T47, T50, T51, X68, appc32_in_gga(T50, T51, X68))
U54_gga(T47, T50, T51, X68, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T47, T50), T51, .(T47, X68))
U53_aa(T25, T28, T31, X41, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T25, T28, T31), X41)

The argument filtering Pi contains the following mapping:
[]  =  []
frontc14_in_aa(x1, x2)  =  frontc14_in_aa
frontc14_out_aa(x1, x2)  =  frontc14_out_aa(x1, x2)
tree(x1, x2, x3)  =  tree(x2, x3)
.(x1, x2)  =  .(x2)
U51_aa(x1, x2, x3, x4, x5)  =  U51_aa(x5)
U52_aa(x1, x2, x3, x4, x5, x6)  =  U52_aa(x2, x5, x6)
U53_aa(x1, x2, x3, x4, x5)  =  U53_aa(x2, x3, x5)
appc32_in_gga(x1, x2, x3)  =  appc32_in_gga(x1, x2)
appc32_out_gga(x1, x2, x3)  =  appc32_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3, x4, x5)  =  U54_gga(x2, x3, x5)
FRONT14_IN_AA(x1, x2)  =  FRONT14_IN_AA
U2_AA(x1, x2, x3, x4, x5)  =  U2_AA(x5)

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

FRONT14_IN_AAU2_AA(frontc14_in_aa)
U2_AA(frontc14_out_aa(T28, T30)) → FRONT14_IN_AA
FRONT14_IN_AAFRONT14_IN_AA

The TRS R consists of the following rules:

frontc14_in_aafrontc14_out_aa(void, [])
frontc14_in_aafrontc14_out_aa(tree(void, void), .([]))
frontc14_in_aaU51_aa(frontc14_in_aa)
U51_aa(frontc14_out_aa(T28, T33)) → U52_aa(T28, T33, frontc14_in_aa)
U52_aa(T28, T33, frontc14_out_aa(T31, T32)) → U53_aa(T28, T31, appc32_in_gga(T33, T32))
appc32_in_gga([], T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T50), T51) → U54_gga(T50, T51, appc32_in_gga(T50, T51))
U54_gga(T50, T51, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T50), T51, .(X68))
U53_aa(T28, T31, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T28, T31), X41)

The set Q consists of the following terms:

frontc14_in_aa
U51_aa(x0)
U52_aa(x0, x1, x2)
appc32_in_gga(x0, x1)
U54_gga(x0, x1, x2)
U53_aa(x0, x1, x2)

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

(26) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule FRONT14_IN_AAU2_AA(frontc14_in_aa) at position [0] we obtained the following new rules [LPAR04]:

FRONT14_IN_AAU2_AA(frontc14_out_aa(void, []))
FRONT14_IN_AAU2_AA(frontc14_out_aa(tree(void, void), .([])))
FRONT14_IN_AAU2_AA(U51_aa(frontc14_in_aa))

(27) Obligation:

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

U2_AA(frontc14_out_aa(T28, T30)) → FRONT14_IN_AA
FRONT14_IN_AAFRONT14_IN_AA
FRONT14_IN_AAU2_AA(frontc14_out_aa(void, []))
FRONT14_IN_AAU2_AA(frontc14_out_aa(tree(void, void), .([])))
FRONT14_IN_AAU2_AA(U51_aa(frontc14_in_aa))

The TRS R consists of the following rules:

frontc14_in_aafrontc14_out_aa(void, [])
frontc14_in_aafrontc14_out_aa(tree(void, void), .([]))
frontc14_in_aaU51_aa(frontc14_in_aa)
U51_aa(frontc14_out_aa(T28, T33)) → U52_aa(T28, T33, frontc14_in_aa)
U52_aa(T28, T33, frontc14_out_aa(T31, T32)) → U53_aa(T28, T31, appc32_in_gga(T33, T32))
appc32_in_gga([], T40) → appc32_out_gga([], T40, T40)
appc32_in_gga(.(T50), T51) → U54_gga(T50, T51, appc32_in_gga(T50, T51))
U54_gga(T50, T51, appc32_out_gga(T50, T51, X68)) → appc32_out_gga(.(T50), T51, .(X68))
U53_aa(T28, T31, appc32_out_gga(T33, T32, X41)) → frontc14_out_aa(tree(T28, T31), X41)

The set Q consists of the following terms:

frontc14_in_aa
U51_aa(x0)
U52_aa(x0, x1, x2)
appc32_in_gga(x0, x1)
U54_gga(x0, x1, x2)
U53_aa(x0, x1, x2)

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

(28) 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 = FRONT14_IN_AA evaluates to t =FRONT14_IN_AA

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



(29) NO