(0) Obligation:

Clauses:

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

Queries:

delete(a,a,g).

(1) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

delmin19(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delmin19(T96, T93, T94).
less34(s(T145), s(T144)) :- less34(T145, T144).
less46(s(T184), s(T186)) :- less46(T184, T186).
p44(T163, T167, T168, T166) :- less46(T163, T167).
p44(T163, T171, T172, T166) :- ','(lessc46(T163, T171), delete1(T171, T172, T166)).
p32(T126, T122, T127, T125) :- less34(T126, T122).
p32(T130, T122, T131, T125) :- ','(lessc34(T130, T122), delete1(T130, T131, T125)).
p72(0, s(T272), T271, T263) :- delete1(s(T272), T271, T263).
p72(s(T281), s(T283), T284, T263) :- p79(T281, T283, T284, T263).
p65(T223, T222, T224, T202) :- less34(T223, T222).
p65(T227, T222, T228, T202) :- ','(lessc34(T227, T222), delete1(s(T227), T228, T202)).
p79(T281, T283, T284, T263) :- less46(T281, T283).
p79(T281, T287, T288, T263) :- ','(lessc46(T281, T287), delete1(s(T287), T288, T263)).
p116(0, s(T470), T469, T461) :- delete1(s(T470), T469, T461).
p116(s(T479), s(T481), T482, T461) :- p79(T479, T481, T482, T461).
delete1(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delmin19(T63, T60, T61).
delete1(T126, tree(T122, T127, T124), tree(T122, T125, T124)) :- p32(T126, T122, T127, T125).
delete1(T167, tree(T163, T164, T168), tree(T163, T164, T166)) :- p44(T163, T167, T168, T166).
delete1(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) :- delete1(0, T210, T202).
delete1(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) :- p65(T223, T222, T224, T202).
delete1(T250, tree(T246, T247, T251), tree(T246, T247, T249)) :- p44(T246, T250, T251, T249).
delete1(T264, tree(T260, T261, T265), tree(T260, T261, T263)) :- p72(T260, T264, T265, T263).
delete1(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) :- delmin19(T346, T343, T344).
delete1(T376, tree(T372, T377, T374), tree(T372, T375, T374)) :- p32(T376, T372, T377, T375).
delete1(T395, tree(T391, T392, T396), tree(T391, T392, T394)) :- p72(T391, T395, T396, T394).
delete1(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) :- delete1(0, T416, T408).
delete1(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) :- p65(T429, T428, T430, T408).
delete1(T448, tree(T444, T445, T449), tree(T444, T445, T447)) :- p72(T444, T448, T449, T447).
delete1(T462, tree(T458, T459, T463), tree(T458, T459, T461)) :- p116(T458, T462, T463, T461).
delete1(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) :- delmin19(T540, T537, T538).
delete1(T570, tree(T566, T571, T568), tree(T566, T569, T568)) :- p32(T570, T566, T571, T569).
delete1(T589, tree(T585, T586, T590), tree(T585, T586, T588)) :- p116(T585, T589, T590, T588).
delete1(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) :- delete1(0, T610, T602).
delete1(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) :- p65(T623, T622, T624, T602).
delete1(T642, tree(T638, T639, T643), tree(T638, T639, T641)) :- p116(T638, T642, T643, T641).
delete1(s(T664), tree(0, T653, T663), tree(0, T653, T655)) :- delete1(s(T664), T663, T655).
delete1(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) :- p79(T673, T675, T676, T655).
delete1(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) :- delmin19(T730, T727, T728).
delete1(T760, tree(T756, T761, T758), tree(T756, T759, T758)) :- p32(T760, T756, T761, T759).
delete1(T779, tree(T775, T776, T780), tree(T775, T776, T778)) :- p116(T775, T779, T780, T778).
delete1(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) :- delete1(0, T800, T792).
delete1(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) :- p65(T813, T812, T814, T792).
delete1(T832, tree(T828, T829, T833), tree(T828, T829, T831)) :- p116(T828, T832, T833, T831).
delete1(s(T854), tree(0, T843, T853), tree(0, T843, T845)) :- delete1(s(T854), T853, T845).
delete1(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) :- p79(T863, T865, T866, T845).

Clauses:

delminc19(tree(T76, void, T77), T76, T77).
delminc19(tree(T90, T96, T92), T93, tree(T90, T94, T95)) :- delminc19(T96, T93, T94).
deletec1(T6, tree(T6, void, T7), T7).
deletec1(T10, tree(T10, T11, void), T11).
deletec1(T17, tree(T17, T18, tree(T31, void, T32)), tree(T31, T18, T32)).
deletec1(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) :- delminc19(T63, T60, T61).
deletec1(T126, tree(T122, T127, T124), tree(T122, T125, T124)) :- qc32(T126, T122, T127, T125).
deletec1(T167, tree(T163, T164, T168), tree(T163, T164, T166)) :- qc44(T163, T167, T168, T166).
deletec1(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) :- deletec1(0, T210, T202).
deletec1(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) :- qc65(T223, T222, T224, T202).
deletec1(T250, tree(T246, T247, T251), tree(T246, T247, T249)) :- qc44(T246, T250, T251, T249).
deletec1(T264, tree(T260, T261, T265), tree(T260, T261, T263)) :- qc72(T260, T264, T265, T263).
deletec1(T300, tree(T300, T301, tree(T314, void, T315)), tree(T314, T301, T315)).
deletec1(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) :- delminc19(T346, T343, T344).
deletec1(T376, tree(T372, T377, T374), tree(T372, T375, T374)) :- qc32(T376, T372, T377, T375).
deletec1(T395, tree(T391, T392, T396), tree(T391, T392, T394)) :- qc72(T391, T395, T396, T394).
deletec1(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) :- deletec1(0, T416, T408).
deletec1(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) :- qc65(T429, T428, T430, T408).
deletec1(T448, tree(T444, T445, T449), tree(T444, T445, T447)) :- qc72(T444, T448, T449, T447).
deletec1(T462, tree(T458, T459, T463), tree(T458, T459, T461)) :- qc116(T458, T462, T463, T461).
deletec1(T487, tree(T487, T488, void), T488).
deletec1(T494, tree(T494, T495, tree(T508, void, T509)), tree(T508, T495, T509)).
deletec1(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) :- delminc19(T540, T537, T538).
deletec1(T570, tree(T566, T571, T568), tree(T566, T569, T568)) :- qc32(T570, T566, T571, T569).
deletec1(T589, tree(T585, T586, T590), tree(T585, T586, T588)) :- qc116(T585, T589, T590, T588).
deletec1(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) :- deletec1(0, T610, T602).
deletec1(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) :- qc65(T623, T622, T624, T602).
deletec1(T642, tree(T638, T639, T643), tree(T638, T639, T641)) :- qc116(T638, T642, T643, T641).
deletec1(s(T664), tree(0, T653, T663), tree(0, T653, T655)) :- deletec1(s(T664), T663, T655).
deletec1(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) :- qc79(T673, T675, T676, T655).
deletec1(T684, tree(T684, T685, tree(T698, void, T699)), tree(T698, T685, T699)).
deletec1(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) :- delminc19(T730, T727, T728).
deletec1(T760, tree(T756, T761, T758), tree(T756, T759, T758)) :- qc32(T760, T756, T761, T759).
deletec1(T779, tree(T775, T776, T780), tree(T775, T776, T778)) :- qc116(T775, T779, T780, T778).
deletec1(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) :- deletec1(0, T800, T792).
deletec1(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) :- qc65(T813, T812, T814, T792).
deletec1(T832, tree(T828, T829, T833), tree(T828, T829, T831)) :- qc116(T828, T832, T833, T831).
deletec1(s(T854), tree(0, T843, T853), tree(0, T843, T845)) :- deletec1(s(T854), T853, T845).
deletec1(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) :- qc79(T863, T865, T866, T845).
lessc34(0, s(T138)).
lessc34(s(T145), s(T144)) :- lessc34(T145, T144).
lessc46(0, s(T179)).
lessc46(s(T184), s(T186)) :- lessc46(T184, T186).
qc44(T163, T171, T172, T166) :- ','(lessc46(T163, T171), deletec1(T171, T172, T166)).
qc32(T130, T122, T131, T125) :- ','(lessc34(T130, T122), deletec1(T130, T131, T125)).
qc72(0, s(T272), T271, T263) :- deletec1(s(T272), T271, T263).
qc72(s(T281), s(T283), T284, T263) :- qc79(T281, T283, T284, T263).
qc65(T227, T222, T228, T202) :- ','(lessc34(T227, T222), deletec1(s(T227), T228, T202)).
qc79(T281, T287, T288, T263) :- ','(lessc46(T281, T287), deletec1(s(T287), T288, T263)).
qc116(0, s(T470), T469, T461) :- deletec1(s(T470), T469, T461).
qc116(s(T479), s(T481), T482, T461) :- qc79(T479, T481, T482, T461).

Afs:

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

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
delete1_in: (f,f,b) (b,f,b)
delmin19_in: (f,b,b)
p32_in: (f,b,f,b) (b,b,f,b)
less34_in: (f,b) (b,b)
lessc34_in: (f,b) (b,b)
p44_in: (b,b,f,b) (b,f,f,b)
less46_in: (b,b) (b,f)
lessc46_in: (b,b) (b,f)
p65_in: (b,b,f,b) (f,b,f,b)
p72_in: (b,b,f,b) (b,f,f,b)
p79_in: (b,b,f,b) (b,f,f,b)
p116_in: (b,b,f,b) (b,f,f,b)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

DELETE1_IN_AAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_AAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_AAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)
DELETE1_IN_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_AAG(T126, T122, T127, T124, T125, p32_in_agag(T126, T122, T127, T125))
DELETE1_IN_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_AGAG(T126, T122, T127, T125)
P32_IN_AGAG(T126, T122, T127, T125) → U7_AGAG(T126, T122, T127, T125, less34_in_ag(T126, T122))
P32_IN_AGAG(T126, T122, T127, T125) → LESS34_IN_AG(T126, T122)
LESS34_IN_AG(s(T145), s(T144)) → U2_AG(T145, T144, less34_in_ag(T145, T144))
LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)
P32_IN_AGAG(T130, T122, T131, T125) → U8_AGAG(T130, T122, T131, T125, lessc34_in_ag(T130, T122))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → U9_AGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_GAG(T126, T122, T127, T124, T125, p32_in_ggag(T126, T122, T127, T125))
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T126, T122, T127, T125) → U7_GGAG(T126, T122, T127, T125, less34_in_gg(T126, T122))
P32_IN_GGAG(T126, T122, T127, T125) → LESS34_IN_GG(T126, T122)
LESS34_IN_GG(s(T145), s(T144)) → U2_GG(T145, T144, less34_in_gg(T145, T144))
LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → U9_GGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_GAG(T167, T163, T164, T168, T166, p44_in_ggag(T163, T167, T168, T166))
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T167, T168, T166) → U4_GGAG(T163, T167, T168, T166, less46_in_gg(T163, T167))
P44_IN_GGAG(T163, T167, T168, T166) → LESS46_IN_GG(T163, T167)
LESS46_IN_GG(s(T184), s(T186)) → U3_GG(T184, T186, less46_in_gg(T184, T186))
LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → U6_GGAG(T163, T171, T172, T166, delete1_in_gag(T171, T172, T166))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_GAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_GAG(T223, T222, T224, T201, T202, p65_in_ggag(T223, T222, T224, T202))
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T223, T222, T224, T202) → U12_GGAG(T223, T222, T224, T202, less34_in_gg(T223, T222))
P65_IN_GGAG(T223, T222, T224, T202) → LESS34_IN_GG(T223, T222)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → U14_GGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_GAG(T250, T246, T247, T251, T249, p44_in_ggag(T246, T250, T251, T249))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_GAG(T264, T260, T261, T265, T263, p72_in_ggag(T260, T264, T265, T263))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → U10_GGAG(T272, T271, T263, delete1_in_gag(s(T272), T271, T263))
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_GAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_GAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_GAG(T376, T372, T377, T374, T375, p32_in_ggag(T376, T372, T377, T375))
DELETE1_IN_GAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_GAG(T395, T391, T392, T396, T394, p72_in_ggag(T391, T395, T396, T394))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → U11_GGAG(T281, T283, T284, T263, p79_in_ggag(T281, T283, T284, T263))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)
P79_IN_GGAG(T281, T283, T284, T263) → U15_GGAG(T281, T283, T284, T263, less46_in_gg(T281, T283))
P79_IN_GGAG(T281, T283, T284, T263) → LESS46_IN_GG(T281, T283)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → U17_GGAG(T281, T287, T288, T263, delete1_in_gag(s(T287), T288, T263))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
DELETE1_IN_GAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_GAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_GAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_GAG(T429, T428, T430, T407, T408, p65_in_ggag(T429, T428, T430, T408))
DELETE1_IN_GAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_GAG(T448, T444, T445, T449, T447, p72_in_ggag(T444, T448, T449, T447))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_GAG(T462, T458, T459, T463, T461, p116_in_ggag(T458, T462, T463, T461))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → U18_GGAG(T470, T469, T461, delete1_in_gag(s(T470), T469, T461))
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_GAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_GAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_GAG(T570, T566, T571, T568, T569, p32_in_ggag(T570, T566, T571, T569))
DELETE1_IN_GAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_GAG(T589, T585, T586, T590, T588, p116_in_ggag(T585, T589, T590, T588))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → U19_GGAG(T479, T481, T482, T461, p79_in_ggag(T479, T481, T482, T461))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
DELETE1_IN_GAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_GAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_GAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_GAG(T623, T622, T624, T601, T602, p65_in_ggag(T623, T622, T624, T602))
DELETE1_IN_GAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_GAG(T642, T638, T639, T643, T641, p116_in_ggag(T638, T642, T643, T641))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_GAG(T664, T653, T663, T655, delete1_in_gag(s(T664), T663, T655))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_GAG(T675, T673, T653, T676, T655, p79_in_ggag(T673, T675, T676, T655))
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
DELETE1_IN_GAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_GAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_GAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_GAG(T760, T756, T761, T758, T759, p32_in_ggag(T760, T756, T761, T759))
DELETE1_IN_GAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_GAG(T779, T775, T776, T780, T778, p116_in_ggag(T775, T779, T780, T778))
DELETE1_IN_GAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_GAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_GAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_GAG(T813, T812, T814, T791, T792, p65_in_ggag(T813, T812, T814, T792))
DELETE1_IN_GAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_GAG(T832, T828, T829, T833, T831, p116_in_ggag(T828, T832, T833, T831))
DELETE1_IN_GAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_GAG(T854, T843, T853, T845, delete1_in_gag(s(T854), T853, T845))
DELETE1_IN_GAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_GAG(T865, T863, T843, T866, T845, p79_in_ggag(T863, T865, T866, T845))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_AAG(T167, T163, T164, T168, T166, p44_in_gaag(T163, T167, T168, T166))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T167, T168, T166) → U4_GAAG(T163, T167, T168, T166, less46_in_ga(T163, T167))
P44_IN_GAAG(T163, T167, T168, T166) → LESS46_IN_GA(T163, T167)
LESS46_IN_GA(s(T184), s(T186)) → U3_GA(T184, T186, less46_in_ga(T184, T186))
LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → U6_GAAG(T163, T171, T172, T166, delete1_in_aag(T171, T172, T166))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_AAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_AAG(T223, T222, T224, T201, T202, p65_in_agag(T223, T222, T224, T202))
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_AGAG(T223, T222, T224, T202)
P65_IN_AGAG(T223, T222, T224, T202) → U12_AGAG(T223, T222, T224, T202, less34_in_ag(T223, T222))
P65_IN_AGAG(T223, T222, T224, T202) → LESS34_IN_AG(T223, T222)
P65_IN_AGAG(T227, T222, T228, T202) → U13_AGAG(T227, T222, T228, T202, lessc34_in_ag(T227, T222))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → U14_AGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_AAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_AAG(T250, T246, T247, T251, T249, p44_in_gaag(T246, T250, T251, T249))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_AAG(T264, T260, T261, T265, T263, p72_in_gaag(T260, T264, T265, T263))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → U10_GAAG(T272, T271, T263, delete1_in_aag(s(T272), T271, T263))
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_AAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_AAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_AAG(T376, T372, T377, T374, T375, p32_in_agag(T376, T372, T377, T375))
DELETE1_IN_AAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_AAG(T395, T391, T392, T396, T394, p72_in_gaag(T391, T395, T396, T394))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → U11_GAAG(T281, T283, T284, T263, p79_in_gaag(T281, T283, T284, T263))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)
P79_IN_GAAG(T281, T283, T284, T263) → U15_GAAG(T281, T283, T284, T263, less46_in_ga(T281, T283))
P79_IN_GAAG(T281, T283, T284, T263) → LESS46_IN_GA(T281, T283)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → U17_GAAG(T281, T287, T288, T263, delete1_in_aag(s(T287), T288, T263))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
DELETE1_IN_AAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_AAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_AAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_AAG(T429, T428, T430, T407, T408, p65_in_agag(T429, T428, T430, T408))
DELETE1_IN_AAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_AAG(T448, T444, T445, T449, T447, p72_in_gaag(T444, T448, T449, T447))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_AAG(T462, T458, T459, T463, T461, p116_in_gaag(T458, T462, T463, T461))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → U18_GAAG(T470, T469, T461, delete1_in_aag(s(T470), T469, T461))
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_AAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_AAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_AAG(T570, T566, T571, T568, T569, p32_in_agag(T570, T566, T571, T569))
DELETE1_IN_AAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_AAG(T589, T585, T586, T590, T588, p116_in_gaag(T585, T589, T590, T588))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → U19_GAAG(T479, T481, T482, T461, p79_in_gaag(T479, T481, T482, T461))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
DELETE1_IN_AAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_AAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_AAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_AAG(T623, T622, T624, T601, T602, p65_in_agag(T623, T622, T624, T602))
DELETE1_IN_AAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_AAG(T642, T638, T639, T643, T641, p116_in_gaag(T638, T642, T643, T641))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_AAG(T664, T653, T663, T655, delete1_in_aag(s(T664), T663, T655))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_AAG(T675, T673, T653, T676, T655, p79_in_gaag(T673, T675, T676, T655))
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
DELETE1_IN_AAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_AAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_AAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_AAG(T760, T756, T761, T758, T759, p32_in_agag(T760, T756, T761, T759))
DELETE1_IN_AAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_AAG(T779, T775, T776, T780, T778, p116_in_gaag(T775, T779, T780, T778))
DELETE1_IN_AAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_AAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_AAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_AAG(T813, T812, T814, T791, T792, p65_in_agag(T813, T812, T814, T792))
DELETE1_IN_AAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_AAG(T832, T828, T829, T833, T831, p116_in_gaag(T828, T832, T833, T831))
DELETE1_IN_AAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_AAG(T854, T843, T853, T845, delete1_in_aag(s(T854), T853, T845))
DELETE1_IN_AAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_AAG(T865, T863, T843, T866, T845, p79_in_gaag(T863, T865, T866, T845))

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
delete1_in_aag(x1, x2, x3)  =  delete1_in_aag(x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
p32_in_agag(x1, x2, x3, x4)  =  p32_in_agag(x2, x4)
less34_in_ag(x1, x2)  =  less34_in_ag(x2)
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
less46_in_gg(x1, x2)  =  less46_in_gg(x1, x2)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
p65_in_ggag(x1, x2, x3, x4)  =  p65_in_ggag(x1, x2, x4)
p72_in_ggag(x1, x2, x3, x4)  =  p72_in_ggag(x1, x2, x4)
p79_in_ggag(x1, x2, x3, x4)  =  p79_in_ggag(x1, x2, x4)
p116_in_ggag(x1, x2, x3, x4)  =  p116_in_ggag(x1, x2, x4)
p44_in_gaag(x1, x2, x3, x4)  =  p44_in_gaag(x1, x4)
less46_in_ga(x1, x2)  =  less46_in_ga(x1)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
p65_in_agag(x1, x2, x3, x4)  =  p65_in_agag(x2, x4)
p72_in_gaag(x1, x2, x3, x4)  =  p72_in_gaag(x1, x4)
p79_in_gaag(x1, x2, x3, x4)  =  p79_in_gaag(x1, x4)
p116_in_gaag(x1, x2, x3, x4)  =  p116_in_gaag(x1, x4)
DELETE1_IN_AAG(x1, x2, x3)  =  DELETE1_IN_AAG(x3)
U20_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_AAG(x2, x3, x6, x7, x8, x9)
DELMIN19_IN_AGG(x1, x2, x3)  =  DELMIN19_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x1, x4, x5, x6, x7)
U21_AAG(x1, x2, x3, x4, x5, x6)  =  U21_AAG(x2, x4, x5, x6)
P32_IN_AGAG(x1, x2, x3, x4)  =  P32_IN_AGAG(x2, x4)
U7_AGAG(x1, x2, x3, x4, x5)  =  U7_AGAG(x2, x4, x5)
LESS34_IN_AG(x1, x2)  =  LESS34_IN_AG(x2)
U2_AG(x1, x2, x3)  =  U2_AG(x2, x3)
U8_AGAG(x1, x2, x3, x4, x5)  =  U8_AGAG(x2, x4, x5)
U9_AGAG(x1, x2, x3, x4, x5)  =  U9_AGAG(x1, x2, x4, x5)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
U20_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_GAG(x1, x2, x3, x6, x7, x8, x9)
U21_GAG(x1, x2, x3, x4, x5, x6)  =  U21_GAG(x1, x2, x4, x5, x6)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5)  =  U7_GGAG(x1, x2, x4, x5)
LESS34_IN_GG(x1, x2)  =  LESS34_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x1, x2, x4, x5)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x2, x4, x5)
U22_GAG(x1, x2, x3, x4, x5, x6)  =  U22_GAG(x1, x2, x3, x5, x6)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U4_GGAG(x1, x2, x3, x4, x5)  =  U4_GGAG(x1, x2, x4, x5)
LESS46_IN_GG(x1, x2)  =  LESS46_IN_GG(x1, x2)
U3_GG(x1, x2, x3)  =  U3_GG(x1, x2, x3)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
U6_GGAG(x1, x2, x3, x4, x5)  =  U6_GGAG(x1, x2, x4, x5)
U23_GAG(x1, x2, x3, x4, x5)  =  U23_GAG(x1, x3, x4, x5)
U24_GAG(x1, x2, x3, x4, x5, x6)  =  U24_GAG(x1, x2, x4, x5, x6)
P65_IN_GGAG(x1, x2, x3, x4)  =  P65_IN_GGAG(x1, x2, x4)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x1, x2, x4, x5)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
U14_GGAG(x1, x2, x3, x4, x5)  =  U14_GGAG(x1, x2, x4, x5)
U25_GAG(x1, x2, x3, x4, x5, x6)  =  U25_GAG(x1, x2, x3, x5, x6)
U26_GAG(x1, x2, x3, x4, x5, x6)  =  U26_GAG(x1, x2, x3, x5, x6)
P72_IN_GGAG(x1, x2, x3, x4)  =  P72_IN_GGAG(x1, x2, x4)
U10_GGAG(x1, x2, x3, x4)  =  U10_GGAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_GAG(x1, x2, x3, x6, x7, x8, x9)
U28_GAG(x1, x2, x3, x4, x5, x6)  =  U28_GAG(x1, x2, x4, x5, x6)
U29_GAG(x1, x2, x3, x4, x5, x6)  =  U29_GAG(x1, x2, x3, x5, x6)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x1, x2, x4, x5)
P79_IN_GGAG(x1, x2, x3, x4)  =  P79_IN_GGAG(x1, x2, x4)
U15_GGAG(x1, x2, x3, x4, x5)  =  U15_GGAG(x1, x2, x4, x5)
U16_GGAG(x1, x2, x3, x4, x5)  =  U16_GGAG(x1, x2, x4, x5)
U17_GGAG(x1, x2, x3, x4, x5)  =  U17_GGAG(x1, x2, x4, x5)
U30_GAG(x1, x2, x3, x4, x5)  =  U30_GAG(x1, x3, x4, x5)
U31_GAG(x1, x2, x3, x4, x5, x6)  =  U31_GAG(x1, x2, x4, x5, x6)
U32_GAG(x1, x2, x3, x4, x5, x6)  =  U32_GAG(x1, x2, x3, x5, x6)
U33_GAG(x1, x2, x3, x4, x5, x6)  =  U33_GAG(x1, x2, x3, x5, x6)
P116_IN_GGAG(x1, x2, x3, x4)  =  P116_IN_GGAG(x1, x2, x4)
U18_GGAG(x1, x2, x3, x4)  =  U18_GGAG(x1, x3, x4)
U34_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_GAG(x1, x2, x3, x6, x7, x8, x9)
U35_GAG(x1, x2, x3, x4, x5, x6)  =  U35_GAG(x1, x2, x4, x5, x6)
U36_GAG(x1, x2, x3, x4, x5, x6)  =  U36_GAG(x1, x2, x3, x5, x6)
U19_GGAG(x1, x2, x3, x4, x5)  =  U19_GGAG(x1, x2, x4, x5)
U37_GAG(x1, x2, x3, x4, x5)  =  U37_GAG(x1, x3, x4, x5)
U38_GAG(x1, x2, x3, x4, x5, x6)  =  U38_GAG(x1, x2, x4, x5, x6)
U39_GAG(x1, x2, x3, x4, x5, x6)  =  U39_GAG(x1, x2, x3, x5, x6)
U40_GAG(x1, x2, x3, x4, x5)  =  U40_GAG(x1, x2, x4, x5)
U41_GAG(x1, x2, x3, x4, x5, x6)  =  U41_GAG(x1, x2, x3, x5, x6)
U42_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U42_GAG(x1, x2, x3, x6, x7, x8, x9)
U43_GAG(x1, x2, x3, x4, x5, x6)  =  U43_GAG(x1, x2, x4, x5, x6)
U44_GAG(x1, x2, x3, x4, x5, x6)  =  U44_GAG(x1, x2, x3, x5, x6)
U45_GAG(x1, x2, x3, x4, x5)  =  U45_GAG(x1, x3, x4, x5)
U46_GAG(x1, x2, x3, x4, x5, x6)  =  U46_GAG(x1, x2, x4, x5, x6)
U47_GAG(x1, x2, x3, x4, x5, x6)  =  U47_GAG(x1, x2, x3, x5, x6)
U48_GAG(x1, x2, x3, x4, x5)  =  U48_GAG(x1, x2, x4, x5)
U49_GAG(x1, x2, x3, x4, x5, x6)  =  U49_GAG(x1, x2, x3, x5, x6)
U22_AAG(x1, x2, x3, x4, x5, x6)  =  U22_AAG(x2, x3, x5, x6)
P44_IN_GAAG(x1, x2, x3, x4)  =  P44_IN_GAAG(x1, x4)
U4_GAAG(x1, x2, x3, x4, x5)  =  U4_GAAG(x1, x4, x5)
LESS46_IN_GA(x1, x2)  =  LESS46_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U5_GAAG(x1, x2, x3, x4, x5)  =  U5_GAAG(x1, x4, x5)
U6_GAAG(x1, x2, x3, x4, x5)  =  U6_GAAG(x1, x4, x5)
U23_AAG(x1, x2, x3, x4, x5)  =  U23_AAG(x1, x3, x4, x5)
U24_AAG(x1, x2, x3, x4, x5, x6)  =  U24_AAG(x2, x4, x5, x6)
P65_IN_AGAG(x1, x2, x3, x4)  =  P65_IN_AGAG(x2, x4)
U12_AGAG(x1, x2, x3, x4, x5)  =  U12_AGAG(x2, x4, x5)
U13_AGAG(x1, x2, x3, x4, x5)  =  U13_AGAG(x2, x4, x5)
U14_AGAG(x1, x2, x3, x4, x5)  =  U14_AGAG(x1, x2, x4, x5)
U25_AAG(x1, x2, x3, x4, x5, x6)  =  U25_AAG(x2, x3, x5, x6)
U26_AAG(x1, x2, x3, x4, x5, x6)  =  U26_AAG(x2, x3, x5, x6)
P72_IN_GAAG(x1, x2, x3, x4)  =  P72_IN_GAAG(x1, x4)
U10_GAAG(x1, x2, x3, x4)  =  U10_GAAG(x3, x4)
U27_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_AAG(x2, x3, x6, x7, x8, x9)
U28_AAG(x1, x2, x3, x4, x5, x6)  =  U28_AAG(x2, x4, x5, x6)
U29_AAG(x1, x2, x3, x4, x5, x6)  =  U29_AAG(x2, x3, x5, x6)
U11_GAAG(x1, x2, x3, x4, x5)  =  U11_GAAG(x1, x4, x5)
P79_IN_GAAG(x1, x2, x3, x4)  =  P79_IN_GAAG(x1, x4)
U15_GAAG(x1, x2, x3, x4, x5)  =  U15_GAAG(x1, x4, x5)
U16_GAAG(x1, x2, x3, x4, x5)  =  U16_GAAG(x1, x4, x5)
U17_GAAG(x1, x2, x3, x4, x5)  =  U17_GAAG(x1, x4, x5)
U30_AAG(x1, x2, x3, x4, x5)  =  U30_AAG(x1, x3, x4, x5)
U31_AAG(x1, x2, x3, x4, x5, x6)  =  U31_AAG(x2, x4, x5, x6)
U32_AAG(x1, x2, x3, x4, x5, x6)  =  U32_AAG(x2, x3, x5, x6)
U33_AAG(x1, x2, x3, x4, x5, x6)  =  U33_AAG(x2, x3, x5, x6)
P116_IN_GAAG(x1, x2, x3, x4)  =  P116_IN_GAAG(x1, x4)
U18_GAAG(x1, x2, x3, x4)  =  U18_GAAG(x3, x4)
U34_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_AAG(x2, x3, x6, x7, x8, x9)
U35_AAG(x1, x2, x3, x4, x5, x6)  =  U35_AAG(x2, x4, x5, x6)
U36_AAG(x1, x2, x3, x4, x5, x6)  =  U36_AAG(x2, x3, x5, x6)
U19_GAAG(x1, x2, x3, x4, x5)  =  U19_GAAG(x1, x4, x5)
U37_AAG(x1, x2, x3, x4, x5)  =  U37_AAG(x1, x3, x4, x5)
U38_AAG(x1, x2, x3, x4, x5, x6)  =  U38_AAG(x2, x4, x5, x6)
U39_AAG(x1, x2, x3, x4, x5, x6)  =  U39_AAG(x2, x3, x5, x6)
U40_AAG(x1, x2, x3, x4, x5)  =  U40_AAG(x2, x4, x5)
U41_AAG(x1, x2, x3, x4, x5, x6)  =  U41_AAG(x2, x3, x5, x6)
U42_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U42_AAG(x2, x3, x6, x7, x8, x9)
U43_AAG(x1, x2, x3, x4, x5, x6)  =  U43_AAG(x2, x4, x5, x6)
U44_AAG(x1, x2, x3, x4, x5, x6)  =  U44_AAG(x2, x3, x5, x6)
U45_AAG(x1, x2, x3, x4, x5)  =  U45_AAG(x1, x3, x4, x5)
U46_AAG(x1, x2, x3, x4, x5, x6)  =  U46_AAG(x2, x4, x5, x6)
U47_AAG(x1, x2, x3, x4, x5, x6)  =  U47_AAG(x2, x3, x5, x6)
U48_AAG(x1, x2, x3, x4, x5)  =  U48_AAG(x2, x4, x5)
U49_AAG(x1, x2, x3, x4, x5, x6)  =  U49_AAG(x2, x3, x5, x6)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

DELETE1_IN_AAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_AAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_AAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → U1_AGG(T90, T96, T92, T93, T94, T95, delmin19_in_agg(T96, T93, T94))
DELMIN19_IN_AGG(tree(T90, T96, T92), T93, tree(T90, T94, T95)) → DELMIN19_IN_AGG(T96, T93, T94)
DELETE1_IN_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_AAG(T126, T122, T127, T124, T125, p32_in_agag(T126, T122, T127, T125))
DELETE1_IN_AAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_AGAG(T126, T122, T127, T125)
P32_IN_AGAG(T126, T122, T127, T125) → U7_AGAG(T126, T122, T127, T125, less34_in_ag(T126, T122))
P32_IN_AGAG(T126, T122, T127, T125) → LESS34_IN_AG(T126, T122)
LESS34_IN_AG(s(T145), s(T144)) → U2_AG(T145, T144, less34_in_ag(T145, T144))
LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)
P32_IN_AGAG(T130, T122, T131, T125) → U8_AGAG(T130, T122, T131, T125, lessc34_in_ag(T130, T122))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → U9_AGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_AGAG(T130, T122, T131, T125, lessc34_out_ag(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → U20_GAG(T17, T18, T57, T63, T59, T60, T61, T62, delmin19_in_agg(T63, T60, T61))
DELETE1_IN_GAG(T17, tree(T17, T18, tree(T57, T63, T59)), tree(T60, T18, tree(T57, T61, T62))) → DELMIN19_IN_AGG(T63, T60, T61)
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → U21_GAG(T126, T122, T127, T124, T125, p32_in_ggag(T126, T122, T127, T125))
DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T126, T122, T127, T125) → U7_GGAG(T126, T122, T127, T125, less34_in_gg(T126, T122))
P32_IN_GGAG(T126, T122, T127, T125) → LESS34_IN_GG(T126, T122)
LESS34_IN_GG(s(T145), s(T144)) → U2_GG(T145, T144, less34_in_gg(T145, T144))
LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → U9_GGAG(T130, T122, T131, T125, delete1_in_gag(T130, T131, T125))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_GAG(T167, T163, T164, T168, T166, p44_in_ggag(T163, T167, T168, T166))
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T167, T168, T166) → U4_GGAG(T163, T167, T168, T166, less46_in_gg(T163, T167))
P44_IN_GGAG(T163, T167, T168, T166) → LESS46_IN_GG(T163, T167)
LESS46_IN_GG(s(T184), s(T186)) → U3_GG(T184, T186, less46_in_gg(T184, T186))
LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → U6_GGAG(T163, T171, T172, T166, delete1_in_gag(T171, T172, T166))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_GAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_GAG(T223, T222, T224, T201, T202, p65_in_ggag(T223, T222, T224, T202))
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T223, T222, T224, T202) → U12_GGAG(T223, T222, T224, T202, less34_in_gg(T223, T222))
P65_IN_GGAG(T223, T222, T224, T202) → LESS34_IN_GG(T223, T222)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → U14_GGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_GAG(T250, T246, T247, T251, T249, p44_in_ggag(T246, T250, T251, T249))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_GAG(T264, T260, T261, T265, T263, p72_in_ggag(T260, T264, T265, T263))
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → U10_GGAG(T272, T271, T263, delete1_in_gag(s(T272), T271, T263))
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_GAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_GAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_GAG(T376, T372, T377, T374, T375, p32_in_ggag(T376, T372, T377, T375))
DELETE1_IN_GAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_GAG(T395, T391, T392, T396, T394, p72_in_ggag(T391, T395, T396, T394))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → U11_GGAG(T281, T283, T284, T263, p79_in_ggag(T281, T283, T284, T263))
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)
P79_IN_GGAG(T281, T283, T284, T263) → U15_GGAG(T281, T283, T284, T263, less46_in_gg(T281, T283))
P79_IN_GGAG(T281, T283, T284, T263) → LESS46_IN_GG(T281, T283)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → U17_GGAG(T281, T287, T288, T263, delete1_in_gag(s(T287), T288, T263))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
DELETE1_IN_GAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_GAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_GAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_GAG(T429, T428, T430, T407, T408, p65_in_ggag(T429, T428, T430, T408))
DELETE1_IN_GAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_GAG(T448, T444, T445, T449, T447, p72_in_ggag(T444, T448, T449, T447))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_GAG(T462, T458, T459, T463, T461, p116_in_ggag(T458, T462, T463, T461))
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → U18_GGAG(T470, T469, T461, delete1_in_gag(s(T470), T469, T461))
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_GAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_GAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_GAG(T570, T566, T571, T568, T569, p32_in_ggag(T570, T566, T571, T569))
DELETE1_IN_GAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_GAG(T589, T585, T586, T590, T588, p116_in_ggag(T585, T589, T590, T588))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → U19_GGAG(T479, T481, T482, T461, p79_in_ggag(T479, T481, T482, T461))
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
DELETE1_IN_GAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_GAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_GAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_GAG(T623, T622, T624, T601, T602, p65_in_ggag(T623, T622, T624, T602))
DELETE1_IN_GAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_GAG(T642, T638, T639, T643, T641, p116_in_ggag(T638, T642, T643, T641))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_GAG(T664, T653, T663, T655, delete1_in_gag(s(T664), T663, T655))
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_GAG(T675, T673, T653, T676, T655, p79_in_ggag(T673, T675, T676, T655))
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
DELETE1_IN_GAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_GAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_GAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_GAG(T760, T756, T761, T758, T759, p32_in_ggag(T760, T756, T761, T759))
DELETE1_IN_GAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_GAG(T779, T775, T776, T780, T778, p116_in_ggag(T775, T779, T780, T778))
DELETE1_IN_GAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_GAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_GAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_GAG(T813, T812, T814, T791, T792, p65_in_ggag(T813, T812, T814, T792))
DELETE1_IN_GAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_GAG(T832, T828, T829, T833, T831, p116_in_ggag(T828, T832, T833, T831))
DELETE1_IN_GAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_GAG(T854, T843, T853, T845, delete1_in_gag(s(T854), T853, T845))
DELETE1_IN_GAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_GAG(T865, T863, T843, T866, T845, p79_in_ggag(T863, T865, T866, T845))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → U22_AAG(T167, T163, T164, T168, T166, p44_in_gaag(T163, T167, T168, T166))
DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T167, T168, T166) → U4_GAAG(T163, T167, T168, T166, less46_in_ga(T163, T167))
P44_IN_GAAG(T163, T167, T168, T166) → LESS46_IN_GA(T163, T167)
LESS46_IN_GA(s(T184), s(T186)) → U3_GA(T184, T186, less46_in_ga(T184, T186))
LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → U6_GAAG(T163, T171, T172, T166, delete1_in_aag(T171, T172, T166))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → U23_AAG(T209, T210, T201, T202, delete1_in_gag(0, T210, T202))
DELETE1_IN_AAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → U24_AAG(T223, T222, T224, T201, T202, p65_in_agag(T223, T222, T224, T202))
DELETE1_IN_AAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_AGAG(T223, T222, T224, T202)
P65_IN_AGAG(T223, T222, T224, T202) → U12_AGAG(T223, T222, T224, T202, less34_in_ag(T223, T222))
P65_IN_AGAG(T223, T222, T224, T202) → LESS34_IN_AG(T223, T222)
P65_IN_AGAG(T227, T222, T228, T202) → U13_AGAG(T227, T222, T228, T202, lessc34_in_ag(T227, T222))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → U14_AGAG(T227, T222, T228, T202, delete1_in_gag(s(T227), T228, T202))
U13_AGAG(T227, T222, T228, T202, lessc34_out_ag(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_AAG(T250, tree(T246, T247, T251), tree(T246, T247, T249)) → U25_AAG(T250, T246, T247, T251, T249, p44_in_gaag(T246, T250, T251, T249))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → U26_AAG(T264, T260, T261, T265, T263, p72_in_gaag(T260, T264, T265, T263))
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → U10_GAAG(T272, T271, T263, delete1_in_aag(s(T272), T271, T263))
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T300, tree(T300, T301, tree(T340, T346, T342)), tree(T343, T301, tree(T340, T344, T345))) → U27_AAG(T300, T301, T340, T346, T342, T343, T344, T345, delmin19_in_agg(T346, T343, T344))
DELETE1_IN_AAG(T376, tree(T372, T377, T374), tree(T372, T375, T374)) → U28_AAG(T376, T372, T377, T374, T375, p32_in_agag(T376, T372, T377, T375))
DELETE1_IN_AAG(T395, tree(T391, T392, T396), tree(T391, T392, T394)) → U29_AAG(T395, T391, T392, T396, T394, p72_in_gaag(T391, T395, T396, T394))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → U11_GAAG(T281, T283, T284, T263, p79_in_gaag(T281, T283, T284, T263))
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)
P79_IN_GAAG(T281, T283, T284, T263) → U15_GAAG(T281, T283, T284, T263, less46_in_ga(T281, T283))
P79_IN_GAAG(T281, T283, T284, T263) → LESS46_IN_GA(T281, T283)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → U17_GAAG(T281, T287, T288, T263, delete1_in_aag(s(T287), T288, T263))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
DELETE1_IN_AAG(0, tree(s(T415), T416, T407), tree(s(T415), T408, T407)) → U30_AAG(T415, T416, T407, T408, delete1_in_gag(0, T416, T408))
DELETE1_IN_AAG(s(T429), tree(s(T428), T430, T407), tree(s(T428), T408, T407)) → U31_AAG(T429, T428, T430, T407, T408, p65_in_agag(T429, T428, T430, T408))
DELETE1_IN_AAG(T448, tree(T444, T445, T449), tree(T444, T445, T447)) → U32_AAG(T448, T444, T445, T449, T447, p72_in_gaag(T444, T448, T449, T447))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → U33_AAG(T462, T458, T459, T463, T461, p116_in_gaag(T458, T462, T463, T461))
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → U18_GAAG(T470, T469, T461, delete1_in_aag(s(T470), T469, T461))
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(T494, tree(T494, T495, tree(T534, T540, T536)), tree(T537, T495, tree(T534, T538, T539))) → U34_AAG(T494, T495, T534, T540, T536, T537, T538, T539, delmin19_in_agg(T540, T537, T538))
DELETE1_IN_AAG(T570, tree(T566, T571, T568), tree(T566, T569, T568)) → U35_AAG(T570, T566, T571, T568, T569, p32_in_agag(T570, T566, T571, T569))
DELETE1_IN_AAG(T589, tree(T585, T586, T590), tree(T585, T586, T588)) → U36_AAG(T589, T585, T586, T590, T588, p116_in_gaag(T585, T589, T590, T588))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → U19_GAAG(T479, T481, T482, T461, p79_in_gaag(T479, T481, T482, T461))
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
DELETE1_IN_AAG(0, tree(s(T609), T610, T601), tree(s(T609), T602, T601)) → U37_AAG(T609, T610, T601, T602, delete1_in_gag(0, T610, T602))
DELETE1_IN_AAG(s(T623), tree(s(T622), T624, T601), tree(s(T622), T602, T601)) → U38_AAG(T623, T622, T624, T601, T602, p65_in_agag(T623, T622, T624, T602))
DELETE1_IN_AAG(T642, tree(T638, T639, T643), tree(T638, T639, T641)) → U39_AAG(T642, T638, T639, T643, T641, p116_in_gaag(T638, T642, T643, T641))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → U40_AAG(T664, T653, T663, T655, delete1_in_aag(s(T664), T663, T655))
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → U41_AAG(T675, T673, T653, T676, T655, p79_in_gaag(T673, T675, T676, T655))
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
DELETE1_IN_AAG(T684, tree(T684, T685, tree(T724, T730, T726)), tree(T727, T685, tree(T724, T728, T729))) → U42_AAG(T684, T685, T724, T730, T726, T727, T728, T729, delmin19_in_agg(T730, T727, T728))
DELETE1_IN_AAG(T760, tree(T756, T761, T758), tree(T756, T759, T758)) → U43_AAG(T760, T756, T761, T758, T759, p32_in_agag(T760, T756, T761, T759))
DELETE1_IN_AAG(T779, tree(T775, T776, T780), tree(T775, T776, T778)) → U44_AAG(T779, T775, T776, T780, T778, p116_in_gaag(T775, T779, T780, T778))
DELETE1_IN_AAG(0, tree(s(T799), T800, T791), tree(s(T799), T792, T791)) → U45_AAG(T799, T800, T791, T792, delete1_in_gag(0, T800, T792))
DELETE1_IN_AAG(s(T813), tree(s(T812), T814, T791), tree(s(T812), T792, T791)) → U46_AAG(T813, T812, T814, T791, T792, p65_in_agag(T813, T812, T814, T792))
DELETE1_IN_AAG(T832, tree(T828, T829, T833), tree(T828, T829, T831)) → U47_AAG(T832, T828, T829, T833, T831, p116_in_gaag(T828, T832, T833, T831))
DELETE1_IN_AAG(s(T854), tree(0, T843, T853), tree(0, T843, T845)) → U48_AAG(T854, T843, T853, T845, delete1_in_aag(s(T854), T853, T845))
DELETE1_IN_AAG(s(T865), tree(s(T863), T843, T866), tree(s(T863), T843, T845)) → U49_AAG(T865, T863, T843, T866, T845, p79_in_gaag(T863, T865, T866, T845))

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
delete1_in_aag(x1, x2, x3)  =  delete1_in_aag(x3)
tree(x1, x2, x3)  =  tree(x1, x2, x3)
delmin19_in_agg(x1, x2, x3)  =  delmin19_in_agg(x2, x3)
p32_in_agag(x1, x2, x3, x4)  =  p32_in_agag(x2, x4)
less34_in_ag(x1, x2)  =  less34_in_ag(x2)
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
delete1_in_gag(x1, x2, x3)  =  delete1_in_gag(x1, x3)
p32_in_ggag(x1, x2, x3, x4)  =  p32_in_ggag(x1, x2, x4)
less34_in_gg(x1, x2)  =  less34_in_gg(x1, x2)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
p44_in_ggag(x1, x2, x3, x4)  =  p44_in_ggag(x1, x2, x4)
less46_in_gg(x1, x2)  =  less46_in_gg(x1, x2)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
p65_in_ggag(x1, x2, x3, x4)  =  p65_in_ggag(x1, x2, x4)
p72_in_ggag(x1, x2, x3, x4)  =  p72_in_ggag(x1, x2, x4)
p79_in_ggag(x1, x2, x3, x4)  =  p79_in_ggag(x1, x2, x4)
p116_in_ggag(x1, x2, x3, x4)  =  p116_in_ggag(x1, x2, x4)
p44_in_gaag(x1, x2, x3, x4)  =  p44_in_gaag(x1, x4)
less46_in_ga(x1, x2)  =  less46_in_ga(x1)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
p65_in_agag(x1, x2, x3, x4)  =  p65_in_agag(x2, x4)
p72_in_gaag(x1, x2, x3, x4)  =  p72_in_gaag(x1, x4)
p79_in_gaag(x1, x2, x3, x4)  =  p79_in_gaag(x1, x4)
p116_in_gaag(x1, x2, x3, x4)  =  p116_in_gaag(x1, x4)
DELETE1_IN_AAG(x1, x2, x3)  =  DELETE1_IN_AAG(x3)
U20_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_AAG(x2, x3, x6, x7, x8, x9)
DELMIN19_IN_AGG(x1, x2, x3)  =  DELMIN19_IN_AGG(x2, x3)
U1_AGG(x1, x2, x3, x4, x5, x6, x7)  =  U1_AGG(x1, x4, x5, x6, x7)
U21_AAG(x1, x2, x3, x4, x5, x6)  =  U21_AAG(x2, x4, x5, x6)
P32_IN_AGAG(x1, x2, x3, x4)  =  P32_IN_AGAG(x2, x4)
U7_AGAG(x1, x2, x3, x4, x5)  =  U7_AGAG(x2, x4, x5)
LESS34_IN_AG(x1, x2)  =  LESS34_IN_AG(x2)
U2_AG(x1, x2, x3)  =  U2_AG(x2, x3)
U8_AGAG(x1, x2, x3, x4, x5)  =  U8_AGAG(x2, x4, x5)
U9_AGAG(x1, x2, x3, x4, x5)  =  U9_AGAG(x1, x2, x4, x5)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
U20_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U20_GAG(x1, x2, x3, x6, x7, x8, x9)
U21_GAG(x1, x2, x3, x4, x5, x6)  =  U21_GAG(x1, x2, x4, x5, x6)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U7_GGAG(x1, x2, x3, x4, x5)  =  U7_GGAG(x1, x2, x4, x5)
LESS34_IN_GG(x1, x2)  =  LESS34_IN_GG(x1, x2)
U2_GG(x1, x2, x3)  =  U2_GG(x1, x2, x3)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x1, x2, x4, x5)
U9_GGAG(x1, x2, x3, x4, x5)  =  U9_GGAG(x1, x2, x4, x5)
U22_GAG(x1, x2, x3, x4, x5, x6)  =  U22_GAG(x1, x2, x3, x5, x6)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U4_GGAG(x1, x2, x3, x4, x5)  =  U4_GGAG(x1, x2, x4, x5)
LESS46_IN_GG(x1, x2)  =  LESS46_IN_GG(x1, x2)
U3_GG(x1, x2, x3)  =  U3_GG(x1, x2, x3)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
U6_GGAG(x1, x2, x3, x4, x5)  =  U6_GGAG(x1, x2, x4, x5)
U23_GAG(x1, x2, x3, x4, x5)  =  U23_GAG(x1, x3, x4, x5)
U24_GAG(x1, x2, x3, x4, x5, x6)  =  U24_GAG(x1, x2, x4, x5, x6)
P65_IN_GGAG(x1, x2, x3, x4)  =  P65_IN_GGAG(x1, x2, x4)
U12_GGAG(x1, x2, x3, x4, x5)  =  U12_GGAG(x1, x2, x4, x5)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
U14_GGAG(x1, x2, x3, x4, x5)  =  U14_GGAG(x1, x2, x4, x5)
U25_GAG(x1, x2, x3, x4, x5, x6)  =  U25_GAG(x1, x2, x3, x5, x6)
U26_GAG(x1, x2, x3, x4, x5, x6)  =  U26_GAG(x1, x2, x3, x5, x6)
P72_IN_GGAG(x1, x2, x3, x4)  =  P72_IN_GGAG(x1, x2, x4)
U10_GGAG(x1, x2, x3, x4)  =  U10_GGAG(x1, x3, x4)
U27_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_GAG(x1, x2, x3, x6, x7, x8, x9)
U28_GAG(x1, x2, x3, x4, x5, x6)  =  U28_GAG(x1, x2, x4, x5, x6)
U29_GAG(x1, x2, x3, x4, x5, x6)  =  U29_GAG(x1, x2, x3, x5, x6)
U11_GGAG(x1, x2, x3, x4, x5)  =  U11_GGAG(x1, x2, x4, x5)
P79_IN_GGAG(x1, x2, x3, x4)  =  P79_IN_GGAG(x1, x2, x4)
U15_GGAG(x1, x2, x3, x4, x5)  =  U15_GGAG(x1, x2, x4, x5)
U16_GGAG(x1, x2, x3, x4, x5)  =  U16_GGAG(x1, x2, x4, x5)
U17_GGAG(x1, x2, x3, x4, x5)  =  U17_GGAG(x1, x2, x4, x5)
U30_GAG(x1, x2, x3, x4, x5)  =  U30_GAG(x1, x3, x4, x5)
U31_GAG(x1, x2, x3, x4, x5, x6)  =  U31_GAG(x1, x2, x4, x5, x6)
U32_GAG(x1, x2, x3, x4, x5, x6)  =  U32_GAG(x1, x2, x3, x5, x6)
U33_GAG(x1, x2, x3, x4, x5, x6)  =  U33_GAG(x1, x2, x3, x5, x6)
P116_IN_GGAG(x1, x2, x3, x4)  =  P116_IN_GGAG(x1, x2, x4)
U18_GGAG(x1, x2, x3, x4)  =  U18_GGAG(x1, x3, x4)
U34_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_GAG(x1, x2, x3, x6, x7, x8, x9)
U35_GAG(x1, x2, x3, x4, x5, x6)  =  U35_GAG(x1, x2, x4, x5, x6)
U36_GAG(x1, x2, x3, x4, x5, x6)  =  U36_GAG(x1, x2, x3, x5, x6)
U19_GGAG(x1, x2, x3, x4, x5)  =  U19_GGAG(x1, x2, x4, x5)
U37_GAG(x1, x2, x3, x4, x5)  =  U37_GAG(x1, x3, x4, x5)
U38_GAG(x1, x2, x3, x4, x5, x6)  =  U38_GAG(x1, x2, x4, x5, x6)
U39_GAG(x1, x2, x3, x4, x5, x6)  =  U39_GAG(x1, x2, x3, x5, x6)
U40_GAG(x1, x2, x3, x4, x5)  =  U40_GAG(x1, x2, x4, x5)
U41_GAG(x1, x2, x3, x4, x5, x6)  =  U41_GAG(x1, x2, x3, x5, x6)
U42_GAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U42_GAG(x1, x2, x3, x6, x7, x8, x9)
U43_GAG(x1, x2, x3, x4, x5, x6)  =  U43_GAG(x1, x2, x4, x5, x6)
U44_GAG(x1, x2, x3, x4, x5, x6)  =  U44_GAG(x1, x2, x3, x5, x6)
U45_GAG(x1, x2, x3, x4, x5)  =  U45_GAG(x1, x3, x4, x5)
U46_GAG(x1, x2, x3, x4, x5, x6)  =  U46_GAG(x1, x2, x4, x5, x6)
U47_GAG(x1, x2, x3, x4, x5, x6)  =  U47_GAG(x1, x2, x3, x5, x6)
U48_GAG(x1, x2, x3, x4, x5)  =  U48_GAG(x1, x2, x4, x5)
U49_GAG(x1, x2, x3, x4, x5, x6)  =  U49_GAG(x1, x2, x3, x5, x6)
U22_AAG(x1, x2, x3, x4, x5, x6)  =  U22_AAG(x2, x3, x5, x6)
P44_IN_GAAG(x1, x2, x3, x4)  =  P44_IN_GAAG(x1, x4)
U4_GAAG(x1, x2, x3, x4, x5)  =  U4_GAAG(x1, x4, x5)
LESS46_IN_GA(x1, x2)  =  LESS46_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U5_GAAG(x1, x2, x3, x4, x5)  =  U5_GAAG(x1, x4, x5)
U6_GAAG(x1, x2, x3, x4, x5)  =  U6_GAAG(x1, x4, x5)
U23_AAG(x1, x2, x3, x4, x5)  =  U23_AAG(x1, x3, x4, x5)
U24_AAG(x1, x2, x3, x4, x5, x6)  =  U24_AAG(x2, x4, x5, x6)
P65_IN_AGAG(x1, x2, x3, x4)  =  P65_IN_AGAG(x2, x4)
U12_AGAG(x1, x2, x3, x4, x5)  =  U12_AGAG(x2, x4, x5)
U13_AGAG(x1, x2, x3, x4, x5)  =  U13_AGAG(x2, x4, x5)
U14_AGAG(x1, x2, x3, x4, x5)  =  U14_AGAG(x1, x2, x4, x5)
U25_AAG(x1, x2, x3, x4, x5, x6)  =  U25_AAG(x2, x3, x5, x6)
U26_AAG(x1, x2, x3, x4, x5, x6)  =  U26_AAG(x2, x3, x5, x6)
P72_IN_GAAG(x1, x2, x3, x4)  =  P72_IN_GAAG(x1, x4)
U10_GAAG(x1, x2, x3, x4)  =  U10_GAAG(x3, x4)
U27_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U27_AAG(x2, x3, x6, x7, x8, x9)
U28_AAG(x1, x2, x3, x4, x5, x6)  =  U28_AAG(x2, x4, x5, x6)
U29_AAG(x1, x2, x3, x4, x5, x6)  =  U29_AAG(x2, x3, x5, x6)
U11_GAAG(x1, x2, x3, x4, x5)  =  U11_GAAG(x1, x4, x5)
P79_IN_GAAG(x1, x2, x3, x4)  =  P79_IN_GAAG(x1, x4)
U15_GAAG(x1, x2, x3, x4, x5)  =  U15_GAAG(x1, x4, x5)
U16_GAAG(x1, x2, x3, x4, x5)  =  U16_GAAG(x1, x4, x5)
U17_GAAG(x1, x2, x3, x4, x5)  =  U17_GAAG(x1, x4, x5)
U30_AAG(x1, x2, x3, x4, x5)  =  U30_AAG(x1, x3, x4, x5)
U31_AAG(x1, x2, x3, x4, x5, x6)  =  U31_AAG(x2, x4, x5, x6)
U32_AAG(x1, x2, x3, x4, x5, x6)  =  U32_AAG(x2, x3, x5, x6)
U33_AAG(x1, x2, x3, x4, x5, x6)  =  U33_AAG(x2, x3, x5, x6)
P116_IN_GAAG(x1, x2, x3, x4)  =  P116_IN_GAAG(x1, x4)
U18_GAAG(x1, x2, x3, x4)  =  U18_GAAG(x3, x4)
U34_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U34_AAG(x2, x3, x6, x7, x8, x9)
U35_AAG(x1, x2, x3, x4, x5, x6)  =  U35_AAG(x2, x4, x5, x6)
U36_AAG(x1, x2, x3, x4, x5, x6)  =  U36_AAG(x2, x3, x5, x6)
U19_GAAG(x1, x2, x3, x4, x5)  =  U19_GAAG(x1, x4, x5)
U37_AAG(x1, x2, x3, x4, x5)  =  U37_AAG(x1, x3, x4, x5)
U38_AAG(x1, x2, x3, x4, x5, x6)  =  U38_AAG(x2, x4, x5, x6)
U39_AAG(x1, x2, x3, x4, x5, x6)  =  U39_AAG(x2, x3, x5, x6)
U40_AAG(x1, x2, x3, x4, x5)  =  U40_AAG(x2, x4, x5)
U41_AAG(x1, x2, x3, x4, x5, x6)  =  U41_AAG(x2, x3, x5, x6)
U42_AAG(x1, x2, x3, x4, x5, x6, x7, x8, x9)  =  U42_AAG(x2, x3, x6, x7, x8, x9)
U43_AAG(x1, x2, x3, x4, x5, x6)  =  U43_AAG(x2, x4, x5, x6)
U44_AAG(x1, x2, x3, x4, x5, x6)  =  U44_AAG(x2, x3, x5, x6)
U45_AAG(x1, x2, x3, x4, x5)  =  U45_AAG(x1, x3, x4, x5)
U46_AAG(x1, x2, x3, x4, x5, x6)  =  U46_AAG(x2, x4, x5, x6)
U47_AAG(x1, x2, x3, x4, x5, x6)  =  U47_AAG(x2, x3, x5, x6)
U48_AAG(x1, x2, x3, x4, x5)  =  U48_AAG(x2, x4, x5)
U49_AAG(x1, x2, x3, x4, x5, x6)  =  U49_AAG(x2, x3, x5, x6)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

(7) Obligation:

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

LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
LESS46_IN_GA(x1, x2)  =  LESS46_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

LESS46_IN_GA(s(T184), s(T186)) → LESS46_IN_GA(T184, T186)

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

LESS46_IN_GA(s(T184)) → LESS46_IN_GA(T184)

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS46_IN_GA(s(T184)) → LESS46_IN_GA(T184)
    The graph contains the following edges 1 > 1

(13) YES

(14) Obligation:

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

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
LESS46_IN_GG(x1, x2)  =  LESS46_IN_GG(x1, x2)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)

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

(17) PiDPToQDPProof (EQUIVALENT transformation)

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

(18) Obligation:

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

LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS46_IN_GG(s(T184), s(T186)) → LESS46_IN_GG(T184, T186)
    The graph contains the following edges 1 > 1, 2 > 2

(20) YES

(21) Obligation:

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

LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
LESS34_IN_GG(x1, x2)  =  LESS34_IN_GG(x1, x2)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)

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

(24) PiDPToQDPProof (EQUIVALENT transformation)

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

(25) Obligation:

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

LESS34_IN_GG(s(T145), s(T144)) → LESS34_IN_GG(T145, T144)

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

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(27) YES

(28) Obligation:

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

LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
LESS34_IN_AG(x1, x2)  =  LESS34_IN_AG(x2)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

LESS34_IN_AG(s(T145), s(T144)) → LESS34_IN_AG(T145, T144)

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

LESS34_IN_AG(s(T144)) → LESS34_IN_AG(T144)

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • LESS34_IN_AG(s(T144)) → LESS34_IN_AG(T144)
    The graph contains the following edges 1 > 1

(34) YES

(35) Obligation:

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

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

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
DELMIN19_IN_AGG(x1, x2, x3)  =  DELMIN19_IN_AGG(x2, x3)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

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

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

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

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

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

(40) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(41) YES

(42) Obligation:

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

DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x1, x2, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
P65_IN_GGAG(x1, x2, x3, x4)  =  P65_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
P72_IN_GGAG(x1, x2, x3, x4)  =  P72_IN_GGAG(x1, x2, x4)
P79_IN_GGAG(x1, x2, x3, x4)  =  P79_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5)  =  U16_GGAG(x1, x2, x4, x5)
P116_IN_GGAG(x1, x2, x3, x4)  =  P116_IN_GGAG(x1, x2, x4)

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

(43) UsableRulesProof (EQUIVALENT transformation)

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

(44) Obligation:

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

DELETE1_IN_GAG(T126, tree(T122, T127, T124), tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T127, T125)
P32_IN_GGAG(T130, T122, T131, T125) → U8_GGAG(T130, T122, T131, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T131, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T131, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T168, T166)
P44_IN_GGAG(T163, T171, T172, T166) → U5_GGAG(T163, T171, T172, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T172, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T172, T166)
DELETE1_IN_GAG(0, tree(s(T209), T210, T201), tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T210, T202)
DELETE1_IN_GAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T265, T263)
P72_IN_GGAG(0, s(T272), T271, T263) → DELETE1_IN_GAG(s(T272), T271, T263)
DELETE1_IN_GAG(s(T223), tree(s(T222), T224, T201), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T224, T202)
P65_IN_GGAG(T227, T222, T228, T202) → U13_GGAG(T227, T222, T228, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T228, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T228, T202)
DELETE1_IN_GAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T463, T461)
P116_IN_GGAG(0, s(T470), T469, T461) → DELETE1_IN_GAG(s(T470), T469, T461)
DELETE1_IN_GAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T663, T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T676, T655)
P79_IN_GGAG(T281, T287, T288, T263) → U16_GGAG(T281, T287, T288, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T288, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T288, T263)
P116_IN_GGAG(s(T479), s(T481), T482, T461) → P79_IN_GGAG(T479, T481, T482, T461)
P72_IN_GGAG(s(T281), s(T283), T284, T263) → P79_IN_GGAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
DELETE1_IN_GAG(x1, x2, x3)  =  DELETE1_IN_GAG(x1, x3)
P32_IN_GGAG(x1, x2, x3, x4)  =  P32_IN_GGAG(x1, x2, x4)
U8_GGAG(x1, x2, x3, x4, x5)  =  U8_GGAG(x1, x2, x4, x5)
P44_IN_GGAG(x1, x2, x3, x4)  =  P44_IN_GGAG(x1, x2, x4)
U5_GGAG(x1, x2, x3, x4, x5)  =  U5_GGAG(x1, x2, x4, x5)
P65_IN_GGAG(x1, x2, x3, x4)  =  P65_IN_GGAG(x1, x2, x4)
U13_GGAG(x1, x2, x3, x4, x5)  =  U13_GGAG(x1, x2, x4, x5)
P72_IN_GGAG(x1, x2, x3, x4)  =  P72_IN_GGAG(x1, x2, x4)
P79_IN_GGAG(x1, x2, x3, x4)  =  P79_IN_GGAG(x1, x2, x4)
U16_GGAG(x1, x2, x3, x4, x5)  =  U16_GGAG(x1, x2, x4, x5)
P116_IN_GGAG(x1, x2, x3, x4)  =  P116_IN_GGAG(x1, x2, x4)

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

(45) PiDPToQDPProof (SOUND transformation)

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

(46) Obligation:

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

DELETE1_IN_GAG(T126, tree(T122, T125, T124)) → P32_IN_GGAG(T126, T122, T125)
P32_IN_GGAG(T130, T122, T125) → U8_GGAG(T130, T122, T125, lessc34_in_gg(T130, T122))
U8_GGAG(T130, T122, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T125)
DELETE1_IN_GAG(T167, tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T166)
P44_IN_GGAG(T163, T171, T166) → U5_GGAG(T163, T171, T166, lessc46_in_gg(T163, T171))
U5_GGAG(T163, T171, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T166)
DELETE1_IN_GAG(0, tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T202)
DELETE1_IN_GAG(T264, tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T263)
P72_IN_GGAG(0, s(T272), T263) → DELETE1_IN_GAG(s(T272), T263)
DELETE1_IN_GAG(s(T223), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T202)
P65_IN_GGAG(T227, T222, T202) → U13_GGAG(T227, T222, T202, lessc34_in_gg(T227, T222))
U13_GGAG(T227, T222, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T202)
DELETE1_IN_GAG(T462, tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T461)
P116_IN_GGAG(0, s(T470), T461) → DELETE1_IN_GAG(s(T470), T461)
DELETE1_IN_GAG(s(T664), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T655)
DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T655)
P79_IN_GGAG(T281, T287, T263) → U16_GGAG(T281, T287, T263, lessc46_in_gg(T281, T287))
U16_GGAG(T281, T287, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T263)
P116_IN_GGAG(s(T479), s(T481), T461) → P79_IN_GGAG(T479, T481, T461)
P72_IN_GGAG(s(T281), s(T283), T263) → P79_IN_GGAG(T281, T283, T263)

The TRS R consists of the following rules:

lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))

The set Q consists of the following terms:

lessc34_in_gg(x0, x1)
lessc46_in_gg(x0, x1)
U82_gg(x0, x1, x2)
U83_gg(x0, x1, x2)

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

(47) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • P32_IN_GGAG(T130, T122, T125) → U8_GGAG(T130, T122, T125, lessc34_in_gg(T130, T122))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U8_GGAG(T130, T122, T125, lessc34_out_gg(T130, T122)) → DELETE1_IN_GAG(T130, T125)
    The graph contains the following edges 1 >= 1, 4 > 1, 3 >= 2

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

  • P44_IN_GGAG(T163, T171, T166) → U5_GGAG(T163, T171, T166, lessc46_in_gg(T163, T171))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U5_GGAG(T163, T171, T166, lessc46_out_gg(T163, T171)) → DELETE1_IN_GAG(T171, T166)
    The graph contains the following edges 2 >= 1, 4 > 1, 3 >= 2

  • DELETE1_IN_GAG(T167, tree(T163, T164, T166)) → P44_IN_GGAG(T163, T167, T166)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • DELETE1_IN_GAG(0, tree(s(T209), T202, T201)) → DELETE1_IN_GAG(0, T202)
    The graph contains the following edges 1 >= 1, 2 > 2

  • DELETE1_IN_GAG(s(T664), tree(0, T653, T655)) → DELETE1_IN_GAG(s(T664), T655)
    The graph contains the following edges 1 >= 1, 2 > 2

  • P72_IN_GGAG(0, s(T272), T263) → DELETE1_IN_GAG(s(T272), T263)
    The graph contains the following edges 2 >= 1, 3 >= 2

  • P72_IN_GGAG(s(T281), s(T283), T263) → P79_IN_GGAG(T281, T283, T263)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • DELETE1_IN_GAG(T264, tree(T260, T261, T263)) → P72_IN_GGAG(T260, T264, T263)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • DELETE1_IN_GAG(T462, tree(T458, T459, T461)) → P116_IN_GGAG(T458, T462, T461)
    The graph contains the following edges 2 > 1, 1 >= 2, 2 > 3

  • P65_IN_GGAG(T227, T222, T202) → U13_GGAG(T227, T222, T202, lessc34_in_gg(T227, T222))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

  • U13_GGAG(T227, T222, T202, lessc34_out_gg(T227, T222)) → DELETE1_IN_GAG(s(T227), T202)
    The graph contains the following edges 3 >= 2

  • DELETE1_IN_GAG(s(T223), tree(s(T222), T202, T201)) → P65_IN_GGAG(T223, T222, T202)
    The graph contains the following edges 1 > 1, 2 > 2, 2 > 3

  • DELETE1_IN_GAG(s(T675), tree(s(T673), T653, T655)) → P79_IN_GGAG(T673, T675, T655)
    The graph contains the following edges 2 > 1, 1 > 2, 2 > 3

  • P116_IN_GGAG(0, s(T470), T461) → DELETE1_IN_GAG(s(T470), T461)
    The graph contains the following edges 2 >= 1, 3 >= 2

  • U16_GGAG(T281, T287, T263, lessc46_out_gg(T281, T287)) → DELETE1_IN_GAG(s(T287), T263)
    The graph contains the following edges 3 >= 2

  • P116_IN_GGAG(s(T479), s(T481), T461) → P79_IN_GGAG(T479, T481, T461)
    The graph contains the following edges 1 > 1, 2 > 2, 3 >= 3

  • P79_IN_GGAG(T281, T287, T263) → U16_GGAG(T281, T287, T263, lessc46_in_gg(T281, T287))
    The graph contains the following edges 1 >= 1, 2 >= 2, 3 >= 3

(48) YES

(49) Obligation:

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

DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc34_in_ag(0, s(T138)) → lessc34_out_ag(0, s(T138))
lessc34_in_ag(s(T145), s(T144)) → U82_ag(T145, T144, lessc34_in_ag(T145, T144))
U82_ag(T145, T144, lessc34_out_ag(T145, T144)) → lessc34_out_ag(s(T145), s(T144))
lessc34_in_gg(0, s(T138)) → lessc34_out_gg(0, s(T138))
lessc34_in_gg(s(T145), s(T144)) → U82_gg(T145, T144, lessc34_in_gg(T145, T144))
U82_gg(T145, T144, lessc34_out_gg(T145, T144)) → lessc34_out_gg(s(T145), s(T144))
lessc46_in_gg(0, s(T179)) → lessc46_out_gg(0, s(T179))
lessc46_in_gg(s(T184), s(T186)) → U83_gg(T184, T186, lessc46_in_gg(T184, T186))
U83_gg(T184, T186, lessc46_out_gg(T184, T186)) → lessc46_out_gg(s(T184), s(T186))
lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
lessc34_in_ag(x1, x2)  =  lessc34_in_ag(x2)
lessc34_out_ag(x1, x2)  =  lessc34_out_ag(x1, x2)
U82_ag(x1, x2, x3)  =  U82_ag(x2, x3)
lessc34_in_gg(x1, x2)  =  lessc34_in_gg(x1, x2)
0  =  0
lessc34_out_gg(x1, x2)  =  lessc34_out_gg(x1, x2)
U82_gg(x1, x2, x3)  =  U82_gg(x1, x2, x3)
lessc46_in_gg(x1, x2)  =  lessc46_in_gg(x1, x2)
lessc46_out_gg(x1, x2)  =  lessc46_out_gg(x1, x2)
U83_gg(x1, x2, x3)  =  U83_gg(x1, x2, x3)
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
DELETE1_IN_AAG(x1, x2, x3)  =  DELETE1_IN_AAG(x3)
P44_IN_GAAG(x1, x2, x3, x4)  =  P44_IN_GAAG(x1, x4)
U5_GAAG(x1, x2, x3, x4, x5)  =  U5_GAAG(x1, x4, x5)
P72_IN_GAAG(x1, x2, x3, x4)  =  P72_IN_GAAG(x1, x4)
P79_IN_GAAG(x1, x2, x3, x4)  =  P79_IN_GAAG(x1, x4)
U16_GAAG(x1, x2, x3, x4, x5)  =  U16_GAAG(x1, x4, x5)
P116_IN_GAAG(x1, x2, x3, x4)  =  P116_IN_GAAG(x1, x4)

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

(50) UsableRulesProof (EQUIVALENT transformation)

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

(51) Obligation:

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

DELETE1_IN_AAG(T167, tree(T163, T164, T168), tree(T163, T164, T166)) → P44_IN_GAAG(T163, T167, T168, T166)
P44_IN_GAAG(T163, T171, T172, T166) → U5_GAAG(T163, T171, T172, T166, lessc46_in_ga(T163, T171))
U5_GAAG(T163, T171, T172, T166, lessc46_out_ga(T163, T171)) → DELETE1_IN_AAG(T171, T172, T166)
DELETE1_IN_AAG(T264, tree(T260, T261, T265), tree(T260, T261, T263)) → P72_IN_GAAG(T260, T264, T265, T263)
P72_IN_GAAG(0, s(T272), T271, T263) → DELETE1_IN_AAG(s(T272), T271, T263)
DELETE1_IN_AAG(T462, tree(T458, T459, T463), tree(T458, T459, T461)) → P116_IN_GAAG(T458, T462, T463, T461)
P116_IN_GAAG(0, s(T470), T469, T461) → DELETE1_IN_AAG(s(T470), T469, T461)
DELETE1_IN_AAG(s(T664), tree(0, T653, T663), tree(0, T653, T655)) → DELETE1_IN_AAG(s(T664), T663, T655)
DELETE1_IN_AAG(s(T675), tree(s(T673), T653, T676), tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T675, T676, T655)
P79_IN_GAAG(T281, T287, T288, T263) → U16_GAAG(T281, T287, T288, T263, lessc46_in_ga(T281, T287))
U16_GAAG(T281, T287, T288, T263, lessc46_out_ga(T281, T287)) → DELETE1_IN_AAG(s(T287), T288, T263)
P116_IN_GAAG(s(T479), s(T481), T482, T461) → P79_IN_GAAG(T479, T481, T482, T461)
P72_IN_GAAG(s(T281), s(T283), T284, T263) → P79_IN_GAAG(T281, T283, T284, T263)

The TRS R consists of the following rules:

lessc46_in_ga(0, s(T179)) → lessc46_out_ga(0, s(T179))
lessc46_in_ga(s(T184), s(T186)) → U83_ga(T184, T186, lessc46_in_ga(T184, T186))
U83_ga(T184, T186, lessc46_out_ga(T184, T186)) → lessc46_out_ga(s(T184), s(T186))

The argument filtering Pi contains the following mapping:
tree(x1, x2, x3)  =  tree(x1, x2, x3)
s(x1)  =  s(x1)
0  =  0
lessc46_in_ga(x1, x2)  =  lessc46_in_ga(x1)
lessc46_out_ga(x1, x2)  =  lessc46_out_ga(x1)
U83_ga(x1, x2, x3)  =  U83_ga(x1, x3)
DELETE1_IN_AAG(x1, x2, x3)  =  DELETE1_IN_AAG(x3)
P44_IN_GAAG(x1, x2, x3, x4)  =  P44_IN_GAAG(x1, x4)
U5_GAAG(x1, x2, x3, x4, x5)  =  U5_GAAG(x1, x4, x5)
P72_IN_GAAG(x1, x2, x3, x4)  =  P72_IN_GAAG(x1, x4)
P79_IN_GAAG(x1, x2, x3, x4)  =  P79_IN_GAAG(x1, x4)
U16_GAAG(x1, x2, x3, x4, x5)  =  U16_GAAG(x1, x4, x5)
P116_IN_GAAG(x1, x2, x3, x4)  =  P116_IN_GAAG(x1, x4)

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

(52) PiDPToQDPProof (SOUND transformation)

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

(53) Obligation:

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

DELETE1_IN_AAG(tree(T163, T164, T166)) → P44_IN_GAAG(T163, T166)
P44_IN_GAAG(T163, T166) → U5_GAAG(T163, T166, lessc46_in_ga(T163))
U5_GAAG(T163, T166, lessc46_out_ga(T163)) → DELETE1_IN_AAG(T166)
DELETE1_IN_AAG(tree(T260, T261, T263)) → P72_IN_GAAG(T260, T263)
P72_IN_GAAG(0, T263) → DELETE1_IN_AAG(T263)
DELETE1_IN_AAG(tree(T458, T459, T461)) → P116_IN_GAAG(T458, T461)
P116_IN_GAAG(0, T461) → DELETE1_IN_AAG(T461)
DELETE1_IN_AAG(tree(0, T653, T655)) → DELETE1_IN_AAG(T655)
DELETE1_IN_AAG(tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T655)
P79_IN_GAAG(T281, T263) → U16_GAAG(T281, T263, lessc46_in_ga(T281))
U16_GAAG(T281, T263, lessc46_out_ga(T281)) → DELETE1_IN_AAG(T263)
P116_IN_GAAG(s(T479), T461) → P79_IN_GAAG(T479, T461)
P72_IN_GAAG(s(T281), T263) → P79_IN_GAAG(T281, T263)

The TRS R consists of the following rules:

lessc46_in_ga(0) → lessc46_out_ga(0)
lessc46_in_ga(s(T184)) → U83_ga(T184, lessc46_in_ga(T184))
U83_ga(T184, lessc46_out_ga(T184)) → lessc46_out_ga(s(T184))

The set Q consists of the following terms:

lessc46_in_ga(x0)
U83_ga(x0, x1)

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

(54) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • P44_IN_GAAG(T163, T166) → U5_GAAG(T163, T166, lessc46_in_ga(T163))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • U5_GAAG(T163, T166, lessc46_out_ga(T163)) → DELETE1_IN_AAG(T166)
    The graph contains the following edges 2 >= 1

  • DELETE1_IN_AAG(tree(T163, T164, T166)) → P44_IN_GAAG(T163, T166)
    The graph contains the following edges 1 > 1, 1 > 2

  • DELETE1_IN_AAG(tree(0, T653, T655)) → DELETE1_IN_AAG(T655)
    The graph contains the following edges 1 > 1

  • P72_IN_GAAG(0, T263) → DELETE1_IN_AAG(T263)
    The graph contains the following edges 2 >= 1

  • P72_IN_GAAG(s(T281), T263) → P79_IN_GAAG(T281, T263)
    The graph contains the following edges 1 > 1, 2 >= 2

  • DELETE1_IN_AAG(tree(T260, T261, T263)) → P72_IN_GAAG(T260, T263)
    The graph contains the following edges 1 > 1, 1 > 2

  • P116_IN_GAAG(0, T461) → DELETE1_IN_AAG(T461)
    The graph contains the following edges 2 >= 1

  • U16_GAAG(T281, T263, lessc46_out_ga(T281)) → DELETE1_IN_AAG(T263)
    The graph contains the following edges 2 >= 1

  • P116_IN_GAAG(s(T479), T461) → P79_IN_GAAG(T479, T461)
    The graph contains the following edges 1 > 1, 2 >= 2

  • P79_IN_GAAG(T281, T263) → U16_GAAG(T281, T263, lessc46_in_ga(T281))
    The graph contains the following edges 1 >= 1, 2 >= 2

  • DELETE1_IN_AAG(tree(T458, T459, T461)) → P116_IN_GAAG(T458, T461)
    The graph contains the following edges 1 > 1, 1 > 2

  • DELETE1_IN_AAG(tree(s(T673), T653, T655)) → P79_IN_GAAG(T673, T655)
    The graph contains the following edges 1 > 1, 1 > 2

(55) YES