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

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

less19(s(T33)) :- less19(T33).
p17(T26, T28) :- less19(T26).
p17(T26, T28) :- ','(less19(T26), delete1(T26, void, T28)).
p33(T59, T54) :- less19(T59).
p33(T59, T54) :- ','(less19(T59), delete1(s(T59), void, T54)).
delmin56(tree(T150, void, T151), T150, T151).
delmin56(tree(T164, T165, T166), T170, tree(T164, T171, T169)) :- delmin56(T165, T170, T171).
p40(s(T84), T81) :- p33(T84, T81).
p71(T199, T200, T202) :- less19(T199).
p71(T199, T200, T202) :- ','(less19(T199), delete1(T199, T200, T202)).
less222(0, s(T571)).
less222(s(T576), s(T577)) :- less222(T576, T577).
less164(0, s(T476)).
less164(s(0), s(s(T489))).
less164(s(s(0)), s(s(s(T502)))).
less164(s(s(s(0))), s(s(s(s(T515))))).
less164(s(s(s(s(0)))), s(s(s(s(s(T528)))))).
less164(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))).
less164(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))).
less164(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) :- less222(T559, T560).
delete1(T6, tree(T6, void, T7), T7).
delete1(T9, tree(T9, void, void), void).
delete1(T26, tree(T26, void, void), tree(T26, T28, void)) :- p17(T26, T28).
delete1(T46, tree(T46, void, void), tree(T46, void, T48)) :- p17(T46, T48).
delete1(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) :- p33(T59, T54).
delete1(T73, tree(T73, void, void), tree(T73, void, T75)) :- p17(T73, T75).
delete1(T79, tree(T79, void, void), tree(T79, void, T81)) :- p40(T79, T81).
delete1(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)).
delete1(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) :- delmin56(T131, T136, T137).
delete1(T188, tree(T188, void, T189), tree(T188, T191, T189)) :- p40(T188, T191).
delete1(T199, tree(T199, void, T200), tree(T199, void, T202)) :- p71(T199, T200, T202).
delete1(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) :- p33(T220, T215).
delete1(T228, tree(T228, void, T229), tree(T228, void, T231)) :- p71(T228, T229, T231).
delete1(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) :- less19(T242).
delete1(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) :- ','(less19(T242), delete1(s(T242), T237, T239)).
delete1(T251, tree(T251, T252, void), T252).
delete1(T275, tree(T275, T276, void), tree(T275, T278, void)) :- less19(T275).
delete1(T275, tree(T275, T276, void), tree(T275, T278, void)) :- ','(less19(T275), delete1(T275, T276, T278)).
delete1(T291, tree(T291, T292, void), tree(T291, T292, T294)) :- p40(T291, T294).
delete1(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) :- less19(T307).
delete1(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) :- ','(less19(T307), delete1(s(T307), T300, T302)).
delete1(T320, tree(T320, T321, void), tree(T320, T321, T323)) :- p40(T320, T323).
delete1(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) :- p33(T334, T331).
delete1(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)).
delete1(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) :- delmin56(T383, T388, T389).
delete1(T410, tree(T410, T411, T412), tree(T410, T414, T412)) :- less19(T410).
delete1(T410, tree(T410, T411, T412), tree(T410, T414, T412)) :- ','(less19(T410), delete1(T410, T411, T414)).
delete1(T429, tree(T429, T430, T431), tree(T429, T430, T433)) :- less19(T429).
delete1(T429, tree(T429, T430, T431), tree(T429, T430, T433)) :- ','(less19(T429), delete1(T429, T431, T433)).
delete1(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) :- delete1(0, T447, T450).
delete1(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) :- less164(T466, T467).
delete1(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) :- ','(less164(T466, T467), delete1(s(T466), T447, T450)).
delete1(T594, tree(T595, T596, T597), tree(T595, T596, T599)) :- less222(T595, T594).
delete1(T594, tree(T595, T596, T597), tree(T595, T596, T599)) :- ','(less222(T595, T594), delete1(T594, T597, T599)).
delete1(s(T623), tree(0, T615, T616), tree(0, T615, T618)) :- delete1(s(T623), T616, T618).
delete1(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) :- less222(T632, T633).
delete1(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) :- ','(less222(T632, T633), delete1(s(T633), T616, T618)).

Queries:

delete1(g,g,a).

(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,b,f)
p17_in: (b,f)
less19_in: (b)
p33_in: (b,f)
p40_in: (b,f)
delmin56_in: (b,f,f)
p71_in: (b,b,f)
less164_in: (b,b)
less222_in: (b,b)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(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_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(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_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_GGA(T26, T28, p17_in_ga(T26, T28))
DELETE1_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → P17_IN_GA(T26, T28)
P17_IN_GA(T26, T28) → U2_GA(T26, T28, less19_in_g(T26))
P17_IN_GA(T26, T28) → LESS19_IN_G(T26)
LESS19_IN_G(s(T33)) → U1_G(T33, less19_in_g(T33))
LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)
U2_GA(T26, T28, less19_out_g(T26)) → U3_GA(T26, T28, delete1_in_gga(T26, void, T28))
U2_GA(T26, T28, less19_out_g(T26)) → DELETE1_IN_GGA(T26, void, T28)
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_GGA(T46, T48, p17_in_ga(T46, T48))
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → P17_IN_GA(T46, T48)
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_GGA(T59, T54, p33_in_ga(T59, T54))
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → P33_IN_GA(T59, T54)
P33_IN_GA(T59, T54) → U4_GA(T59, T54, less19_in_g(T59))
P33_IN_GA(T59, T54) → LESS19_IN_G(T59)
U4_GA(T59, T54, less19_out_g(T59)) → U5_GA(T59, T54, delete1_in_gga(s(T59), void, T54))
U4_GA(T59, T54, less19_out_g(T59)) → DELETE1_IN_GGA(s(T59), void, T54)
DELETE1_IN_GGA(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_GGA(T73, T75, p17_in_ga(T73, T75))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_GGA(T79, T81, p40_in_ga(T79, T81))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → P40_IN_GA(T79, T81)
P40_IN_GA(s(T84), T81) → U7_GA(T84, T81, p33_in_ga(T84, T81))
P40_IN_GA(s(T84), T81) → P33_IN_GA(T84, T81)
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_GGA(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → DELMIN56_IN_GAA(T131, T136, T137)
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_GAA(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_GGA(T188, T189, T191, p40_in_ga(T188, T191))
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → P40_IN_GA(T188, T191)
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_GGA(T199, T200, T202, p71_in_gga(T199, T200, T202))
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U8_GGA(T199, T200, T202, less19_in_g(T199))
P71_IN_GGA(T199, T200, T202) → LESS19_IN_G(T199)
U8_GGA(T199, T200, T202, less19_out_g(T199)) → U9_GGA(T199, T200, T202, delete1_in_gga(T199, T200, T202))
U8_GGA(T199, T200, T202, less19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_GGA(T220, T213, T215, p33_in_ga(T220, T215))
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → P33_IN_GA(T220, T215)
DELETE1_IN_GGA(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_GGA(T228, T229, T231, p71_in_gga(T228, T229, T231))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_GGA(T242, T237, T239, less19_in_g(T242))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → LESS19_IN_G(T242)
U22_GGA(T242, T237, T239, less19_out_g(T242)) → U23_GGA(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
U22_GGA(T242, T237, T239, less19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_GGA(T275, T276, T278, less19_in_g(T275))
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → LESS19_IN_G(T275)
U24_GGA(T275, T276, T278, less19_out_g(T275)) → U25_GGA(T275, T276, T278, delete1_in_gga(T275, T276, T278))
U24_GGA(T275, T276, T278, less19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_GGA(T291, T292, T294, p40_in_ga(T291, T294))
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → P40_IN_GA(T291, T294)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_GGA(T307, T300, T302, less19_in_g(T307))
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → LESS19_IN_G(T307)
U27_GGA(T307, T300, T302, less19_out_g(T307)) → U28_GGA(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
U27_GGA(T307, T300, T302, less19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_GGA(T320, T321, T323, p40_in_ga(T320, T323))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_GGA(T334, T329, T331, p33_in_ga(T334, T331))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → P33_IN_GA(T334, T331)
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_GGA(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → DELMIN56_IN_GAA(T383, T388, T389)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_GGA(T410, T411, T412, T414, less19_in_g(T410))
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → LESS19_IN_G(T410)
U32_GGA(T410, T411, T412, T414, less19_out_g(T410)) → U33_GGA(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
U32_GGA(T410, T411, T412, T414, less19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_GGA(T429, T430, T431, T433, less19_in_g(T429))
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → LESS19_IN_G(T429)
U34_GGA(T429, T430, T431, T433, less19_out_g(T429)) → U35_GGA(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
U34_GGA(T429, T430, T431, T433, less19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_GGA(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_GGA(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → LESS164_IN_GG(T466, T467)
LESS164_IN_GG(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_GG(T559, T560, less222_in_gg(T559, T560))
LESS164_IN_GG(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → LESS222_IN_GG(T559, T560)
LESS222_IN_GG(s(T576), s(T577)) → U10_GG(T576, T577, less222_in_gg(T576, T577))
LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)
U37_GGA(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_GGA(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
U37_GGA(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_GGA(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → LESS222_IN_GG(T595, T594)
U39_GGA(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_GGA(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
U39_GGA(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_GGA(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_GGA(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → LESS222_IN_GG(T632, T633)
U42_GGA(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_GGA(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U42_GGA(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x6)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
P17_IN_GA(x1, x2)  =  P17_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
LESS19_IN_G(x1)  =  LESS19_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x2)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
P33_IN_GA(x1, x2)  =  P33_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x3)
P40_IN_GA(x1, x2)  =  P40_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U17_GGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_GGA(x8)
DELMIN56_IN_GAA(x1, x2, x3)  =  DELMIN56_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x7)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x4)
P71_IN_GGA(x1, x2, x3)  =  P71_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x4)
U31_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_GGA(x9)
U32_GGA(x1, x2, x3, x4, x5)  =  U32_GGA(x1, x2, x5)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x3, x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x5)
U36_GGA(x1, x2, x3, x4, x5)  =  U36_GGA(x5)
U37_GGA(x1, x2, x3, x4, x5, x6)  =  U37_GGA(x1, x3, x6)
LESS164_IN_GG(x1, x2)  =  LESS164_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x3)
LESS222_IN_GG(x1, x2)  =  LESS222_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U38_GGA(x1, x2, x3, x4, x5, x6)  =  U38_GGA(x6)
U39_GGA(x1, x2, x3, x4, x5, x6)  =  U39_GGA(x1, x4, x6)
U40_GGA(x1, x2, x3, x4, x5, x6)  =  U40_GGA(x6)
U41_GGA(x1, x2, x3, x4, x5)  =  U41_GGA(x5)
U42_GGA(x1, x2, x3, x4, x5, x6)  =  U42_GGA(x1, x4, x6)
U43_GGA(x1, x2, x3, x4, x5, x6)  =  U43_GGA(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_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_GGA(T26, T28, p17_in_ga(T26, T28))
DELETE1_IN_GGA(T26, tree(T26, void, void), tree(T26, T28, void)) → P17_IN_GA(T26, T28)
P17_IN_GA(T26, T28) → U2_GA(T26, T28, less19_in_g(T26))
P17_IN_GA(T26, T28) → LESS19_IN_G(T26)
LESS19_IN_G(s(T33)) → U1_G(T33, less19_in_g(T33))
LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)
U2_GA(T26, T28, less19_out_g(T26)) → U3_GA(T26, T28, delete1_in_gga(T26, void, T28))
U2_GA(T26, T28, less19_out_g(T26)) → DELETE1_IN_GGA(T26, void, T28)
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_GGA(T46, T48, p17_in_ga(T46, T48))
DELETE1_IN_GGA(T46, tree(T46, void, void), tree(T46, void, T48)) → P17_IN_GA(T46, T48)
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_GGA(T59, T54, p33_in_ga(T59, T54))
DELETE1_IN_GGA(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → P33_IN_GA(T59, T54)
P33_IN_GA(T59, T54) → U4_GA(T59, T54, less19_in_g(T59))
P33_IN_GA(T59, T54) → LESS19_IN_G(T59)
U4_GA(T59, T54, less19_out_g(T59)) → U5_GA(T59, T54, delete1_in_gga(s(T59), void, T54))
U4_GA(T59, T54, less19_out_g(T59)) → DELETE1_IN_GGA(s(T59), void, T54)
DELETE1_IN_GGA(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_GGA(T73, T75, p17_in_ga(T73, T75))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_GGA(T79, T81, p40_in_ga(T79, T81))
DELETE1_IN_GGA(T79, tree(T79, void, void), tree(T79, void, T81)) → P40_IN_GA(T79, T81)
P40_IN_GA(s(T84), T81) → U7_GA(T84, T81, p33_in_ga(T84, T81))
P40_IN_GA(s(T84), T81) → P33_IN_GA(T84, T81)
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_GGA(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
DELETE1_IN_GGA(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → DELMIN56_IN_GAA(T131, T136, T137)
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_GAA(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_GGA(T188, T189, T191, p40_in_ga(T188, T191))
DELETE1_IN_GGA(T188, tree(T188, void, T189), tree(T188, T191, T189)) → P40_IN_GA(T188, T191)
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_GGA(T199, T200, T202, p71_in_gga(T199, T200, T202))
DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U8_GGA(T199, T200, T202, less19_in_g(T199))
P71_IN_GGA(T199, T200, T202) → LESS19_IN_G(T199)
U8_GGA(T199, T200, T202, less19_out_g(T199)) → U9_GGA(T199, T200, T202, delete1_in_gga(T199, T200, T202))
U8_GGA(T199, T200, T202, less19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_GGA(T220, T213, T215, p33_in_ga(T220, T215))
DELETE1_IN_GGA(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → P33_IN_GA(T220, T215)
DELETE1_IN_GGA(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_GGA(T228, T229, T231, p71_in_gga(T228, T229, T231))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_GGA(T242, T237, T239, less19_in_g(T242))
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → LESS19_IN_G(T242)
U22_GGA(T242, T237, T239, less19_out_g(T242)) → U23_GGA(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
U22_GGA(T242, T237, T239, less19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_GGA(T275, T276, T278, less19_in_g(T275))
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → LESS19_IN_G(T275)
U24_GGA(T275, T276, T278, less19_out_g(T275)) → U25_GGA(T275, T276, T278, delete1_in_gga(T275, T276, T278))
U24_GGA(T275, T276, T278, less19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_GGA(T291, T292, T294, p40_in_ga(T291, T294))
DELETE1_IN_GGA(T291, tree(T291, T292, void), tree(T291, T292, T294)) → P40_IN_GA(T291, T294)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_GGA(T307, T300, T302, less19_in_g(T307))
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → LESS19_IN_G(T307)
U27_GGA(T307, T300, T302, less19_out_g(T307)) → U28_GGA(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
U27_GGA(T307, T300, T302, less19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_GGA(T320, T321, T323, p40_in_ga(T320, T323))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_GGA(T334, T329, T331, p33_in_ga(T334, T331))
DELETE1_IN_GGA(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → P33_IN_GA(T334, T331)
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_GGA(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
DELETE1_IN_GGA(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → DELMIN56_IN_GAA(T383, T388, T389)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_GGA(T410, T411, T412, T414, less19_in_g(T410))
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → LESS19_IN_G(T410)
U32_GGA(T410, T411, T412, T414, less19_out_g(T410)) → U33_GGA(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
U32_GGA(T410, T411, T412, T414, less19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_GGA(T429, T430, T431, T433, less19_in_g(T429))
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → LESS19_IN_G(T429)
U34_GGA(T429, T430, T431, T433, less19_out_g(T429)) → U35_GGA(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
U34_GGA(T429, T430, T431, T433, less19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_GGA(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_GGA(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → LESS164_IN_GG(T466, T467)
LESS164_IN_GG(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_GG(T559, T560, less222_in_gg(T559, T560))
LESS164_IN_GG(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → LESS222_IN_GG(T559, T560)
LESS222_IN_GG(s(T576), s(T577)) → U10_GG(T576, T577, less222_in_gg(T576, T577))
LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)
U37_GGA(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_GGA(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
U37_GGA(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_GGA(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → LESS222_IN_GG(T595, T594)
U39_GGA(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_GGA(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
U39_GGA(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_GGA(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_GGA(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → LESS222_IN_GG(T632, T633)
U42_GGA(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_GGA(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U42_GGA(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x6)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
U12_GGA(x1, x2, x3)  =  U12_GGA(x3)
P17_IN_GA(x1, x2)  =  P17_IN_GA(x1)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
LESS19_IN_G(x1)  =  LESS19_IN_G(x1)
U1_G(x1, x2)  =  U1_G(x2)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U13_GGA(x1, x2, x3)  =  U13_GGA(x3)
U14_GGA(x1, x2, x3)  =  U14_GGA(x3)
P33_IN_GA(x1, x2)  =  P33_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U15_GGA(x1, x2, x3)  =  U15_GGA(x3)
U16_GGA(x1, x2, x3)  =  U16_GGA(x3)
P40_IN_GA(x1, x2)  =  P40_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x3)
U17_GGA(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_GGA(x8)
DELMIN56_IN_GAA(x1, x2, x3)  =  DELMIN56_IN_GAA(x1)
U6_GAA(x1, x2, x3, x4, x5, x6, x7)  =  U6_GAA(x7)
U18_GGA(x1, x2, x3, x4)  =  U18_GGA(x4)
U19_GGA(x1, x2, x3, x4)  =  U19_GGA(x4)
P71_IN_GGA(x1, x2, x3)  =  P71_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U9_GGA(x1, x2, x3, x4)  =  U9_GGA(x4)
U20_GGA(x1, x2, x3, x4)  =  U20_GGA(x4)
U21_GGA(x1, x2, x3, x4)  =  U21_GGA(x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U23_GGA(x1, x2, x3, x4)  =  U23_GGA(x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U25_GGA(x1, x2, x3, x4)  =  U25_GGA(x4)
U26_GGA(x1, x2, x3, x4)  =  U26_GGA(x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U28_GGA(x1, x2, x3, x4)  =  U28_GGA(x4)
U29_GGA(x1, x2, x3, x4)  =  U29_GGA(x4)
U30_GGA(x1, x2, x3, x4)  =  U30_GGA(x4)
U31_GGA(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_GGA(x9)
U32_GGA(x1, x2, x3, x4, x5)  =  U32_GGA(x1, x2, x5)
U33_GGA(x1, x2, x3, x4, x5)  =  U33_GGA(x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x3, x5)
U35_GGA(x1, x2, x3, x4, x5)  =  U35_GGA(x5)
U36_GGA(x1, x2, x3, x4, x5)  =  U36_GGA(x5)
U37_GGA(x1, x2, x3, x4, x5, x6)  =  U37_GGA(x1, x3, x6)
LESS164_IN_GG(x1, x2)  =  LESS164_IN_GG(x1, x2)
U11_GG(x1, x2, x3)  =  U11_GG(x3)
LESS222_IN_GG(x1, x2)  =  LESS222_IN_GG(x1, x2)
U10_GG(x1, x2, x3)  =  U10_GG(x3)
U38_GGA(x1, x2, x3, x4, x5, x6)  =  U38_GGA(x6)
U39_GGA(x1, x2, x3, x4, x5, x6)  =  U39_GGA(x1, x4, x6)
U40_GGA(x1, x2, x3, x4, x5, x6)  =  U40_GGA(x6)
U41_GGA(x1, x2, x3, x4, x5)  =  U41_GGA(x5)
U42_GGA(x1, x2, x3, x4, x5, x6)  =  U42_GGA(x1, x4, x6)
U43_GGA(x1, x2, x3, x4, x5, x6)  =  U43_GGA(x6)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 4 SCCs with 59 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)

The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x6)
LESS222_IN_GG(x1, x2)  =  LESS222_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:

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)

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:

LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)

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:

  • LESS222_IN_GG(s(T576), s(T577)) → LESS222_IN_GG(T576, T577)
    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:

DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)

The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x6)
DELMIN56_IN_GAA(x1, x2, x3)  =  DELMIN56_IN_GAA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

DELMIN56_IN_GAA(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → DELMIN56_IN_GAA(T165, T170, T171)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

DELMIN56_IN_GAA(tree(T164, T165, T166)) → DELMIN56_IN_GAA(T165)

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:

  • DELMIN56_IN_GAA(tree(T164, T165, T166)) → DELMIN56_IN_GAA(T165)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)

The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x6)
LESS19_IN_G(x1)  =  LESS19_IN_G(x1)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)

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

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

LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS19_IN_G(s(T33)) → LESS19_IN_G(T33)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

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

DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U8_GGA(T199, T200, T202, less19_in_g(T199))
U8_GGA(T199, T200, T202, less19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_GGA(T242, T237, T239, less19_in_g(T242))
U22_GGA(T242, T237, T239, less19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_GGA(T275, T276, T278, less19_in_g(T275))
U24_GGA(T275, T276, T278, less19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_GGA(T307, T300, T302, less19_in_g(T307))
U27_GGA(T307, T300, T302, less19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_GGA(T410, T411, T412, T414, less19_in_g(T410))
U32_GGA(T410, T411, T412, T414, less19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_GGA(T429, T430, T431, T433, less19_in_g(T429))
U34_GGA(T429, T430, T431, T433, less19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_GGA(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_GGA(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_GGA(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
U37_GGA(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_GGA(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_GGA(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

delete1_in_gga(T6, tree(T6, void, T7), T7) → delete1_out_gga(T6, tree(T6, void, T7), T7)
delete1_in_gga(T9, tree(T9, void, void), void) → delete1_out_gga(T9, tree(T9, void, void), void)
delete1_in_gga(T26, tree(T26, void, void), tree(T26, T28, void)) → U12_gga(T26, T28, p17_in_ga(T26, T28))
p17_in_ga(T26, T28) → U2_ga(T26, T28, less19_in_g(T26))
less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U2_ga(T26, T28, less19_out_g(T26)) → p17_out_ga(T26, T28)
U2_ga(T26, T28, less19_out_g(T26)) → U3_ga(T26, T28, delete1_in_gga(T26, void, T28))
delete1_in_gga(T46, tree(T46, void, void), tree(T46, void, T48)) → U13_gga(T46, T48, p17_in_ga(T46, T48))
U13_gga(T46, T48, p17_out_ga(T46, T48)) → delete1_out_gga(T46, tree(T46, void, void), tree(T46, void, T48))
delete1_in_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void)) → U14_gga(T59, T54, p33_in_ga(T59, T54))
p33_in_ga(T59, T54) → U4_ga(T59, T54, less19_in_g(T59))
U4_ga(T59, T54, less19_out_g(T59)) → p33_out_ga(T59, T54)
U4_ga(T59, T54, less19_out_g(T59)) → U5_ga(T59, T54, delete1_in_gga(s(T59), void, T54))
delete1_in_gga(T73, tree(T73, void, void), tree(T73, void, T75)) → U15_gga(T73, T75, p17_in_ga(T73, T75))
U15_gga(T73, T75, p17_out_ga(T73, T75)) → delete1_out_gga(T73, tree(T73, void, void), tree(T73, void, T75))
delete1_in_gga(T79, tree(T79, void, void), tree(T79, void, T81)) → U16_gga(T79, T81, p40_in_ga(T79, T81))
p40_in_ga(s(T84), T81) → U7_ga(T84, T81, p33_in_ga(T84, T81))
U7_ga(T84, T81, p33_out_ga(T84, T81)) → p40_out_ga(s(T84), T81)
U16_gga(T79, T81, p40_out_ga(T79, T81)) → delete1_out_gga(T79, tree(T79, void, void), tree(T79, void, T81))
delete1_in_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105)) → delete1_out_gga(T90, tree(T90, void, tree(T104, void, T105)), tree(T104, void, T105))
delete1_in_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135))) → U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_in_gaa(T131, T136, T137))
delmin56_in_gaa(tree(T150, void, T151), T150, T151) → delmin56_out_gaa(tree(T150, void, T151), T150, T151)
delmin56_in_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169)) → U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_in_gaa(T165, T170, T171))
U6_gaa(T164, T165, T166, T170, T171, T169, delmin56_out_gaa(T165, T170, T171)) → delmin56_out_gaa(tree(T164, T165, T166), T170, tree(T164, T171, T169))
U17_gga(T90, T130, T131, T132, T136, T137, T135, delmin56_out_gaa(T131, T136, T137)) → delete1_out_gga(T90, tree(T90, void, tree(T130, T131, T132)), tree(T136, void, tree(T130, T137, T135)))
delete1_in_gga(T188, tree(T188, void, T189), tree(T188, T191, T189)) → U18_gga(T188, T189, T191, p40_in_ga(T188, T191))
U18_gga(T188, T189, T191, p40_out_ga(T188, T191)) → delete1_out_gga(T188, tree(T188, void, T189), tree(T188, T191, T189))
delete1_in_gga(T199, tree(T199, void, T200), tree(T199, void, T202)) → U19_gga(T199, T200, T202, p71_in_gga(T199, T200, T202))
p71_in_gga(T199, T200, T202) → U8_gga(T199, T200, T202, less19_in_g(T199))
U8_gga(T199, T200, T202, less19_out_g(T199)) → p71_out_gga(T199, T200, T202)
U8_gga(T199, T200, T202, less19_out_g(T199)) → U9_gga(T199, T200, T202, delete1_in_gga(T199, T200, T202))
delete1_in_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213)) → U20_gga(T220, T213, T215, p33_in_ga(T220, T215))
U20_gga(T220, T213, T215, p33_out_ga(T220, T215)) → delete1_out_gga(s(T220), tree(s(T220), void, T213), tree(s(T220), T215, T213))
delete1_in_gga(T228, tree(T228, void, T229), tree(T228, void, T231)) → U21_gga(T228, T229, T231, p71_in_gga(T228, T229, T231))
U21_gga(T228, T229, T231, p71_out_gga(T228, T229, T231)) → delete1_out_gga(T228, tree(T228, void, T229), tree(T228, void, T231))
delete1_in_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_gga(T242, T237, T239, less19_in_g(T242))
U22_gga(T242, T237, T239, less19_out_g(T242)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U22_gga(T242, T237, T239, less19_out_g(T242)) → U23_gga(T242, T237, T239, delete1_in_gga(s(T242), T237, T239))
delete1_in_gga(T251, tree(T251, T252, void), T252) → delete1_out_gga(T251, tree(T251, T252, void), T252)
delete1_in_gga(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_gga(T275, T276, T278, less19_in_g(T275))
U24_gga(T275, T276, T278, less19_out_g(T275)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U24_gga(T275, T276, T278, less19_out_g(T275)) → U25_gga(T275, T276, T278, delete1_in_gga(T275, T276, T278))
delete1_in_gga(T291, tree(T291, T292, void), tree(T291, T292, T294)) → U26_gga(T291, T292, T294, p40_in_ga(T291, T294))
U26_gga(T291, T292, T294, p40_out_ga(T291, T294)) → delete1_out_gga(T291, tree(T291, T292, void), tree(T291, T292, T294))
delete1_in_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_gga(T307, T300, T302, less19_in_g(T307))
U27_gga(T307, T300, T302, less19_out_g(T307)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U27_gga(T307, T300, T302, less19_out_g(T307)) → U28_gga(T307, T300, T302, delete1_in_gga(s(T307), T300, T302))
delete1_in_gga(T320, tree(T320, T321, void), tree(T320, T321, T323)) → U29_gga(T320, T321, T323, p40_in_ga(T320, T323))
U29_gga(T320, T321, T323, p40_out_ga(T320, T323)) → delete1_out_gga(T320, tree(T320, T321, void), tree(T320, T321, T323))
delete1_in_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331)) → U30_gga(T334, T329, T331, p33_in_ga(T334, T331))
U30_gga(T334, T329, T331, p33_out_ga(T334, T331)) → delete1_out_gga(s(T334), tree(s(T334), T329, void), tree(s(T334), T329, T331))
delete1_in_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357)) → delete1_out_gga(T341, tree(T341, T342, tree(T356, void, T357)), tree(T356, T342, T357))
delete1_in_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387))) → U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_in_gaa(T383, T388, T389))
U31_gga(T341, T342, T382, T383, T384, T388, T389, T387, delmin56_out_gaa(T383, T388, T389)) → delete1_out_gga(T341, tree(T341, T342, tree(T382, T383, T384)), tree(T388, T342, tree(T382, T389, T387)))
delete1_in_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_gga(T410, T411, T412, T414, less19_in_g(T410))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U32_gga(T410, T411, T412, T414, less19_out_g(T410)) → U33_gga(T410, T411, T412, T414, delete1_in_gga(T410, T411, T414))
delete1_in_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_gga(T429, T430, T431, T433, less19_in_g(T429))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U34_gga(T429, T430, T431, T433, less19_out_g(T429)) → U35_gga(T429, T430, T431, T433, delete1_in_gga(T429, T431, T433))
delete1_in_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → U36_gga(T455, T447, T448, T450, delete1_in_gga(0, T447, T450))
delete1_in_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_gga(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U37_gga(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → U38_gga(T466, T467, T447, T448, T450, delete1_in_gga(s(T466), T447, T450))
delete1_in_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_gga(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U39_gga(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → U40_gga(T594, T595, T596, T597, T599, delete1_in_gga(T594, T597, T599))
delete1_in_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → U41_gga(T623, T615, T616, T618, delete1_in_gga(s(T623), T616, T618))
delete1_in_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_gga(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U42_gga(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → U43_gga(T633, T632, T615, T616, T618, delete1_in_gga(s(T633), T616, T618))
U43_gga(T633, T632, T615, T616, T618, delete1_out_gga(s(T633), T616, T618)) → delete1_out_gga(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618))
U41_gga(T623, T615, T616, T618, delete1_out_gga(s(T623), T616, T618)) → delete1_out_gga(s(T623), tree(0, T615, T616), tree(0, T615, T618))
U40_gga(T594, T595, T596, T597, T599, delete1_out_gga(T594, T597, T599)) → delete1_out_gga(T594, tree(T595, T596, T597), tree(T595, T596, T599))
U38_gga(T466, T467, T447, T448, T450, delete1_out_gga(s(T466), T447, T450)) → delete1_out_gga(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448))
U36_gga(T455, T447, T448, T450, delete1_out_gga(0, T447, T450)) → delete1_out_gga(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448))
U35_gga(T429, T430, T431, T433, delete1_out_gga(T429, T431, T433)) → delete1_out_gga(T429, tree(T429, T430, T431), tree(T429, T430, T433))
U33_gga(T410, T411, T412, T414, delete1_out_gga(T410, T411, T414)) → delete1_out_gga(T410, tree(T410, T411, T412), tree(T410, T414, T412))
U28_gga(T307, T300, T302, delete1_out_gga(s(T307), T300, T302)) → delete1_out_gga(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void))
U25_gga(T275, T276, T278, delete1_out_gga(T275, T276, T278)) → delete1_out_gga(T275, tree(T275, T276, void), tree(T275, T278, void))
U23_gga(T242, T237, T239, delete1_out_gga(s(T242), T237, T239)) → delete1_out_gga(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239))
U9_gga(T199, T200, T202, delete1_out_gga(T199, T200, T202)) → p71_out_gga(T199, T200, T202)
U19_gga(T199, T200, T202, p71_out_gga(T199, T200, T202)) → delete1_out_gga(T199, tree(T199, void, T200), tree(T199, void, T202))
U5_ga(T59, T54, delete1_out_gga(s(T59), void, T54)) → p33_out_ga(T59, T54)
U14_gga(T59, T54, p33_out_ga(T59, T54)) → delete1_out_gga(s(T59), tree(s(T59), void, void), tree(s(T59), T54, void))
U3_ga(T26, T28, delete1_out_gga(T26, void, T28)) → p17_out_ga(T26, T28)
U12_gga(T26, T28, p17_out_ga(T26, T28)) → delete1_out_gga(T26, tree(T26, void, void), tree(T26, T28, void))

The argument filtering Pi contains the following mapping:
delete1_in_gga(x1, x2, x3)  =  delete1_in_gga(x1, x2)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
delete1_out_gga(x1, x2, x3)  =  delete1_out_gga
U12_gga(x1, x2, x3)  =  U12_gga(x3)
p17_in_ga(x1, x2)  =  p17_in_ga(x1)
U2_ga(x1, x2, x3)  =  U2_ga(x1, x3)
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
p17_out_ga(x1, x2)  =  p17_out_ga
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U13_gga(x1, x2, x3)  =  U13_gga(x3)
U14_gga(x1, x2, x3)  =  U14_gga(x3)
p33_in_ga(x1, x2)  =  p33_in_ga(x1)
U4_ga(x1, x2, x3)  =  U4_ga(x1, x3)
p33_out_ga(x1, x2)  =  p33_out_ga
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U15_gga(x1, x2, x3)  =  U15_gga(x3)
U16_gga(x1, x2, x3)  =  U16_gga(x3)
p40_in_ga(x1, x2)  =  p40_in_ga(x1)
U7_ga(x1, x2, x3)  =  U7_ga(x3)
p40_out_ga(x1, x2)  =  p40_out_ga
U17_gga(x1, x2, x3, x4, x5, x6, x7, x8)  =  U17_gga(x8)
delmin56_in_gaa(x1, x2, x3)  =  delmin56_in_gaa(x1)
delmin56_out_gaa(x1, x2, x3)  =  delmin56_out_gaa(x2)
U6_gaa(x1, x2, x3, x4, x5, x6, x7)  =  U6_gaa(x7)
U18_gga(x1, x2, x3, x4)  =  U18_gga(x4)
U19_gga(x1, x2, x3, x4)  =  U19_gga(x4)
p71_in_gga(x1, x2, x3)  =  p71_in_gga(x1, x2)
U8_gga(x1, x2, x3, x4)  =  U8_gga(x1, x2, x4)
p71_out_gga(x1, x2, x3)  =  p71_out_gga
U9_gga(x1, x2, x3, x4)  =  U9_gga(x4)
U20_gga(x1, x2, x3, x4)  =  U20_gga(x4)
U21_gga(x1, x2, x3, x4)  =  U21_gga(x4)
U22_gga(x1, x2, x3, x4)  =  U22_gga(x1, x2, x4)
U23_gga(x1, x2, x3, x4)  =  U23_gga(x4)
U24_gga(x1, x2, x3, x4)  =  U24_gga(x1, x2, x4)
U25_gga(x1, x2, x3, x4)  =  U25_gga(x4)
U26_gga(x1, x2, x3, x4)  =  U26_gga(x4)
U27_gga(x1, x2, x3, x4)  =  U27_gga(x1, x2, x4)
U28_gga(x1, x2, x3, x4)  =  U28_gga(x4)
U29_gga(x1, x2, x3, x4)  =  U29_gga(x4)
U30_gga(x1, x2, x3, x4)  =  U30_gga(x4)
U31_gga(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U31_gga(x9)
U32_gga(x1, x2, x3, x4, x5)  =  U32_gga(x1, x2, x5)
U33_gga(x1, x2, x3, x4, x5)  =  U33_gga(x5)
U34_gga(x1, x2, x3, x4, x5)  =  U34_gga(x1, x3, x5)
U35_gga(x1, x2, x3, x4, x5)  =  U35_gga(x5)
0  =  0
U36_gga(x1, x2, x3, x4, x5)  =  U36_gga(x5)
U37_gga(x1, x2, x3, x4, x5, x6)  =  U37_gga(x1, x3, x6)
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
U38_gga(x1, x2, x3, x4, x5, x6)  =  U38_gga(x6)
U39_gga(x1, x2, x3, x4, x5, x6)  =  U39_gga(x1, x4, x6)
U40_gga(x1, x2, x3, x4, x5, x6)  =  U40_gga(x6)
U41_gga(x1, x2, x3, x4, x5)  =  U41_gga(x5)
U42_gga(x1, x2, x3, x4, x5, x6)  =  U42_gga(x1, x4, x6)
U43_gga(x1, x2, x3, x4, x5, x6)  =  U43_gga(x6)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
P71_IN_GGA(x1, x2, x3)  =  P71_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4, x5)  =  U32_GGA(x1, x2, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x3, x5)
U37_GGA(x1, x2, x3, x4, x5, x6)  =  U37_GGA(x1, x3, x6)
U39_GGA(x1, x2, x3, x4, x5, x6)  =  U39_GGA(x1, x4, x6)
U42_GGA(x1, x2, x3, x4, x5, x6)  =  U42_GGA(x1, x4, x6)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

DELETE1_IN_GGA(T199, tree(T199, void, T200), tree(T199, void, T202)) → P71_IN_GGA(T199, T200, T202)
P71_IN_GGA(T199, T200, T202) → U8_GGA(T199, T200, T202, less19_in_g(T199))
U8_GGA(T199, T200, T202, less19_out_g(T199)) → DELETE1_IN_GGA(T199, T200, T202)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237), tree(s(T242), void, T239)) → U22_GGA(T242, T237, T239, less19_in_g(T242))
U22_GGA(T242, T237, T239, less19_out_g(T242)) → DELETE1_IN_GGA(s(T242), T237, T239)
DELETE1_IN_GGA(T275, tree(T275, T276, void), tree(T275, T278, void)) → U24_GGA(T275, T276, T278, less19_in_g(T275))
U24_GGA(T275, T276, T278, less19_out_g(T275)) → DELETE1_IN_GGA(T275, T276, T278)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void), tree(s(T307), T302, void)) → U27_GGA(T307, T300, T302, less19_in_g(T307))
U27_GGA(T307, T300, T302, less19_out_g(T307)) → DELETE1_IN_GGA(s(T307), T300, T302)
DELETE1_IN_GGA(T410, tree(T410, T411, T412), tree(T410, T414, T412)) → U32_GGA(T410, T411, T412, T414, less19_in_g(T410))
U32_GGA(T410, T411, T412, T414, less19_out_g(T410)) → DELETE1_IN_GGA(T410, T411, T414)
DELETE1_IN_GGA(T429, tree(T429, T430, T431), tree(T429, T430, T433)) → U34_GGA(T429, T430, T431, T433, less19_in_g(T429))
U34_GGA(T429, T430, T431, T433, less19_out_g(T429)) → DELETE1_IN_GGA(T429, T431, T433)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448), tree(s(T455), T450, T448)) → DELETE1_IN_GGA(0, T447, T450)
DELETE1_IN_GGA(T594, tree(T595, T596, T597), tree(T595, T596, T599)) → U39_GGA(T594, T595, T596, T597, T599, less222_in_gg(T595, T594))
U39_GGA(T594, T595, T596, T597, T599, less222_out_gg(T595, T594)) → DELETE1_IN_GGA(T594, T597, T599)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448), tree(s(T467), T450, T448)) → U37_GGA(T466, T467, T447, T448, T450, less164_in_gg(T466, T467))
U37_GGA(T466, T467, T447, T448, T450, less164_out_gg(T466, T467)) → DELETE1_IN_GGA(s(T466), T447, T450)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616), tree(0, T615, T618)) → DELETE1_IN_GGA(s(T623), T616, T618)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616), tree(s(T632), T615, T618)) → U42_GGA(T633, T632, T615, T616, T618, less222_in_gg(T632, T633))
U42_GGA(T633, T632, T615, T616, T618, less222_out_gg(T632, T633)) → DELETE1_IN_GGA(s(T633), T616, T618)

The TRS R consists of the following rules:

less19_in_g(s(T33)) → U1_g(T33, less19_in_g(T33))
less222_in_gg(0, s(T571)) → less222_out_gg(0, s(T571))
less222_in_gg(s(T576), s(T577)) → U10_gg(T576, T577, less222_in_gg(T576, T577))
less164_in_gg(0, s(T476)) → less164_out_gg(0, s(T476))
less164_in_gg(s(0), s(s(T489))) → less164_out_gg(s(0), s(s(T489)))
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg(s(s(0)), s(s(s(T502))))
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg(s(s(s(0))), s(s(s(s(T515)))))
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg(s(s(s(s(0)))), s(s(s(s(s(T528))))))
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541)))))))
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554))))))))
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(T559, T560, less222_in_gg(T559, T560))
U1_g(T33, less19_out_g(T33)) → less19_out_g(s(T33))
U10_gg(T576, T577, less222_out_gg(T576, T577)) → less222_out_gg(s(T576), s(T577))
U11_gg(T559, T560, less222_out_gg(T559, T560)) → less164_out_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560))))))))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
void  =  void
less19_in_g(x1)  =  less19_in_g(x1)
s(x1)  =  s(x1)
U1_g(x1, x2)  =  U1_g(x2)
less19_out_g(x1)  =  less19_out_g
0  =  0
less164_in_gg(x1, x2)  =  less164_in_gg(x1, x2)
less164_out_gg(x1, x2)  =  less164_out_gg
U11_gg(x1, x2, x3)  =  U11_gg(x3)
less222_in_gg(x1, x2)  =  less222_in_gg(x1, x2)
less222_out_gg(x1, x2)  =  less222_out_gg
U10_gg(x1, x2, x3)  =  U10_gg(x3)
DELETE1_IN_GGA(x1, x2, x3)  =  DELETE1_IN_GGA(x1, x2)
P71_IN_GGA(x1, x2, x3)  =  P71_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3, x4)  =  U8_GGA(x1, x2, x4)
U22_GGA(x1, x2, x3, x4)  =  U22_GGA(x1, x2, x4)
U24_GGA(x1, x2, x3, x4)  =  U24_GGA(x1, x2, x4)
U27_GGA(x1, x2, x3, x4)  =  U27_GGA(x1, x2, x4)
U32_GGA(x1, x2, x3, x4, x5)  =  U32_GGA(x1, x2, x5)
U34_GGA(x1, x2, x3, x4, x5)  =  U34_GGA(x1, x3, x5)
U37_GGA(x1, x2, x3, x4, x5, x6)  =  U37_GGA(x1, x3, x6)
U39_GGA(x1, x2, x3, x4, x5, x6)  =  U39_GGA(x1, x4, x6)
U42_GGA(x1, x2, x3, x4, x5, x6)  =  U42_GGA(x1, x4, x6)

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

DELETE1_IN_GGA(T199, tree(T199, void, T200)) → P71_IN_GGA(T199, T200)
P71_IN_GGA(T199, T200) → U8_GGA(T199, T200, less19_in_g(T199))
U8_GGA(T199, T200, less19_out_g) → DELETE1_IN_GGA(T199, T200)
DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237)) → U22_GGA(T242, T237, less19_in_g(T242))
U22_GGA(T242, T237, less19_out_g) → DELETE1_IN_GGA(s(T242), T237)
DELETE1_IN_GGA(T275, tree(T275, T276, void)) → U24_GGA(T275, T276, less19_in_g(T275))
U24_GGA(T275, T276, less19_out_g) → DELETE1_IN_GGA(T275, T276)
DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void)) → U27_GGA(T307, T300, less19_in_g(T307))
U27_GGA(T307, T300, less19_out_g) → DELETE1_IN_GGA(s(T307), T300)
DELETE1_IN_GGA(T410, tree(T410, T411, T412)) → U32_GGA(T410, T411, less19_in_g(T410))
U32_GGA(T410, T411, less19_out_g) → DELETE1_IN_GGA(T410, T411)
DELETE1_IN_GGA(T429, tree(T429, T430, T431)) → U34_GGA(T429, T431, less19_in_g(T429))
U34_GGA(T429, T431, less19_out_g) → DELETE1_IN_GGA(T429, T431)
DELETE1_IN_GGA(0, tree(s(T455), T447, T448)) → DELETE1_IN_GGA(0, T447)
DELETE1_IN_GGA(T594, tree(T595, T596, T597)) → U39_GGA(T594, T597, less222_in_gg(T595, T594))
U39_GGA(T594, T597, less222_out_gg) → DELETE1_IN_GGA(T594, T597)
DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448)) → U37_GGA(T466, T447, less164_in_gg(T466, T467))
U37_GGA(T466, T447, less164_out_gg) → DELETE1_IN_GGA(s(T466), T447)
DELETE1_IN_GGA(s(T623), tree(0, T615, T616)) → DELETE1_IN_GGA(s(T623), T616)
DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616)) → U42_GGA(T633, T616, less222_in_gg(T632, T633))
U42_GGA(T633, T616, less222_out_gg) → DELETE1_IN_GGA(s(T633), T616)

The TRS R consists of the following rules:

less19_in_g(s(T33)) → U1_g(less19_in_g(T33))
less222_in_gg(0, s(T571)) → less222_out_gg
less222_in_gg(s(T576), s(T577)) → U10_gg(less222_in_gg(T576, T577))
less164_in_gg(0, s(T476)) → less164_out_gg
less164_in_gg(s(0), s(s(T489))) → less164_out_gg
less164_in_gg(s(s(0)), s(s(s(T502)))) → less164_out_gg
less164_in_gg(s(s(s(0))), s(s(s(s(T515))))) → less164_out_gg
less164_in_gg(s(s(s(s(0)))), s(s(s(s(s(T528)))))) → less164_out_gg
less164_in_gg(s(s(s(s(s(0))))), s(s(s(s(s(s(T541))))))) → less164_out_gg
less164_in_gg(s(s(s(s(s(s(0)))))), s(s(s(s(s(s(s(T554)))))))) → less164_out_gg
less164_in_gg(s(s(s(s(s(s(s(T559))))))), s(s(s(s(s(s(s(T560)))))))) → U11_gg(less222_in_gg(T559, T560))
U1_g(less19_out_g) → less19_out_g
U10_gg(less222_out_gg) → less222_out_gg
U11_gg(less222_out_gg) → less164_out_gg

The set Q consists of the following terms:

less19_in_g(x0)
less222_in_gg(x0, x1)
less164_in_gg(x0, x1)
U1_g(x0)
U10_gg(x0)
U11_gg(x0)

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

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

  • P71_IN_GGA(T199, T200) → U8_GGA(T199, T200, less19_in_g(T199))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U8_GGA(T199, T200, less19_out_g) → DELETE1_IN_GGA(T199, T200)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GGA(T199, tree(T199, void, T200)) → P71_IN_GGA(T199, T200)
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • DELETE1_IN_GGA(s(T623), tree(0, T615, T616)) → DELETE1_IN_GGA(s(T623), T616)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETE1_IN_GGA(0, tree(s(T455), T447, T448)) → DELETE1_IN_GGA(0, T447)
    The graph contains the following edges 1 >= 1, 2 > 2

  • U22_GGA(T242, T237, less19_out_g) → DELETE1_IN_GGA(s(T242), T237)
    The graph contains the following edges 2 >= 2

  • DELETE1_IN_GGA(s(T242), tree(s(T242), void, T237)) → U22_GGA(T242, T237, less19_in_g(T242))
    The graph contains the following edges 1 > 1, 2 > 1, 2 > 2

  • U24_GGA(T275, T276, less19_out_g) → DELETE1_IN_GGA(T275, T276)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GGA(T275, tree(T275, T276, void)) → U24_GGA(T275, T276, less19_in_g(T275))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U27_GGA(T307, T300, less19_out_g) → DELETE1_IN_GGA(s(T307), T300)
    The graph contains the following edges 2 >= 2

  • DELETE1_IN_GGA(s(T307), tree(s(T307), T300, void)) → U27_GGA(T307, T300, less19_in_g(T307))
    The graph contains the following edges 1 > 1, 2 > 1, 2 > 2

  • U32_GGA(T410, T411, less19_out_g) → DELETE1_IN_GGA(T410, T411)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GGA(T410, tree(T410, T411, T412)) → U32_GGA(T410, T411, less19_in_g(T410))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U34_GGA(T429, T431, less19_out_g) → DELETE1_IN_GGA(T429, T431)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GGA(T429, tree(T429, T430, T431)) → U34_GGA(T429, T431, less19_in_g(T429))
    The graph contains the following edges 1 >= 1, 2 > 1, 2 > 2

  • U39_GGA(T594, T597, less222_out_gg) → DELETE1_IN_GGA(T594, T597)
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_GGA(T594, tree(T595, T596, T597)) → U39_GGA(T594, T597, less222_in_gg(T595, T594))
    The graph contains the following edges 1 >= 1, 2 > 2

  • U37_GGA(T466, T447, less164_out_gg) → DELETE1_IN_GGA(s(T466), T447)
    The graph contains the following edges 2 >= 2

  • U42_GGA(T633, T616, less222_out_gg) → DELETE1_IN_GGA(s(T633), T616)
    The graph contains the following edges 2 >= 2

  • DELETE1_IN_GGA(s(T466), tree(s(T467), T447, T448)) → U37_GGA(T466, T447, less164_in_gg(T466, T467))
    The graph contains the following edges 1 > 1, 2 > 2

  • DELETE1_IN_GGA(s(T633), tree(s(T632), T615, T616)) → U42_GGA(T633, T616, less222_in_gg(T632, T633))
    The graph contains the following edges 1 > 1, 2 > 2

(36) YES