(0) Obligation:

Clauses:

delete(X, tree(X, void, Right), Right).
delete(X, tree(X, Left, void), Left).
delete(X, tree(X, Left, Right), tree(Y, Left, Right1)) :- delmin(Right, Y, Right1).
delete(X, tree(Y, Left, Right), tree(Y, Left1, Right)) :- ','(less(X, Y), delete(X, Left, Left1)).
delete(X, tree(Y, Left, Right), tree(Y, Left, Right1)) :- ','(less(Y, X), delete(X, Right, Right1)).
delmin(tree(Y, void, Right), Y, Right).
delmin(tree(X, Left, X1), Y, tree(X, Left1, X2)) :- delmin(Left, Y, Left1).
less(0, s(X3)).
less(s(X), s(Y)) :- less(X, Y).

Queries:

delete(a,g,a).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

less19(s(T52), s(T51)) :- less19(T52, T51).
less31(s(T88), s(T90)) :- less31(T88, T90).
p29(T69, T71, T72) :- less31(T69, T71).
p29(T69, T75, T76) :- ','(lessc31(T69, T75), delete1(T75, void, T76)).
delmin78(tree(T273, T274, T275), T279, tree(T273, T280, T278)) :- delmin78(T274, T279, T280).
p17(T33, T31, T34) :- less19(T33, T31).
p17(T37, T31, T38) :- ','(lessc19(T37, T31), delete1(T37, void, T38)).
p50(T124, T123, T125) :- less19(T124, T123).
p50(T128, T123, T129) :- ','(lessc19(T128, T123), delete1(s(T128), void, T129)).
p93(T318, T321, T319, T322) :- less31(T318, T321).
p93(T318, T325, T319, T326) :- ','(lessc31(T318, T325), delete1(T325, T319, T326)).
p64(T178, T180, T181) :- less31(T178, T180).
p64(T178, T184, T185) :- ','(lessc31(T178, T184), delete1(s(T184), void, T185)).
delete1(T33, tree(T31, void, void), tree(T31, T34, void)) :- p17(T33, T31, T34).
delete1(T71, tree(T69, void, void), tree(T69, void, T72)) :- p29(T69, T71, T72).
delete1(0, tree(s(T112), void, void), tree(s(T112), T113, void)) :- delete1(0, void, T113).
delete1(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) :- p50(T124, T123, T125).
delete1(T148, tree(T146, void, void), tree(T146, void, T149)) :- p29(T146, T148, T149).
delete1(s(T166), tree(0, void, void), tree(0, void, T165)) :- delete1(s(T166), void, T165).
delete1(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) :- p64(T178, T180, T181).
delete1(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) :- delmin78(T240, T245, T246).
delete1(T305, tree(T302, void, T303), tree(T302, T306, T303)) :- p17(T305, T302, T306).
delete1(T321, tree(T318, void, T319), tree(T318, void, T322)) :- p93(T318, T321, T319, T322).
delete1(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) :- delete1(0, void, T352).
delete1(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) :- p50(T363, T362, T364).
delete1(T379, tree(T376, void, T377), tree(T376, void, T380)) :- p93(T376, T379, T377, T380).
delete1(s(T399), tree(0, void, T389), tree(0, void, T398)) :- delete1(s(T399), T389, T398).
delete1(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) :- less31(T408, T410).
delete1(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) :- ','(lessc31(T408, T414), delete1(s(T414), T389, T415)).
delete1(T460, tree(T457, T458, void), tree(T457, T461, void)) :- less19(T460, T457).
delete1(T464, tree(T457, T458, void), tree(T457, T465, void)) :- ','(lessc19(T464, T457), delete1(T464, T458, T465)).
delete1(T488, tree(T485, T486, void), tree(T485, T486, T489)) :- p29(T485, T488, T489).
delete1(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) :- delete1(0, T498, T507).
delete1(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) :- less19(T520, T519).
delete1(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) :- ','(lessc19(T524, T519), delete1(s(T524), T498, T525)).
delete1(T548, tree(T545, T546, void), tree(T545, T546, T549)) :- p29(T545, T548, T549).
delete1(s(T568), tree(0, T558, void), tree(0, T558, T567)) :- delete1(s(T568), void, T567).
delete1(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) :- p64(T580, T582, T583).
delete1(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) :- delmin78(T633, T638, T639).
delete1(T669, tree(T665, T666, T667), tree(T665, T670, T667)) :- less19(T669, T665).
delete1(T673, tree(T665, T666, T676), tree(T665, T674, T676)) :- ','(lessc19(T673, T665), delete1(T673, T666, T674)).
delete1(T703, tree(T699, T700, T701), tree(T699, T700, T704)) :- less31(T699, T703).
delete1(T707, tree(T699, T710, T701), tree(T699, T710, T708)) :- ','(lessc31(T699, T707), delete1(T707, T701, T708)).
delete1(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) :- delete1(0, T729, T739).
delete1(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) :- less19(T752, T751).
delete1(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) :- ','(lessc19(T756, T751), delete1(s(T756), T729, T757)).
delete1(T784, tree(T780, T781, T782), tree(T780, T781, T785)) :- less31(T780, T784).
delete1(T788, tree(T780, T791, T782), tree(T780, T791, T789)) :- ','(lessc31(T780, T788), delete1(T788, T782, T789)).
delete1(s(T826), tree(0, T815, T816), tree(0, T815, T825)) :- delete1(s(T826), T816, T825).
delete1(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) :- less31(T835, T837).
delete1(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) :- ','(lessc31(T835, T841), delete1(s(T841), T816, T842)).

Clauses:

deletec1(T6, tree(T6, void, T7), T7).
deletec1(T9, tree(T9, void, void), void).
deletec1(T33, tree(T31, void, void), tree(T31, T34, void)) :- qc17(T33, T31, T34).
deletec1(T71, tree(T69, void, void), tree(T69, void, T72)) :- qc29(T69, T71, T72).
deletec1(0, tree(s(T112), void, void), tree(s(T112), T113, void)) :- deletec1(0, void, T113).
deletec1(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) :- qc50(T124, T123, T125).
deletec1(T148, tree(T146, void, void), tree(T146, void, T149)) :- qc29(T146, T148, T149).
deletec1(s(T166), tree(0, void, void), tree(0, void, T165)) :- deletec1(s(T166), void, T165).
deletec1(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) :- qc64(T178, T180, T181).
deletec1(T199, tree(T199, void, tree(T213, void, T214)), tree(T213, void, T214)).
deletec1(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) :- delminc78(T240, T245, T246).
deletec1(T305, tree(T302, void, T303), tree(T302, T306, T303)) :- qc17(T305, T302, T306).
deletec1(T321, tree(T318, void, T319), tree(T318, void, T322)) :- qc93(T318, T321, T319, T322).
deletec1(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) :- deletec1(0, void, T352).
deletec1(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) :- qc50(T363, T362, T364).
deletec1(T379, tree(T376, void, T377), tree(T376, void, T380)) :- qc93(T376, T379, T377, T380).
deletec1(s(T399), tree(0, void, T389), tree(0, void, T398)) :- deletec1(s(T399), T389, T398).
deletec1(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) :- ','(lessc31(T408, T414), deletec1(s(T414), T389, T415)).
deletec1(T428, tree(T428, T429, void), T429).
deletec1(T464, tree(T457, T458, void), tree(T457, T465, void)) :- ','(lessc19(T464, T457), deletec1(T464, T458, T465)).
deletec1(T488, tree(T485, T486, void), tree(T485, T486, T489)) :- qc29(T485, T488, T489).
deletec1(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) :- deletec1(0, T498, T507).
deletec1(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) :- ','(lessc19(T524, T519), deletec1(s(T524), T498, T525)).
deletec1(T548, tree(T545, T546, void), tree(T545, T546, T549)) :- qc29(T545, T548, T549).
deletec1(s(T568), tree(0, T558, void), tree(0, T558, T567)) :- deletec1(s(T568), void, T567).
deletec1(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) :- qc64(T580, T582, T583).
deletec1(T591, tree(T591, T592, tree(T606, void, T607)), tree(T606, T592, T607)).
deletec1(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) :- delminc78(T633, T638, T639).
deletec1(T673, tree(T665, T666, T676), tree(T665, T674, T676)) :- ','(lessc19(T673, T665), deletec1(T673, T666, T674)).
deletec1(T707, tree(T699, T710, T701), tree(T699, T710, T708)) :- ','(lessc31(T699, T707), deletec1(T707, T701, T708)).
deletec1(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) :- deletec1(0, T729, T739).
deletec1(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) :- ','(lessc19(T756, T751), deletec1(s(T756), T729, T757)).
deletec1(T788, tree(T780, T791, T782), tree(T780, T791, T789)) :- ','(lessc31(T780, T788), deletec1(T788, T782, T789)).
deletec1(s(T826), tree(0, T815, T816), tree(0, T815, T825)) :- deletec1(s(T826), T816, T825).
deletec1(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) :- ','(lessc31(T835, T841), deletec1(s(T841), T816, T842)).
lessc19(0, s(T45)).
lessc19(s(T52), s(T51)) :- lessc19(T52, T51).
lessc31(0, s(T83)).
lessc31(s(T88), s(T90)) :- lessc31(T88, T90).
qc29(T69, T75, T76) :- ','(lessc31(T69, T75), deletec1(T75, void, T76)).
delminc78(tree(T259, void, T260), T259, T260).
delminc78(tree(T273, T274, T275), T279, tree(T273, T280, T278)) :- delminc78(T274, T279, T280).
qc17(T37, T31, T38) :- ','(lessc19(T37, T31), deletec1(T37, void, T38)).
qc50(T128, T123, T129) :- ','(lessc19(T128, T123), deletec1(s(T128), void, T129)).
qc93(T318, T325, T319, T326) :- ','(lessc31(T318, T325), deletec1(T325, T319, T326)).
qc64(T178, T184, T185) :- ','(lessc31(T178, T184), deletec1(s(T184), void, T185)).

Afs:

delete1(x1, x2, x3)  =  delete1(x2)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
delete1_in: (f,b,f) (b,b,f)
p17_in: (f,b,f) (b,b,f)
less19_in: (f,b) (b,b)
lessc19_in: (f,b) (b,b)
p29_in: (b,b,f) (b,f,f)
less31_in: (b,b) (b,f)
lessc31_in: (b,b) (b,f)
p50_in: (b,b,f) (f,b,f)
p64_in: (b,b,f) (b,f,f)
delmin78_in: (b,f,f)
p93_in: (b,b,b,f) (b,f,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_AGA(T33, tree(T31, void, void), tree(T31, T34, void)) → U19_AGA(T33, T31, T34, p17_in_aga(T33, T31, T34))
DELETE1_IN_AGA(T33, tree(T31, void, void), tree(T31, T34, void)) → P17_IN_AGA(T33, T31, T34)
P17_IN_AGA(T33, T31, T34) → U7_AGA(T33, T31, T34, less19_in_ag(T33, T31))
P17_IN_AGA(T33, T31, T34) → LESS19_IN_AG(T33, T31)
LESS19_IN_AG(s(T52), s(T51)) → U1_AG(T52, T51, less19_in_ag(T52, T51))
LESS19_IN_AG(s(T52), s(T51)) → LESS19_IN_AG(T52, T51)
P17_IN_AGA(T37, T31, T38) → U8_AGA(T37, T31, T38, lessc19_in_ag(T37, T31))
U8_AGA(T37, T31, T38, lessc19_out_ag(T37, T31)) → U9_AGA(T37, T31, T38, delete1_in_gga(T37, void, T38))
U8_AGA(T37, T31, T38, lessc19_out_ag(T37, T31)) → DELETE1_IN_GGA(T37, void, T38)
DELETE1_IN_GGA(T33, tree(T31, void, void), tree(T31, T34, void)) → U19_GGA(T33, T31, T34, p17_in_gga(T33, T31, T34))
DELETE1_IN_GGA(T33, tree(T31, void, void), tree(T31, T34, void)) → P17_IN_GGA(T33, T31, T34)
P17_IN_GGA(T33, T31, T34) → U7_GGA(T33, T31, T34, less19_in_gg(T33, T31))
P17_IN_GGA(T33, T31, T34) → LESS19_IN_GG(T33, T31)
LESS19_IN_GG(s(T52), s(T51)) → U1_GG(T52, T51, less19_in_gg(T52, T51))
LESS19_IN_GG(s(T52), s(T51)) → LESS19_IN_GG(T52, T51)
P17_IN_GGA(T37, T31, T38) → U8_GGA(T37, T31, T38, lessc19_in_gg(T37, T31))
U8_GGA(T37, T31, T38, lessc19_out_gg(T37, T31)) → U9_GGA(T37, T31, T38, delete1_in_gga(T37, void, T38))
U8_GGA(T37, T31, T38, lessc19_out_gg(T37, T31)) → DELETE1_IN_GGA(T37, void, T38)
DELETE1_IN_GGA(T71, tree(T69, void, void), tree(T69, void, T72)) → U20_GGA(T71, T69, T72, p29_in_gga(T69, T71, T72))
DELETE1_IN_GGA(T71, tree(T69, void, void), tree(T69, void, T72)) → P29_IN_GGA(T69, T71, T72)
P29_IN_GGA(T69, T71, T72) → U3_GGA(T69, T71, T72, less31_in_gg(T69, T71))
P29_IN_GGA(T69, T71, T72) → LESS31_IN_GG(T69, T71)
LESS31_IN_GG(s(T88), s(T90)) → U2_GG(T88, T90, less31_in_gg(T88, T90))
LESS31_IN_GG(s(T88), s(T90)) → LESS31_IN_GG(T88, T90)
P29_IN_GGA(T69, T75, T76) → U4_GGA(T69, T75, T76, lessc31_in_gg(T69, T75))
U4_GGA(T69, T75, T76, lessc31_out_gg(T69, T75)) → U5_GGA(T69, T75, T76, delete1_in_gga(T75, void, T76))
U4_GGA(T69, T75, T76, lessc31_out_gg(T69, T75)) → DELETE1_IN_GGA(T75, void, T76)
DELETE1_IN_GGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → U21_GGA(T112, T113, delete1_in_gga(0, void, T113))
DELETE1_IN_GGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → DELETE1_IN_GGA(0, void, T113)
DELETE1_IN_GGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → U22_GGA(T124, T123, T125, p50_in_gga(T124, T123, T125))
DELETE1_IN_GGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → P50_IN_GGA(T124, T123, T125)
P50_IN_GGA(T124, T123, T125) → U10_GGA(T124, T123, T125, less19_in_gg(T124, T123))
P50_IN_GGA(T124, T123, T125) → LESS19_IN_GG(T124, T123)
P50_IN_GGA(T128, T123, T129) → U11_GGA(T128, T123, T129, lessc19_in_gg(T128, T123))
U11_GGA(T128, T123, T129, lessc19_out_gg(T128, T123)) → U12_GGA(T128, T123, T129, delete1_in_gga(s(T128), void, T129))
U11_GGA(T128, T123, T129, lessc19_out_gg(T128, T123)) → DELETE1_IN_GGA(s(T128), void, T129)
DELETE1_IN_GGA(T148, tree(T146, void, void), tree(T146, void, T149)) → U23_GGA(T148, T146, T149, p29_in_gga(T146, T148, T149))
DELETE1_IN_GGA(s(T166), tree(0, void, void), tree(0, void, T165)) → U24_GGA(T166, T165, delete1_in_gga(s(T166), void, T165))
DELETE1_IN_GGA(s(T166), tree(0, void, void), tree(0, void, T165)) → DELETE1_IN_GGA(s(T166), void, T165)
DELETE1_IN_GGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → U25_GGA(T180, T178, T181, p64_in_gga(T178, T180, T181))
DELETE1_IN_GGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → P64_IN_GGA(T178, T180, T181)
P64_IN_GGA(T178, T180, T181) → U16_GGA(T178, T180, T181, less31_in_gg(T178, T180))
P64_IN_GGA(T178, T180, T181) → LESS31_IN_GG(T178, T180)
P64_IN_GGA(T178, T184, T185) → U17_GGA(T178, T184, T185, lessc31_in_gg(T178, T184))
U17_GGA(T178, T184, T185, lessc31_out_gg(T178, T184)) → U18_GGA(T178, T184, T185, delete1_in_gga(s(T184), void, T185))
U17_GGA(T178, T184, T185, lessc31_out_gg(T178, T184)) → DELETE1_IN_GGA(s(T184), void, T185)
DELETE1_IN_GGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → U26_GGA(T199, T239, T240, T241, T245, T246, T244, delmin78_in_gaa(T240, T245, T246))
DELETE1_IN_GGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → DELMIN78_IN_GAA(T240, T245, T246)
DELMIN78_IN_GAA(tree(T273, T274, T275), T279, tree(T273, T280, T278)) → U6_GAA(T273, T274, T275, T279, T280, T278, delmin78_in_gaa(T274, T279, T280))
DELMIN78_IN_GAA(tree(T273, T274, T275), T279, tree(T273, T280, T278)) → DELMIN78_IN_GAA(T274, T279, T280)
DELETE1_IN_GGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → U27_GGA(T305, T302, T303, T306, p17_in_gga(T305, T302, T306))
DELETE1_IN_GGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → P17_IN_GGA(T305, T302, T306)
DELETE1_IN_GGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → U28_GGA(T321, T318, T319, T322, p93_in_ggga(T318, T321, T319, T322))
DELETE1_IN_GGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GGGA(T318, T321, T319, T322)
P93_IN_GGGA(T318, T321, T319, T322) → U13_GGGA(T318, T321, T319, T322, less31_in_gg(T318, T321))
P93_IN_GGGA(T318, T321, T319, T322) → LESS31_IN_GG(T318, T321)
P93_IN_GGGA(T318, T325, T319, T326) → U14_GGGA(T318, T325, T319, T326, lessc31_in_gg(T318, T325))
U14_GGGA(T318, T325, T319, T326, lessc31_out_gg(T318, T325)) → U15_GGGA(T318, T325, T319, T326, delete1_in_gga(T325, T319, T326))
U14_GGGA(T318, T325, T319, T326, lessc31_out_gg(T318, T325)) → DELETE1_IN_GGA(T325, T319, T326)
DELETE1_IN_GGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → U29_GGA(T351, T343, T352, delete1_in_gga(0, void, T352))
DELETE1_IN_GGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → DELETE1_IN_GGA(0, void, T352)
DELETE1_IN_GGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → U30_GGA(T363, T362, T343, T364, p50_in_gga(T363, T362, T364))
DELETE1_IN_GGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → P50_IN_GGA(T363, T362, T364)
DELETE1_IN_GGA(T379, tree(T376, void, T377), tree(T376, void, T380)) → U31_GGA(T379, T376, T377, T380, p93_in_ggga(T376, T379, T377, T380))
DELETE1_IN_GGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → U32_GGA(T399, T389, T398, delete1_in_gga(s(T399), T389, T398))
DELETE1_IN_GGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_GGA(s(T399), T389, T398)
DELETE1_IN_GGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → U33_GGA(T410, T408, T389, T411, less31_in_gg(T408, T410))
DELETE1_IN_GGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → LESS31_IN_GG(T408, T410)
DELETE1_IN_GGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_GGA(T414, T408, T389, T415, lessc31_in_gg(T408, T414))
U34_GGA(T414, T408, T389, T415, lessc31_out_gg(T408, T414)) → U35_GGA(T414, T408, T389, T415, delete1_in_gga(s(T414), T389, T415))
U34_GGA(T414, T408, T389, T415, lessc31_out_gg(T408, T414)) → DELETE1_IN_GGA(s(T414), T389, T415)
DELETE1_IN_GGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → U36_GGA(T460, T457, T458, T461, less19_in_gg(T460, T457))
DELETE1_IN_GGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → LESS19_IN_GG(T460, T457)
DELETE1_IN_GGA(T464, tree(T457, T458, void), tree(T457, T465, void)) → U37_GGA(T464, T457, T458, T465, lessc19_in_gg(T464, T457))
U37_GGA(T464, T457, T458, T465, lessc19_out_gg(T464, T457)) → U38_GGA(T464, T457, T458, T465, delete1_in_gga(T464, T458, T465))
U37_GGA(T464, T457, T458, T465, lessc19_out_gg(T464, T457)) → DELETE1_IN_GGA(T464, T458, T465)
DELETE1_IN_GGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → U39_GGA(T488, T485, T486, T489, p29_in_gga(T485, T488, T489))
DELETE1_IN_GGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → P29_IN_GGA(T485, T488, T489)
DELETE1_IN_GGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → U40_GGA(T506, T498, T507, delete1_in_gga(0, T498, T507))
DELETE1_IN_GGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → DELETE1_IN_GGA(0, T498, T507)
DELETE1_IN_GGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → U41_GGA(T520, T519, T498, T521, less19_in_gg(T520, T519))
DELETE1_IN_GGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → LESS19_IN_GG(T520, T519)
DELETE1_IN_GGA(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) → U42_GGA(T524, T519, T498, T525, lessc19_in_gg(T524, T519))
U42_GGA(T524, T519, T498, T525, lessc19_out_gg(T524, T519)) → U43_GGA(T524, T519, T498, T525, delete1_in_gga(s(T524), T498, T525))
U42_GGA(T524, T519, T498, T525, lessc19_out_gg(T524, T519)) → DELETE1_IN_GGA(s(T524), T498, T525)
DELETE1_IN_GGA(T548, tree(T545, T546, void), tree(T545, T546, T549)) → U44_GGA(T548, T545, T546, T549, p29_in_gga(T545, T548, T549))
DELETE1_IN_GGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → U45_GGA(T568, T558, T567, delete1_in_gga(s(T568), void, T567))
DELETE1_IN_GGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → DELETE1_IN_GGA(s(T568), void, T567)
DELETE1_IN_GGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → U46_GGA(T582, T580, T558, T583, p64_in_gga(T580, T582, T583))
DELETE1_IN_GGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → P64_IN_GGA(T580, T582, T583)
DELETE1_IN_GGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → U47_GGA(T591, T592, T632, T633, T634, T638, T639, T637, delmin78_in_gaa(T633, T638, T639))
DELETE1_IN_GGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → DELMIN78_IN_GAA(T633, T638, T639)
DELETE1_IN_GGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → U48_GGA(T669, T665, T666, T667, T670, less19_in_gg(T669, T665))
DELETE1_IN_GGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → LESS19_IN_GG(T669, T665)
DELETE1_IN_GGA(T673, tree(T665, T666, T676), tree(T665, T674, T676)) → U49_GGA(T673, T665, T666, T676, T674, lessc19_in_gg(T673, T665))
U49_GGA(T673, T665, T666, T676, T674, lessc19_out_gg(T673, T665)) → U50_GGA(T673, T665, T666, T676, T674, delete1_in_gga(T673, T666, T674))
U49_GGA(T673, T665, T666, T676, T674, lessc19_out_gg(T673, T665)) → DELETE1_IN_GGA(T673, T666, T674)
DELETE1_IN_GGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → U51_GGA(T703, T699, T700, T701, T704, less31_in_gg(T699, T703))
DELETE1_IN_GGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → LESS31_IN_GG(T699, T703)
DELETE1_IN_GGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_GGA(T707, T699, T710, T701, T708, lessc31_in_gg(T699, T707))
U52_GGA(T707, T699, T710, T701, T708, lessc31_out_gg(T699, T707)) → U53_GGA(T707, T699, T710, T701, T708, delete1_in_gga(T707, T701, T708))
U52_GGA(T707, T699, T710, T701, T708, lessc31_out_gg(T699, T707)) → DELETE1_IN_GGA(T707, T701, T708)
DELETE1_IN_GGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → U54_GGA(T738, T729, T730, T739, delete1_in_gga(0, T729, T739))
DELETE1_IN_GGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → DELETE1_IN_GGA(0, T729, T739)
DELETE1_IN_GGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → U55_GGA(T752, T751, T729, T730, T753, less19_in_gg(T752, T751))
DELETE1_IN_GGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → LESS19_IN_GG(T752, T751)
DELETE1_IN_GGA(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) → U56_GGA(T756, T751, T729, T759, T757, lessc19_in_gg(T756, T751))
U56_GGA(T756, T751, T729, T759, T757, lessc19_out_gg(T756, T751)) → U57_GGA(T756, T751, T729, T759, T757, delete1_in_gga(s(T756), T729, T757))
U56_GGA(T756, T751, T729, T759, T757, lessc19_out_gg(T756, T751)) → DELETE1_IN_GGA(s(T756), T729, T757)
DELETE1_IN_GGA(T784, tree(T780, T781, T782), tree(T780, T781, T785)) → U58_GGA(T784, T780, T781, T782, T785, less31_in_gg(T780, T784))
DELETE1_IN_GGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_GGA(T788, T780, T791, T782, T789, lessc31_in_gg(T780, T788))
U59_GGA(T788, T780, T791, T782, T789, lessc31_out_gg(T780, T788)) → U60_GGA(T788, T780, T791, T782, T789, delete1_in_gga(T788, T782, T789))
U59_GGA(T788, T780, T791, T782, T789, lessc31_out_gg(T780, T788)) → DELETE1_IN_GGA(T788, T782, T789)
DELETE1_IN_GGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → U61_GGA(T826, T815, T816, T825, delete1_in_gga(s(T826), T816, T825))
DELETE1_IN_GGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_GGA(s(T826), T816, T825)
DELETE1_IN_GGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → U62_GGA(T837, T835, T815, T816, T838, less31_in_gg(T835, T837))
DELETE1_IN_GGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → LESS31_IN_GG(T835, T837)
DELETE1_IN_GGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_GGA(T841, T835, T844, T816, T842, lessc31_in_gg(T835, T841))
U63_GGA(T841, T835, T844, T816, T842, lessc31_out_gg(T835, T841)) → U64_GGA(T841, T835, T844, T816, T842, delete1_in_gga(s(T841), T816, T842))
U63_GGA(T841, T835, T844, T816, T842, lessc31_out_gg(T835, T841)) → DELETE1_IN_GGA(s(T841), T816, T842)
DELETE1_IN_AGA(T71, tree(T69, void, void), tree(T69, void, T72)) → U20_AGA(T71, T69, T72, p29_in_gaa(T69, T71, T72))
DELETE1_IN_AGA(T71, tree(T69, void, void), tree(T69, void, T72)) → P29_IN_GAA(T69, T71, T72)
P29_IN_GAA(T69, T71, T72) → U3_GAA(T69, T71, T72, less31_in_ga(T69, T71))
P29_IN_GAA(T69, T71, T72) → LESS31_IN_GA(T69, T71)
LESS31_IN_GA(s(T88), s(T90)) → U2_GA(T88, T90, less31_in_ga(T88, T90))
LESS31_IN_GA(s(T88), s(T90)) → LESS31_IN_GA(T88, T90)
P29_IN_GAA(T69, T75, T76) → U4_GAA(T69, T75, T76, lessc31_in_ga(T69, T75))
U4_GAA(T69, T75, T76, lessc31_out_ga(T69, T75)) → U5_GAA(T69, T75, T76, delete1_in_aga(T75, void, T76))
U4_GAA(T69, T75, T76, lessc31_out_ga(T69, T75)) → DELETE1_IN_AGA(T75, void, T76)
DELETE1_IN_AGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → U21_AGA(T112, T113, delete1_in_gga(0, void, T113))
DELETE1_IN_AGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → DELETE1_IN_GGA(0, void, T113)
DELETE1_IN_AGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → U22_AGA(T124, T123, T125, p50_in_aga(T124, T123, T125))
DELETE1_IN_AGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → P50_IN_AGA(T124, T123, T125)
P50_IN_AGA(T124, T123, T125) → U10_AGA(T124, T123, T125, less19_in_ag(T124, T123))
P50_IN_AGA(T124, T123, T125) → LESS19_IN_AG(T124, T123)
P50_IN_AGA(T128, T123, T129) → U11_AGA(T128, T123, T129, lessc19_in_ag(T128, T123))
U11_AGA(T128, T123, T129, lessc19_out_ag(T128, T123)) → U12_AGA(T128, T123, T129, delete1_in_gga(s(T128), void, T129))
U11_AGA(T128, T123, T129, lessc19_out_ag(T128, T123)) → DELETE1_IN_GGA(s(T128), void, T129)
DELETE1_IN_AGA(T148, tree(T146, void, void), tree(T146, void, T149)) → U23_AGA(T148, T146, T149, p29_in_gaa(T146, T148, T149))
DELETE1_IN_AGA(s(T166), tree(0, void, void), tree(0, void, T165)) → U24_AGA(T166, T165, delete1_in_aga(s(T166), void, T165))
DELETE1_IN_AGA(s(T166), tree(0, void, void), tree(0, void, T165)) → DELETE1_IN_AGA(s(T166), void, T165)
DELETE1_IN_AGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → U25_AGA(T180, T178, T181, p64_in_gaa(T178, T180, T181))
DELETE1_IN_AGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → P64_IN_GAA(T178, T180, T181)
P64_IN_GAA(T178, T180, T181) → U16_GAA(T178, T180, T181, less31_in_ga(T178, T180))
P64_IN_GAA(T178, T180, T181) → LESS31_IN_GA(T178, T180)
P64_IN_GAA(T178, T184, T185) → U17_GAA(T178, T184, T185, lessc31_in_ga(T178, T184))
U17_GAA(T178, T184, T185, lessc31_out_ga(T178, T184)) → U18_GAA(T178, T184, T185, delete1_in_aga(s(T184), void, T185))
U17_GAA(T178, T184, T185, lessc31_out_ga(T178, T184)) → DELETE1_IN_AGA(s(T184), void, T185)
DELETE1_IN_AGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → U26_AGA(T199, T239, T240, T241, T245, T246, T244, delmin78_in_gaa(T240, T245, T246))
DELETE1_IN_AGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → DELMIN78_IN_GAA(T240, T245, T246)
DELETE1_IN_AGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → U27_AGA(T305, T302, T303, T306, p17_in_aga(T305, T302, T306))
DELETE1_IN_AGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → P17_IN_AGA(T305, T302, T306)
DELETE1_IN_AGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → U28_AGA(T321, T318, T319, T322, p93_in_gaga(T318, T321, T319, T322))
DELETE1_IN_AGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GAGA(T318, T321, T319, T322)
P93_IN_GAGA(T318, T321, T319, T322) → U13_GAGA(T318, T321, T319, T322, less31_in_ga(T318, T321))
P93_IN_GAGA(T318, T321, T319, T322) → LESS31_IN_GA(T318, T321)
P93_IN_GAGA(T318, T325, T319, T326) → U14_GAGA(T318, T325, T319, T326, lessc31_in_ga(T318, T325))
U14_GAGA(T318, T325, T319, T326, lessc31_out_ga(T318, T325)) → U15_GAGA(T318, T325, T319, T326, delete1_in_aga(T325, T319, T326))
U14_GAGA(T318, T325, T319, T326, lessc31_out_ga(T318, T325)) → DELETE1_IN_AGA(T325, T319, T326)
DELETE1_IN_AGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → U29_AGA(T351, T343, T352, delete1_in_gga(0, void, T352))
DELETE1_IN_AGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → DELETE1_IN_GGA(0, void, T352)
DELETE1_IN_AGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → U30_AGA(T363, T362, T343, T364, p50_in_aga(T363, T362, T364))
DELETE1_IN_AGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → P50_IN_AGA(T363, T362, T364)
DELETE1_IN_AGA(T379, tree(T376, void, T377), tree(T376, void, T380)) → U31_AGA(T379, T376, T377, T380, p93_in_gaga(T376, T379, T377, T380))
DELETE1_IN_AGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → U32_AGA(T399, T389, T398, delete1_in_aga(s(T399), T389, T398))
DELETE1_IN_AGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_AGA(s(T399), T389, T398)
DELETE1_IN_AGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → U33_AGA(T410, T408, T389, T411, less31_in_ga(T408, T410))
DELETE1_IN_AGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → LESS31_IN_GA(T408, T410)
DELETE1_IN_AGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_AGA(T414, T408, T389, T415, lessc31_in_ga(T408, T414))
U34_AGA(T414, T408, T389, T415, lessc31_out_ga(T408, T414)) → U35_AGA(T414, T408, T389, T415, delete1_in_aga(s(T414), T389, T415))
U34_AGA(T414, T408, T389, T415, lessc31_out_ga(T408, T414)) → DELETE1_IN_AGA(s(T414), T389, T415)
DELETE1_IN_AGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → U36_AGA(T460, T457, T458, T461, less19_in_ag(T460, T457))
DELETE1_IN_AGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → LESS19_IN_AG(T460, T457)
DELETE1_IN_AGA(T464, tree(T457, T458, void), tree(T457, T465, void)) → U37_AGA(T464, T457, T458, T465, lessc19_in_ag(T464, T457))
U37_AGA(T464, T457, T458, T465, lessc19_out_ag(T464, T457)) → U38_AGA(T464, T457, T458, T465, delete1_in_gga(T464, T458, T465))
U37_AGA(T464, T457, T458, T465, lessc19_out_ag(T464, T457)) → DELETE1_IN_GGA(T464, T458, T465)
DELETE1_IN_AGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → U39_AGA(T488, T485, T486, T489, p29_in_gaa(T485, T488, T489))
DELETE1_IN_AGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → P29_IN_GAA(T485, T488, T489)
DELETE1_IN_AGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → U40_AGA(T506, T498, T507, delete1_in_gga(0, T498, T507))
DELETE1_IN_AGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → DELETE1_IN_GGA(0, T498, T507)
DELETE1_IN_AGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → U41_AGA(T520, T519, T498, T521, less19_in_ag(T520, T519))
DELETE1_IN_AGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → LESS19_IN_AG(T520, T519)
DELETE1_IN_AGA(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) → U42_AGA(T524, T519, T498, T525, lessc19_in_ag(T524, T519))
U42_AGA(T524, T519, T498, T525, lessc19_out_ag(T524, T519)) → U43_AGA(T524, T519, T498, T525, delete1_in_gga(s(T524), T498, T525))
U42_AGA(T524, T519, T498, T525, lessc19_out_ag(T524, T519)) → DELETE1_IN_GGA(s(T524), T498, T525)
DELETE1_IN_AGA(T548, tree(T545, T546, void), tree(T545, T546, T549)) → U44_AGA(T548, T545, T546, T549, p29_in_gaa(T545, T548, T549))
DELETE1_IN_AGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → U45_AGA(T568, T558, T567, delete1_in_aga(s(T568), void, T567))
DELETE1_IN_AGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → DELETE1_IN_AGA(s(T568), void, T567)
DELETE1_IN_AGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → U46_AGA(T582, T580, T558, T583, p64_in_gaa(T580, T582, T583))
DELETE1_IN_AGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → P64_IN_GAA(T580, T582, T583)
DELETE1_IN_AGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → U47_AGA(T591, T592, T632, T633, T634, T638, T639, T637, delmin78_in_gaa(T633, T638, T639))
DELETE1_IN_AGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → DELMIN78_IN_GAA(T633, T638, T639)
DELETE1_IN_AGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → U48_AGA(T669, T665, T666, T667, T670, less19_in_ag(T669, T665))
DELETE1_IN_AGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → LESS19_IN_AG(T669, T665)
DELETE1_IN_AGA(T673, tree(T665, T666, T676), tree(T665, T674, T676)) → U49_AGA(T673, T665, T666, T676, T674, lessc19_in_ag(T673, T665))
U49_AGA(T673, T665, T666, T676, T674, lessc19_out_ag(T673, T665)) → U50_AGA(T673, T665, T666, T676, T674, delete1_in_gga(T673, T666, T674))
U49_AGA(T673, T665, T666, T676, T674, lessc19_out_ag(T673, T665)) → DELETE1_IN_GGA(T673, T666, T674)
DELETE1_IN_AGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → U51_AGA(T703, T699, T700, T701, T704, less31_in_ga(T699, T703))
DELETE1_IN_AGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → LESS31_IN_GA(T699, T703)
DELETE1_IN_AGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_AGA(T707, T699, T710, T701, T708, lessc31_in_ga(T699, T707))
U52_AGA(T707, T699, T710, T701, T708, lessc31_out_ga(T699, T707)) → U53_AGA(T707, T699, T710, T701, T708, delete1_in_aga(T707, T701, T708))
U52_AGA(T707, T699, T710, T701, T708, lessc31_out_ga(T699, T707)) → DELETE1_IN_AGA(T707, T701, T708)
DELETE1_IN_AGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → U54_AGA(T738, T729, T730, T739, delete1_in_gga(0, T729, T739))
DELETE1_IN_AGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → DELETE1_IN_GGA(0, T729, T739)
DELETE1_IN_AGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → U55_AGA(T752, T751, T729, T730, T753, less19_in_ag(T752, T751))
DELETE1_IN_AGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → LESS19_IN_AG(T752, T751)
DELETE1_IN_AGA(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) → U56_AGA(T756, T751, T729, T759, T757, lessc19_in_ag(T756, T751))
U56_AGA(T756, T751, T729, T759, T757, lessc19_out_ag(T756, T751)) → U57_AGA(T756, T751, T729, T759, T757, delete1_in_gga(s(T756), T729, T757))
U56_AGA(T756, T751, T729, T759, T757, lessc19_out_ag(T756, T751)) → DELETE1_IN_GGA(s(T756), T729, T757)
DELETE1_IN_AGA(T784, tree(T780, T781, T782), tree(T780, T781, T785)) → U58_AGA(T784, T780, T781, T782, T785, less31_in_ga(T780, T784))
DELETE1_IN_AGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_AGA(T788, T780, T791, T782, T789, lessc31_in_ga(T780, T788))
U59_AGA(T788, T780, T791, T782, T789, lessc31_out_ga(T780, T788)) → U60_AGA(T788, T780, T791, T782, T789, delete1_in_aga(T788, T782, T789))
U59_AGA(T788, T780, T791, T782, T789, lessc31_out_ga(T780, T788)) → DELETE1_IN_AGA(T788, T782, T789)
DELETE1_IN_AGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → U61_AGA(T826, T815, T816, T825, delete1_in_aga(s(T826), T816, T825))
DELETE1_IN_AGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_AGA(s(T826), T816, T825)
DELETE1_IN_AGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → U62_AGA(T837, T835, T815, T816, T838, less31_in_ga(T835, T837))
DELETE1_IN_AGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → LESS31_IN_GA(T835, T837)
DELETE1_IN_AGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_AGA(T841, T835, T844, T816, T842, lessc31_in_ga(T835, T841))
U63_AGA(T841, T835, T844, T816, T842, lessc31_out_ga(T835, T841)) → U64_AGA(T841, T835, T844, T816, T842, delete1_in_aga(s(T841), T816, T842))
U63_AGA(T841, T835, T844, T816, T842, lessc31_out_ga(T835, T841)) → DELETE1_IN_AGA(s(T841), T816, T842)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
delete1_in_aga(x1, x2, x3)  =  delete1_in_aga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
p17_in_aga(x1, x2, x3)  =  p17_in_aga(x2)
less19_in_ag(x1, x2)  =  less19_in_ag(x2)
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
p17_in_gga(x1, x2, x3)  =  p17_in_gga(x1, x2)
less19_in_gg(x1, x2)  =  less19_in_gg(x1, x2)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
p29_in_gga(x1, x2, x3)  =  p29_in_gga(x1, x2)
less31_in_gg(x1, x2)  =  less31_in_gg(x1, x2)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
p50_in_gga(x1, x2, x3)  =  p50_in_gga(x1, x2)
p64_in_gga(x1, x2, x3)  =  p64_in_gga(x1, x2)
delmin78_in_gaa(x1, x2, x3)  =  delmin78_in_gaa(x1)
p93_in_ggga(x1, x2, x3, x4)  =  p93_in_ggga(x1, x2, x3)
p29_in_gaa(x1, x2, x3)  =  p29_in_gaa(x1)
less31_in_ga(x1, x2)  =  less31_in_ga(x1)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
p50_in_aga(x1, x2, x3)  =  p50_in_aga(x2)
p64_in_gaa(x1, x2, x3)  =  p64_in_gaa(x1)
p93_in_gaga(x1, x2, x3, x4)  =  p93_in_gaga(x1, x3)
DELETE1_IN_AGA(x1, x2, x3)  =  DELETE1_IN_AGA(x2)
U19_AGA(x1, x2, x3, x4)  =  U19_AGA(x2, x4)
P17_IN_AGA(x1, x2, x3)  =  P17_IN_AGA(x2)
U7_AGA(x1, x2, x3, x4)  =  U7_AGA(x2, x4)
LESS19_IN_AG(x1, x2)  =  LESS19_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U8_AGA(x1, x2, x3, x4)  =  U8_AGA(x2, x4)
U9_AGA(x1, x2, x3, x4)  =  U9_AGA(x1, x2, x4)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
P17_IN_GGA(x1, x2, x3)  =  P17_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
LESS19_IN_GG(x1, x2)  =  LESS19_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA'(x1, x2, x4)
P29_IN_GGA(x1, x2, x3)  =  P29_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
LESS31_IN_GG(x1, x2)  =  LESS31_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
P50_IN_GGA(x1, x2, x3)  =  P50_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3)  =  U24_GGA(x1, x3)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
P64_IN_GGA(x1, x2, x3)  =  P64_IN_GGA(x1, x2)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U26_GGA(x1, x2, x3, x4, x8)
DELMIN78_IN_GAA(x1, x2, x3)  =  DELMIN78_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x1, x2, x3, x7)
U27_GGA(x1, x2, x3, x4, x5)  =  U27_GGA(x1, x2, x3, x5)
U28_GGA(x1, x2, x3, x4, x5)  =  U28_GGA(x1, x2, x3, x5)
P93_IN_GGGA(x1, x2, x3, x4)  =  P93_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5)  =  U13_GGGA(x1, x2, x3, x5)
U14_GGGA(x1, x2, x3, x4, x5)  =  U14_GGGA(x1, x2, x3, x5)
U15_GGGA(x1, x2, x3, x4, x5)  =  U15_GGGA(x1, x2, x3, x5)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4, x5)  =  U30_GGA(x1, x2, x3, x5)
U31_GGA(x1, x2, x3, x4, x5)  =  U31_GGA'(x1, x2, x3, x5)
U32_GGA(x1, x2, x3, x4)  =  U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x1, x2, x3, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x2, x3, x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x1, x2, x3, x5)
U36_GGA(x1, x2, x3, x4, x5)  =  U36_GGA(x1, x2, x3, x5)
U37_GGA(x1, x2, x3, x4, x5)  =  U37_GGA(x1, x2, x3, x5)
U38_GGA(x1, x2, x3, x4, x5)  =  U38_GGA(x1, x2, x3, x5)
U39_GGA(x1, x2, x3, x4, x5)  =  U39_GGA(x1, x2, x3, x5)
U40_GGA(x1, x2, x3, x4)  =  U40_GGA(x1, x2, x4)
U41_GGA(x1, x2, x3, x4, x5)  =  U41_GGA(x1, x2, x3, x5)
U42_GGA(x1, x2, x3, x4, x5)  =  U42_GGA(x1, x2, x3, x5)
U43_GGA(x1, x2, x3, x4, x5)  =  U43_GGA(x1, x2, x3, x5)
U44_GGA(x1, x2, x3, x4, x5)  =  U44_GGA(x1, x2, x3, x5)
U45_GGA(x1, x2, x3, x4)  =  U45_GGA(x1, x2, x4)
U46_GGA(x1, x2, x3, x4, x5)  =  U46_GGA(x1, x2, x3, x5)
U47_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_GGA(x1, x2, x3, x4, x5, x9)
U48_GGA(x1, x2, x3, x4, x5, x6)  =  U48_GGA(x1, x2, x3, x4, x6)
U49_GGA(x1, x2, x3, x4, x5, x6)  =  U49_GGA(x1, x2, x3, x4, x6)
U50_GGA(x1, x2, x3, x4, x5, x6)  =  U50_GGA(x1, x2, x3, x4, x6)
U51_GGA(x1, x2, x3, x4, x5, x6)  =  U51_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6)  =  U52_GGA(x1, x2, x3, x4, x6)
U53_GGA(x1, x2, x3, x4, x5, x6)  =  U53_GGA(x1, x2, x3, x4, x6)
U54_GGA(x1, x2, x3, x4, x5)  =  U54_GGA(x1, x2, x3, x5)
U55_GGA(x1, x2, x3, x4, x5, x6)  =  U55_GGA'(x1, x2, x3, x4, x6)
U56_GGA(x1, x2, x3, x4, x5, x6)  =  U56_GGA(x1, x2, x3, x4, x6)
U57_GGA(x1, x2, x3, x4, x5, x6)  =  U57_GGA(x1, x2, x3, x4, x6)
U58_GGA(x1, x2, x3, x4, x5, x6)  =  U58_GGA(x1, x2, x3, x4, x6)
U59_GGA(x1, x2, x3, x4, x5, x6)  =  U59_GGA(x1, x2, x3, x4, x6)
U60_GGA(x1, x2, x3, x4, x5, x6)  =  U60_GGA(x1, x2, x3, x4, x6)
U61_GGA(x1, x2, x3, x4, x5)  =  U61_GGA(x1, x2, x3, x5)
U62_GGA(x1, x2, x3, x4, x5, x6)  =  U62_GGA(x1, x2, x3, x4, x6)
U63_GGA(x1, x2, x3, x4, x5, x6)  =  U63_GGA(x1, x2, x3, x4, x6)
U64_GGA(x1, x2, x3, x4, x5, x6)  =  U64_GGA(x1, x2, x3, x4, x6)
U20_AGA(x1, x2, x3, x4)  =  U20_AGA'(x2, x4)
P29_IN_GAA(x1, x2, x3)  =  P29_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
LESS31_IN_GA(x1, x2)  =  LESS31_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U21_AGA(x1, x2, x3)  =  U21_AGA(x1, x3)
U22_AGA(x1, x2, x3, x4)  =  U22_AGA(x2, x4)
P50_IN_AGA(x1, x2, x3)  =  P50_IN_AGA(x2)
U10_AGA(x1, x2, x3, x4)  =  U10_AGA(x2, x4)
U11_AGA(x1, x2, x3, x4)  =  U11_AGA(x2, x4)
U12_AGA(x1, x2, x3, x4)  =  U12_AGA(x1, x2, x4)
U23_AGA(x1, x2, x3, x4)  =  U23_AGA(x2, x4)
U24_AGA(x1, x2, x3)  =  U24_AGA(x3)
U25_AGA(x1, x2, x3, x4)  =  U25_AGA'(x2, x4)
P64_IN_GAA(x1, x2, x3)  =  P64_IN_GAA(x1)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
U26_AGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U26_AGA(x1, x2, x3, x4, x8)
U27_AGA(x1, x2, x3, x4, x5)  =  U27_AGA(x2, x3, x5)
U28_AGA(x1, x2, x3, x4, x5)  =  U28_AGA(x2, x3, x5)
P93_IN_GAGA(x1, x2, x3, x4)  =  P93_IN_GAGA(x1, x3)
U13_GAGA(x1, x2, x3, x4, x5)  =  U13_GAGA(x1, x3, x5)
U14_GAGA(x1, x2, x3, x4, x5)  =  U14_GAGA(x1, x3, x5)
U15_GAGA(x1, x2, x3, x4, x5)  =  U15_GAGA(x1, x3, x5)
U29_AGA(x1, x2, x3, x4)  =  U29_AGA'(x1, x2, x4)
U30_AGA(x1, x2, x3, x4, x5)  =  U30_AGA(x2, x3, x5)
U31_AGA(x1, x2, x3, x4, x5)  =  U31_AGA(x2, x3, x5)
U32_AGA(x1, x2, x3, x4)  =  U32_AGA(x2, x4)
U33_AGA(x1, x2, x3, x4, x5)  =  U33_AGA(x2, x3, x5)
U34_AGA(x1, x2, x3, x4, x5)  =  U34_AGA(x2, x3, x5)
U35_AGA(x1, x2, x3, x4, x5)  =  U35_AGA(x2, x3, x5)
U36_AGA(x1, x2, x3, x4, x5)  =  U36_AGA(x2, x3, x5)
U37_AGA(x1, x2, x3, x4, x5)  =  U37_AGA(x2, x3, x5)
U38_AGA(x1, x2, x3, x4, x5)  =  U38_AGA(x1, x2, x3, x5)
U39_AGA(x1, x2, x3, x4, x5)  =  U39_AGA(x2, x3, x5)
U40_AGA(x1, x2, x3, x4)  =  U40_AGA(x1, x2, x4)
U41_AGA(x1, x2, x3, x4, x5)  =  U41_AGA(x2, x3, x5)
U42_AGA(x1, x2, x3, x4, x5)  =  U42_AGA(x2, x3, x5)
U43_AGA(x1, x2, x3, x4, x5)  =  U43_AGA(x1, x2, x3, x5)
U44_AGA(x1, x2, x3, x4, x5)  =  U44_AGA(x2, x3, x5)
U45_AGA(x1, x2, x3, x4)  =  U45_AGA(x2, x4)
U46_AGA(x1, x2, x3, x4, x5)  =  U46_AGA(x2, x3, x5)
U47_AGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_AGA(x1, x2, x3, x4, x5, x9)
U48_AGA(x1, x2, x3, x4, x5, x6)  =  U48_AGA(x2, x3, x4, x6)
U49_AGA(x1, x2, x3, x4, x5, x6)  =  U49_AGA(x2, x3, x4, x6)
U50_AGA(x1, x2, x3, x4, x5, x6)  =  U50_AGA(x1, x2, x3, x4, x6)
U51_AGA(x1, x2, x3, x4, x5, x6)  =  U51_AGA(x2, x3, x4, x6)
U52_AGA(x1, x2, x3, x4, x5, x6)  =  U52_AGA(x2, x3, x4, x6)
U53_AGA(x1, x2, x3, x4, x5, x6)  =  U53_AGA(x2, x3, x4, x6)
U54_AGA(x1, x2, x3, x4, x5)  =  U54_AGA(x1, x2, x3, x5)
U55_AGA(x1, x2, x3, x4, x5, x6)  =  U55_AGA(x2, x3, x4, x6)
U56_AGA(x1, x2, x3, x4, x5, x6)  =  U56_AGA(x2, x3, x4, x6)
U57_AGA(x1, x2, x3, x4, x5, x6)  =  U57_AGA(x1, x2, x3, x4, x6)
U58_AGA(x1, x2, x3, x4, x5, x6)  =  U58_AGA'(x2, x3, x4, x6)
U59_AGA(x1, x2, x3, x4, x5, x6)  =  U59_AGA(x2, x3, x4, x6)
U60_AGA(x1, x2, x3, x4, x5, x6)  =  U60_AGA(x2, x3, x4, x6)
U61_AGA(x1, x2, x3, x4, x5)  =  U61_AGA(x2, x3, x5)
U62_AGA(x1, x2, x3, x4, x5, x6)  =  U62_AGA(x2, x3, x4, x6)
U63_AGA(x1, x2, x3, x4, x5, x6)  =  U63_AGA(x2, x3, x4, x6)
U64_AGA(x1, x2, x3, x4, x5, x6)  =  U64_AGA(x2, x3, x4, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

DELETE1_IN_AGA(T33, tree(T31, void, void), tree(T31, T34, void)) → U19_AGA(T33, T31, T34, p17_in_aga(T33, T31, T34))
DELETE1_IN_AGA(T33, tree(T31, void, void), tree(T31, T34, void)) → P17_IN_AGA(T33, T31, T34)
P17_IN_AGA(T33, T31, T34) → U7_AGA(T33, T31, T34, less19_in_ag(T33, T31))
P17_IN_AGA(T33, T31, T34) → LESS19_IN_AG(T33, T31)
LESS19_IN_AG(s(T52), s(T51)) → U1_AG(T52, T51, less19_in_ag(T52, T51))
LESS19_IN_AG(s(T52), s(T51)) → LESS19_IN_AG(T52, T51)
P17_IN_AGA(T37, T31, T38) → U8_AGA(T37, T31, T38, lessc19_in_ag(T37, T31))
U8_AGA(T37, T31, T38, lessc19_out_ag(T37, T31)) → U9_AGA(T37, T31, T38, delete1_in_gga(T37, void, T38))
U8_AGA(T37, T31, T38, lessc19_out_ag(T37, T31)) → DELETE1_IN_GGA(T37, void, T38)
DELETE1_IN_GGA(T33, tree(T31, void, void), tree(T31, T34, void)) → U19_GGA(T33, T31, T34, p17_in_gga(T33, T31, T34))
DELETE1_IN_GGA(T33, tree(T31, void, void), tree(T31, T34, void)) → P17_IN_GGA(T33, T31, T34)
P17_IN_GGA(T33, T31, T34) → U7_GGA(T33, T31, T34, less19_in_gg(T33, T31))
P17_IN_GGA(T33, T31, T34) → LESS19_IN_GG(T33, T31)
LESS19_IN_GG(s(T52), s(T51)) → U1_GG(T52, T51, less19_in_gg(T52, T51))
LESS19_IN_GG(s(T52), s(T51)) → LESS19_IN_GG(T52, T51)
P17_IN_GGA(T37, T31, T38) → U8_GGA(T37, T31, T38, lessc19_in_gg(T37, T31))
U8_GGA(T37, T31, T38, lessc19_out_gg(T37, T31)) → U9_GGA(T37, T31, T38, delete1_in_gga(T37, void, T38))
U8_GGA(T37, T31, T38, lessc19_out_gg(T37, T31)) → DELETE1_IN_GGA(T37, void, T38)
DELETE1_IN_GGA(T71, tree(T69, void, void), tree(T69, void, T72)) → U20_GGA(T71, T69, T72, p29_in_gga(T69, T71, T72))
DELETE1_IN_GGA(T71, tree(T69, void, void), tree(T69, void, T72)) → P29_IN_GGA(T69, T71, T72)
P29_IN_GGA(T69, T71, T72) → U3_GGA(T69, T71, T72, less31_in_gg(T69, T71))
P29_IN_GGA(T69, T71, T72) → LESS31_IN_GG(T69, T71)
LESS31_IN_GG(s(T88), s(T90)) → U2_GG(T88, T90, less31_in_gg(T88, T90))
LESS31_IN_GG(s(T88), s(T90)) → LESS31_IN_GG(T88, T90)
P29_IN_GGA(T69, T75, T76) → U4_GGA(T69, T75, T76, lessc31_in_gg(T69, T75))
U4_GGA(T69, T75, T76, lessc31_out_gg(T69, T75)) → U5_GGA(T69, T75, T76, delete1_in_gga(T75, void, T76))
U4_GGA(T69, T75, T76, lessc31_out_gg(T69, T75)) → DELETE1_IN_GGA(T75, void, T76)
DELETE1_IN_GGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → U21_GGA(T112, T113, delete1_in_gga(0, void, T113))
DELETE1_IN_GGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → DELETE1_IN_GGA(0, void, T113)
DELETE1_IN_GGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → U22_GGA(T124, T123, T125, p50_in_gga(T124, T123, T125))
DELETE1_IN_GGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → P50_IN_GGA(T124, T123, T125)
P50_IN_GGA(T124, T123, T125) → U10_GGA(T124, T123, T125, less19_in_gg(T124, T123))
P50_IN_GGA(T124, T123, T125) → LESS19_IN_GG(T124, T123)
P50_IN_GGA(T128, T123, T129) → U11_GGA(T128, T123, T129, lessc19_in_gg(T128, T123))
U11_GGA(T128, T123, T129, lessc19_out_gg(T128, T123)) → U12_GGA(T128, T123, T129, delete1_in_gga(s(T128), void, T129))
U11_GGA(T128, T123, T129, lessc19_out_gg(T128, T123)) → DELETE1_IN_GGA(s(T128), void, T129)
DELETE1_IN_GGA(T148, tree(T146, void, void), tree(T146, void, T149)) → U23_GGA(T148, T146, T149, p29_in_gga(T146, T148, T149))
DELETE1_IN_GGA(s(T166), tree(0, void, void), tree(0, void, T165)) → U24_GGA(T166, T165, delete1_in_gga(s(T166), void, T165))
DELETE1_IN_GGA(s(T166), tree(0, void, void), tree(0, void, T165)) → DELETE1_IN_GGA(s(T166), void, T165)
DELETE1_IN_GGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → U25_GGA(T180, T178, T181, p64_in_gga(T178, T180, T181))
DELETE1_IN_GGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → P64_IN_GGA(T178, T180, T181)
P64_IN_GGA(T178, T180, T181) → U16_GGA(T178, T180, T181, less31_in_gg(T178, T180))
P64_IN_GGA(T178, T180, T181) → LESS31_IN_GG(T178, T180)
P64_IN_GGA(T178, T184, T185) → U17_GGA(T178, T184, T185, lessc31_in_gg(T178, T184))
U17_GGA(T178, T184, T185, lessc31_out_gg(T178, T184)) → U18_GGA(T178, T184, T185, delete1_in_gga(s(T184), void, T185))
U17_GGA(T178, T184, T185, lessc31_out_gg(T178, T184)) → DELETE1_IN_GGA(s(T184), void, T185)
DELETE1_IN_GGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → U26_GGA(T199, T239, T240, T241, T245, T246, T244, delmin78_in_gaa(T240, T245, T246))
DELETE1_IN_GGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → DELMIN78_IN_GAA(T240, T245, T246)
DELMIN78_IN_GAA(tree(T273, T274, T275), T279, tree(T273, T280, T278)) → U6_GAA(T273, T274, T275, T279, T280, T278, delmin78_in_gaa(T274, T279, T280))
DELMIN78_IN_GAA(tree(T273, T274, T275), T279, tree(T273, T280, T278)) → DELMIN78_IN_GAA(T274, T279, T280)
DELETE1_IN_GGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → U27_GGA(T305, T302, T303, T306, p17_in_gga(T305, T302, T306))
DELETE1_IN_GGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → P17_IN_GGA(T305, T302, T306)
DELETE1_IN_GGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → U28_GGA(T321, T318, T319, T322, p93_in_ggga(T318, T321, T319, T322))
DELETE1_IN_GGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GGGA(T318, T321, T319, T322)
P93_IN_GGGA(T318, T321, T319, T322) → U13_GGGA(T318, T321, T319, T322, less31_in_gg(T318, T321))
P93_IN_GGGA(T318, T321, T319, T322) → LESS31_IN_GG(T318, T321)
P93_IN_GGGA(T318, T325, T319, T326) → U14_GGGA(T318, T325, T319, T326, lessc31_in_gg(T318, T325))
U14_GGGA(T318, T325, T319, T326, lessc31_out_gg(T318, T325)) → U15_GGGA(T318, T325, T319, T326, delete1_in_gga(T325, T319, T326))
U14_GGGA(T318, T325, T319, T326, lessc31_out_gg(T318, T325)) → DELETE1_IN_GGA(T325, T319, T326)
DELETE1_IN_GGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → U29_GGA(T351, T343, T352, delete1_in_gga(0, void, T352))
DELETE1_IN_GGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → DELETE1_IN_GGA(0, void, T352)
DELETE1_IN_GGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → U30_GGA(T363, T362, T343, T364, p50_in_gga(T363, T362, T364))
DELETE1_IN_GGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → P50_IN_GGA(T363, T362, T364)
DELETE1_IN_GGA(T379, tree(T376, void, T377), tree(T376, void, T380)) → U31_GGA(T379, T376, T377, T380, p93_in_ggga(T376, T379, T377, T380))
DELETE1_IN_GGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → U32_GGA(T399, T389, T398, delete1_in_gga(s(T399), T389, T398))
DELETE1_IN_GGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_GGA(s(T399), T389, T398)
DELETE1_IN_GGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → U33_GGA(T410, T408, T389, T411, less31_in_gg(T408, T410))
DELETE1_IN_GGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → LESS31_IN_GG(T408, T410)
DELETE1_IN_GGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_GGA(T414, T408, T389, T415, lessc31_in_gg(T408, T414))
U34_GGA(T414, T408, T389, T415, lessc31_out_gg(T408, T414)) → U35_GGA(T414, T408, T389, T415, delete1_in_gga(s(T414), T389, T415))
U34_GGA(T414, T408, T389, T415, lessc31_out_gg(T408, T414)) → DELETE1_IN_GGA(s(T414), T389, T415)
DELETE1_IN_GGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → U36_GGA(T460, T457, T458, T461, less19_in_gg(T460, T457))
DELETE1_IN_GGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → LESS19_IN_GG(T460, T457)
DELETE1_IN_GGA(T464, tree(T457, T458, void), tree(T457, T465, void)) → U37_GGA(T464, T457, T458, T465, lessc19_in_gg(T464, T457))
U37_GGA(T464, T457, T458, T465, lessc19_out_gg(T464, T457)) → U38_GGA(T464, T457, T458, T465, delete1_in_gga(T464, T458, T465))
U37_GGA(T464, T457, T458, T465, lessc19_out_gg(T464, T457)) → DELETE1_IN_GGA(T464, T458, T465)
DELETE1_IN_GGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → U39_GGA(T488, T485, T486, T489, p29_in_gga(T485, T488, T489))
DELETE1_IN_GGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → P29_IN_GGA(T485, T488, T489)
DELETE1_IN_GGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → U40_GGA(T506, T498, T507, delete1_in_gga(0, T498, T507))
DELETE1_IN_GGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → DELETE1_IN_GGA(0, T498, T507)
DELETE1_IN_GGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → U41_GGA(T520, T519, T498, T521, less19_in_gg(T520, T519))
DELETE1_IN_GGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → LESS19_IN_GG(T520, T519)
DELETE1_IN_GGA(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) → U42_GGA(T524, T519, T498, T525, lessc19_in_gg(T524, T519))
U42_GGA(T524, T519, T498, T525, lessc19_out_gg(T524, T519)) → U43_GGA(T524, T519, T498, T525, delete1_in_gga(s(T524), T498, T525))
U42_GGA(T524, T519, T498, T525, lessc19_out_gg(T524, T519)) → DELETE1_IN_GGA(s(T524), T498, T525)
DELETE1_IN_GGA(T548, tree(T545, T546, void), tree(T545, T546, T549)) → U44_GGA(T548, T545, T546, T549, p29_in_gga(T545, T548, T549))
DELETE1_IN_GGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → U45_GGA(T568, T558, T567, delete1_in_gga(s(T568), void, T567))
DELETE1_IN_GGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → DELETE1_IN_GGA(s(T568), void, T567)
DELETE1_IN_GGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → U46_GGA(T582, T580, T558, T583, p64_in_gga(T580, T582, T583))
DELETE1_IN_GGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → P64_IN_GGA(T580, T582, T583)
DELETE1_IN_GGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → U47_GGA(T591, T592, T632, T633, T634, T638, T639, T637, delmin78_in_gaa(T633, T638, T639))
DELETE1_IN_GGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → DELMIN78_IN_GAA(T633, T638, T639)
DELETE1_IN_GGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → U48_GGA(T669, T665, T666, T667, T670, less19_in_gg(T669, T665))
DELETE1_IN_GGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → LESS19_IN_GG(T669, T665)
DELETE1_IN_GGA(T673, tree(T665, T666, T676), tree(T665, T674, T676)) → U49_GGA(T673, T665, T666, T676, T674, lessc19_in_gg(T673, T665))
U49_GGA(T673, T665, T666, T676, T674, lessc19_out_gg(T673, T665)) → U50_GGA(T673, T665, T666, T676, T674, delete1_in_gga(T673, T666, T674))
U49_GGA(T673, T665, T666, T676, T674, lessc19_out_gg(T673, T665)) → DELETE1_IN_GGA(T673, T666, T674)
DELETE1_IN_GGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → U51_GGA(T703, T699, T700, T701, T704, less31_in_gg(T699, T703))
DELETE1_IN_GGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → LESS31_IN_GG(T699, T703)
DELETE1_IN_GGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_GGA(T707, T699, T710, T701, T708, lessc31_in_gg(T699, T707))
U52_GGA(T707, T699, T710, T701, T708, lessc31_out_gg(T699, T707)) → U53_GGA(T707, T699, T710, T701, T708, delete1_in_gga(T707, T701, T708))
U52_GGA(T707, T699, T710, T701, T708, lessc31_out_gg(T699, T707)) → DELETE1_IN_GGA(T707, T701, T708)
DELETE1_IN_GGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → U54_GGA(T738, T729, T730, T739, delete1_in_gga(0, T729, T739))
DELETE1_IN_GGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → DELETE1_IN_GGA(0, T729, T739)
DELETE1_IN_GGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → U55_GGA(T752, T751, T729, T730, T753, less19_in_gg(T752, T751))
DELETE1_IN_GGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → LESS19_IN_GG(T752, T751)
DELETE1_IN_GGA(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) → U56_GGA(T756, T751, T729, T759, T757, lessc19_in_gg(T756, T751))
U56_GGA(T756, T751, T729, T759, T757, lessc19_out_gg(T756, T751)) → U57_GGA(T756, T751, T729, T759, T757, delete1_in_gga(s(T756), T729, T757))
U56_GGA(T756, T751, T729, T759, T757, lessc19_out_gg(T756, T751)) → DELETE1_IN_GGA(s(T756), T729, T757)
DELETE1_IN_GGA(T784, tree(T780, T781, T782), tree(T780, T781, T785)) → U58_GGA(T784, T780, T781, T782, T785, less31_in_gg(T780, T784))
DELETE1_IN_GGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_GGA(T788, T780, T791, T782, T789, lessc31_in_gg(T780, T788))
U59_GGA(T788, T780, T791, T782, T789, lessc31_out_gg(T780, T788)) → U60_GGA(T788, T780, T791, T782, T789, delete1_in_gga(T788, T782, T789))
U59_GGA(T788, T780, T791, T782, T789, lessc31_out_gg(T780, T788)) → DELETE1_IN_GGA(T788, T782, T789)
DELETE1_IN_GGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → U61_GGA(T826, T815, T816, T825, delete1_in_gga(s(T826), T816, T825))
DELETE1_IN_GGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_GGA(s(T826), T816, T825)
DELETE1_IN_GGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → U62_GGA(T837, T835, T815, T816, T838, less31_in_gg(T835, T837))
DELETE1_IN_GGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → LESS31_IN_GG(T835, T837)
DELETE1_IN_GGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_GGA(T841, T835, T844, T816, T842, lessc31_in_gg(T835, T841))
U63_GGA(T841, T835, T844, T816, T842, lessc31_out_gg(T835, T841)) → U64_GGA(T841, T835, T844, T816, T842, delete1_in_gga(s(T841), T816, T842))
U63_GGA(T841, T835, T844, T816, T842, lessc31_out_gg(T835, T841)) → DELETE1_IN_GGA(s(T841), T816, T842)
DELETE1_IN_AGA(T71, tree(T69, void, void), tree(T69, void, T72)) → U20_AGA(T71, T69, T72, p29_in_gaa(T69, T71, T72))
DELETE1_IN_AGA(T71, tree(T69, void, void), tree(T69, void, T72)) → P29_IN_GAA(T69, T71, T72)
P29_IN_GAA(T69, T71, T72) → U3_GAA(T69, T71, T72, less31_in_ga(T69, T71))
P29_IN_GAA(T69, T71, T72) → LESS31_IN_GA(T69, T71)
LESS31_IN_GA(s(T88), s(T90)) → U2_GA(T88, T90, less31_in_ga(T88, T90))
LESS31_IN_GA(s(T88), s(T90)) → LESS31_IN_GA(T88, T90)
P29_IN_GAA(T69, T75, T76) → U4_GAA(T69, T75, T76, lessc31_in_ga(T69, T75))
U4_GAA(T69, T75, T76, lessc31_out_ga(T69, T75)) → U5_GAA(T69, T75, T76, delete1_in_aga(T75, void, T76))
U4_GAA(T69, T75, T76, lessc31_out_ga(T69, T75)) → DELETE1_IN_AGA(T75, void, T76)
DELETE1_IN_AGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → U21_AGA(T112, T113, delete1_in_gga(0, void, T113))
DELETE1_IN_AGA(0, tree(s(T112), void, void), tree(s(T112), T113, void)) → DELETE1_IN_GGA(0, void, T113)
DELETE1_IN_AGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → U22_AGA(T124, T123, T125, p50_in_aga(T124, T123, T125))
DELETE1_IN_AGA(s(T124), tree(s(T123), void, void), tree(s(T123), T125, void)) → P50_IN_AGA(T124, T123, T125)
P50_IN_AGA(T124, T123, T125) → U10_AGA(T124, T123, T125, less19_in_ag(T124, T123))
P50_IN_AGA(T124, T123, T125) → LESS19_IN_AG(T124, T123)
P50_IN_AGA(T128, T123, T129) → U11_AGA(T128, T123, T129, lessc19_in_ag(T128, T123))
U11_AGA(T128, T123, T129, lessc19_out_ag(T128, T123)) → U12_AGA(T128, T123, T129, delete1_in_gga(s(T128), void, T129))
U11_AGA(T128, T123, T129, lessc19_out_ag(T128, T123)) → DELETE1_IN_GGA(s(T128), void, T129)
DELETE1_IN_AGA(T148, tree(T146, void, void), tree(T146, void, T149)) → U23_AGA(T148, T146, T149, p29_in_gaa(T146, T148, T149))
DELETE1_IN_AGA(s(T166), tree(0, void, void), tree(0, void, T165)) → U24_AGA(T166, T165, delete1_in_aga(s(T166), void, T165))
DELETE1_IN_AGA(s(T166), tree(0, void, void), tree(0, void, T165)) → DELETE1_IN_AGA(s(T166), void, T165)
DELETE1_IN_AGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → U25_AGA(T180, T178, T181, p64_in_gaa(T178, T180, T181))
DELETE1_IN_AGA(s(T180), tree(s(T178), void, void), tree(s(T178), void, T181)) → P64_IN_GAA(T178, T180, T181)
P64_IN_GAA(T178, T180, T181) → U16_GAA(T178, T180, T181, less31_in_ga(T178, T180))
P64_IN_GAA(T178, T180, T181) → LESS31_IN_GA(T178, T180)
P64_IN_GAA(T178, T184, T185) → U17_GAA(T178, T184, T185, lessc31_in_ga(T178, T184))
U17_GAA(T178, T184, T185, lessc31_out_ga(T178, T184)) → U18_GAA(T178, T184, T185, delete1_in_aga(s(T184), void, T185))
U17_GAA(T178, T184, T185, lessc31_out_ga(T178, T184)) → DELETE1_IN_AGA(s(T184), void, T185)
DELETE1_IN_AGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → U26_AGA(T199, T239, T240, T241, T245, T246, T244, delmin78_in_gaa(T240, T245, T246))
DELETE1_IN_AGA(T199, tree(T199, void, tree(T239, T240, T241)), tree(T245, void, tree(T239, T246, T244))) → DELMIN78_IN_GAA(T240, T245, T246)
DELETE1_IN_AGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → U27_AGA(T305, T302, T303, T306, p17_in_aga(T305, T302, T306))
DELETE1_IN_AGA(T305, tree(T302, void, T303), tree(T302, T306, T303)) → P17_IN_AGA(T305, T302, T306)
DELETE1_IN_AGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → U28_AGA(T321, T318, T319, T322, p93_in_gaga(T318, T321, T319, T322))
DELETE1_IN_AGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GAGA(T318, T321, T319, T322)
P93_IN_GAGA(T318, T321, T319, T322) → U13_GAGA(T318, T321, T319, T322, less31_in_ga(T318, T321))
P93_IN_GAGA(T318, T321, T319, T322) → LESS31_IN_GA(T318, T321)
P93_IN_GAGA(T318, T325, T319, T326) → U14_GAGA(T318, T325, T319, T326, lessc31_in_ga(T318, T325))
U14_GAGA(T318, T325, T319, T326, lessc31_out_ga(T318, T325)) → U15_GAGA(T318, T325, T319, T326, delete1_in_aga(T325, T319, T326))
U14_GAGA(T318, T325, T319, T326, lessc31_out_ga(T318, T325)) → DELETE1_IN_AGA(T325, T319, T326)
DELETE1_IN_AGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → U29_AGA(T351, T343, T352, delete1_in_gga(0, void, T352))
DELETE1_IN_AGA(0, tree(s(T351), void, T343), tree(s(T351), T352, T343)) → DELETE1_IN_GGA(0, void, T352)
DELETE1_IN_AGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → U30_AGA(T363, T362, T343, T364, p50_in_aga(T363, T362, T364))
DELETE1_IN_AGA(s(T363), tree(s(T362), void, T343), tree(s(T362), T364, T343)) → P50_IN_AGA(T363, T362, T364)
DELETE1_IN_AGA(T379, tree(T376, void, T377), tree(T376, void, T380)) → U31_AGA(T379, T376, T377, T380, p93_in_gaga(T376, T379, T377, T380))
DELETE1_IN_AGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → U32_AGA(T399, T389, T398, delete1_in_aga(s(T399), T389, T398))
DELETE1_IN_AGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_AGA(s(T399), T389, T398)
DELETE1_IN_AGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → U33_AGA(T410, T408, T389, T411, less31_in_ga(T408, T410))
DELETE1_IN_AGA(s(T410), tree(s(T408), void, T389), tree(s(T408), void, T411)) → LESS31_IN_GA(T408, T410)
DELETE1_IN_AGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_AGA(T414, T408, T389, T415, lessc31_in_ga(T408, T414))
U34_AGA(T414, T408, T389, T415, lessc31_out_ga(T408, T414)) → U35_AGA(T414, T408, T389, T415, delete1_in_aga(s(T414), T389, T415))
U34_AGA(T414, T408, T389, T415, lessc31_out_ga(T408, T414)) → DELETE1_IN_AGA(s(T414), T389, T415)
DELETE1_IN_AGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → U36_AGA(T460, T457, T458, T461, less19_in_ag(T460, T457))
DELETE1_IN_AGA(T460, tree(T457, T458, void), tree(T457, T461, void)) → LESS19_IN_AG(T460, T457)
DELETE1_IN_AGA(T464, tree(T457, T458, void), tree(T457, T465, void)) → U37_AGA(T464, T457, T458, T465, lessc19_in_ag(T464, T457))
U37_AGA(T464, T457, T458, T465, lessc19_out_ag(T464, T457)) → U38_AGA(T464, T457, T458, T465, delete1_in_gga(T464, T458, T465))
U37_AGA(T464, T457, T458, T465, lessc19_out_ag(T464, T457)) → DELETE1_IN_GGA(T464, T458, T465)
DELETE1_IN_AGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → U39_AGA(T488, T485, T486, T489, p29_in_gaa(T485, T488, T489))
DELETE1_IN_AGA(T488, tree(T485, T486, void), tree(T485, T486, T489)) → P29_IN_GAA(T485, T488, T489)
DELETE1_IN_AGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → U40_AGA(T506, T498, T507, delete1_in_gga(0, T498, T507))
DELETE1_IN_AGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → DELETE1_IN_GGA(0, T498, T507)
DELETE1_IN_AGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → U41_AGA(T520, T519, T498, T521, less19_in_ag(T520, T519))
DELETE1_IN_AGA(s(T520), tree(s(T519), T498, void), tree(s(T519), T521, void)) → LESS19_IN_AG(T520, T519)
DELETE1_IN_AGA(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) → U42_AGA(T524, T519, T498, T525, lessc19_in_ag(T524, T519))
U42_AGA(T524, T519, T498, T525, lessc19_out_ag(T524, T519)) → U43_AGA(T524, T519, T498, T525, delete1_in_gga(s(T524), T498, T525))
U42_AGA(T524, T519, T498, T525, lessc19_out_ag(T524, T519)) → DELETE1_IN_GGA(s(T524), T498, T525)
DELETE1_IN_AGA(T548, tree(T545, T546, void), tree(T545, T546, T549)) → U44_AGA(T548, T545, T546, T549, p29_in_gaa(T545, T548, T549))
DELETE1_IN_AGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → U45_AGA(T568, T558, T567, delete1_in_aga(s(T568), void, T567))
DELETE1_IN_AGA(s(T568), tree(0, T558, void), tree(0, T558, T567)) → DELETE1_IN_AGA(s(T568), void, T567)
DELETE1_IN_AGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → U46_AGA(T582, T580, T558, T583, p64_in_gaa(T580, T582, T583))
DELETE1_IN_AGA(s(T582), tree(s(T580), T558, void), tree(s(T580), T558, T583)) → P64_IN_GAA(T580, T582, T583)
DELETE1_IN_AGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → U47_AGA(T591, T592, T632, T633, T634, T638, T639, T637, delmin78_in_gaa(T633, T638, T639))
DELETE1_IN_AGA(T591, tree(T591, T592, tree(T632, T633, T634)), tree(T638, T592, tree(T632, T639, T637))) → DELMIN78_IN_GAA(T633, T638, T639)
DELETE1_IN_AGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → U48_AGA(T669, T665, T666, T667, T670, less19_in_ag(T669, T665))
DELETE1_IN_AGA(T669, tree(T665, T666, T667), tree(T665, T670, T667)) → LESS19_IN_AG(T669, T665)
DELETE1_IN_AGA(T673, tree(T665, T666, T676), tree(T665, T674, T676)) → U49_AGA(T673, T665, T666, T676, T674, lessc19_in_ag(T673, T665))
U49_AGA(T673, T665, T666, T676, T674, lessc19_out_ag(T673, T665)) → U50_AGA(T673, T665, T666, T676, T674, delete1_in_gga(T673, T666, T674))
U49_AGA(T673, T665, T666, T676, T674, lessc19_out_ag(T673, T665)) → DELETE1_IN_GGA(T673, T666, T674)
DELETE1_IN_AGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → U51_AGA(T703, T699, T700, T701, T704, less31_in_ga(T699, T703))
DELETE1_IN_AGA(T703, tree(T699, T700, T701), tree(T699, T700, T704)) → LESS31_IN_GA(T699, T703)
DELETE1_IN_AGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_AGA(T707, T699, T710, T701, T708, lessc31_in_ga(T699, T707))
U52_AGA(T707, T699, T710, T701, T708, lessc31_out_ga(T699, T707)) → U53_AGA(T707, T699, T710, T701, T708, delete1_in_aga(T707, T701, T708))
U52_AGA(T707, T699, T710, T701, T708, lessc31_out_ga(T699, T707)) → DELETE1_IN_AGA(T707, T701, T708)
DELETE1_IN_AGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → U54_AGA(T738, T729, T730, T739, delete1_in_gga(0, T729, T739))
DELETE1_IN_AGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → DELETE1_IN_GGA(0, T729, T739)
DELETE1_IN_AGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → U55_AGA(T752, T751, T729, T730, T753, less19_in_ag(T752, T751))
DELETE1_IN_AGA(s(T752), tree(s(T751), T729, T730), tree(s(T751), T753, T730)) → LESS19_IN_AG(T752, T751)
DELETE1_IN_AGA(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) → U56_AGA(T756, T751, T729, T759, T757, lessc19_in_ag(T756, T751))
U56_AGA(T756, T751, T729, T759, T757, lessc19_out_ag(T756, T751)) → U57_AGA(T756, T751, T729, T759, T757, delete1_in_gga(s(T756), T729, T757))
U56_AGA(T756, T751, T729, T759, T757, lessc19_out_ag(T756, T751)) → DELETE1_IN_GGA(s(T756), T729, T757)
DELETE1_IN_AGA(T784, tree(T780, T781, T782), tree(T780, T781, T785)) → U58_AGA(T784, T780, T781, T782, T785, less31_in_ga(T780, T784))
DELETE1_IN_AGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_AGA(T788, T780, T791, T782, T789, lessc31_in_ga(T780, T788))
U59_AGA(T788, T780, T791, T782, T789, lessc31_out_ga(T780, T788)) → U60_AGA(T788, T780, T791, T782, T789, delete1_in_aga(T788, T782, T789))
U59_AGA(T788, T780, T791, T782, T789, lessc31_out_ga(T780, T788)) → DELETE1_IN_AGA(T788, T782, T789)
DELETE1_IN_AGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → U61_AGA(T826, T815, T816, T825, delete1_in_aga(s(T826), T816, T825))
DELETE1_IN_AGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_AGA(s(T826), T816, T825)
DELETE1_IN_AGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → U62_AGA(T837, T835, T815, T816, T838, less31_in_ga(T835, T837))
DELETE1_IN_AGA(s(T837), tree(s(T835), T815, T816), tree(s(T835), T815, T838)) → LESS31_IN_GA(T835, T837)
DELETE1_IN_AGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_AGA(T841, T835, T844, T816, T842, lessc31_in_ga(T835, T841))
U63_AGA(T841, T835, T844, T816, T842, lessc31_out_ga(T835, T841)) → U64_AGA(T841, T835, T844, T816, T842, delete1_in_aga(s(T841), T816, T842))
U63_AGA(T841, T835, T844, T816, T842, lessc31_out_ga(T835, T841)) → DELETE1_IN_AGA(s(T841), T816, T842)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
delete1_in_aga(x1, x2, x3)  =  delete1_in_aga(x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
p17_in_aga(x1, x2, x3)  =  p17_in_aga(x2)
less19_in_ag(x1, x2)  =  less19_in_ag(x2)
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
p17_in_gga(x1, x2, x3)  =  p17_in_gga(x1, x2)
less19_in_gg(x1, x2)  =  less19_in_gg(x1, x2)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
p29_in_gga(x1, x2, x3)  =  p29_in_gga(x1, x2)
less31_in_gg(x1, x2)  =  less31_in_gg(x1, x2)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
p50_in_gga(x1, x2, x3)  =  p50_in_gga(x1, x2)
p64_in_gga(x1, x2, x3)  =  p64_in_gga(x1, x2)
delmin78_in_gaa(x1, x2, x3)  =  delmin78_in_gaa(x1)
p93_in_ggga(x1, x2, x3, x4)  =  p93_in_ggga(x1, x2, x3)
p29_in_gaa(x1, x2, x3)  =  p29_in_gaa(x1)
less31_in_ga(x1, x2)  =  less31_in_ga(x1)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
p50_in_aga(x1, x2, x3)  =  p50_in_aga(x2)
p64_in_gaa(x1, x2, x3)  =  p64_in_gaa(x1)
p93_in_gaga(x1, x2, x3, x4)  =  p93_in_gaga(x1, x3)
DELETE1_IN_AGA(x1, x2, x3)  =  DELETE1_IN_AGA(x2)
U19_AGA(x1, x2, x3, x4)  =  U19_AGA(x2, x4)
P17_IN_AGA(x1, x2, x3)  =  P17_IN_AGA(x2)
U7_AGA(x1, x2, x3, x4)  =  U7_AGA(x2, x4)
LESS19_IN_AG(x1, x2)  =  LESS19_IN_AG(x2)
U1_AG(x1, x2, x3)  =  U1_AG(x2, x3)
U8_AGA(x1, x2, x3, x4)  =  U8_AGA(x2, x4)
U9_AGA(x1, x2, x3, x4)  =  U9_AGA(x1, x2, x4)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x1, x2, x4)
P17_IN_GGA(x1, x2, x3)  =  P17_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3, x4)  =  U7_GGA(x1, x2, x4)
LESS19_IN_GG(x1, x2)  =  LESS19_IN_GG(x1, x2)
U1_GG(x1, x2, x3)  =  U1_GG(x1, x2, x3)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x1, x2, x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x1, x2, x4)
P29_IN_GGA(x1, x2, x3)  =  P29_IN_GGA(x1, x2)
U3_GGA(x1, x2, x3, x4)  =  U3_GGA(x1, x2, x4)
LESS31_IN_GG(x1, x2)  =  LESS31_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U4_GGA(x1, x2, x3, x4)  =  U4_GGA(x1, x2, x4)
U5_GGA(x1, x2, x3, x4)  =  U5_GGA(x1, x2, x4)
U21_GGA(x1, x2, x3)  =  U21_GGA(x1, x3)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
P50_IN_GGA(x1, x2, x3)  =  P50_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3, x4)  =  U10_GGA(x1, x2, x4)
U11_GGA(x1, x2, x3, x4)  =  U11_GGA(x1, x2, x4)
U12_GGA(x1, x2, x3, x4)  =  U12_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3)  =  U24_GGA(x1, x3)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x1, x2, x4)
P64_IN_GGA(x1, x2, x3)  =  P64_IN_GGA(x1, x2)
U16_GGA(x1, x2, x3, x4)  =  U16_GGA(x1, x2, x4)
U17_GGA(x1, x2, x3, x4)  =  U17_GGA(x1, x2, x4)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x1, x2, x4)
U26_GGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U26_GGA(x1, x2, x3, x4, x8)
DELMIN78_IN_GAA(x1, x2, x3)  =  DELMIN78_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x1, x2, x3, x7)
U27_GGA(x1, x2, x3, x4, x5)  =  U27_GGA(x1, x2, x3, x5)
U28_GGA(x1, x2, x3, x4, x5)  =  U28_GGA(x1, x2, x3, x5)
P93_IN_GGGA(x1, x2, x3, x4)  =  P93_IN_GGGA(x1, x2, x3)
U13_GGGA(x1, x2, x3, x4, x5)  =  U13_GGGA(x1, x2, x3, x5)
U14_GGGA(x1, x2, x3, x4, x5)  =  U14_GGGA(x1, x2, x3, x5)
U15_GGGA(x1, x2, x3, x4, x5)  =  U15_GGGA(x1, x2, x3, x5)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x1, x2, x4)
U30_GGA(x1, x2, x3, x4, x5)  =  U30_GGA(x1, x2, x3, x5)
U31_GGA(x1, x2, x3, x4, x5)  =  U31_GGA(x1, x2, x3, x5)
U32_GGA(x1, x2, x3, x4)  =  U32_GGA(x1, x2, x4)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x1, x2, x3, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x2, x3, x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x1, x2, x3, x5)
U36_GGA(x1, x2, x3, x4, x5)  =  U36_GGA(x1, x2, x3, x5)
U37_GGA(x1, x2, x3, x4, x5)  =  U37_GGA(x1, x2, x3, x5)
U38_GGA(x1, x2, x3, x4, x5)  =  U38_GGA(x1, x2, x3, x5)
U39_GGA(x1, x2, x3, x4, x5)  =  U39_GGA(x1, x2, x3, x5)
U40_GGA(x1, x2, x3, x4)  =  U40_GGA(x1, x2, x4)
U41_GGA(x1, x2, x3, x4, x5)  =  U41_GGA'(x1, x2, x3, x5)
U42_GGA(x1, x2, x3, x4, x5)  =  U42_GGA(x1, x2, x3, x5)
U43_GGA(x1, x2, x3, x4, x5)  =  U43_GGA(x1, x2, x3, x5)
U44_GGA(x1, x2, x3, x4, x5)  =  U44_GGA(x1, x2, x3, x5)
U45_GGA(x1, x2, x3, x4)  =  U45_GGA'(x1, x2, x4)
U46_GGA(x1, x2, x3, x4, x5)  =  U46_GGA(x1, x2, x3, x5)
U47_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_GGA(x1, x2, x3, x4, x5, x9)
U48_GGA(x1, x2, x3, x4, x5, x6)  =  U48_GGA(x1, x2, x3, x4, x6)
U49_GGA(x1, x2, x3, x4, x5, x6)  =  U49_GGA(x1, x2, x3, x4, x6)
U50_GGA(x1, x2, x3, x4, x5, x6)  =  U50_GGA(x1, x2, x3, x4, x6)
U51_GGA(x1, x2, x3, x4, x5, x6)  =  U51_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6)  =  U52_GGA(x1, x2, x3, x4, x6)
U53_GGA(x1, x2, x3, x4, x5, x6)  =  U53_GGA(x1, x2, x3, x4, x6)
U54_GGA(x1, x2, x3, x4, x5)  =  U54_GGA(x1, x2, x3, x5)
U55_GGA(x1, x2, x3, x4, x5, x6)  =  U55_GGA(x1, x2, x3, x4, x6)
U56_GGA(x1, x2, x3, x4, x5, x6)  =  U56_GGA(x1, x2, x3, x4, x6)
U57_GGA(x1, x2, x3, x4, x5, x6)  =  U57_GGA(x1, x2, x3, x4, x6)
U58_GGA(x1, x2, x3, x4, x5, x6)  =  U58_GGA(x1, x2, x3, x4, x6)
U59_GGA(x1, x2, x3, x4, x5, x6)  =  U59_GGA(x1, x2, x3, x4, x6)
U60_GGA(x1, x2, x3, x4, x5, x6)  =  U60_GGA(x1, x2, x3, x4, x6)
U61_GGA(x1, x2, x3, x4, x5)  =  U61_GGA(x1, x2, x3, x5)
U62_GGA(x1, x2, x3, x4, x5, x6)  =  U62_GGA(x1, x2, x3, x4, x6)
U63_GGA(x1, x2, x3, x4, x5, x6)  =  U63_GGA(x1, x2, x3, x4, x6)
U64_GGA(x1, x2, x3, x4, x5, x6)  =  U64_GGA(x1, x2, x3, x4, x6)
U20_AGA(x1, x2, x3, x4)  =  U20_AGA(x2, x4)
P29_IN_GAA(x1, x2, x3)  =  P29_IN_GAA(x1)
U3_GAA(x1, x2, x3, x4)  =  U3_GAA(x1, x4)
LESS31_IN_GA(x1, x2)  =  LESS31_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U4_GAA(x1, x2, x3, x4)  =  U4_GAA(x1, x4)
U5_GAA(x1, x2, x3, x4)  =  U5_GAA(x1, x4)
U21_AGA(x1, x2, x3)  =  U21_AGA(x1, x3)
U22_AGA(x1, x2, x3, x4)  =  U22_AGA(x2, x4)
P50_IN_AGA(x1, x2, x3)  =  P50_IN_AGA(x2)
U10_AGA(x1, x2, x3, x4)  =  U10_AGA(x2, x4)
U11_AGA(x1, x2, x3, x4)  =  U11_AGA'(x2, x4)
U12_AGA(x1, x2, x3, x4)  =  U12_AGA(x1, x2, x4)
U23_AGA(x1, x2, x3, x4)  =  U23_AGA(x2, x4)
U24_AGA(x1, x2, x3)  =  U24_AGA(x3)
U25_AGA(x1, x2, x3, x4)  =  U25_AGA(x2, x4)
P64_IN_GAA(x1, x2, x3)  =  P64_IN_GAA(x1)
U16_GAA(x1, x2, x3, x4)  =  U16_GAA(x1, x4)
U17_GAA(x1, x2, x3, x4)  =  U17_GAA(x1, x4)
U18_GAA(x1, x2, x3, x4)  =  U18_GAA(x1, x4)
U26_AGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U26_AGA(x1, x2, x3, x4, x8)
U27_AGA(x1, x2, x3, x4, x5)  =  U27_AGA(x2, x3, x5)
U28_AGA(x1, x2, x3, x4, x5)  =  U28_AGA'(x2, x3, x5)
P93_IN_GAGA(x1, x2, x3, x4)  =  P93_IN_GAGA(x1, x3)
U13_GAGA(x1, x2, x3, x4, x5)  =  U13_GAGA(x1, x3, x5)
U14_GAGA(x1, x2, x3, x4, x5)  =  U14_GAGA(x1, x3, x5)
U15_GAGA(x1, x2, x3, x4, x5)  =  U15_GAGA(x1, x3, x5)
U29_AGA(x1, x2, x3, x4)  =  U29_AGA(x1, x2, x4)
U30_AGA(x1, x2, x3, x4, x5)  =  U30_AGA(x2, x3, x5)
U31_AGA(x1, x2, x3, x4, x5)  =  U31_AGA(x2, x3, x5)
U32_AGA(x1, x2, x3, x4)  =  U32_AGA(x2, x4)
U33_AGA(x1, x2, x3, x4, x5)  =  U33_AGA(x2, x3, x5)
U34_AGA(x1, x2, x3, x4, x5)  =  U34_AGA(x2, x3, x5)
U35_AGA(x1, x2, x3, x4, x5)  =  U35_AGA(x2, x3, x5)
U36_AGA(x1, x2, x3, x4, x5)  =  U36_AGA(x2, x3, x5)
U37_AGA(x1, x2, x3, x4, x5)  =  U37_AGA(x2, x3, x5)
U38_AGA(x1, x2, x3, x4, x5)  =  U38_AGA(x1, x2, x3, x5)
U39_AGA(x1, x2, x3, x4, x5)  =  U39_AGA(x2, x3, x5)
U40_AGA(x1, x2, x3, x4)  =  U40_AGA(x1, x2, x4)
U41_AGA(x1, x2, x3, x4, x5)  =  U41_AGA(x2, x3, x5)
U42_AGA(x1, x2, x3, x4, x5)  =  U42_AGA(x2, x3, x5)
U43_AGA(x1, x2, x3, x4, x5)  =  U43_AGA(x1, x2, x3, x5)
U44_AGA(x1, x2, x3, x4, x5)  =  U44_AGA(x2, x3, x5)
U45_AGA(x1, x2, x3, x4)  =  U45_AGA(x2, x4)
U46_AGA(x1, x2, x3, x4, x5)  =  U46_AGA(x2, x3, x5)
U47_AGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U47_AGA(x1, x2, x3, x4, x5, x9)
U48_AGA(x1, x2, x3, x4, x5, x6)  =  U48_AGA(x2, x3, x4, x6)
U49_AGA(x1, x2, x3, x4, x5, x6)  =  U49_AGA(x2, x3, x4, x6)
U50_AGA(x1, x2, x3, x4, x5, x6)  =  U50_AGA'(x1, x2, x3, x4, x6)
U51_AGA(x1, x2, x3, x4, x5, x6)  =  U51_AGA(x2, x3, x4, x6)
U52_AGA(x1, x2, x3, x4, x5, x6)  =  U52_AGA(x2, x3, x4, x6)
U53_AGA(x1, x2, x3, x4, x5, x6)  =  U53_AGA(x2, x3, x4, x6)
U54_AGA(x1, x2, x3, x4, x5)  =  U54_AGA(x1, x2, x3, x5)
U55_AGA(x1, x2, x3, x4, x5, x6)  =  U55_AGA(x2, x3, x4, x6)
U56_AGA(x1, x2, x3, x4, x5, x6)  =  U56_AGA(x2, x3, x4, x6)
U57_AGA(x1, x2, x3, x4, x5, x6)  =  U57_AGA(x1, x2, x3, x4, x6)
U58_AGA(x1, x2, x3, x4, x5, x6)  =  U58_AGA(x2, x3, x4, x6)
U59_AGA(x1, x2, x3, x4, x5, x6)  =  U59_AGA(x2, x3, x4, x6)
U60_AGA(x1, x2, x3, x4, x5, x6)  =  U60_AGA(x2, x3, x4, x6)
U61_AGA(x1, x2, x3, x4, x5)  =  U61_AGA(x2, x3, x5)
U62_AGA(x1, x2, x3, x4, x5, x6)  =  U62_AGA(x2, x3, x4, x6)
U63_AGA(x1, x2, x3, x4, x5, x6)  =  U63_AGA(x2, x3, x4, x6)
U64_AGA(x1, x2, x3, x4, x5, x6)  =  U64_AGA(x2, x3, x4, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESS31_IN_GA(s(T88), s(T90)) → LESS31_IN_GA(T88, T90)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
LESS31_IN_GA(x1, x2)  =  LESS31_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LESS31_IN_GA(s(T88), s(T90)) → LESS31_IN_GA(T88, T90)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

LESS31_IN_GA(s(T88)) → LESS31_IN_GA(T88)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS31_IN_GA(s(T88)) → LESS31_IN_GA(T88)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

DELMIN78_IN_GAA(tree(T273, T274, T275), T279, tree(T273, T280, T278)) → DELMIN78_IN_GAA(T274, T279, T280)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
DELMIN78_IN_GAA(x1, x2, x3)  =  DELMIN78_IN_GAA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

DELMIN78_IN_GAA(tree(T273, T274, T275), T279, tree(T273, T280, T278)) → DELMIN78_IN_GAA(T274, T279, T280)

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

DELMIN78_IN_GAA(tree(T273, T274, T275)) → DELMIN78_IN_GAA(T274)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • DELMIN78_IN_GAA(tree(T273, T274, T275)) → DELMIN78_IN_GAA(T274)
    The graph contains the following edges 1 > 1

(20) YES

(21) Obligation:

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

LESS31_IN_GG(s(T88), s(T90)) → LESS31_IN_GG(T88, T90)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
LESS31_IN_GG(x1, x2)  =  LESS31_IN_GG(x1, x2)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

LESS31_IN_GG(s(T88), s(T90)) → LESS31_IN_GG(T88, T90)

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

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

LESS31_IN_GG(s(T88), s(T90)) → LESS31_IN_GG(T88, T90)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS31_IN_GG(s(T88), s(T90)) → LESS31_IN_GG(T88, T90)
    The graph contains the following edges 1 > 1, 2 > 2

(27) YES

(28) Obligation:

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

LESS19_IN_GG(s(T52), s(T51)) → LESS19_IN_GG(T52, T51)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
LESS19_IN_GG(x1, x2)  =  LESS19_IN_GG(x1, x2)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

LESS19_IN_GG(s(T52), s(T51)) → LESS19_IN_GG(T52, T51)

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

(31) PiDPToQDPProof (EQUIVALENT transformation)

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

(32) Obligation:

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

LESS19_IN_GG(s(T52), s(T51)) → LESS19_IN_GG(T52, T51)

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

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

  • LESS19_IN_GG(s(T52), s(T51)) → LESS19_IN_GG(T52, T51)
    The graph contains the following edges 1 > 1, 2 > 2

(34) YES

(35) Obligation:

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

DELETE1_IN_GGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GGGA(T318, T321, T319, T322)
P93_IN_GGGA(T318, T325, T319, T326) → U14_GGGA(T318, T325, T319, T326, lessc31_in_gg(T318, T325))
U14_GGGA(T318, T325, T319, T326, lessc31_out_gg(T318, T325)) → DELETE1_IN_GGA(T325, T319, T326)
DELETE1_IN_GGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_GGA(s(T399), T389, T398)
DELETE1_IN_GGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_GGA(T414, T408, T389, T415, lessc31_in_gg(T408, T414))
U34_GGA(T414, T408, T389, T415, lessc31_out_gg(T408, T414)) → DELETE1_IN_GGA(s(T414), T389, T415)
DELETE1_IN_GGA(T464, tree(T457, T458, void), tree(T457, T465, void)) → U37_GGA(T464, T457, T458, T465, lessc19_in_gg(T464, T457))
U37_GGA(T464, T457, T458, T465, lessc19_out_gg(T464, T457)) → DELETE1_IN_GGA(T464, T458, T465)
DELETE1_IN_GGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → DELETE1_IN_GGA(0, T498, T507)
DELETE1_IN_GGA(T673, tree(T665, T666, T676), tree(T665, T674, T676)) → U49_GGA(T673, T665, T666, T676, T674, lessc19_in_gg(T673, T665))
U49_GGA(T673, T665, T666, T676, T674, lessc19_out_gg(T673, T665)) → DELETE1_IN_GGA(T673, T666, T674)
DELETE1_IN_GGA(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) → U42_GGA(T524, T519, T498, T525, lessc19_in_gg(T524, T519))
U42_GGA(T524, T519, T498, T525, lessc19_out_gg(T524, T519)) → DELETE1_IN_GGA(s(T524), T498, T525)
DELETE1_IN_GGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_GGA(T707, T699, T710, T701, T708, lessc31_in_gg(T699, T707))
U52_GGA(T707, T699, T710, T701, T708, lessc31_out_gg(T699, T707)) → DELETE1_IN_GGA(T707, T701, T708)
DELETE1_IN_GGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → DELETE1_IN_GGA(0, T729, T739)
DELETE1_IN_GGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_GGA(T788, T780, T791, T782, T789, lessc31_in_gg(T780, T788))
U59_GGA(T788, T780, T791, T782, T789, lessc31_out_gg(T780, T788)) → DELETE1_IN_GGA(T788, T782, T789)
DELETE1_IN_GGA(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) → U56_GGA(T756, T751, T729, T759, T757, lessc19_in_gg(T756, T751))
U56_GGA(T756, T751, T729, T759, T757, lessc19_out_gg(T756, T751)) → DELETE1_IN_GGA(s(T756), T729, T757)
DELETE1_IN_GGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_GGA(s(T826), T816, T825)
DELETE1_IN_GGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_GGA(T841, T835, T844, T816, T842, lessc31_in_gg(T835, T841))
U63_GGA(T841, T835, T844, T816, T842, lessc31_out_gg(T835, T841)) → DELETE1_IN_GGA(s(T841), T816, T842)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
P93_IN_GGGA(x1, x2, x3, x4)  =  P93_IN_GGGA(x1, x2, x3)
U14_GGGA(x1, x2, x3, x4, x5)  =  U14_GGGA(x1, x2, x3, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x2, x3, x5)
U37_GGA(x1, x2, x3, x4, x5)  =  U37_GGA(x1, x2, x3, x5)
U42_GGA(x1, x2, x3, x4, x5)  =  U42_GGA(x1, x2, x3, x5)
U49_GGA(x1, x2, x3, x4, x5, x6)  =  U49_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6)  =  U52_GGA(x1, x2, x3, x4, x6)
U56_GGA(x1, x2, x3, x4, x5, x6)  =  U56_GGA(x1, x2, x3, x4, x6)
U59_GGA(x1, x2, x3, x4, x5, x6)  =  U59_GGA(x1, x2, x3, x4, x6)
U63_GGA(x1, x2, x3, x4, x5, x6)  =  U63_GGA(x1, x2, x3, x4, x6)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

DELETE1_IN_GGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GGGA(T318, T321, T319, T322)
P93_IN_GGGA(T318, T325, T319, T326) → U14_GGGA(T318, T325, T319, T326, lessc31_in_gg(T318, T325))
U14_GGGA(T318, T325, T319, T326, lessc31_out_gg(T318, T325)) → DELETE1_IN_GGA(T325, T319, T326)
DELETE1_IN_GGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_GGA(s(T399), T389, T398)
DELETE1_IN_GGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_GGA(T414, T408, T389, T415, lessc31_in_gg(T408, T414))
U34_GGA(T414, T408, T389, T415, lessc31_out_gg(T408, T414)) → DELETE1_IN_GGA(s(T414), T389, T415)
DELETE1_IN_GGA(T464, tree(T457, T458, void), tree(T457, T465, void)) → U37_GGA(T464, T457, T458, T465, lessc19_in_gg(T464, T457))
U37_GGA(T464, T457, T458, T465, lessc19_out_gg(T464, T457)) → DELETE1_IN_GGA(T464, T458, T465)
DELETE1_IN_GGA(0, tree(s(T506), T498, void), tree(s(T506), T507, void)) → DELETE1_IN_GGA(0, T498, T507)
DELETE1_IN_GGA(T673, tree(T665, T666, T676), tree(T665, T674, T676)) → U49_GGA(T673, T665, T666, T676, T674, lessc19_in_gg(T673, T665))
U49_GGA(T673, T665, T666, T676, T674, lessc19_out_gg(T673, T665)) → DELETE1_IN_GGA(T673, T666, T674)
DELETE1_IN_GGA(s(T524), tree(s(T519), T498, void), tree(s(T519), T525, void)) → U42_GGA(T524, T519, T498, T525, lessc19_in_gg(T524, T519))
U42_GGA(T524, T519, T498, T525, lessc19_out_gg(T524, T519)) → DELETE1_IN_GGA(s(T524), T498, T525)
DELETE1_IN_GGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_GGA(T707, T699, T710, T701, T708, lessc31_in_gg(T699, T707))
U52_GGA(T707, T699, T710, T701, T708, lessc31_out_gg(T699, T707)) → DELETE1_IN_GGA(T707, T701, T708)
DELETE1_IN_GGA(0, tree(s(T738), T729, T730), tree(s(T738), T739, T730)) → DELETE1_IN_GGA(0, T729, T739)
DELETE1_IN_GGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_GGA(T788, T780, T791, T782, T789, lessc31_in_gg(T780, T788))
U59_GGA(T788, T780, T791, T782, T789, lessc31_out_gg(T780, T788)) → DELETE1_IN_GGA(T788, T782, T789)
DELETE1_IN_GGA(s(T756), tree(s(T751), T729, T759), tree(s(T751), T757, T759)) → U56_GGA(T756, T751, T729, T759, T757, lessc19_in_gg(T756, T751))
U56_GGA(T756, T751, T729, T759, T757, lessc19_out_gg(T756, T751)) → DELETE1_IN_GGA(s(T756), T729, T757)
DELETE1_IN_GGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_GGA(s(T826), T816, T825)
DELETE1_IN_GGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_GGA(T841, T835, T844, T816, T842, lessc31_in_gg(T835, T841))
U63_GGA(T841, T835, T844, T816, T842, lessc31_out_gg(T835, T841)) → DELETE1_IN_GGA(s(T841), T816, T842)

The TRS R consists of the following rules:

lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
s(x1)  =  s(x1)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
P93_IN_GGGA(x1, x2, x3, x4)  =  P93_IN_GGGA(x1, x2, x3)
U14_GGGA(x1, x2, x3, x4, x5)  =  U14_GGGA(x1, x2, x3, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x2, x3, x5)
U37_GGA(x1, x2, x3, x4, x5)  =  U37_GGA(x1, x2, x3, x5)
U42_GGA(x1, x2, x3, x4, x5)  =  U42_GGA(x1, x2, x3, x5)
U49_GGA(x1, x2, x3, x4, x5, x6)  =  U49_GGA(x1, x2, x3, x4, x6)
U52_GGA(x1, x2, x3, x4, x5, x6)  =  U52_GGA(x1, x2, x3, x4, x6)
U56_GGA(x1, x2, x3, x4, x5, x6)  =  U56_GGA(x1, x2, x3, x4, x6)
U59_GGA(x1, x2, x3, x4, x5, x6)  =  U59_GGA(x1, x2, x3, x4, x6)
U63_GGA(x1, x2, x3, x4, x5, x6)  =  U63_GGA(x1, x2, x3, x4, x6)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

DELETE1_IN_GGA(T321, tree(T318, void, T319)) → P93_IN_GGGA(T318, T321, T319)
P93_IN_GGGA(T318, T325, T319) → U14_GGGA(T318, T325, T319, lessc31_in_gg(T318, T325))
U14_GGGA(T318, T325, T319, lessc31_out_gg(T318, T325)) → DELETE1_IN_GGA(T325, T319)
DELETE1_IN_GGA(s(T399), tree(0, void, T389)) → DELETE1_IN_GGA(s(T399), T389)
DELETE1_IN_GGA(s(T414), tree(s(T408), void, T389)) → U34_GGA(T414, T408, T389, lessc31_in_gg(T408, T414))
U34_GGA(T414, T408, T389, lessc31_out_gg(T408, T414)) → DELETE1_IN_GGA(s(T414), T389)
DELETE1_IN_GGA(T464, tree(T457, T458, void)) → U37_GGA(T464, T457, T458, lessc19_in_gg(T464, T457))
U37_GGA(T464, T457, T458, lessc19_out_gg(T464, T457)) → DELETE1_IN_GGA(T464, T458)
DELETE1_IN_GGA(0, tree(s(T506), T498, void)) → DELETE1_IN_GGA(0, T498)
DELETE1_IN_GGA(T673, tree(T665, T666, T676)) → U49_GGA(T673, T665, T666, T676, lessc19_in_gg(T673, T665))
U49_GGA(T673, T665, T666, T676, lessc19_out_gg(T673, T665)) → DELETE1_IN_GGA(T673, T666)
DELETE1_IN_GGA(s(T524), tree(s(T519), T498, void)) → U42_GGA(T524, T519, T498, lessc19_in_gg(T524, T519))
U42_GGA(T524, T519, T498, lessc19_out_gg(T524, T519)) → DELETE1_IN_GGA(s(T524), T498)
DELETE1_IN_GGA(T707, tree(T699, T710, T701)) → U52_GGA(T707, T699, T710, T701, lessc31_in_gg(T699, T707))
U52_GGA(T707, T699, T710, T701, lessc31_out_gg(T699, T707)) → DELETE1_IN_GGA(T707, T701)
DELETE1_IN_GGA(0, tree(s(T738), T729, T730)) → DELETE1_IN_GGA(0, T729)
DELETE1_IN_GGA(T788, tree(T780, T791, T782)) → U59_GGA(T788, T780, T791, T782, lessc31_in_gg(T780, T788))
U59_GGA(T788, T780, T791, T782, lessc31_out_gg(T780, T788)) → DELETE1_IN_GGA(T788, T782)
DELETE1_IN_GGA(s(T756), tree(s(T751), T729, T759)) → U56_GGA(T756, T751, T729, T759, lessc19_in_gg(T756, T751))
U56_GGA(T756, T751, T729, T759, lessc19_out_gg(T756, T751)) → DELETE1_IN_GGA(s(T756), T729)
DELETE1_IN_GGA(s(T826), tree(0, T815, T816)) → DELETE1_IN_GGA(s(T826), T816)
DELETE1_IN_GGA(s(T841), tree(s(T835), T844, T816)) → U63_GGA(T841, T835, T844, T816, lessc31_in_gg(T835, T841))
U63_GGA(T841, T835, T844, T816, lessc31_out_gg(T835, T841)) → DELETE1_IN_GGA(s(T841), T816)

The TRS R consists of the following rules:

lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))

The set Q consists of the following terms:

lessc31_in_gg(x0, x1)
lessc19_in_gg(x0, x1)
U105_gg(x0, x1, x2)
U104_gg(x0, x1, x2)

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

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

  • P93_IN_GGGA(T318, T325, T319) → U14_GGGA(T318, T325, T319, lessc31_in_gg(T318, T325))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U14_GGGA(T318, T325, T319, lessc31_out_gg(T318, T325)) → DELETE1_IN_GGA(T325, T319)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • DELETE1_IN_GGA(T321, tree(T318, void, T319)) → P93_IN_GGGA(T318, T321, T319)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • U34_GGA(T414, T408, T389, lessc31_out_gg(T408, T414)) → DELETE1_IN_GGA(s(T414), T389)
    The graph contains the following edges 3 >= 2

  • DELETE1_IN_GGA(s(T414), tree(s(T408), void, T389)) → U34_GGA(T414, T408, T389, lessc31_in_gg(T408, T414))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • U37_GGA(T464, T457, T458, lessc19_out_gg(T464, T457)) → DELETE1_IN_GGA(T464, T458)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

  • DELETE1_IN_GGA(T464, tree(T457, T458, void)) → U37_GGA(T464, T457, T458, lessc19_in_gg(T464, T457))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • U49_GGA(T673, T665, T666, T676, lessc19_out_gg(T673, T665)) → DELETE1_IN_GGA(T673, T666)
    The graph contains the following edges 1 >= 1, 5 > 1, 3 >= 2

  • DELETE1_IN_GGA(T673, tree(T665, T666, T676)) → U49_GGA(T673, T665, T666, T676, lessc19_in_gg(T673, T665))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

  • U42_GGA(T524, T519, T498, lessc19_out_gg(T524, T519)) → DELETE1_IN_GGA(s(T524), T498)
    The graph contains the following edges 3 >= 2

  • DELETE1_IN_GGA(s(T524), tree(s(T519), T498, void)) → U42_GGA(T524, T519, T498, lessc19_in_gg(T524, T519))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • U52_GGA(T707, T699, T710, T701, lessc31_out_gg(T699, T707)) → DELETE1_IN_GGA(T707, T701)
    The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2

  • U59_GGA(T788, T780, T791, T782, lessc31_out_gg(T780, T788)) → DELETE1_IN_GGA(T788, T782)
    The graph contains the following edges 1 >= 1, 5 > 1, 4 >= 2

  • DELETE1_IN_GGA(T707, tree(T699, T710, T701)) → U52_GGA(T707, T699, T710, T701, lessc31_in_gg(T699, T707))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

  • DELETE1_IN_GGA(T788, tree(T780, T791, T782)) → U59_GGA(T788, T780, T791, T782, lessc31_in_gg(T780, T788))
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3, 2 > 4

  • U56_GGA(T756, T751, T729, T759, lessc19_out_gg(T756, T751)) → DELETE1_IN_GGA(s(T756), T729)
    The graph contains the following edges 3 >= 2

  • U63_GGA(T841, T835, T844, T816, lessc31_out_gg(T835, T841)) → DELETE1_IN_GGA(s(T841), T816)
    The graph contains the following edges 4 >= 2

  • DELETE1_IN_GGA(s(T756), tree(s(T751), T729, T759)) → U56_GGA(T756, T751, T729, T759, lessc19_in_gg(T756, T751))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3, 2 > 4

  • DELETE1_IN_GGA(s(T841), tree(s(T835), T844, T816)) → U63_GGA(T841, T835, T844, T816, lessc31_in_gg(T835, T841))
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3, 2 > 4

  • DELETE1_IN_GGA(s(T399), tree(0, void, T389)) → DELETE1_IN_GGA(s(T399), T389)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETE1_IN_GGA(s(T826), tree(0, T815, T816)) → DELETE1_IN_GGA(s(T826), T816)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETE1_IN_GGA(0, tree(s(T506), T498, void)) → DELETE1_IN_GGA(0, T498)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETE1_IN_GGA(0, tree(s(T738), T729, T730)) → DELETE1_IN_GGA(0, T729)
    The graph contains the following edges 1 >= 1, 2 > 2

(41) YES

(42) Obligation:

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

LESS19_IN_AG(s(T52), s(T51)) → LESS19_IN_AG(T52, T51)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
LESS19_IN_AG(x1, x2)  =  LESS19_IN_AG(x2)

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

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

LESS19_IN_AG(s(T52), s(T51)) → LESS19_IN_AG(T52, T51)

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

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

LESS19_IN_AG(s(T51)) → LESS19_IN_AG(T51)

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

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

  • LESS19_IN_AG(s(T51)) → LESS19_IN_AG(T51)
    The graph contains the following edges 1 > 1

(48) YES

(49) Obligation:

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

DELETE1_IN_AGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GAGA(T318, T321, T319, T322)
P93_IN_GAGA(T318, T325, T319, T326) → U14_GAGA(T318, T325, T319, T326, lessc31_in_ga(T318, T325))
U14_GAGA(T318, T325, T319, T326, lessc31_out_ga(T318, T325)) → DELETE1_IN_AGA(T325, T319, T326)
DELETE1_IN_AGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_AGA(s(T399), T389, T398)
DELETE1_IN_AGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_AGA(T414, T408, T389, T415, lessc31_in_ga(T408, T414))
U34_AGA(T414, T408, T389, T415, lessc31_out_ga(T408, T414)) → DELETE1_IN_AGA(s(T414), T389, T415)
DELETE1_IN_AGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_AGA(T707, T699, T710, T701, T708, lessc31_in_ga(T699, T707))
U52_AGA(T707, T699, T710, T701, T708, lessc31_out_ga(T699, T707)) → DELETE1_IN_AGA(T707, T701, T708)
DELETE1_IN_AGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_AGA(T788, T780, T791, T782, T789, lessc31_in_ga(T780, T788))
U59_AGA(T788, T780, T791, T782, T789, lessc31_out_ga(T780, T788)) → DELETE1_IN_AGA(T788, T782, T789)
DELETE1_IN_AGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_AGA(s(T826), T816, T825)
DELETE1_IN_AGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_AGA(T841, T835, T844, T816, T842, lessc31_in_ga(T835, T841))
U63_AGA(T841, T835, T844, T816, T842, lessc31_out_ga(T835, T841)) → DELETE1_IN_AGA(s(T841), T816, T842)

The TRS R consists of the following rules:

lessc19_in_ag(0, s(T45)) → lessc19_out_ag(0, s(T45))
lessc19_in_ag(s(T52), s(T51)) → U104_ag(T52, T51, lessc19_in_ag(T52, T51))
U104_ag(T52, T51, lessc19_out_ag(T52, T51)) → lessc19_out_ag(s(T52), s(T51))
lessc19_in_gg(0, s(T45)) → lessc19_out_gg(0, s(T45))
lessc19_in_gg(s(T52), s(T51)) → U104_gg(T52, T51, lessc19_in_gg(T52, T51))
U104_gg(T52, T51, lessc19_out_gg(T52, T51)) → lessc19_out_gg(s(T52), s(T51))
lessc31_in_gg(0, s(T83)) → lessc31_out_gg(0, s(T83))
lessc31_in_gg(s(T88), s(T90)) → U105_gg(T88, T90, lessc31_in_gg(T88, T90))
U105_gg(T88, T90, lessc31_out_gg(T88, T90)) → lessc31_out_gg(s(T88), s(T90))
lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
s(x1)  =  s(x1)
lessc19_in_ag(x1, x2)  =  lessc19_in_ag(x2)
lessc19_out_ag(x1, x2)  =  lessc19_out_ag(x1, x2)
U104_ag(x1, x2, x3)  =  U104_ag(x2, x3)
lessc19_in_gg(x1, x2)  =  lessc19_in_gg(x1, x2)
0  =  0
lessc19_out_gg(x1, x2)  =  lessc19_out_gg(x1, x2)
U104_gg(x1, x2, x3)  =  U104_gg(x1, x2, x3)
lessc31_in_gg(x1, x2)  =  lessc31_in_gg(x1, x2)
lessc31_out_gg(x1, x2)  =  lessc31_out_gg(x1, x2)
U105_gg(x1, x2, x3)  =  U105_gg(x1, x2, x3)
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
DELETE1_IN_AGA(x1, x2, x3)  =  DELETE1_IN_AGA(x2)
P93_IN_GAGA(x1, x2, x3, x4)  =  P93_IN_GAGA(x1, x3)
U14_GAGA(x1, x2, x3, x4, x5)  =  U14_GAGA(x1, x3, x5)
U34_AGA(x1, x2, x3, x4, x5)  =  U34_AGA(x2, x3, x5)
U52_AGA(x1, x2, x3, x4, x5, x6)  =  U52_AGA(x2, x3, x4, x6)
U59_AGA(x1, x2, x3, x4, x5, x6)  =  U59_AGA(x2, x3, x4, x6)
U63_AGA(x1, x2, x3, x4, x5, x6)  =  U63_AGA(x2, x3, x4, x6)

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

(50) UsableRulesProof (EQUIVALENT transformation)

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

(51) Obligation:

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

DELETE1_IN_AGA(T321, tree(T318, void, T319), tree(T318, void, T322)) → P93_IN_GAGA(T318, T321, T319, T322)
P93_IN_GAGA(T318, T325, T319, T326) → U14_GAGA(T318, T325, T319, T326, lessc31_in_ga(T318, T325))
U14_GAGA(T318, T325, T319, T326, lessc31_out_ga(T318, T325)) → DELETE1_IN_AGA(T325, T319, T326)
DELETE1_IN_AGA(s(T399), tree(0, void, T389), tree(0, void, T398)) → DELETE1_IN_AGA(s(T399), T389, T398)
DELETE1_IN_AGA(s(T414), tree(s(T408), void, T389), tree(s(T408), void, T415)) → U34_AGA(T414, T408, T389, T415, lessc31_in_ga(T408, T414))
U34_AGA(T414, T408, T389, T415, lessc31_out_ga(T408, T414)) → DELETE1_IN_AGA(s(T414), T389, T415)
DELETE1_IN_AGA(T707, tree(T699, T710, T701), tree(T699, T710, T708)) → U52_AGA(T707, T699, T710, T701, T708, lessc31_in_ga(T699, T707))
U52_AGA(T707, T699, T710, T701, T708, lessc31_out_ga(T699, T707)) → DELETE1_IN_AGA(T707, T701, T708)
DELETE1_IN_AGA(T788, tree(T780, T791, T782), tree(T780, T791, T789)) → U59_AGA(T788, T780, T791, T782, T789, lessc31_in_ga(T780, T788))
U59_AGA(T788, T780, T791, T782, T789, lessc31_out_ga(T780, T788)) → DELETE1_IN_AGA(T788, T782, T789)
DELETE1_IN_AGA(s(T826), tree(0, T815, T816), tree(0, T815, T825)) → DELETE1_IN_AGA(s(T826), T816, T825)
DELETE1_IN_AGA(s(T841), tree(s(T835), T844, T816), tree(s(T835), T844, T842)) → U63_AGA(T841, T835, T844, T816, T842, lessc31_in_ga(T835, T841))
U63_AGA(T841, T835, T844, T816, T842, lessc31_out_ga(T835, T841)) → DELETE1_IN_AGA(s(T841), T816, T842)

The TRS R consists of the following rules:

lessc31_in_ga(0, s(T83)) → lessc31_out_ga(0, s(T83))
lessc31_in_ga(s(T88), s(T90)) → U105_ga(T88, T90, lessc31_in_ga(T88, T90))
U105_ga(T88, T90, lessc31_out_ga(T88, T90)) → lessc31_out_ga(s(T88), s(T90))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
s(x1)  =  s(x1)
0  =  0
lessc31_in_ga(x1, x2)  =  lessc31_in_ga(x1)
lessc31_out_ga(x1, x2)  =  lessc31_out_ga(x1)
U105_ga(x1, x2, x3)  =  U105_ga(x1, x3)
DELETE1_IN_AGA(x1, x2, x3)  =  DELETE1_IN_AGA(x2)
P93_IN_GAGA(x1, x2, x3, x4)  =  P93_IN_GAGA(x1, x3)
U14_GAGA(x1, x2, x3, x4, x5)  =  U14_GAGA(x1, x3, x5)
U34_AGA(x1, x2, x3, x4, x5)  =  U34_AGA(x2, x3, x5)
U52_AGA(x1, x2, x3, x4, x5, x6)  =  U52_AGA(x2, x3, x4, x6)
U59_AGA(x1, x2, x3, x4, x5, x6)  =  U59_AGA(x2, x3, x4, x6)
U63_AGA(x1, x2, x3, x4, x5, x6)  =  U63_AGA(x2, x3, x4, x6)

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

(52) PiDPToQDPProof (SOUND transformation)

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

(53) Obligation:

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

DELETE1_IN_AGA(tree(T318, void, T319)) → P93_IN_GAGA(T318, T319)
P93_IN_GAGA(T318, T319) → U14_GAGA(T318, T319, lessc31_in_ga(T318))
U14_GAGA(T318, T319, lessc31_out_ga(T318)) → DELETE1_IN_AGA(T319)
DELETE1_IN_AGA(tree(0, void, T389)) → DELETE1_IN_AGA(T389)
DELETE1_IN_AGA(tree(s(T408), void, T389)) → U34_AGA(T408, T389, lessc31_in_ga(T408))
U34_AGA(T408, T389, lessc31_out_ga(T408)) → DELETE1_IN_AGA(T389)
DELETE1_IN_AGA(tree(T699, T710, T701)) → U52_AGA(T699, T710, T701, lessc31_in_ga(T699))
U52_AGA(T699, T710, T701, lessc31_out_ga(T699)) → DELETE1_IN_AGA(T701)
DELETE1_IN_AGA(tree(T780, T791, T782)) → U59_AGA(T780, T791, T782, lessc31_in_ga(T780))
U59_AGA(T780, T791, T782, lessc31_out_ga(T780)) → DELETE1_IN_AGA(T782)
DELETE1_IN_AGA(tree(0, T815, T816)) → DELETE1_IN_AGA(T816)
DELETE1_IN_AGA(tree(s(T835), T844, T816)) → U63_AGA(T835, T844, T816, lessc31_in_ga(T835))
U63_AGA(T835, T844, T816, lessc31_out_ga(T835)) → DELETE1_IN_AGA(T816)

The TRS R consists of the following rules:

lessc31_in_ga(0) → lessc31_out_ga(0)
lessc31_in_ga(s(T88)) → U105_ga(T88, lessc31_in_ga(T88))
U105_ga(T88, lessc31_out_ga(T88)) → lessc31_out_ga(s(T88))

The set Q consists of the following terms:

lessc31_in_ga(x0)
U105_ga(x0, x1)

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

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

  • P93_IN_GAGA(T318, T319) → U14_GAGA(T318, T319, lessc31_in_ga(T318))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U14_GAGA(T318, T319, lessc31_out_ga(T318)) → DELETE1_IN_AGA(T319)
    The graph contains the following edges 2 >= 1

  • DELETE1_IN_AGA(tree(T318, void, T319)) → P93_IN_GAGA(T318, T319)
    The graph contains the following edges 1 > 1, 1 > 2

  • U34_AGA(T408, T389, lessc31_out_ga(T408)) → DELETE1_IN_AGA(T389)
    The graph contains the following edges 2 >= 1

  • DELETE1_IN_AGA(tree(s(T408), void, T389)) → U34_AGA(T408, T389, lessc31_in_ga(T408))
    The graph contains the following edges 1 > 1, 1 > 2

  • U52_AGA(T699, T710, T701, lessc31_out_ga(T699)) → DELETE1_IN_AGA(T701)
    The graph contains the following edges 3 >= 1

  • DELETE1_IN_AGA(tree(T699, T710, T701)) → U52_AGA(T699, T710, T701, lessc31_in_ga(T699))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

  • U59_AGA(T780, T791, T782, lessc31_out_ga(T780)) → DELETE1_IN_AGA(T782)
    The graph contains the following edges 3 >= 1

  • U63_AGA(T835, T844, T816, lessc31_out_ga(T835)) → DELETE1_IN_AGA(T816)
    The graph contains the following edges 3 >= 1

  • DELETE1_IN_AGA(tree(T780, T791, T782)) → U59_AGA(T780, T791, T782, lessc31_in_ga(T780))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

  • DELETE1_IN_AGA(tree(s(T835), T844, T816)) → U63_AGA(T835, T844, T816, lessc31_in_ga(T835))
    The graph contains the following edges 1 > 1, 1 > 2, 1 > 3

  • DELETE1_IN_AGA(tree(0, void, T389)) → DELETE1_IN_AGA(T389)
    The graph contains the following edges 1 > 1

  • DELETE1_IN_AGA(tree(0, T815, T816)) → DELETE1_IN_AGA(T816)
    The graph contains the following edges 1 > 1

(55) YES