(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(g,a,g).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

delmin19(tree(T76, void, T77), T76, T77).
delmin19(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delmin19(T96, T93, T94).
less34(0, s(T135)).
less34(s(T140), s(T141)) :- less34(T140, T141).
p44(T159, T158, T163, T162) :- less34(T159, T158).
p44(T159, T158, T163, T162) :- ','(less34(T159, T158), delete1(T158, T163, T162)).
p32(T121, T122, T126, T125) :- less34(T121, T122).
p32(T121, T122, T126, T125) :- ','(less34(T121, T122), delete1(T121, T126, T125)).
p64(0, s(T241), T236, T235) :- delete1(s(T241), T236, T235).
p64(s(T250), s(T251), T236, T235) :- p71(T250, T251, T236, T235).
p57(T198, T199, T182, T181) :- less34(T198, T199).
p57(T198, T199, T182, T181) :- ','(less34(T198, T199), delete1(s(T198), T182, T181)).
p71(T250, T251, T236, T235) :- less34(T250, T251).
p71(T250, T251, T236, T235) :- ','(less34(T250, T251), delete1(s(T251), T236, T235)).
p108(0, s(T425), T420, T419) :- delete1(s(T425), T420, T419).
p108(s(T434), s(T435), T420, T419) :- p71(T434, T435, T420, T419).
delete1(T6, tree(T6, void, T7), T7).
delete1(T10, tree(T10, T11, void), T11).
delete1(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)).
delete1(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delmin19(T63, T60, T61).
delete1(T121, tree(T122, T126, T124), tree(T122, T125, T124)) :- p32(T121, T122, T126, T125).
delete1(T158, tree(T159, T160, T163), tree(T159, T160, T162)) :- p44(T159, T158, T163, T162).
delete1(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) :- delete1(0, T182, T181).
delete1(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) :- p57(T198, T199, T182, T181).
delete1(T218, tree(T219, T220, T223), tree(T219, T220, T222)) :- p44(T219, T218, T223, T222).
delete1(T231, tree(T232, T233, T236), tree(T232, T233, T235)) :- p64(T232, T231, T236, T235).
delete1(T265, tree(T265, T266, tree(T279, void, T280)), tree(T279, T266, T280)).
delete1(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) :- delmin19(T311, T308, T309).
delete1(T336, tree(T337, T341, T339), tree(T337, T340, T339)) :- p32(T336, T337, T341, T340).
delete1(T354, tree(T355, T356, T359), tree(T355, T356, T358)) :- p64(T355, T354, T359, T358).
delete1(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) :- delete1(0, T372, T371).
delete1(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) :- p57(T388, T389, T372, T371).
delete1(T402, tree(T403, T404, T407), tree(T403, T404, T406)) :- p64(T403, T402, T407, T406).
delete1(T415, tree(T416, T417, T420), tree(T416, T417, T419)) :- p108(T416, T415, T420, T419).
delete1(T440, tree(T440, T441, void), T441).
delete1(T447, tree(T447, T448, tree(T461, void, T462)), tree(T461, T448, T462)).
delete1(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) :- delmin19(T493, T490, T491).
delete1(T518, tree(T519, T523, T521), tree(T519, T522, T521)) :- p32(T518, T519, T523, T522).
delete1(T536, tree(T537, T538, T541), tree(T537, T538, T540)) :- p108(T537, T536, T541, T540).
delete1(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) :- delete1(0, T554, T553).
delete1(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) :- p57(T570, T571, T554, T553).
delete1(T584, tree(T585, T586, T589), tree(T585, T586, T588)) :- p108(T585, T584, T589, T588).
delete1(s(T607), tree(0, T599, T602), tree(0, T599, T601)) :- delete1(s(T607), T602, T601).
delete1(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) :- p71(T616, T617, T602, T601).
delete1(T625, tree(T625, T626, tree(T639, void, T640)), tree(T639, T626, T640)).
delete1(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) :- delmin19(T671, T668, T669).
delete1(T696, tree(T697, T701, T699), tree(T697, T700, T699)) :- p32(T696, T697, T701, T700).
delete1(T714, tree(T715, T716, T719), tree(T715, T716, T718)) :- p108(T715, T714, T719, T718).
delete1(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) :- delete1(0, T732, T731).
delete1(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) :- p57(T748, T749, T732, T731).
delete1(T762, tree(T763, T764, T767), tree(T763, T764, T766)) :- p108(T763, T762, T767, T766).
delete1(s(T785), tree(0, T777, T780), tree(0, T777, T779)) :- delete1(s(T785), T780, T779).
delete1(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) :- p71(T794, T795, T780, T779).

Queries:

delete1(g,a,g).

(3) PrologToPiTRSProof (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: (b,f,b)
delmin19_in: (f,b,b)
p32_in: (b,b,f,b)
less34_in: (b,b)
p44_in: (b,b,f,b)
p57_in: (b,b,f,b)
p64_in: (b,b,f,b)
p71_in: (b,b,f,b)
p108_in: (b,b,f,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

Pi-finite rewrite system:
The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)

(5) DependencyPairsProof (EQUIVALENT transformation)

Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_GAG(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, less34_in_gg(T121, T122))
P32_IN_GGAG(T121, T122, T126, T125) → LESS34_IN_GG(T121, T122)
LESS34_IN_GG(s(T140), s(T141)) → U2_GG(T140, T141, less34_in_gg(T140, T141))
LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)
U5_GGAG(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_GGAG(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
U5_GGAG(T121, T122, T126, T125, less34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_GAG(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, less34_in_gg(T159, T158))
P44_IN_GGAG(T159, T158, T163, T162) → LESS34_IN_GG(T159, T158)
U3_GGAG(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_GGAG(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
U3_GGAG(T159, T158, T163, T162, less34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_GAG(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_GAG(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U9_GGAG(T198, T199, T182, T181, less34_in_gg(T198, T199))
P57_IN_GGAG(T198, T199, T182, T181) → LESS34_IN_GG(T198, T199)
U9_GGAG(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_GGAG(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
U9_GGAG(T198, T199, T182, T181, less34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_GAG(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_GAG(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → U7_GGAG(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_GAG(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
DELETE1_IN_GAG(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_GAG(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
DELETE1_IN_GAG(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_GAG(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → U8_GGAG(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)
P71_IN_GGAG(T250, T251, T236, T235) → U11_GGAG(T250, T251, T236, T235, less34_in_gg(T250, T251))
P71_IN_GGAG(T250, T251, T236, T235) → LESS34_IN_GG(T250, T251)
U11_GGAG(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_GGAG(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
U11_GGAG(T250, T251, T236, T235, less34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
DELETE1_IN_GAG(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_GAG(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
DELETE1_IN_GAG(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_GAG(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
DELETE1_IN_GAG(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_GAG(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_GAG(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → U13_GGAG(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_GAG(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
DELETE1_IN_GAG(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_GAG(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
DELETE1_IN_GAG(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_GAG(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → U14_GGAG(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
DELETE1_IN_GAG(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_GAG(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
DELETE1_IN_GAG(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_GAG(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
DELETE1_IN_GAG(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_GAG(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_GAG(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_GAG(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
DELETE1_IN_GAG(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_GAG(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
DELETE1_IN_GAG(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_GAG(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
DELETE1_IN_GAG(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_GAG(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
DELETE1_IN_GAG(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_GAG(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
DELETE1_IN_GAG(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_GAG(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
DELETE1_IN_GAG(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_GAG(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
DELETE1_IN_GAG(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_GAG(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
DELETE1_IN_GAG(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_GAG(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))

The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
U15_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GAG(x9)
DELMIN19_IN_AGG(x1, x2, x3)  =  DELMIN19_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x7)
U16_GAG(x1, x2, x3, x4, x5, x6)  =  U16_GAG(x6)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x4, x5)
LESS34_IN_GG(x1, x2)  =  LESS34_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)
U6_GGAG(x1, x2, x3, x4, x5)  =  U6_GGAG(x5)
U17_GAG(x1, x2, x3, x4, x5, x6)  =  U17_GAG(x6)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x2, x4, x5)
U4_GGAG(x1, x2, x3, x4, x5)  =  U4_GGAG(x5)
U18_GAG(x1, x2, x3, x4, x5)  =  U18_GAG(x5)
U19_GAG(x1, x2, x3, x4, x5, x6)  =  U19_GAG(x6)
P57_IN_GGAG(x1, x2, x3, x4)  =  P57_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x4, x5)
U10_GGAG(x1, x2, x3, x4, x5)  =  U10_GGAG(x5)
U20_GAG(x1, x2, x3, x4, x5, x6)  =  U20_GAG(x6)
U21_GAG(x1, x2, x3, x4, x5, x6)  =  U21_GAG(x6)
P64_IN_GGAG(x1, x2, x3, x4)  =  P64_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4)  =  U7_GGAG(x4)
U22_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_GAG(x9)
U23_GAG(x1, x2, x3, x4, x5, x6)  =  U23_GAG(x6)
U24_GAG(x1, x2, x3, x4, x5, x6)  =  U24_GAG(x6)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x5)
P71_IN_GGAG(x1, x2, x3, x4)  =  P71_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x2, x4, x5)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x5)
U25_GAG(x1, x2, x3, x4, x5)  =  U25_GAG(x5)
U26_GAG(x1, x2, x3, x4, x5, x6)  =  U26_GAG(x6)
U27_GAG(x1, x2, x3, x4, x5, x6)  =  U27_GAG(x6)
U28_GAG(x1, x2, x3, x4, x5, x6)  =  U28_GAG(x6)
P108_IN_GGAG(x1, x2, x3, x4)  =  P108_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4)  =  U13_GGAG(x4)
U29_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_GAG(x9)
U30_GAG(x1, x2, x3, x4, x5, x6)  =  U30_GAG(x6)
U31_GAG(x1, x2, x3, x4, x5, x6)  =  U31_GAG(x6)
U14_GGAG(x1, x2, x3, x4, x5)  =  U14_GGAG(x5)
U32_GAG(x1, x2, x3, x4, x5)  =  U32_GAG(x5)
U33_GAG(x1, x2, x3, x4, x5, x6)  =  U33_GAG(x6)
U34_GAG(x1, x2, x3, x4, x5, x6)  =  U34_GAG(x6)
U35_GAG(x1, x2, x3, x4, x5)  =  U35_GAG(x5)
U36_GAG(x1, x2, x3, x4, x5, x6)  =  U36_GAG(x6)
U37_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_GAG(x9)
U38_GAG(x1, x2, x3, x4, x5, x6)  =  U38_GAG(x6)
U39_GAG(x1, x2, x3, x4, x5, x6)  =  U39_GAG(x6)
U40_GAG(x1, x2, x3, x4, x5)  =  U40_GAG(x5)
U41_GAG(x1, x2, x3, x4, x5, x6)  =  U41_GAG(x6)
U42_GAG(x1, x2, x3, x4, x5, x6)  =  U42_GAG(x6)
U43_GAG(x1, x2, x3, x4, x5)  =  U43_GAG(x5)
U44_GAG(x1, x2, x3, x4, x5, x6)  =  U44_GAG(x6)

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

(6) Obligation:

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

DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_GAG(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, less34_in_gg(T121, T122))
P32_IN_GGAG(T121, T122, T126, T125) → LESS34_IN_GG(T121, T122)
LESS34_IN_GG(s(T140), s(T141)) → U2_GG(T140, T141, less34_in_gg(T140, T141))
LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)
U5_GGAG(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_GGAG(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
U5_GGAG(T121, T122, T126, T125, less34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_GAG(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, less34_in_gg(T159, T158))
P44_IN_GGAG(T159, T158, T163, T162) → LESS34_IN_GG(T159, T158)
U3_GGAG(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_GGAG(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
U3_GGAG(T159, T158, T163, T162, less34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_GAG(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_GAG(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U9_GGAG(T198, T199, T182, T181, less34_in_gg(T198, T199))
P57_IN_GGAG(T198, T199, T182, T181) → LESS34_IN_GG(T198, T199)
U9_GGAG(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_GGAG(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
U9_GGAG(T198, T199, T182, T181, less34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_GAG(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_GAG(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → U7_GGAG(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_GAG(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
DELETE1_IN_GAG(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_GAG(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
DELETE1_IN_GAG(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_GAG(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → U8_GGAG(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)
P71_IN_GGAG(T250, T251, T236, T235) → U11_GGAG(T250, T251, T236, T235, less34_in_gg(T250, T251))
P71_IN_GGAG(T250, T251, T236, T235) → LESS34_IN_GG(T250, T251)
U11_GGAG(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_GGAG(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
U11_GGAG(T250, T251, T236, T235, less34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
DELETE1_IN_GAG(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_GAG(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
DELETE1_IN_GAG(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_GAG(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
DELETE1_IN_GAG(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_GAG(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_GAG(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → U13_GGAG(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_GAG(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
DELETE1_IN_GAG(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_GAG(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
DELETE1_IN_GAG(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_GAG(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → U14_GGAG(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
DELETE1_IN_GAG(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_GAG(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
DELETE1_IN_GAG(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_GAG(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
DELETE1_IN_GAG(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_GAG(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_GAG(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_GAG(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
DELETE1_IN_GAG(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_GAG(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
DELETE1_IN_GAG(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_GAG(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
DELETE1_IN_GAG(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_GAG(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
DELETE1_IN_GAG(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_GAG(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
DELETE1_IN_GAG(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_GAG(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
DELETE1_IN_GAG(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_GAG(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
DELETE1_IN_GAG(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_GAG(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
DELETE1_IN_GAG(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_GAG(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))

The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
U15_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_GAG(x9)
DELMIN19_IN_AGG(x1, x2, x3)  =  DELMIN19_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x7)
U16_GAG(x1, x2, x3, x4, x5, x6)  =  U16_GAG(x6)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x4, x5)
LESS34_IN_GG(x1, x2)  =  LESS34_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x3)
U6_GGAG(x1, x2, x3, x4, x5)  =  U6_GGAG(x5)
U17_GAG(x1, x2, x3, x4, x5, x6)  =  U17_GAG(x6)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x2, x4, x5)
U4_GGAG(x1, x2, x3, x4, x5)  =  U4_GGAG(x5)
U18_GAG(x1, x2, x3, x4, x5)  =  U18_GAG(x5)
U19_GAG(x1, x2, x3, x4, x5, x6)  =  U19_GAG(x6)
P57_IN_GGAG(x1, x2, x3, x4)  =  P57_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x4, x5)
U10_GGAG(x1, x2, x3, x4, x5)  =  U10_GGAG(x5)
U20_GAG(x1, x2, x3, x4, x5, x6)  =  U20_GAG(x6)
U21_GAG(x1, x2, x3, x4, x5, x6)  =  U21_GAG(x6)
P64_IN_GGAG(x1, x2, x3, x4)  =  P64_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4)  =  U7_GGAG(x4)
U22_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_GAG(x9)
U23_GAG(x1, x2, x3, x4, x5, x6)  =  U23_GAG(x6)
U24_GAG(x1, x2, x3, x4, x5, x6)  =  U24_GAG(x6)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x5)
P71_IN_GGAG(x1, x2, x3, x4)  =  P71_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x2, x4, x5)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x5)
U25_GAG(x1, x2, x3, x4, x5)  =  U25_GAG(x5)
U26_GAG(x1, x2, x3, x4, x5, x6)  =  U26_GAG(x6)
U27_GAG(x1, x2, x3, x4, x5, x6)  =  U27_GAG(x6)
U28_GAG(x1, x2, x3, x4, x5, x6)  =  U28_GAG(x6)
P108_IN_GGAG(x1, x2, x3, x4)  =  P108_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4)  =  U13_GGAG(x4)
U29_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_GAG(x9)
U30_GAG(x1, x2, x3, x4, x5, x6)  =  U30_GAG(x6)
U31_GAG(x1, x2, x3, x4, x5, x6)  =  U31_GAG(x6)
U14_GGAG(x1, x2, x3, x4, x5)  =  U14_GGAG(x5)
U32_GAG(x1, x2, x3, x4, x5)  =  U32_GAG(x5)
U33_GAG(x1, x2, x3, x4, x5, x6)  =  U33_GAG(x6)
U34_GAG(x1, x2, x3, x4, x5, x6)  =  U34_GAG(x6)
U35_GAG(x1, x2, x3, x4, x5)  =  U35_GAG(x5)
U36_GAG(x1, x2, x3, x4, x5, x6)  =  U36_GAG(x6)
U37_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_GAG(x9)
U38_GAG(x1, x2, x3, x4, x5, x6)  =  U38_GAG(x6)
U39_GAG(x1, x2, x3, x4, x5, x6)  =  U39_GAG(x6)
U40_GAG(x1, x2, x3, x4, x5)  =  U40_GAG(x5)
U41_GAG(x1, x2, x3, x4, x5, x6)  =  U41_GAG(x6)
U42_GAG(x1, x2, x3, x4, x5, x6)  =  U42_GAG(x6)
U43_GAG(x1, x2, x3, x4, x5)  =  U43_GAG(x5)
U44_GAG(x1, x2, x3, x4, x5, x6)  =  U44_GAG(x6)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

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

(8) Complex Obligation (AND)

(9) Obligation:

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

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)

The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)
LESS34_IN_GG(x1, x2)  =  LESS34_IN_GG(x1, x2)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)

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

(12) PiDPToQDPProof (EQUIVALENT transformation)

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

(13) Obligation:

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

LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS34_IN_GG(s(T140), s(T141)) → LESS34_IN_GG(T140, T141)
    The graph contains the following edges 1 > 1, 2 > 2

(15) YES

(16) Obligation:

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

DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)

The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)
DELMIN19_IN_AGG(x1, x2, x3)  =  DELMIN19_IN_AGG(x2, x3)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

DELMIN19_IN_AGG(T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T93, T94)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • DELMIN19_IN_AGG(T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T93, T94)
    The graph contains the following edges 1 >= 1, 2 > 2

(22) YES

(23) Obligation:

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

DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, less34_in_gg(T121, T122))
U5_GGAG(T121, T122, T126, T125, less34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_GGAG(T159, T158, T163, T162, less34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U9_GGAG(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_GGAG(T198, T199, T182, T181, less34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
P71_IN_GGAG(T250, T251, T236, T235) → U11_GGAG(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_GGAG(T250, T251, T236, T235, less34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)

The TRS R consists of the following rules:

delete1_in_gag(T6, tree(T6, void, T7), T7) → delete1_out_gag(T6, tree(T6, void, T7), T7)
delete1_in_gag(T10, tree(T10, T11, void), T11) → delete1_out_gag(T10, tree(T10, T11, void), T11)
delete1_in_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)) → delete1_out_gag(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32))
delete1_in_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
delmin19_in_agg(tree(T76, void, T77), T76, T77) → delmin19_out_agg(tree(T76, void, T77), T76, T77)
delmin19_in_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_agg(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
U1_agg(T90, T96, T92, T93, T94, T95, delmin19_out_agg(T96, T93, T94)) → delmin19_out_agg(tree(T90, T96, T92), T93, tree(T90, T94, T95))
U15_gag(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_out_agg(T63, T60, T61)) → delete1_out_gag(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62)))
delete1_in_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → U16_gag(T121, T122, T126, T124, T125, p32_in_ggag(T121, T122, T126, T125))
p32_in_ggag(T121, T122, T126, T125) → U5_ggag(T121, T122, T126, T125, less34_in_gg(T121, T122))
less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → p32_out_ggag(T121, T122, T126, T125)
U5_ggag(T121, T122, T126, T125, less34_out_gg(T121, T122)) → U6_ggag(T121, T122, T126, T125, delete1_in_gag(T121, T126, T125))
delete1_in_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → U17_gag(T158, T159, T160, T163, T162, p44_in_ggag(T159, T158, T163, T162))
p44_in_ggag(T159, T158, T163, T162) → U3_ggag(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → p44_out_ggag(T159, T158, T163, T162)
U3_ggag(T159, T158, T163, T162, less34_out_gg(T159, T158)) → U4_ggag(T159, T158, T163, T162, delete1_in_gag(T158, T163, T162))
delete1_in_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → U18_gag(T187, T182, T180, T181, delete1_in_gag(0, T182, T181))
delete1_in_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → U19_gag(T198, T199, T182, T180, T181, p57_in_ggag(T198, T199, T182, T181))
p57_in_ggag(T198, T199, T182, T181) → U9_ggag(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → p57_out_ggag(T198, T199, T182, T181)
U9_ggag(T198, T199, T182, T181, less34_out_gg(T198, T199)) → U10_ggag(T198, T199, T182, T181, delete1_in_gag(s(T198), T182, T181))
delete1_in_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222)) → U20_gag(T218, T219, T220, T223, T222, p44_in_ggag(T219, T218, T223, T222))
U20_gag(T218, T219, T220, T223, T222, p44_out_ggag(T219, T218, T223, T222)) → delete1_out_gag(T218, tree(T219, T220, T223), tree(T219, T220, T222))
delete1_in_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → U21_gag(T231, T232, T233, T236, T235, p64_in_ggag(T232, T231, T236, T235))
p64_in_ggag(0, s(T241), T236, T235) → U7_ggag(T241, T236, T235, delete1_in_gag(s(T241), T236, T235))
delete1_in_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310))) → U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_in_agg(T311, T308, T309))
U22_gag(T265, T266, T305, T311, T307, T308, T309, T310, delmin19_out_agg(T311, T308, T309)) → delete1_out_gag(T265, tree(T265, T266, tree(T305, T311, T307)), tree(T308, T266, tree(T305, T309, T310)))
delete1_in_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339)) → U23_gag(T336, T337, T341, T339, T340, p32_in_ggag(T336, T337, T341, T340))
U23_gag(T336, T337, T341, T339, T340, p32_out_ggag(T336, T337, T341, T340)) → delete1_out_gag(T336, tree(T337, T341, T339), tree(T337, T340, T339))
delete1_in_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358)) → U24_gag(T354, T355, T356, T359, T358, p64_in_ggag(T355, T354, T359, T358))
p64_in_ggag(s(T250), s(T251), T236, T235) → U8_ggag(T250, T251, T236, T235, p71_in_ggag(T250, T251, T236, T235))
p71_in_ggag(T250, T251, T236, T235) → U11_ggag(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → p71_out_ggag(T250, T251, T236, T235)
U11_ggag(T250, T251, T236, T235, less34_out_gg(T250, T251)) → U12_ggag(T250, T251, T236, T235, delete1_in_gag(s(T251), T236, T235))
delete1_in_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370)) → U25_gag(T377, T372, T370, T371, delete1_in_gag(0, T372, T371))
delete1_in_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370)) → U26_gag(T388, T389, T372, T370, T371, p57_in_ggag(T388, T389, T372, T371))
U26_gag(T388, T389, T372, T370, T371, p57_out_ggag(T388, T389, T372, T371)) → delete1_out_gag(s(T388), tree(s(T389), T372, T370), tree(s(T389), T371, T370))
delete1_in_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406)) → U27_gag(T402, T403, T404, T407, T406, p64_in_ggag(T403, T402, T407, T406))
U27_gag(T402, T403, T404, T407, T406, p64_out_ggag(T403, T402, T407, T406)) → delete1_out_gag(T402, tree(T403, T404, T407), tree(T403, T404, T406))
delete1_in_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → U28_gag(T415, T416, T417, T420, T419, p108_in_ggag(T416, T415, T420, T419))
p108_in_ggag(0, s(T425), T420, T419) → U13_ggag(T425, T420, T419, delete1_in_gag(s(T425), T420, T419))
delete1_in_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492))) → U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_in_agg(T493, T490, T491))
U29_gag(T447, T448, T487, T493, T489, T490, T491, T492, delmin19_out_agg(T493, T490, T491)) → delete1_out_gag(T447, tree(T447, T448, tree(T487, T493, T489)), tree(T490, T448, tree(T487, T491, T492)))
delete1_in_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521)) → U30_gag(T518, T519, T523, T521, T522, p32_in_ggag(T518, T519, T523, T522))
U30_gag(T518, T519, T523, T521, T522, p32_out_ggag(T518, T519, T523, T522)) → delete1_out_gag(T518, tree(T519, T523, T521), tree(T519, T522, T521))
delete1_in_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540)) → U31_gag(T536, T537, T538, T541, T540, p108_in_ggag(T537, T536, T541, T540))
p108_in_ggag(s(T434), s(T435), T420, T419) → U14_ggag(T434, T435, T420, T419, p71_in_ggag(T434, T435, T420, T419))
U14_ggag(T434, T435, T420, T419, p71_out_ggag(T434, T435, T420, T419)) → p108_out_ggag(s(T434), s(T435), T420, T419)
U31_gag(T536, T537, T538, T541, T540, p108_out_ggag(T537, T536, T541, T540)) → delete1_out_gag(T536, tree(T537, T538, T541), tree(T537, T538, T540))
delete1_in_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552)) → U32_gag(T559, T554, T552, T553, delete1_in_gag(0, T554, T553))
delete1_in_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552)) → U33_gag(T570, T571, T554, T552, T553, p57_in_ggag(T570, T571, T554, T553))
U33_gag(T570, T571, T554, T552, T553, p57_out_ggag(T570, T571, T554, T553)) → delete1_out_gag(s(T570), tree(s(T571), T554, T552), tree(s(T571), T553, T552))
delete1_in_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588)) → U34_gag(T584, T585, T586, T589, T588, p108_in_ggag(T585, T584, T589, T588))
U34_gag(T584, T585, T586, T589, T588, p108_out_ggag(T585, T584, T589, T588)) → delete1_out_gag(T584, tree(T585, T586, T589), tree(T585, T586, T588))
delete1_in_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → U35_gag(T607, T599, T602, T601, delete1_in_gag(s(T607), T602, T601))
delete1_in_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → U36_gag(T617, T616, T599, T602, T601, p71_in_ggag(T616, T617, T602, T601))
U36_gag(T617, T616, T599, T602, T601, p71_out_ggag(T616, T617, T602, T601)) → delete1_out_gag(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601))
delete1_in_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670))) → U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_in_agg(T671, T668, T669))
U37_gag(T625, T626, T665, T671, T667, T668, T669, T670, delmin19_out_agg(T671, T668, T669)) → delete1_out_gag(T625, tree(T625, T626, tree(T665, T671, T667)), tree(T668, T626, tree(T665, T669, T670)))
delete1_in_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699)) → U38_gag(T696, T697, T701, T699, T700, p32_in_ggag(T696, T697, T701, T700))
U38_gag(T696, T697, T701, T699, T700, p32_out_ggag(T696, T697, T701, T700)) → delete1_out_gag(T696, tree(T697, T701, T699), tree(T697, T700, T699))
delete1_in_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718)) → U39_gag(T714, T715, T716, T719, T718, p108_in_ggag(T715, T714, T719, T718))
U39_gag(T714, T715, T716, T719, T718, p108_out_ggag(T715, T714, T719, T718)) → delete1_out_gag(T714, tree(T715, T716, T719), tree(T715, T716, T718))
delete1_in_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730)) → U40_gag(T737, T732, T730, T731, delete1_in_gag(0, T732, T731))
delete1_in_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730)) → U41_gag(T748, T749, T732, T730, T731, p57_in_ggag(T748, T749, T732, T731))
U41_gag(T748, T749, T732, T730, T731, p57_out_ggag(T748, T749, T732, T731)) → delete1_out_gag(s(T748), tree(s(T749), T732, T730), tree(s(T749), T731, T730))
delete1_in_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766)) → U42_gag(T762, T763, T764, T767, T766, p108_in_ggag(T763, T762, T767, T766))
U42_gag(T762, T763, T764, T767, T766, p108_out_ggag(T763, T762, T767, T766)) → delete1_out_gag(T762, tree(T763, T764, T767), tree(T763, T764, T766))
delete1_in_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779)) → U43_gag(T785, T777, T780, T779, delete1_in_gag(s(T785), T780, T779))
delete1_in_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779)) → U44_gag(T795, T794, T777, T780, T779, p71_in_ggag(T794, T795, T780, T779))
U44_gag(T795, T794, T777, T780, T779, p71_out_ggag(T794, T795, T780, T779)) → delete1_out_gag(s(T795), tree(s(T794), T777, T780), tree(s(T794), T777, T779))
U43_gag(T785, T777, T780, T779, delete1_out_gag(s(T785), T780, T779)) → delete1_out_gag(s(T785), tree(0, T777, T780), tree(0, T777, T779))
U40_gag(T737, T732, T730, T731, delete1_out_gag(0, T732, T731)) → delete1_out_gag(0, tree(s(T737), T732, T730), tree(s(T737), T731, T730))
U35_gag(T607, T599, T602, T601, delete1_out_gag(s(T607), T602, T601)) → delete1_out_gag(s(T607), tree(0, T599, T602), tree(0, T599, T601))
U32_gag(T559, T554, T552, T553, delete1_out_gag(0, T554, T553)) → delete1_out_gag(0, tree(s(T559), T554, T552), tree(s(T559), T553, T552))
U13_ggag(T425, T420, T419, delete1_out_gag(s(T425), T420, T419)) → p108_out_ggag(0, s(T425), T420, T419)
U28_gag(T415, T416, T417, T420, T419, p108_out_ggag(T416, T415, T420, T419)) → delete1_out_gag(T415, tree(T416, T417, T420), tree(T416, T417, T419))
U25_gag(T377, T372, T370, T371, delete1_out_gag(0, T372, T371)) → delete1_out_gag(0, tree(s(T377), T372, T370), tree(s(T377), T371, T370))
U12_ggag(T250, T251, T236, T235, delete1_out_gag(s(T251), T236, T235)) → p71_out_ggag(T250, T251, T236, T235)
U8_ggag(T250, T251, T236, T235, p71_out_ggag(T250, T251, T236, T235)) → p64_out_ggag(s(T250), s(T251), T236, T235)
U24_gag(T354, T355, T356, T359, T358, p64_out_ggag(T355, T354, T359, T358)) → delete1_out_gag(T354, tree(T355, T356, T359), tree(T355, T356, T358))
U7_ggag(T241, T236, T235, delete1_out_gag(s(T241), T236, T235)) → p64_out_ggag(0, s(T241), T236, T235)
U21_gag(T231, T232, T233, T236, T235, p64_out_ggag(T232, T231, T236, T235)) → delete1_out_gag(T231, tree(T232, T233, T236), tree(T232, T233, T235))
U10_ggag(T198, T199, T182, T181, delete1_out_gag(s(T198), T182, T181)) → p57_out_ggag(T198, T199, T182, T181)
U19_gag(T198, T199, T182, T180, T181, p57_out_ggag(T198, T199, T182, T181)) → delete1_out_gag(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180))
U18_gag(T187, T182, T180, T181, delete1_out_gag(0, T182, T181)) → delete1_out_gag(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180))
U4_ggag(T159, T158, T163, T162, delete1_out_gag(T158, T163, T162)) → p44_out_ggag(T159, T158, T163, T162)
U17_gag(T158, T159, T160, T163, T162, p44_out_ggag(T159, T158, T163, T162)) → delete1_out_gag(T158, tree(T159, T160, T163), tree(T159, T160, T162))
U6_ggag(T121, T122, T126, T125, delete1_out_gag(T121, T126, T125)) → p32_out_ggag(T121, T122, T126, T125)
U16_gag(T121, T122, T126, T124, T125, p32_out_ggag(T121, T122, T126, T125)) → delete1_out_gag(T121, tree(T122, T126, T124), tree(T122, T125, T124))

The argument filtering Pi contains the following mapping:
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
delete1_out_gag(x1, x2, x3)  =  delete1_out_gag
tree(x1, x2, x3)  =  tree(x1, x2, x3)
U15_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U15_gag(x9)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
delmin19_out_agg(x1, x2, x3)  =  delmin19_out_agg
U1_agg(x1, x2, x3, x4, x5, x6, x7)  =  U1_agg(x7)
U16_gag(x1, x2, x3, x4, x5, x6)  =  U16_gag(x6)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
U5_ggag(x1, x2, x3, x4, x5)  =  U5_ggag(x1, x4, x5)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
p32_out_ggag(x1, x2, x3, x4)  =  p32_out_ggag
U6_ggag(x1, x2, x3, x4, x5)  =  U6_ggag(x5)
U17_gag(x1, x2, x3, x4, x5, x6)  =  U17_gag(x6)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
U3_ggag(x1, x2, x3, x4, x5)  =  U3_ggag(x2, x4, x5)
p44_out_ggag(x1, x2, x3, x4)  =  p44_out_ggag
U4_ggag(x1, x2, x3, x4, x5)  =  U4_ggag(x5)
U18_gag(x1, x2, x3, x4, x5)  =  U18_gag(x5)
U19_gag(x1, x2, x3, x4, x5, x6)  =  U19_gag(x6)
p57_in_ggag(x1, x2, x3, x4)  =  p57_in_ggag(x1, x2, x4)
U9_ggag(x1, x2, x3, x4, x5)  =  U9_ggag(x1, x4, x5)
p57_out_ggag(x1, x2, x3, x4)  =  p57_out_ggag
U10_ggag(x1, x2, x3, x4, x5)  =  U10_ggag(x5)
U20_gag(x1, x2, x3, x4, x5, x6)  =  U20_gag(x6)
U21_gag(x1, x2, x3, x4, x5, x6)  =  U21_gag(x6)
p64_in_ggag(x1, x2, x3, x4)  =  p64_in_ggag(x1, x2, x4)
U7_ggag(x1, x2, x3, x4)  =  U7_ggag(x4)
U22_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U22_gag(x9)
U23_gag(x1, x2, x3, x4, x5, x6)  =  U23_gag(x6)
U24_gag(x1, x2, x3, x4, x5, x6)  =  U24_gag(x6)
U8_ggag(x1, x2, x3, x4, x5)  =  U8_ggag(x5)
p71_in_ggag(x1, x2, x3, x4)  =  p71_in_ggag(x1, x2, x4)
U11_ggag(x1, x2, x3, x4, x5)  =  U11_ggag(x2, x4, x5)
p71_out_ggag(x1, x2, x3, x4)  =  p71_out_ggag
U12_ggag(x1, x2, x3, x4, x5)  =  U12_ggag(x5)
U25_gag(x1, x2, x3, x4, x5)  =  U25_gag(x5)
U26_gag(x1, x2, x3, x4, x5, x6)  =  U26_gag(x6)
U27_gag(x1, x2, x3, x4, x5, x6)  =  U27_gag(x6)
p64_out_ggag(x1, x2, x3, x4)  =  p64_out_ggag
U28_gag(x1, x2, x3, x4, x5, x6)  =  U28_gag(x6)
p108_in_ggag(x1, x2, x3, x4)  =  p108_in_ggag(x1, x2, x4)
U13_ggag(x1, x2, x3, x4)  =  U13_ggag(x4)
U29_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U29_gag(x9)
U30_gag(x1, x2, x3, x4, x5, x6)  =  U30_gag(x6)
U31_gag(x1, x2, x3, x4, x5, x6)  =  U31_gag(x6)
U14_ggag(x1, x2, x3, x4, x5)  =  U14_ggag(x5)
p108_out_ggag(x1, x2, x3, x4)  =  p108_out_ggag
U32_gag(x1, x2, x3, x4, x5)  =  U32_gag(x5)
U33_gag(x1, x2, x3, x4, x5, x6)  =  U33_gag(x6)
U34_gag(x1, x2, x3, x4, x5, x6)  =  U34_gag(x6)
U35_gag(x1, x2, x3, x4, x5)  =  U35_gag(x5)
U36_gag(x1, x2, x3, x4, x5, x6)  =  U36_gag(x6)
U37_gag(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U37_gag(x9)
U38_gag(x1, x2, x3, x4, x5, x6)  =  U38_gag(x6)
U39_gag(x1, x2, x3, x4, x5, x6)  =  U39_gag(x6)
U40_gag(x1, x2, x3, x4, x5)  =  U40_gag(x5)
U41_gag(x1, x2, x3, x4, x5, x6)  =  U41_gag(x6)
U42_gag(x1, x2, x3, x4, x5, x6)  =  U42_gag(x6)
U43_gag(x1, x2, x3, x4, x5)  =  U43_gag(x5)
U44_gag(x1, x2, x3, x4, x5, x6)  =  U44_gag(x6)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x2, x4, x5)
P57_IN_GGAG(x1, x2, x3, x4)  =  P57_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x4, x5)
P64_IN_GGAG(x1, x2, x3, x4)  =  P64_IN_GGAG(x1, x2, x4)
P71_IN_GGAG(x1, x2, x3, x4)  =  P71_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x2, x4, x5)
P108_IN_GGAG(x1, x2, x3, x4)  =  P108_IN_GGAG(x1, x2, x4)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

DELETE1_IN_GAG(T121, tree(T122, T126, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T126, T125)
P32_IN_GGAG(T121, T122, T126, T125) → U5_GGAG(T121, T122, T126, T125, less34_in_gg(T121, T122))
U5_GGAG(T121, T122, T126, T125, less34_out_gg(T121, T122)) → DELETE1_IN_GAG(T121, T126, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T163), tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T163, T162)
P44_IN_GGAG(T159, T158, T163, T162) → U3_GGAG(T159, T158, T163, T162, less34_in_gg(T159, T158))
U3_GGAG(T159, T158, T163, T162, less34_out_gg(T159, T158)) → DELETE1_IN_GAG(T158, T163, T162)
DELETE1_IN_GAG(0, tree(s(T187), T182, T180), tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T182, T181)
DELETE1_IN_GAG(T231, tree(T232, T233, T236), tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T236, T235)
P64_IN_GGAG(0, s(T241), T236, T235) → DELETE1_IN_GAG(s(T241), T236, T235)
DELETE1_IN_GAG(s(T198), tree(s(T199), T182, T180), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T182, T181)
P57_IN_GGAG(T198, T199, T182, T181) → U9_GGAG(T198, T199, T182, T181, less34_in_gg(T198, T199))
U9_GGAG(T198, T199, T182, T181, less34_out_gg(T198, T199)) → DELETE1_IN_GAG(s(T198), T182, T181)
DELETE1_IN_GAG(T415, tree(T416, T417, T420), tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T420, T419)
P108_IN_GGAG(0, s(T425), T420, T419) → DELETE1_IN_GAG(s(T425), T420, T419)
DELETE1_IN_GAG(s(T607), tree(0, T599, T602), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T602, T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T602), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T602, T601)
P71_IN_GGAG(T250, T251, T236, T235) → U11_GGAG(T250, T251, T236, T235, less34_in_gg(T250, T251))
U11_GGAG(T250, T251, T236, T235, less34_out_gg(T250, T251)) → DELETE1_IN_GAG(s(T251), T236, T235)
P108_IN_GGAG(s(T434), s(T435), T420, T419) → P71_IN_GGAG(T434, T435, T420, T419)
P64_IN_GGAG(s(T250), s(T251), T236, T235) → P71_IN_GGAG(T250, T251, T236, T235)

The TRS R consists of the following rules:

less34_in_gg(0, s(T135)) → less34_out_gg(0, s(T135))
less34_in_gg(s(T140), s(T141)) → U2_gg(T140, T141, less34_in_gg(T140, T141))
U2_gg(T140, T141, less34_out_gg(T140, T141)) → less34_out_gg(s(T140), s(T141))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
0  =  0
s(x1)  =  s(x1)
less34_out_gg(x1, x2)  =  less34_out_gg
U2_gg(x1, x2, x3)  =  U2_gg(x3)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U3_GGAG(x1, x2, x3, x4, x5)  =  U3_GGAG(x2, x4, x5)
P57_IN_GGAG(x1, x2, x3, x4)  =  P57_IN_GGAG(x1, x2, x4)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x4, x5)
P64_IN_GGAG(x1, x2, x3, x4)  =  P64_IN_GGAG(x1, x2, x4)
P71_IN_GGAG(x1, x2, x3, x4)  =  P71_IN_GGAG(x1, x2, x4)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x2, x4, x5)
P108_IN_GGAG(x1, x2, x3, x4)  =  P108_IN_GGAG(x1, x2, x4)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

DELETE1_IN_GAG(T121, tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T125)
P32_IN_GGAG(T121, T122, T125) → U5_GGAG(T121, T125, less34_in_gg(T121, T122))
U5_GGAG(T121, T125, less34_out_gg) → DELETE1_IN_GAG(T121, T125)
DELETE1_IN_GAG(T158, tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T162)
P44_IN_GGAG(T159, T158, T162) → U3_GGAG(T158, T162, less34_in_gg(T159, T158))
U3_GGAG(T158, T162, less34_out_gg) → DELETE1_IN_GAG(T158, T162)
DELETE1_IN_GAG(0, tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T181)
DELETE1_IN_GAG(T231, tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T235)
P64_IN_GGAG(0, s(T241), T235) → DELETE1_IN_GAG(s(T241), T235)
DELETE1_IN_GAG(s(T198), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T181)
P57_IN_GGAG(T198, T199, T181) → U9_GGAG(T198, T181, less34_in_gg(T198, T199))
U9_GGAG(T198, T181, less34_out_gg) → DELETE1_IN_GAG(s(T198), T181)
DELETE1_IN_GAG(T415, tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T419)
P108_IN_GGAG(0, s(T425), T419) → DELETE1_IN_GAG(s(T425), T419)
DELETE1_IN_GAG(s(T607), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T601)
DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T601)
P71_IN_GGAG(T250, T251, T235) → U11_GGAG(T251, T235, less34_in_gg(T250, T251))
U11_GGAG(T251, T235, less34_out_gg) → DELETE1_IN_GAG(s(T251), T235)
P108_IN_GGAG(s(T434), s(T435), T419) → P71_IN_GGAG(T434, T435, T419)
P64_IN_GGAG(s(T250), s(T251), T235) → P71_IN_GGAG(T250, T251, T235)

The TRS R consists of the following rules:

less34_in_gg(0, s(T135)) → less34_out_gg
less34_in_gg(s(T140), s(T141)) → U2_gg(less34_in_gg(T140, T141))
U2_gg(less34_out_gg) → less34_out_gg

The set Q consists of the following terms:

less34_in_gg(x0, x1)
U2_gg(x0)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • P32_IN_GGAG(T121, T122, T125) → U5_GGAG(T121, T125, less34_in_gg(T121, T122))
    The graph contains the following edges 1 >= 1, 3 >= 2

  • U5_GGAG(T121, T125, less34_out_gg) → DELETE1_IN_GAG(T121, T125)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GAG(T121, tree(T122, T125, T124)) → P32_IN_GGAG(T121, T122, T125)
    The graph contains the following edges 1 >= 1, 2 > 2, 2 > 3

  • P44_IN_GGAG(T159, T158, T162) → U3_GGAG(T158, T162, less34_in_gg(T159, T158))
    The graph contains the following edges 2 >= 1, 3 >= 2

  • U3_GGAG(T158, T162, less34_out_gg) → DELETE1_IN_GAG(T158, T162)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GAG(T158, tree(T159, T160, T162)) → P44_IN_GGAG(T159, T158, T162)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • DELETE1_IN_GAG(0, tree(s(T187), T181, T180)) → DELETE1_IN_GAG(0, T181)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETE1_IN_GAG(s(T607), tree(0, T599, T601)) → DELETE1_IN_GAG(s(T607), T601)
    The graph contains the following edges 1 >= 1, 2 > 2

  • P64_IN_GGAG(0, s(T241), T235) → DELETE1_IN_GAG(s(T241), T235)
    The graph contains the following edges 2 >= 1, 3 >= 2

  • P64_IN_GGAG(s(T250), s(T251), T235) → P71_IN_GGAG(T250, T251, T235)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • DELETE1_IN_GAG(T231, tree(T232, T233, T235)) → P64_IN_GGAG(T232, T231, T235)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • DELETE1_IN_GAG(T415, tree(T416, T417, T419)) → P108_IN_GGAG(T416, T415, T419)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • P57_IN_GGAG(T198, T199, T181) → U9_GGAG(T198, T181, less34_in_gg(T198, T199))
    The graph contains the following edges 1 >= 1, 3 >= 2

  • U9_GGAG(T198, T181, less34_out_gg) → DELETE1_IN_GAG(s(T198), T181)
    The graph contains the following edges 2 >= 2

  • DELETE1_IN_GAG(s(T198), tree(s(T199), T181, T180)) → P57_IN_GGAG(T198, T199, T181)
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • DELETE1_IN_GAG(s(T617), tree(s(T616), T599, T601)) → P71_IN_GGAG(T616, T617, T601)
    The graph contains the following edges 2 > 1, 1 > 2, 2 > 3

  • P108_IN_GGAG(0, s(T425), T419) → DELETE1_IN_GAG(s(T425), T419)
    The graph contains the following edges 2 >= 1, 3 >= 2

  • U11_GGAG(T251, T235, less34_out_gg) → DELETE1_IN_GAG(s(T251), T235)
    The graph contains the following edges 2 >= 2

  • P108_IN_GGAG(s(T434), s(T435), T419) → P71_IN_GGAG(T434, T435, T419)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • P71_IN_GGAG(T250, T251, T235) → U11_GGAG(T251, T235, less34_in_gg(T250, T251))
    The graph contains the following edges 2 >= 1, 3 >= 2

(29) YES