(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) PrologToDTProblemTransformerProof (SOUND transformation)

Built DT problem from termination graph.

(2) Obligation:

Triples:

max44(.(t, T76), T78) :- max44(T76, T78).
max44(.(f, T76), T78) :- max44(T76, T78).
del101(.(t, T149), .(t, X285)) :- del101(T149, X285).
max150(.(f, T202), T204) :- max150(T202, T204).
max150(.(t, T212), T214) :- max44(T212, T214).
del203(.(f, T275), .(f, X547)) :- del203(T275, X547).
maxsort1(.(T17, []), .(T17, T18)) :- ','(delc15(T17, T22), maxsort1(T22, T18)).
maxsort1(.(t, .(t, T55)), .(T57, T58)) :- max44(T55, T57).
maxsort1(.(t, .(t, T133)), .(f, T62)) :- ','(maxc44(T133, f), del101(T133, X240)).
maxsort1(.(t, .(t, T55)), .(T61, T62)) :- ','(maxc44(T55, T61), ','(delc71(T61, T55, T95), maxsort1(T95, T62))).
maxsort1(.(t, .(f, T55)), .(T57, T58)) :- max44(T55, T57).
maxsort1(.(t, .(f, T181)), .(f, T151)) :- ','(maxc44(T181, f), del101(.(f, T181), X343)).
maxsort1(.(t, .(f, T55)), .(T150, T151)) :- ','(maxc44(T55, T150), ','(delc129(T150, T55, T156), maxsort1(T156, T151))).
maxsort1(.(f, .(f, T55)), .(T57, T58)) :- max150(T55, T57).
maxsort1(.(f, .(f, T259)), .(t, T188)) :- ','(maxc150(T259, t), del203(T259, X500)).
maxsort1(.(f, .(f, T55)), .(T187, T188)) :- ','(maxc150(T55, T187), ','(delc173(T187, T55, T221), maxsort1(T221, T188))).
maxsort1(.(f, .(t, T286)), .(T288, T289)) :- max44(T286, T288).
maxsort1(.(f, .(t, T323)), .(t, T293)) :- ','(maxc44(T323, t), del203(.(t, T323), X623)).
maxsort1(.(f, .(t, T286)), .(T292, T293)) :- ','(maxc44(T286, T292), ','(delc238(T292, T286, T298), maxsort1(T298, T293))).

Clauses:

maxsortc1([], []).
maxsortc1(.(T17, []), .(T17, T18)) :- ','(delc15(T17, T22), maxsortc1(T22, T18)).
maxsortc1(.(t, .(t, T55)), .(T61, T62)) :- ','(maxc44(T55, T61), ','(delc71(T61, T55, T95), maxsortc1(T95, T62))).
maxsortc1(.(t, .(f, T55)), .(T150, T151)) :- ','(maxc44(T55, T150), ','(delc129(T150, T55, T156), maxsortc1(T156, T151))).
maxsortc1(.(f, .(f, T55)), .(T187, T188)) :- ','(maxc150(T55, T187), ','(delc173(T187, T55, T221), maxsortc1(T221, T188))).
maxsortc1(.(f, .(t, T286)), .(T292, T293)) :- ','(maxc44(T286, T292), ','(delc238(T292, T286, T298), maxsortc1(T298, T293))).
maxc44([], t).
maxc44(.(t, T76), T78) :- maxc44(T76, T78).
maxc44(.(f, T76), T78) :- maxc44(T76, T78).
delc101([], []).
delc101(.(f, T143), T143).
delc101(.(t, T149), .(t, X285)) :- delc101(T149, X285).
maxc150([], f).
maxc150(.(f, T202), T204) :- maxc150(T202, T204).
maxc150(.(t, T212), T214) :- maxc44(T212, T214).
delc203([], []).
delc203(.(t, T269), T269).
delc203(.(f, T275), .(f, X547)) :- delc203(T275, X547).
delc15(t, []).
delc15(f, []).
delc71(t, T110, .(t, T110)).
delc71(f, T133, .(t, .(t, X240))) :- delc101(T133, X240).
delc129(t, T171, .(f, T171)).
delc129(f, T181, .(t, X343)) :- delc101(.(f, T181), X343).
delc173(f, T236, .(f, T236)).
delc173(t, T259, .(f, .(f, X500))) :- delc203(T259, X500).
delc238(f, T313, .(t, T313)).
delc238(t, T323, .(f, X623)) :- delc203(.(t, T323), X623).

Afs:

maxsort1(x1, x2)  =  maxsort1(x1)

(3) TriplesToPiDPProof (SOUND transformation)

We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
maxsort1_in: (b,f)
max44_in: (b,f)
maxc44_in: (b,b) (b,f)
del101_in: (b,f)
delc71_in: (b,b,f)
delc101_in: (b,f)
delc129_in: (b,b,f)
max150_in: (b,f)
maxc150_in: (b,b) (b,f)
del203_in: (b,f)
delc173_in: (b,b,f)
delc203_in: (b,f)
delc238_in: (b,b,f)
Transforming TRIPLES into the following Term Rewriting System:
Pi DP problem:
The TRS P consists of the following rules:

MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U7_GA(T17, T18, delc15_in_ga(T17, T22))
U7_GA(T17, T18, delc15_out_ga(T17, T22)) → U8_GA(T17, T18, maxsort1_in_ga(T22, T18))
U7_GA(T17, T18, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → U9_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, T133)), .(f, T62)) → U10_GA(T133, T62, maxc44_in_gg(T133, f))
U10_GA(T133, T62, maxc44_out_gg(T133, f)) → U11_GA(T133, T62, del101_in_ga(T133, X240))
U10_GA(T133, T62, maxc44_out_gg(T133, f)) → 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)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U12_GA(T55, T61, T62, maxc44_in_ga(T55, T61))
U12_GA(T55, T61, T62, maxc44_out_ga(T55, T61)) → U13_GA(T55, T61, T62, delc71_in_gga(T61, T55, T95))
U13_GA(T55, T61, T62, delc71_out_gga(T61, T55, T95)) → U14_GA(T55, T61, T62, maxsort1_in_ga(T95, T62))
U13_GA(T55, T61, T62, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → U15_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, T181)), .(f, T151)) → U16_GA(T181, T151, maxc44_in_gg(T181, f))
U16_GA(T181, T151, maxc44_out_gg(T181, f)) → U17_GA(T181, T151, del101_in_ga(.(f, T181), X343))
U16_GA(T181, T151, maxc44_out_gg(T181, f)) → DEL101_IN_GA(.(f, T181), X343)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U18_GA(T55, T150, T151, maxc44_in_ga(T55, T150))
U18_GA(T55, T150, T151, maxc44_out_ga(T55, T150)) → U19_GA(T55, T150, T151, delc129_in_gga(T150, T55, T156))
U19_GA(T55, T150, T151, delc129_out_gga(T150, T55, T156)) → U20_GA(T55, T150, T151, maxsort1_in_ga(T156, T151))
U19_GA(T55, T150, T151, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → U21_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, T259)), .(t, T188)) → U22_GA(T259, T188, maxc150_in_gg(T259, t))
U22_GA(T259, T188, maxc150_out_gg(T259, t)) → U23_GA(T259, T188, del203_in_ga(T259, X500))
U22_GA(T259, T188, maxc150_out_gg(T259, t)) → 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)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U24_GA(T55, T187, T188, maxc150_in_ga(T55, T187))
U24_GA(T55, T187, T188, maxc150_out_ga(T55, T187)) → U25_GA(T55, T187, T188, delc173_in_gga(T187, T55, T221))
U25_GA(T55, T187, T188, delc173_out_gga(T187, T55, T221)) → U26_GA(T55, T187, T188, maxsort1_in_ga(T221, T188))
U25_GA(T55, T187, T188, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → U27_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, T323)), .(t, T293)) → U28_GA(T323, T293, maxc44_in_gg(T323, t))
U28_GA(T323, T293, maxc44_out_gg(T323, t)) → U29_GA(T323, T293, del203_in_ga(.(t, T323), X623))
U28_GA(T323, T293, maxc44_out_gg(T323, t)) → DEL203_IN_GA(.(t, T323), X623)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, maxc44_in_ga(T286, T292))
U30_GA(T286, T292, T293, maxc44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, delc238_in_gga(T292, T286, T298))
U31_GA(T286, T292, T293, delc238_out_gga(T292, T286, T298)) → U32_GA(T286, T292, T293, maxsort1_in_ga(T298, T293))
U31_GA(T286, T292, T293, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
DEL101_IN_GA(x1, x2)  =  DEL101_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x4)
MAX150_IN_GA(x1, x2)  =  MAX150_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
DEL203_IN_GA(x1, x2)  =  DEL203_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U26_GA(x1, x2, x3, x4)  =  U26_GA(x1, x4)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x1, x4)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U29_GA(x1, x2, x3)  =  U29_GA(x1, x3)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x1, x4)

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

Infinitary Constructor Rewriting Termination of PiDP implies Termination of TRIPLES

(4) Obligation:

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

MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U7_GA(T17, T18, delc15_in_ga(T17, T22))
U7_GA(T17, T18, delc15_out_ga(T17, T22)) → U8_GA(T17, T18, maxsort1_in_ga(T22, T18))
U7_GA(T17, T18, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → U9_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, T133)), .(f, T62)) → U10_GA(T133, T62, maxc44_in_gg(T133, f))
U10_GA(T133, T62, maxc44_out_gg(T133, f)) → U11_GA(T133, T62, del101_in_ga(T133, X240))
U10_GA(T133, T62, maxc44_out_gg(T133, f)) → 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)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U12_GA(T55, T61, T62, maxc44_in_ga(T55, T61))
U12_GA(T55, T61, T62, maxc44_out_ga(T55, T61)) → U13_GA(T55, T61, T62, delc71_in_gga(T61, T55, T95))
U13_GA(T55, T61, T62, delc71_out_gga(T61, T55, T95)) → U14_GA(T55, T61, T62, maxsort1_in_ga(T95, T62))
U13_GA(T55, T61, T62, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → U15_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, T181)), .(f, T151)) → U16_GA(T181, T151, maxc44_in_gg(T181, f))
U16_GA(T181, T151, maxc44_out_gg(T181, f)) → U17_GA(T181, T151, del101_in_ga(.(f, T181), X343))
U16_GA(T181, T151, maxc44_out_gg(T181, f)) → DEL101_IN_GA(.(f, T181), X343)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U18_GA(T55, T150, T151, maxc44_in_ga(T55, T150))
U18_GA(T55, T150, T151, maxc44_out_ga(T55, T150)) → U19_GA(T55, T150, T151, delc129_in_gga(T150, T55, T156))
U19_GA(T55, T150, T151, delc129_out_gga(T150, T55, T156)) → U20_GA(T55, T150, T151, maxsort1_in_ga(T156, T151))
U19_GA(T55, T150, T151, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → U21_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, T259)), .(t, T188)) → U22_GA(T259, T188, maxc150_in_gg(T259, t))
U22_GA(T259, T188, maxc150_out_gg(T259, t)) → U23_GA(T259, T188, del203_in_ga(T259, X500))
U22_GA(T259, T188, maxc150_out_gg(T259, t)) → 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)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U24_GA(T55, T187, T188, maxc150_in_ga(T55, T187))
U24_GA(T55, T187, T188, maxc150_out_ga(T55, T187)) → U25_GA(T55, T187, T188, delc173_in_gga(T187, T55, T221))
U25_GA(T55, T187, T188, delc173_out_gga(T187, T55, T221)) → U26_GA(T55, T187, T188, maxsort1_in_ga(T221, T188))
U25_GA(T55, T187, T188, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → U27_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, T323)), .(t, T293)) → U28_GA(T323, T293, maxc44_in_gg(T323, t))
U28_GA(T323, T293, maxc44_out_gg(T323, t)) → U29_GA(T323, T293, del203_in_ga(.(t, T323), X623))
U28_GA(T323, T293, maxc44_out_gg(T323, t)) → DEL203_IN_GA(.(t, T323), X623)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, maxc44_in_ga(T286, T292))
U30_GA(T286, T292, T293, maxc44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, delc238_in_gga(T292, T286, T298))
U31_GA(T286, T292, T293, delc238_out_gga(T292, T286, T298)) → U32_GA(T286, T292, T293, maxsort1_in_ga(T298, T293))
U31_GA(T286, T292, T293, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
maxsort1_in_ga(x1, x2)  =  maxsort1_in_ga(x1)
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
max44_in_ga(x1, x2)  =  max44_in_ga(x1)
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
del101_in_ga(x1, x2)  =  del101_in_ga(x1)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
max150_in_ga(x1, x2)  =  max150_in_ga(x1)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
del203_in_ga(x1, x2)  =  del203_in_ga(x1)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U8_GA(x1, x2, x3)  =  U8_GA(x1, x3)
U9_GA(x1, x2, x3, x4)  =  U9_GA(x1, x4)
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)
U1_GA(x1, x2, x3)  =  U1_GA(x1, x3)
U2_GA(x1, x2, x3)  =  U2_GA(x1, x3)
U10_GA(x1, x2, x3)  =  U10_GA(x1, x3)
U11_GA(x1, x2, x3)  =  U11_GA(x1, x3)
DEL101_IN_GA(x1, x2)  =  DEL101_IN_GA(x1)
U3_GA(x1, x2, x3)  =  U3_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U14_GA(x1, x2, x3, x4)  =  U14_GA(x1, x4)
U15_GA(x1, x2, x3, x4)  =  U15_GA(x1, x4)
U16_GA(x1, x2, x3)  =  U16_GA(x1, x3)
U17_GA(x1, x2, x3)  =  U17_GA(x1, x3)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U20_GA(x1, x2, x3, x4)  =  U20_GA(x1, x4)
U21_GA(x1, x2, x3, x4)  =  U21_GA(x1, x4)
MAX150_IN_GA(x1, x2)  =  MAX150_IN_GA(x1)
U4_GA(x1, x2, x3)  =  U4_GA(x1, x3)
U5_GA(x1, x2, x3)  =  U5_GA(x1, x3)
U22_GA(x1, x2, x3)  =  U22_GA(x1, x3)
U23_GA(x1, x2, x3)  =  U23_GA(x1, x3)
DEL203_IN_GA(x1, x2)  =  DEL203_IN_GA(x1)
U6_GA(x1, x2, x3)  =  U6_GA(x1, x3)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U26_GA(x1, x2, x3, x4)  =  U26_GA(x1, x4)
U27_GA(x1, x2, x3, x4)  =  U27_GA(x1, x4)
U28_GA(x1, x2, x3)  =  U28_GA(x1, x3)
U29_GA(x1, x2, x3)  =  U29_GA(x1, x3)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)
U32_GA(x1, x2, x3, x4)  =  U32_GA(x1, x4)

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

(5) DependencyGraphProof (EQUIVALENT transformation)

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

(6) Complex Obligation (AND)

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

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
DEL203_IN_GA(x1, x2)  =  DEL203_IN_GA(x1)

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

(8) UsableRulesProof (EQUIVALENT transformation)

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

(9) Obligation:

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

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

(10) PiDPToQDPProof (SOUND transformation)

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

(11) Obligation:

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

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

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

(12) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(13) YES

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

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
DEL101_IN_GA(x1, x2)  =  DEL101_IN_GA(x1)

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

(15) UsableRulesProof (EQUIVALENT transformation)

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

(16) Obligation:

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

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

(17) PiDPToQDPProof (SOUND transformation)

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

(18) Obligation:

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

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

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

(19) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(20) YES

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

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAX44_IN_GA(x1, x2)  =  MAX44_IN_GA(x1)

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

(22) UsableRulesProof (EQUIVALENT transformation)

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

(23) Obligation:

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

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

(24) PiDPToQDPProof (SOUND transformation)

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

(25) Obligation:

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

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.

(26) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

  • 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

(27) YES

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

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAX150_IN_GA(x1, x2)  =  MAX150_IN_GA(x1)

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

(29) UsableRulesProof (EQUIVALENT transformation)

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

(30) Obligation:

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

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

(31) PiDPToQDPProof (SOUND transformation)

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

(32) Obligation:

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

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

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

(33) QDPSizeChangeProof (EQUIVALENT transformation)

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

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

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

(34) YES

(35) Obligation:

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

U7_GA(T17, T18, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U7_GA(T17, T18, delc15_in_ga(T17, T22))
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U12_GA(T55, T61, T62, maxc44_in_ga(T55, T61))
U12_GA(T55, T61, T62, maxc44_out_ga(T55, T61)) → U13_GA(T55, T61, T62, delc71_in_gga(T61, T55, T95))
U13_GA(T55, T61, T62, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U18_GA(T55, T150, T151, maxc44_in_ga(T55, T150))
U18_GA(T55, T150, T151, maxc44_out_ga(T55, T150)) → U19_GA(T55, T150, T151, delc129_in_gga(T150, T55, T156))
U19_GA(T55, T150, T151, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U24_GA(T55, T187, T188, maxc150_in_ga(T55, T187))
U24_GA(T55, T187, T188, maxc150_out_ga(T55, T187)) → U25_GA(T55, T187, T188, delc173_in_gga(T187, T55, T221))
U25_GA(T55, T187, T188, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, maxc44_in_ga(T286, T292))
U30_GA(T286, T292, T293, maxc44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, delc238_in_gga(T292, T286, T298))
U31_GA(T286, T292, T293, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_gg([], t) → maxc44_out_gg([], t)
maxc44_in_gg(.(t, T76), T78) → U48_gg(T76, T78, maxc44_in_gg(T76, T78))
maxc44_in_gg(.(f, T76), T78) → U49_gg(T76, T78, maxc44_in_gg(T76, T78))
U49_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(f, T76), T78)
U48_gg(T76, T78, maxc44_out_gg(T76, T78)) → maxc44_out_gg(.(t, T76), T78)
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
maxc150_in_gg([], f) → maxc150_out_gg([], f)
maxc150_in_gg(.(f, T202), T204) → U51_gg(T202, T204, maxc150_in_gg(T202, T204))
maxc150_in_gg(.(t, T212), T214) → U52_gg(T212, T214, maxc44_in_gg(T212, T214))
U52_gg(T212, T214, maxc44_out_gg(T212, T214)) → maxc150_out_gg(.(t, T212), T214)
U51_gg(T202, T204, maxc150_out_gg(T202, T204)) → maxc150_out_gg(.(f, T202), T204)
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
maxc44_in_gg(x1, x2)  =  maxc44_in_gg(x1, x2)
maxc44_out_gg(x1, x2)  =  maxc44_out_gg(x1, x2)
U48_gg(x1, x2, x3)  =  U48_gg(x1, x2, x3)
U49_gg(x1, x2, x3)  =  U49_gg(x1, x2, x3)
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxc150_in_gg(x1, x2)  =  maxc150_in_gg(x1, x2)
maxc150_out_gg(x1, x2)  =  maxc150_out_gg(x1, x2)
U51_gg(x1, x2, x3)  =  U51_gg(x1, x2, x3)
U52_gg(x1, x2, x3)  =  U52_gg(x1, x2, x3)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)

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

(36) UsableRulesProof (EQUIVALENT transformation)

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

(37) Obligation:

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

U7_GA(T17, T18, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U7_GA(T17, T18, delc15_in_ga(T17, T22))
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U12_GA(T55, T61, T62, maxc44_in_ga(T55, T61))
U12_GA(T55, T61, T62, maxc44_out_ga(T55, T61)) → U13_GA(T55, T61, T62, delc71_in_gga(T61, T55, T95))
U13_GA(T55, T61, T62, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U18_GA(T55, T150, T151, maxc44_in_ga(T55, T150))
U18_GA(T55, T150, T151, maxc44_out_ga(T55, T150)) → U19_GA(T55, T150, T151, delc129_in_gga(T150, T55, T156))
U19_GA(T55, T150, T151, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U24_GA(T55, T187, T188, maxc150_in_ga(T55, T187))
U24_GA(T55, T187, T188, maxc150_out_ga(T55, T187)) → U25_GA(T55, T187, T188, delc173_in_gga(T187, T55, T221))
U25_GA(T55, T187, T188, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, maxc44_in_ga(T286, T292))
U30_GA(T286, T292, T293, maxc44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, delc238_in_gga(T292, T286, T298))
U31_GA(T286, T292, T293, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)

The TRS R consists of the following rules:

delc15_in_ga(t, []) → delc15_out_ga(t, [])
delc15_in_ga(f, []) → delc15_out_ga(f, [])
maxc44_in_ga([], t) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76), T78) → U48_ga(T76, T78, maxc44_in_ga(T76, T78))
maxc44_in_ga(.(f, T76), T78) → U49_ga(T76, T78, maxc44_in_ga(T76, T78))
delc71_in_gga(t, T110, .(t, T110)) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133, .(t, .(t, X240))) → U54_gga(T133, X240, delc101_in_ga(T133, X240))
delc129_in_gga(t, T171, .(f, T171)) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181, .(t, X343)) → U55_gga(T181, X343, delc101_in_ga(.(f, T181), X343))
maxc150_in_ga([], f) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202), T204) → U51_ga(T202, T204, maxc150_in_ga(T202, T204))
maxc150_in_ga(.(t, T212), T214) → U52_ga(T212, T214, maxc44_in_ga(T212, T214))
delc173_in_gga(f, T236, .(f, T236)) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259, .(f, .(f, X500))) → U56_gga(T259, X500, delc203_in_ga(T259, X500))
delc238_in_gga(f, T313, .(t, T313)) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323, .(f, X623)) → U57_gga(T323, X623, delc203_in_ga(.(t, T323), X623))
U48_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U49_ga(T76, T78, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U54_gga(T133, X240, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U55_gga(T181, X343, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
U51_ga(T202, T204, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
U52_ga(T212, T214, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U56_gga(T259, X500, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U57_gga(T323, X623, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
delc101_in_ga([], []) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143), T143) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149), .(t, X285)) → U50_ga(T149, X285, delc101_in_ga(T149, X285))
delc203_in_ga([], []) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269), T269) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275), .(f, X547)) → U53_ga(T275, X547, delc203_in_ga(T275, X547))
U50_ga(T149, X285, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U53_ga(T275, X547, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))

The argument filtering Pi contains the following mapping:
.(x1, x2)  =  .(x1, x2)
[]  =  []
delc15_in_ga(x1, x2)  =  delc15_in_ga(x1)
t  =  t
delc15_out_ga(x1, x2)  =  delc15_out_ga(x1, x2)
f  =  f
maxc44_in_ga(x1, x2)  =  maxc44_in_ga(x1)
maxc44_out_ga(x1, x2)  =  maxc44_out_ga(x1, x2)
U48_ga(x1, x2, x3)  =  U48_ga(x1, x3)
U49_ga(x1, x2, x3)  =  U49_ga(x1, x3)
delc71_in_gga(x1, x2, x3)  =  delc71_in_gga(x1, x2)
delc71_out_gga(x1, x2, x3)  =  delc71_out_gga(x1, x2, x3)
U54_gga(x1, x2, x3)  =  U54_gga(x1, x3)
delc101_in_ga(x1, x2)  =  delc101_in_ga(x1)
delc101_out_ga(x1, x2)  =  delc101_out_ga(x1, x2)
U50_ga(x1, x2, x3)  =  U50_ga(x1, x3)
delc129_in_gga(x1, x2, x3)  =  delc129_in_gga(x1, x2)
delc129_out_gga(x1, x2, x3)  =  delc129_out_gga(x1, x2, x3)
U55_gga(x1, x2, x3)  =  U55_gga(x1, x3)
maxc150_in_ga(x1, x2)  =  maxc150_in_ga(x1)
maxc150_out_ga(x1, x2)  =  maxc150_out_ga(x1, x2)
U51_ga(x1, x2, x3)  =  U51_ga(x1, x3)
U52_ga(x1, x2, x3)  =  U52_ga(x1, x3)
delc173_in_gga(x1, x2, x3)  =  delc173_in_gga(x1, x2)
delc173_out_gga(x1, x2, x3)  =  delc173_out_gga(x1, x2, x3)
U56_gga(x1, x2, x3)  =  U56_gga(x1, x3)
delc203_in_ga(x1, x2)  =  delc203_in_ga(x1)
delc203_out_ga(x1, x2)  =  delc203_out_ga(x1, x2)
U53_ga(x1, x2, x3)  =  U53_ga(x1, x3)
delc238_in_gga(x1, x2, x3)  =  delc238_in_gga(x1, x2)
delc238_out_gga(x1, x2, x3)  =  delc238_out_gga(x1, x2, x3)
U57_gga(x1, x2, x3)  =  U57_gga(x1, x3)
MAXSORT1_IN_GA(x1, x2)  =  MAXSORT1_IN_GA(x1)
U7_GA(x1, x2, x3)  =  U7_GA(x1, x3)
U12_GA(x1, x2, x3, x4)  =  U12_GA(x1, x4)
U13_GA(x1, x2, x3, x4)  =  U13_GA(x1, x4)
U18_GA(x1, x2, x3, x4)  =  U18_GA(x1, x4)
U19_GA(x1, x2, x3, x4)  =  U19_GA(x1, x4)
U24_GA(x1, x2, x3, x4)  =  U24_GA(x1, x4)
U25_GA(x1, x2, x3, x4)  =  U25_GA(x1, x4)
U30_GA(x1, x2, x3, x4)  =  U30_GA(x1, x4)
U31_GA(x1, x2, x3, x4)  =  U31_GA(x1, x4)

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

(38) PiDPToQDPProof (SOUND transformation)

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

(39) Obligation:

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

U7_GA(T17, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(T17, [])) → U7_GA(T17, delc15_in_ga(T17))
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U30_GA(T286, maxc44_out_ga(T286, T292)) → U31_GA(T286, delc238_in_gga(T292, T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

delc15_in_ga(t) → delc15_out_ga(t, [])
delc15_in_ga(f) → delc15_out_ga(f, [])
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))

The set Q consists of the following terms:

delc15_in_ga(x0)
maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(40) Narrowing (SOUND transformation)

By narrowing [LPAR04] the rule MAXSORT1_IN_GA(.(T17, [])) → U7_GA(T17, delc15_in_ga(T17)) at position [1] we obtained the following new rules [LPAR04]:

MAXSORT1_IN_GA(.(t, [])) → U7_GA(t, delc15_out_ga(t, []))
MAXSORT1_IN_GA(.(f, [])) → U7_GA(f, delc15_out_ga(f, []))

(41) Obligation:

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

U7_GA(T17, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U30_GA(T286, maxc44_out_ga(T286, T292)) → U31_GA(T286, delc238_in_gga(T292, T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U7_GA(t, delc15_out_ga(t, []))
MAXSORT1_IN_GA(.(f, [])) → U7_GA(f, delc15_out_ga(f, []))

The TRS R consists of the following rules:

delc15_in_ga(t) → delc15_out_ga(t, [])
delc15_in_ga(f) → delc15_out_ga(f, [])
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))

The set Q consists of the following terms:

delc15_in_ga(x0)
maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(42) 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.

(43) Obligation:

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

U7_GA(T17, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U30_GA(T286, maxc44_out_ga(T286, T292)) → U31_GA(T286, delc238_in_gga(T292, T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U7_GA(t, delc15_out_ga(t, []))
MAXSORT1_IN_GA(.(f, [])) → U7_GA(f, delc15_out_ga(f, []))

The TRS R consists of the following rules:

delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

delc15_in_ga(x0)
maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(44) 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].

delc15_in_ga(x0)

(45) Obligation:

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

U7_GA(T17, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U30_GA(T286, maxc44_out_ga(T286, T292)) → U31_GA(T286, delc238_in_gga(T292, T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U7_GA(t, delc15_out_ga(t, []))
MAXSORT1_IN_GA(.(f, [])) → U7_GA(f, delc15_out_ga(f, []))

The TRS R consists of the following rules:

delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(46) Instantiation (EQUIVALENT transformation)

By instantiating [LPAR04] the rule U7_GA(T17, delc15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22) we obtained the following new rules [LPAR04]:

U7_GA(t, delc15_out_ga(t, [])) → MAXSORT1_IN_GA([])
U7_GA(f, delc15_out_ga(f, [])) → MAXSORT1_IN_GA([])

(47) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U30_GA(T286, maxc44_out_ga(T286, T292)) → U31_GA(T286, delc238_in_gga(T292, T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U7_GA(t, delc15_out_ga(t, []))
MAXSORT1_IN_GA(.(f, [])) → U7_GA(f, delc15_out_ga(f, []))
U7_GA(t, delc15_out_ga(t, [])) → MAXSORT1_IN_GA([])
U7_GA(f, delc15_out_ga(f, [])) → MAXSORT1_IN_GA([])

The TRS R consists of the following rules:

delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(48) DependencyGraphProof (EQUIVALENT transformation)

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

(49) Obligation:

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

U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U30_GA(T286, maxc44_out_ga(T286, T292)) → U31_GA(T286, delc238_in_gga(T292, T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(50) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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

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

POL(maxc44_out_ga(x1, x2)) =
/0\
\0/
+
/11\
\10/
·x1 +
/00\
\10/
·x2

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

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

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

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

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

POL(t) =
/1\
\0/

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

POL(f) =
/0\
\0/

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

POL(U52_ga(x1, x2)) =
/0\
\1/
+
/11\
\00/
·x1 +
/00\
\00/
·x2

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

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

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

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

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

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

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

The following usable rules [FROCOS05] were oriented:

delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

(51) Obligation:

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

U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, maxc44_in_ga(T286))
U31_GA(T286, delc238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298)

The TRS R consists of the following rules:

delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(52) DependencyGraphProof (EQUIVALENT transformation)

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

(53) Obligation:

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

U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc238_in_gga(f, T313) → delc238_out_gga(f, T313, .(t, T313))
delc238_in_gga(t, T323) → U57_gga(T323, delc203_in_ga(.(t, T323)))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
U57_gga(T323, delc203_out_ga(.(t, T323), X623)) → delc238_out_gga(t, T323, .(f, X623))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

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

(55) Obligation:

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

U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
delc238_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
U57_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(56) 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].

delc238_in_gga(x0, x1)
U57_gga(x0, x1)

(57) Obligation:

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

U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(58) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U18_GA(T55, maxc44_out_ga(T55, T150)) → U19_GA(T55, delc129_in_gga(T150, T55))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

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

POL(delc71_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/10\
\00/
·x3

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

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

POL(t) =
/1\
\0/

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

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

POL(maxc44_out_ga(x1, x2)) =
/0\
\0/
+
/01\
\01/
·x1 +
/01\
\11/
·x2

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

POL(f) =
/0\
\1/

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

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

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

POL(delc129_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\10/
·x3

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

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

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

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

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

POL(delc173_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\10/
·x3

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

POL(U48_ga(x1, x2)) =
/0\
\0/
+
/00\
\00/
·x1 +
/10\
\11/
·x2

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

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

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

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

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

POL(U52_ga(x1, x2)) =
/0\
\0/
+
/11\
\11/
·x1 +
/11\
\01/
·x2

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

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

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

POL(U53_ga(x1, x2)) =
/1\
\0/
+
/11\
\01/
·x1 +
/01\
\11/
·x2

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

POL(U50_ga(x1, x2)) =
/0\
\0/
+
/11\
\10/
·x1 +
/00\
\00/
·x2

The following usable rules [FROCOS05] were oriented:

maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))

(59) Obligation:

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

U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U18_GA(T55, maxc44_in_ga(T55))
U19_GA(T55, delc129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(60) DependencyGraphProof (EQUIVALENT transformation)

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

(61) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc129_in_gga(t, T171) → delc129_out_gga(t, T171, .(f, T171))
delc129_in_gga(f, T181) → U55_gga(T181, delc101_in_ga(.(f, T181)))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
U55_gga(T181, delc101_out_ga(.(f, T181), X343)) → delc129_out_gga(f, T181, .(t, X343))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(62) 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.

(63) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
delc129_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U55_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(64) 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].

delc129_in_gga(x0, x1)
U55_gga(x0, x1)

(65) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(66) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


U13_GA(T55, delc71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:

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

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

POL(t) =
/0\
\1/

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

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

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

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

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

POL(delc71_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\10/
·x3

POL(f) =
/1\
\0/

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

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

POL(maxc150_out_ga(x1, x2)) =
/1\
\1/
+
/10\
\10/
·x1 +
/00\
\00/
·x2

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

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

POL(delc173_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\00/
·x2 +
/00\
\10/
·x3

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

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

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

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

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

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

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

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

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

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

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

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

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

The following usable rules [FROCOS05] were oriented:

maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

(67) Obligation:

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

MAXSORT1_IN_GA(.(t, .(t, T55))) → U12_GA(T55, maxc44_in_ga(T55))
U12_GA(T55, maxc44_out_ga(T55, T61)) → U13_GA(T55, delc71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(68) DependencyGraphProof (EQUIVALENT transformation)

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

(69) Obligation:

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

MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
delc71_in_gga(t, T110) → delc71_out_gga(t, T110, .(t, T110))
delc71_in_gga(f, T133) → U54_gga(T133, delc101_in_ga(T133))
delc101_in_ga(.(f, T143)) → delc101_out_ga(.(f, T143), T143)
delc101_in_ga([]) → delc101_out_ga([], [])
delc101_in_ga(.(t, T149)) → U50_ga(T149, delc101_in_ga(T149))
U54_gga(T133, delc101_out_ga(T133, X240)) → delc71_out_gga(f, T133, .(t, .(t, X240)))
U50_ga(T149, delc101_out_ga(T149, X285)) → delc101_out_ga(.(t, T149), .(t, X285))

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(70) 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.

(71) Obligation:

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

MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)

The set Q consists of the following terms:

maxc44_in_ga(x0)
delc71_in_gga(x0, x1)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U54_gga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc101_in_ga(x0)
delc203_in_ga(x0)
U50_ga(x0, x1)
U53_ga(x0, x1)

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

(72) 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].

delc71_in_gga(x0, x1)
U54_gga(x0, x1)
delc101_in_ga(x0)
U50_ga(x0, x1)

(73) Obligation:

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

MAXSORT1_IN_GA(.(f, .(f, T55))) → U24_GA(T55, maxc150_in_ga(T55))
U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)

The set Q consists of the following terms:

maxc44_in_ga(x0)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc203_in_ga(x0)
U53_ga(x0, x1)

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

(74) QDPOrderProof (EQUIVALENT transformation)

We use the reduction pair processor [LPAR04].


The following pairs can be oriented strictly and are deleted.


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

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

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

POL(f) =
/0\
\1/

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

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

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

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

POL(delc173_in_gga(x1, x2)) =
/1\
\0/
+
/10\
\00/
·x1 +
/11\
\10/
·x2

POL(delc173_out_gga(x1, x2, x3)) =
/0\
\0/
+
/00\
\00/
·x1 +
/00\
\10/
·x2 +
/10\
\00/
·x3

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

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

POL(t) =
/1\
\0/

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

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

POL(U56_gga(x1, x2)) =
/1\
\0/
+
/00\
\10/
·x1 +
/11\
\00/
·x2

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

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

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

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

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

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

The following usable rules [FROCOS05] were oriented:

maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)

(75) Obligation:

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

U24_GA(T55, maxc150_out_ga(T55, T187)) → U25_GA(T55, delc173_in_gga(T187, T55))
U25_GA(T55, delc173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221)

The TRS R consists of the following rules:

delc173_in_gga(f, T236) → delc173_out_gga(f, T236, .(f, T236))
delc173_in_gga(t, T259) → U56_gga(T259, delc203_in_ga(T259))
delc203_in_ga(.(t, T269)) → delc203_out_ga(.(t, T269), T269)
delc203_in_ga([]) → delc203_out_ga([], [])
delc203_in_ga(.(f, T275)) → U53_ga(T275, delc203_in_ga(T275))
U56_gga(T259, delc203_out_ga(T259, X500)) → delc173_out_gga(t, T259, .(f, .(f, X500)))
U53_ga(T275, delc203_out_ga(T275, X547)) → delc203_out_ga(.(f, T275), .(f, X547))
maxc150_in_ga([]) → maxc150_out_ga([], f)
maxc150_in_ga(.(f, T202)) → U51_ga(T202, maxc150_in_ga(T202))
maxc150_in_ga(.(t, T212)) → U52_ga(T212, maxc44_in_ga(T212))
maxc44_in_ga([]) → maxc44_out_ga([], t)
maxc44_in_ga(.(t, T76)) → U48_ga(T76, maxc44_in_ga(T76))
maxc44_in_ga(.(f, T76)) → U49_ga(T76, maxc44_in_ga(T76))
U52_ga(T212, maxc44_out_ga(T212, T214)) → maxc150_out_ga(.(t, T212), T214)
U49_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(f, T76), T78)
U48_ga(T76, maxc44_out_ga(T76, T78)) → maxc44_out_ga(.(t, T76), T78)
U51_ga(T202, maxc150_out_ga(T202, T204)) → maxc150_out_ga(.(f, T202), T204)

The set Q consists of the following terms:

maxc44_in_ga(x0)
maxc150_in_ga(x0)
delc173_in_gga(x0, x1)
U48_ga(x0, x1)
U49_ga(x0, x1)
U51_ga(x0, x1)
U52_ga(x0, x1)
U56_gga(x0, x1)
delc203_in_ga(x0)
U53_ga(x0, x1)

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

(76) DependencyGraphProof (EQUIVALENT transformation)

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

(77) TRUE