(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 | + | | · | x1 | + | | · | x2 |
POL(maxc44_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U13_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc71_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc71_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(MAXSORT1_IN_GA(x1)) = | 0 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(maxc44_in_ga(x1)) = | | + | | · | x1 |
POL(U18_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(U19_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc129_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc129_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U24_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(maxc150_in_ga(x1)) = | | + | | · | x1 |
POL(maxc150_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U25_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc173_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U30_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(U31_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc238_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc238_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U54_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc101_in_ga(x1)) = | | + | | · | x1 |
POL(U48_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U49_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U55_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U51_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U52_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U56_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc203_in_ga(x1)) = | | + | | · | x1 |
POL(U57_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc203_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U53_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc101_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U50_ga(x1, x2)) = | | + | | · | x1 | + | | · | 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 | + | | · | x1 | + | | · | x2 |
POL(delc71_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(MAXSORT1_IN_GA(x1)) = | 0 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(maxc44_in_ga(x1)) = | | + | | · | x1 |
POL(maxc44_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc71_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U18_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(U19_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc129_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc129_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U24_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(maxc150_in_ga(x1)) = | | + | | · | x1 |
POL(maxc150_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U25_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc173_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U48_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U49_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U54_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc101_in_ga(x1)) = | | + | | · | x1 |
POL(U55_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U51_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U52_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U56_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc203_in_ga(x1)) = | | + | | · | x1 |
POL(delc203_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U53_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc101_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U50_ga(x1, x2)) = | | + | | · | x1 | + | | · | 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 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U12_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(maxc44_in_ga(x1)) = | | + | | · | x1 |
POL(maxc44_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U13_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(delc71_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc71_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U24_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(maxc150_in_ga(x1)) = | | + | | · | x1 |
POL(maxc150_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U25_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc173_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U48_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U49_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U54_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc101_in_ga(x1)) = | | + | | · | x1 |
POL(U51_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U52_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U56_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc203_in_ga(x1)) = | | + | | · | x1 |
POL(delc203_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U53_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc101_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U50_ga(x1, x2)) = | | + | | · | x1 | + | | · | 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 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U24_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(maxc150_in_ga(x1)) = | | + | | · | x1 |
POL(maxc150_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U25_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(delc173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc173_out_gga(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
POL(U51_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U52_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(maxc44_in_ga(x1)) = | | + | | · | x1 |
POL(U56_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(delc203_in_ga(x1)) = | | + | | · | x1 |
POL(delc203_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U53_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(maxc44_out_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U48_ga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U49_ga(x1, x2)) = | | + | | · | x1 | + | | · | 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