(0) Obligation:

Clauses:

eq(t, t).
eq(f, f).
neq(t, f).
neq(f, t).
del(X1, [], []).
del(X, .(Y, YS), YS) :- eq(X, Y).
del(X, .(Y, YS), .(Y, ZS)) :- ','(neq(X, Y), del(X, YS, ZS)).
ge(t, t).
ge(t, f).
ge(f, f).
gt(t, f).
max([], f).
max(.(X, []), X).
max(.(X, .(Y, XS)), Z) :- ','(ge(X, Y), max(.(X, XS), Z)).
max(.(X, .(Y, XS)), Z) :- ','(gt(Y, X), max(.(Y, XS), Z)).
maxsort([], []).
maxsort(.(X, XS), .(Y, YS)) :- ','(max(.(X, XS), Y), ','(del(Y, .(X, XS), ZS), maxsort(ZS, YS))).

Queries:

maxsort(g,a).

(1) PrologToPrologProblemTransformerProof (SOUND transformation)

Built Prolog problem from termination graph.

(2) Obligation:

Clauses:

max44([], t).
max44(.(t, T76), T78) :- max44(T76, T78).
max44(.(f, T76), T78) :- max44(T76, T78).
del101([], []).
del101(.(f, T143), T143).
del101(.(t, T149), .(t, X285)) :- del101(T149, X285).
max150([], f).
max150(.(f, T202), T204) :- max150(T202, T204).
max150(.(t, T212), T214) :- max44(T212, T214).
del203([], []).
del203(.(t, T269), T269).
del203(.(f, T275), .(f, X547)) :- del203(T275, X547).
del15(t, []).
del15(f, []).
del71(t, T110, .(t, T110)).
del71(f, T133, .(t, .(t, X240))) :- del101(T133, X240).
del129(t, T171, .(f, T171)).
del129(f, T181, .(t, X343)) :- del101(.(f, T181), X343).
del173(f, T236, .(f, T236)).
del173(t, T259, .(f, .(f, X500))) :- del203(T259, X500).
del238(f, T313, .(t, T313)).
del238(t, T323, .(f, X623)) :- del203(.(t, T323), X623).
maxsort1([], []).
maxsort1(.(T17, []), .(T17, T18)) :- del15(T17, X14).
maxsort1(.(T17, []), .(T17, T18)) :- ','(del15(T17, T22), maxsort1(T22, T18)).
maxsort1(.(t, .(t, T55)), .(T57, T58)) :- max44(T55, T57).
maxsort1(.(t, .(t, T55)), .(T61, T62)) :- ','(max44(T55, T61), del71(T61, T55, X14)).
maxsort1(.(t, .(t, T55)), .(T61, T62)) :- ','(max44(T55, T61), ','(del71(T61, T55, T95), maxsort1(T95, T62))).
maxsort1(.(t, .(f, T55)), .(T57, T58)) :- max44(T55, T57).
maxsort1(.(t, .(f, T55)), .(T150, T151)) :- ','(max44(T55, T150), del129(T150, T55, X14)).
maxsort1(.(t, .(f, T55)), .(T150, T151)) :- ','(max44(T55, T150), ','(del129(T150, T55, T156), maxsort1(T156, T151))).
maxsort1(.(f, .(f, T55)), .(T57, T58)) :- max150(T55, T57).
maxsort1(.(f, .(f, T55)), .(T187, T188)) :- ','(max150(T55, T187), del173(T187, T55, X14)).
maxsort1(.(f, .(f, T55)), .(T187, T188)) :- ','(max150(T55, T187), ','(del173(T187, T55, T221), maxsort1(T221, T188))).
maxsort1(.(f, .(t, T286)), .(T288, T289)) :- max44(T286, T288).
maxsort1(.(f, .(t, T286)), .(T292, T293)) :- ','(max44(T286, T292), del238(T292, T286, X14)).
maxsort1(.(f, .(t, T286)), .(T292, T293)) :- ','(max44(T286, T292), ','(del238(T292, T286, T298), maxsort1(T298, T293))).

Queries:

maxsort1(g,a).

(3) PrologToPiTRSProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
maxsort1_in: (b,f)
max44_in: (b,f)
del71_in: (b,b,f)
del101_in: (b,f)
del129_in: (b,b,f)
max150_in: (b,f)
del173_in: (b,b,f)
del203_in: (b,f)
del238_in: (b,b,f)
Transforming Prolog into the following Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)

Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog

(4) Obligation:

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

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)

(5) DependencyPairsProof (EQUIVALENT transformation)

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

MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U11_GA(T17, T18, del15_in_ga(T17, X14))
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → DEL15_IN_GA(T17, X14)
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → U13_GA(T17, T18, maxsort1_in_ga(T22, T18))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → U14_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAX44_IN_GA(.(t, T76), T78) → U1_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(f, T76), T78) → U2_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U16_GA(T55, T61, T62, del71_in_gga(T61, T55, X14))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → DEL71_IN_GGA(T61, T55, X14)
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → U7_GGA(T133, X240, del101_in_ga(T133, X240))
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → DEL101_IN_GA(T133, X240)
DEL101_IN_GA(.(t, T149), .(t, X285)) → U3_GA(T149, X285, del101_in_ga(T149, X285))
DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_GA(T55, T61, T62, maxsort1_in_ga(T95, T62))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → U19_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U21_GA(T55, T150, T151, del129_in_gga(T150, T55, X14))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → DEL129_IN_GGA(T150, T55, X14)
DEL129_IN_GGA(f, T181, .(t, X343)) → U8_GGA(T181, X343, del101_in_ga(.(f, T181), X343))
DEL129_IN_GGA(f, T181, .(t, X343)) → DEL101_IN_GA(.(f, T181), X343)
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_GA(T55, T150, T151, maxsort1_in_ga(T156, T151))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → U24_GA(T55, T57, T58, max150_in_ga(T55, T57))
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → MAX150_IN_GA(T55, T57)
MAX150_IN_GA(.(f, T202), T204) → U4_GA(T202, T204, max150_in_ga(T202, T204))
MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)
MAX150_IN_GA(.(t, T212), T214) → U5_GA(T212, T214, max44_in_ga(T212, T214))
MAX150_IN_GA(.(t, T212), T214) → MAX44_IN_GA(T212, T214)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U26_GA(T55, T187, T188, del173_in_gga(T187, T55, X14))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → DEL173_IN_GGA(T187, T55, X14)
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → U9_GGA(T259, X500, del203_in_ga(T259, X500))
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → DEL203_IN_GA(T259, X500)
DEL203_IN_GA(.(f, T275), .(f, X547)) → U6_GA(T275, X547, del203_in_ga(T275, X547))
DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_GA(T55, T187, T188, maxsort1_in_ga(T221, T188))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → U29_GA(T286, T288, T289, max44_in_ga(T286, T288))
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → MAX44_IN_GA(T286, T288)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, del238_in_gga(T292, T286, X14))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → DEL238_IN_GGA(T292, T286, X14)
DEL238_IN_GGA(t, T323, .(f, X623)) → U10_GGA(T323, X623, del203_in_ga(.(t, T323), X623))
DEL238_IN_GGA(t, T323, .(f, X623)) → DEL203_IN_GA(.(t, T323), X623)
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_GA(T286, T292, T293, maxsort1_in_ga(T298, T293))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
DEL15_IN_GA(x1, x2)  =  DEL15_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x4)
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x4)
DEL71_IN_GGA(x1, x2, x3)  =  DEL71_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
DEL101_IN_GA(x1, x2)  =  DEL101_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x4)
DEL129_IN_GGA(x1, x2, x3)  =  DEL129_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x4)
U23_GA(x1, x2, x3, x4)  =  U23_GA(x4)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x4)
MAX150_IN_GA(x1, x2)  =  MAX150_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U26_GA(x1, x2, x3, x4)  =  U26_GA(x4)
DEL173_IN_GGA(x1, x2, x3)  =  DEL173_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
DEL203_IN_GA(x1, x2)  =  DEL203_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x4)
U28_GA(x1, x2, x3, x4)  =  U28_GA(x4)
U29_GA(x1, x2, x3, x4)  =  U29_GA(x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x4)
DEL238_IN_GGA(x1, x2, x3)  =  DEL238_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x4)
U33_GA(x1, x2, x3, x4)  =  U33_GA(x4)

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

(6) Obligation:

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

MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U11_GA(T17, T18, del15_in_ga(T17, X14))
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → DEL15_IN_GA(T17, X14)
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → U13_GA(T17, T18, maxsort1_in_ga(T22, T18))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → U14_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAX44_IN_GA(.(t, T76), T78) → U1_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(f, T76), T78) → U2_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U16_GA(T55, T61, T62, del71_in_gga(T61, T55, X14))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → DEL71_IN_GGA(T61, T55, X14)
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → U7_GGA(T133, X240, del101_in_ga(T133, X240))
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → DEL101_IN_GA(T133, X240)
DEL101_IN_GA(.(t, T149), .(t, X285)) → U3_GA(T149, X285, del101_in_ga(T149, X285))
DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_GA(T55, T61, T62, maxsort1_in_ga(T95, T62))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → U19_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U21_GA(T55, T150, T151, del129_in_gga(T150, T55, X14))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → DEL129_IN_GGA(T150, T55, X14)
DEL129_IN_GGA(f, T181, .(t, X343)) → U8_GGA(T181, X343, del101_in_ga(.(f, T181), X343))
DEL129_IN_GGA(f, T181, .(t, X343)) → DEL101_IN_GA(.(f, T181), X343)
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_GA(T55, T150, T151, maxsort1_in_ga(T156, T151))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → U24_GA(T55, T57, T58, max150_in_ga(T55, T57))
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → MAX150_IN_GA(T55, T57)
MAX150_IN_GA(.(f, T202), T204) → U4_GA(T202, T204, max150_in_ga(T202, T204))
MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)
MAX150_IN_GA(.(t, T212), T214) → U5_GA(T212, T214, max44_in_ga(T212, T214))
MAX150_IN_GA(.(t, T212), T214) → MAX44_IN_GA(T212, T214)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U26_GA(T55, T187, T188, del173_in_gga(T187, T55, X14))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → DEL173_IN_GGA(T187, T55, X14)
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → U9_GGA(T259, X500, del203_in_ga(T259, X500))
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → DEL203_IN_GA(T259, X500)
DEL203_IN_GA(.(f, T275), .(f, X547)) → U6_GA(T275, X547, del203_in_ga(T275, X547))
DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_GA(T55, T187, T188, maxsort1_in_ga(T221, T188))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → U29_GA(T286, T288, T289, max44_in_ga(T286, T288))
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → MAX44_IN_GA(T286, T288)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, del238_in_gga(T292, T286, X14))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → DEL238_IN_GGA(T292, T286, X14)
DEL238_IN_GGA(t, T323, .(f, X623)) → U10_GGA(T323, X623, del203_in_ga(.(t, T323), X623))
DEL238_IN_GGA(t, T323, .(f, X623)) → DEL203_IN_GA(.(t, T323), X623)
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_GA(T286, T292, T293, maxsort1_in_ga(T298, T293))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U11_GA(x1, x2, x3)  =  U11_GA(x3)
DEL15_IN_GA(x1, x2)  =  DEL15_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U13_GA(x1, x2, x3)  =  U13_GA(x3)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x4)
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x3)
U2_GA(x1, x2, x3)  =  U2_GA(x3)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U16_GA(x1, x2, x3, x4)  =  U16_GA(x4)
DEL71_IN_GGA(x1, x2, x3)  =  DEL71_IN_GGA(x1, x2)
U7_GGA(x1, x2, x3)  =  U7_GGA(x3)
DEL101_IN_GA(x1, x2)  =  DEL101_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x3)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x4)
DEL129_IN_GGA(x1, x2, x3)  =  DEL129_IN_GGA(x1, x2)
U8_GGA(x1, x2, x3)  =  U8_GGA(x3)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x4)
U23_GA(x1, x2, x3, x4)  =  U23_GA(x4)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x4)
MAX150_IN_GA(x1, x2)  =  MAX150_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x3)
U5_GA(x1, x2, x3)  =  U5_GA(x3)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U26_GA(x1, x2, x3, x4)  =  U26_GA(x4)
DEL173_IN_GGA(x1, x2, x3)  =  DEL173_IN_GGA(x1, x2)
U9_GGA(x1, x2, x3)  =  U9_GGA(x3)
DEL203_IN_GA(x1, x2)  =  DEL203_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x3)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x4)
U28_GA(x1, x2, x3, x4)  =  U28_GA(x4)
U29_GA(x1, x2, x3, x4)  =  U29_GA(x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x4)
DEL238_IN_GGA(x1, x2, x3)  =  DEL238_IN_GGA(x1, x2)
U10_GGA(x1, x2, x3)  =  U10_GGA(x3)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x4)
U33_GA(x1, x2, x3, x4)  =  U33_GA(x4)

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

(7) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 38 less nodes.

(8) Complex Obligation (AND)

(9) Obligation:

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

DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
DEL203_IN_GA(x1, x2)  =  DEL203_IN_GA(x1)

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

(10) UsableRulesProof (EQUIVALENT transformation)

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

(11) Obligation:

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

DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)

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

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

(12) PiDPToQDPProof (SOUND transformation)

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

(13) Obligation:

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

DEL203_IN_GA(.(f, T275)) → DEL203_IN_GA(T275)

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

(14) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • DEL203_IN_GA(.(f, T275)) → DEL203_IN_GA(T275)
    The graph contains the following edges 1 > 1

(15) YES

(16) Obligation:

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

DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
DEL101_IN_GA(x1, x2)  =  DEL101_IN_GA(x1)

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

(17) UsableRulesProof (EQUIVALENT transformation)

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

(18) Obligation:

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

DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)

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

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

(19) PiDPToQDPProof (SOUND transformation)

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

(20) Obligation:

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

DEL101_IN_GA(.(t, T149)) → DEL101_IN_GA(T149)

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

(21) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • DEL101_IN_GA(.(t, T149)) → DEL101_IN_GA(T149)
    The graph contains the following edges 1 > 1

(22) YES

(23) Obligation:

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

MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)

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

(24) UsableRulesProof (EQUIVALENT transformation)

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

(25) Obligation:

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

MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)

R is empty.
The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
t  =  t
f  =  f
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)

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

(26) PiDPToQDPProof (SOUND transformation)

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

(27) Obligation:

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

MAX44_IN_GA(.(f, T76)) → MAX44_IN_GA(T76)
MAX44_IN_GA(.(t, T76)) → MAX44_IN_GA(T76)

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

(28) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • MAX44_IN_GA(.(f, T76)) → MAX44_IN_GA(T76)
    The graph contains the following edges 1 > 1

  • MAX44_IN_GA(.(t, T76)) → MAX44_IN_GA(T76)
    The graph contains the following edges 1 > 1

(29) YES

(30) Obligation:

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

MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
MAX150_IN_GA(x1, x2)  =  MAX150_IN_GA(x1)

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

(31) UsableRulesProof (EQUIVALENT transformation)

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

(32) Obligation:

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

MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)

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

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

(33) PiDPToQDPProof (SOUND transformation)

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

(34) Obligation:

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

MAX150_IN_GA(.(f, T202)) → MAX150_IN_GA(T202)

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

(35) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • MAX150_IN_GA(.(f, T202)) → MAX150_IN_GA(T202)
    The graph contains the following edges 1 > 1

(36) YES

(37) Obligation:

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

MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
[]  =  []
maxsort1_out_ga(x1, x2)  =  maxsort1_out_ga
.(x1, x2)  =  .(x1, x2)
U11_ga(x1, x2, x3)  =  U11_ga(x3)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
U12_ga(x1, x2, x3)  =  U12_ga(x3)
U13_ga(x1, x2, x3)  =  U13_ga(x3)
U14_ga(x1, x2, x3, x4)  =  U14_ga(x4)
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
U15_ga(x1, x2, x3, x4)  =  U15_ga(x1, x4)
U16_ga(x1, x2, x3, x4)  =  U16_ga(x4)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
U17_ga(x1, x2, x3, x4)  =  U17_ga(x4)
U18_ga(x1, x2, x3, x4)  =  U18_ga(x4)
U19_ga(x1, x2, x3, x4)  =  U19_ga(x4)
U20_ga(x1, x2, x3, x4)  =  U20_ga(x1, x4)
U21_ga(x1, x2, x3, x4)  =  U21_ga(x4)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
U22_ga(x1, x2, x3, x4)  =  U22_ga(x4)
U23_ga(x1, x2, x3, x4)  =  U23_ga(x4)
U24_ga(x1, x2, x3, x4)  =  U24_ga(x4)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
U25_ga(x1, x2, x3, x4)  =  U25_ga(x1, x4)
U26_ga(x1, x2, x3, x4)  =  U26_ga(x4)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
U27_ga(x1, x2, x3, x4)  =  U27_ga(x4)
U28_ga(x1, x2, x3, x4)  =  U28_ga(x4)
U29_ga(x1, x2, x3, x4)  =  U29_ga(x4)
U30_ga(x1, x2, x3, x4)  =  U30_ga(x1, x4)
U31_ga(x1, x2, x3, x4)  =  U31_ga(x4)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
U32_ga(x1, x2, x3, x4)  =  U32_ga(x4)
U33_ga(x1, x2, x3, x4)  =  U33_ga(x4)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x4)

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

(38) UsableRulesProof (EQUIVALENT transformation)

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

(39) Obligation:

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

MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))

The argument filtering Pi contains the following mapping:
[]  =  []
.(x1, x2)  =  .(x1, x2)
del15_in_ga(x1, x2)  =  del15_in_ga(x1)
t  =  t
del15_out_ga(x1, x2)  =  del15_out_ga(x2)
f  =  f
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
max44_out_ga(x1, x2)  =  max44_out_ga(x2)
U1_ga(x1, x2, x3)  =  U1_ga(x3)
U2_ga(x1, x2, x3)  =  U2_ga(x3)
del71_in_gga(x1, x2, x3)  =  del71_in_gga(x1, x2)
del71_out_gga(x1, x2, x3)  =  del71_out_gga(x3)
U7_gga(x1, x2, x3)  =  U7_gga(x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
del101_out_ga(x1, x2)  =  del101_out_ga(x2)
U3_ga(x1, x2, x3)  =  U3_ga(x3)
del129_in_gga(x1, x2, x3)  =  del129_in_gga(x1, x2)
del129_out_gga(x1, x2, x3)  =  del129_out_gga(x3)
U8_gga(x1, x2, x3)  =  U8_gga(x3)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
max150_out_ga(x1, x2)  =  max150_out_ga(x2)
U4_ga(x1, x2, x3)  =  U4_ga(x3)
U5_ga(x1, x2, x3)  =  U5_ga(x3)
del173_in_gga(x1, x2, x3)  =  del173_in_gga(x1, x2)
del173_out_gga(x1, x2, x3)  =  del173_out_gga(x3)
U9_gga(x1, x2, x3)  =  U9_gga(x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
del203_out_ga(x1, x2)  =  del203_out_ga(x2)
U6_ga(x1, x2, x3)  =  U6_ga(x3)
del238_in_gga(x1, x2, x3)  =  del238_in_gga(x1, x2)
del238_out_gga(x1, x2, x3)  =  del238_out_gga(x3)
U10_gga(x1, x2, x3)  =  U10_gga(x3)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U12_GA(x1, x2, x3)  =  U12_GA(x3)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U17_GA(x1, x2, x3, x4)  =  U17_GA(x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U22_GA(x1, x2, x3, x4)  =  U22_GA(x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x4)

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

(40) PiDPToQDPProof (SOUND transformation)

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

(41) Obligation:

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

MAXSORT1_IN_GA(.(T17, [])) → U12_GA(del15_in_ga(T17))
U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del15_in_ga(t) → del15_out_ga([])
del15_in_ga(f) → del15_out_ga([])
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

del15_in_ga(x0)
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(42) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule MAXSORT1_IN_GA(.(T17, [])) → U12_GA(del15_in_ga(T17)) at position [0] we obtained the following new rules [LPAR04]:

MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))

(43) Obligation:

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

U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))

The TRS R consists of the following rules:

del15_in_ga(t) → del15_out_ga([])
del15_in_ga(f) → del15_out_ga([])
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

del15_in_ga(x0)
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(44) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(45) Obligation:

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

U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

del15_in_ga(x0)
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(46) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del15_in_ga(x0)

(47) Obligation:

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

U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(48) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22) we obtained the following new rules [LPAR04]:

U12_GA(del15_out_ga([])) → MAXSORT1_IN_GA([])

(49) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))
U12_GA(del15_out_ga([])) → MAXSORT1_IN_GA([])

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(50) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.

(51) Obligation:

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

U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(52) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U15_GA(x1, x2)) = 0 +
[0,1]
·x1 +
[0,0]
·x2

POL(max44_out_ga(x1)) =
/0\
\0/
+
/11\
\01/
·x1

POL(U17_GA(x1)) = 0 +
[0,1]
·x1

POL(del71_in_gga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/01\
\01/
·x2

POL(del71_out_gga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(MAXSORT1_IN_GA(x1)) = 0 +
[1,0]
·x1

POL(.(x1, x2)) =
/0\
\0/
+
/00\
\10/
·x1 +
/01\
\01/
·x2

POL(t) =
/0\
\1/

POL(max44_in_ga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(f) =
/1\
\0/

POL(U20_GA(x1, x2)) = 1 +
[0,1]
·x1 +
[0,0]
·x2

POL(U22_GA(x1)) = 0 +
[1,0]
·x1

POL(del129_in_gga(x1, x2)) =
/0\
\1/
+
/00\
\10/
·x1 +
/01\
\00/
·x2

POL(del129_out_gga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL(U25_GA(x1, x2)) = 1 +
[0,1]
·x1 +
[0,0]
·x2

POL(max150_in_ga(x1)) =
/0\
\0/
+
/00\
\00/
·x1

POL(max150_out_ga(x1)) =
/0\
\0/
+
/10\
\10/
·x1

POL(U27_GA(x1)) = 0 +
[0,1]
·x1

POL(del173_in_gga(x1, x2)) =
/0\
\1/
+
/00\
\00/
·x1 +
/01\
\01/
·x2

POL(del173_out_gga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(U30_GA(x1, x2)) = 0 +
[0,1]
·x1 +
[0,0]
·x2

POL(U32_GA(x1)) = 0 +
[0,1]
·x1

POL(del238_in_gga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/10\
\01/
·x2

POL(del238_out_gga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(U7_gga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(del101_in_ga(x1)) =
/0\
\0/
+
/01\
\10/
·x1

POL([]) =
/0\
\0/

POL(U1_ga(x1)) =
/0\
\0/
+
/01\
\11/
·x1

POL(U2_ga(x1)) =
/0\
\1/
+
/01\
\01/
·x1

POL(U8_gga(x1)) =
/0\
\0/
+
/01\
\00/
·x1

POL(U4_ga(x1)) =
/1\
\1/
+
/00\
\00/
·x1

POL(U5_ga(x1)) =
/0\
\1/
+
/00\
\00/
·x1

POL(U9_gga(x1)) =
/0\
\1/
+
/00\
\01/
·x1

POL(del203_in_ga(x1)) =
/0\
\0/
+
/01\
\01/
·x1

POL(U10_gga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(del203_out_ga(x1)) =
/0\
\0/
+
/01\
\01/
·x1

POL(U6_ga(x1)) =
/1\
\1/
+
/01\
\10/
·x1

POL(del101_out_ga(x1)) =
/0\
\0/
+
/01\
\01/
·x1

POL(U3_ga(x1)) =
/0\
\0/
+
/10\
\10/
·x1

The following usable rules [FROCOS05] were oriented:

del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

(53) Obligation:

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

U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(54) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(55) Obligation:

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

U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(56) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(57) Obligation:

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

U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(58) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del129_in_gga(x0, x1)
U8_gga(x0)

(59) Obligation:

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

U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(60) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(U17_GA(x1)) = 0 +
[1,0]
·x1

POL(del71_out_gga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL(MAXSORT1_IN_GA(x1)) = 0 +
[1,0]
·x1

POL(.(x1, x2)) =
/0\
\0/
+
/00\
\01/
·x1 +
/01\
\01/
·x2

POL(t) =
/0\
\1/

POL(U15_GA(x1, x2)) = 1 +
[0,1]
·x1 +
[0,0]
·x2

POL(max44_in_ga(x1)) =
/0\
\0/
+
/00\
\00/
·x1

POL(max44_out_ga(x1)) =
/1\
\1/
+
/00\
\00/
·x1

POL(del71_in_gga(x1, x2)) =
/1\
\0/
+
/00\
\00/
·x1 +
/01\
\10/
·x2

POL(f) =
/0\
\0/

POL(U25_GA(x1, x2)) = 0 +
[0,1]
·x1 +
[0,0]
·x2

POL(max150_in_ga(x1)) =
/0\
\0/
+
/00\
\00/
·x1

POL(max150_out_ga(x1)) =
/1\
\1/
+
/00\
\00/
·x1

POL(U27_GA(x1)) = 0 +
[0,1]
·x1

POL(del173_in_gga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\01/
·x2

POL(del173_out_gga(x1)) =
/0\
\0/
+
/00\
\10/
·x1

POL(U30_GA(x1, x2)) = 1 +
[0,1]
·x1 +
[0,0]
·x2

POL(U32_GA(x1)) = 0 +
[1,0]
·x1

POL(del238_in_gga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/01\
\00/
·x2

POL(del238_out_gga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL([]) =
/0\
\0/

POL(U1_ga(x1)) =
/1\
\0/
+
/01\
\00/
·x1

POL(U2_ga(x1)) =
/1\
\0/
+
/00\
\00/
·x1

POL(U7_gga(x1)) =
/0\
\0/
+
/11\
\00/
·x1

POL(del101_in_ga(x1)) =
/0\
\1/
+
/01\
\00/
·x1

POL(U4_ga(x1)) =
/0\
\1/
+
/00\
\00/
·x1

POL(U5_ga(x1)) =
/0\
\1/
+
/00\
\00/
·x1

POL(U9_gga(x1)) =
/0\
\0/
+
/00\
\01/
·x1

POL(del203_in_ga(x1)) =
/0\
\0/
+
/10\
\01/
·x1

POL(U10_gga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL(del203_out_ga(x1)) =
/0\
\0/
+
/01\
\01/
·x1

POL(U6_ga(x1)) =
/0\
\0/
+
/01\
\01/
·x1

POL(del101_out_ga(x1)) =
/0\
\1/
+
/01\
\00/
·x1

POL(U3_ga(x1)) =
/1\
\1/
+
/10\
\00/
·x1

The following usable rules [FROCOS05] were oriented:

del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

(61) Obligation:

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

U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(62) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(63) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(64) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(65) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(66) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del238_in_gga(x0, x1)
U10_gga(x0)

(67) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(68) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

POL(MAXSORT1_IN_GA(x1)) = 0 +
[0,1]
·x1

POL(.(x1, x2)) =
/0\
\0/
+
/00\
\01/
·x1 +
/00\
\01/
·x2

POL(t) =
/0\
\1/

POL(U15_GA(x1, x2)) = 1 +
[0,1]
·x1 +
[1,0]
·x2

POL(max44_in_ga(x1)) =
/0\
\0/
+
/00\
\00/
·x1

POL(max44_out_ga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL(U17_GA(x1)) = 0 +
[1,0]
·x1

POL(del71_in_gga(x1, x2)) =
/1\
\0/
+
/10\
\00/
·x1 +
/01\
\00/
·x2

POL(del71_out_gga(x1)) =
/0\
\0/
+
/01\
\00/
·x1

POL(f) =
/1\
\0/

POL(U25_GA(x1, x2)) = 0 +
[0,1]
·x1 +
[0,0]
·x2

POL(max150_in_ga(x1)) =
/0\
\0/
+
/00\
\00/
·x1

POL(max150_out_ga(x1)) =
/1\
\0/
+
/00\
\00/
·x1

POL(U27_GA(x1)) = 0 +
[0,1]
·x1

POL(del173_in_gga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\01/
·x2

POL(del173_out_gga(x1)) =
/0\
\0/
+
/00\
\01/
·x1

POL([]) =
/0\
\0/

POL(U1_ga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL(U2_ga(x1)) =
/0\
\0/
+
/10\
\00/
·x1

POL(U7_gga(x1)) =
/1\
\0/
+
/01\
\00/
·x1

POL(del101_in_ga(x1)) =
/0\
\1/
+
/00\
\01/
·x1

POL(U4_ga(x1)) =
/1\
\1/
+
/10\
\10/
·x1

POL(U5_ga(x1)) =
/0\
\1/
+
/00\
\00/
·x1

POL(U9_gga(x1)) =
/0\
\0/
+
/00\
\01/
·x1

POL(del203_in_ga(x1)) =
/0\
\0/
+
/00\
\01/
·x1

POL(del203_out_ga(x1)) =
/0\
\0/
+
/00\
\01/
·x1

POL(U6_ga(x1)) =
/0\
\0/
+
/00\
\01/
·x1

POL(del101_out_ga(x1)) =
/0\
\1/
+
/00\
\01/
·x1

POL(U3_ga(x1)) =
/0\
\1/
+
/00\
\01/
·x1

The following usable rules [FROCOS05] were oriented:

max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

(69) Obligation:

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

U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(70) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.

(71) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(72) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(73) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)

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

(74) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

del71_in_gga(x0, x1)
U7_gga(x0)
del101_in_ga(x0)
U3_ga(x0)

(75) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

max44_in_ga(x0)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

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

(76) MRRProof (EQUIVALENT transformation)

By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.

Strictly oriented rules of the TRS R:

max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))

Used ordering: Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2·x1 + 2·x2   
POL(MAXSORT1_IN_GA(x1)) = x1   
POL(U1_ga(x1)) = 1 + x1   
POL(U25_GA(x1, x2)) = 2·x1 + x2   
POL(U27_GA(x1)) = x1   
POL(U2_ga(x1)) = x1   
POL(U4_ga(x1)) = x1   
POL(U5_ga(x1)) = 1 + x1   
POL(U6_ga(x1)) = 2·x1   
POL(U9_gga(x1)) = 1 + 2·x1   
POL([]) = 0   
POL(del173_in_gga(x1, x2)) = x1 + 2·x2   
POL(del173_out_gga(x1)) = x1   
POL(del203_in_ga(x1)) = x1   
POL(del203_out_ga(x1)) = 2·x1   
POL(f) = 0   
POL(max150_in_ga(x1)) = 2·x1   
POL(max150_out_ga(x1)) = x1   
POL(max44_in_ga(x1)) = 2 + x1   
POL(max44_out_ga(x1)) = x1   
POL(t) = 1   

(77) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

max44_in_ga(x0)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

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

(78) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(79) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

max44_in_ga(x0)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

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

(80) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

max44_in_ga(x0)
U1_ga(x0)
U2_ga(x0)
U5_ga(x0)

(81) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

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

(82) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

No dependency pairs are removed.

The following rules are removed from R:

del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x1, x2)) = 2·x1 + 2·x2   
POL(MAXSORT1_IN_GA(x1)) = x1   
POL(U25_GA(x1, x2)) = 2·x1 + x2   
POL(U27_GA(x1)) = x1   
POL(U4_ga(x1)) = x1   
POL(U6_ga(x1)) = 2·x1   
POL(U9_gga(x1)) = 2 + x1   
POL([]) = 0   
POL(del173_in_gga(x1, x2)) = x1 + 2·x2   
POL(del173_out_gga(x1)) = x1   
POL(del203_in_ga(x1)) = x1   
POL(del203_out_ga(x1)) = x1   
POL(f) = 0   
POL(max150_in_ga(x1)) = 2·x1   
POL(max150_out_ga(x1)) = 2·x1   
POL(t) = 2   

(83) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))

The set Q consists of the following terms:

max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

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

(84) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(85) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))

The set Q consists of the following terms:

max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

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

(86) QReductionProof (EQUIVALENT transformation)

We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].

U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)

(87) Obligation:

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

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))

The set Q consists of the following terms:

max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)

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

(88) UsableRulesReductionPairsProof (EQUIVALENT transformation)

By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.

The following dependency pairs can be deleted:

U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
The following rules are removed from R:

max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
Used ordering: POLO with Polynomial interpretation [POLO]:

POL(.(x1, x2)) = x1 + 2·x2   
POL(MAXSORT1_IN_GA(x1)) = x1   
POL(U25_GA(x1, x2)) = 2 + 2·x1 + x2   
POL(U27_GA(x1)) = 1 + x1   
POL(U4_ga(x1)) = x1   
POL([]) = 2   
POL(del173_in_gga(x1, x2)) = x1 + 2·x2   
POL(del173_out_gga(x1)) = x1   
POL(f) = 1   
POL(max150_in_ga(x1)) = 1 + x1   
POL(max150_out_ga(x1)) = 2·x1   

(89) Obligation:

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

MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))

The TRS R consists of the following rules:

U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))

The set Q consists of the following terms:

max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)

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

(90) DependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(91) TRUE