(0) Obligation:
Clauses:
eq(t, t).
eq(f, f).
neq(t, f).
neq(f, t).
del(X1, [], []).
del(X, .(Y, YS), YS) :- eq(X, Y).
del(X, .(Y, YS), .(Y, ZS)) :- ','(neq(X, Y), del(X, YS, ZS)).
ge(t, t).
ge(t, f).
ge(f, f).
gt(t, f).
max([], f).
max(.(X, []), X).
max(.(X, .(Y, XS)), Z) :- ','(ge(X, Y), max(.(X, XS), Z)).
max(.(X, .(Y, XS)), Z) :- ','(gt(Y, X), max(.(Y, XS), Z)).
maxsort([], []).
maxsort(.(X, XS), .(Y, YS)) :- ','(max(.(X, XS), Y), ','(del(Y, .(X, XS), ZS), maxsort(ZS, YS))).
Queries:
maxsort(g,a).
(1) PrologToPrologProblemTransformerProof (SOUND transformation)
Built Prolog problem from termination graph.
(2) Obligation:
Clauses:
max44([], t).
max44(.(t, T76), T78) :- max44(T76, T78).
max44(.(f, T76), T78) :- max44(T76, T78).
del101([], []).
del101(.(f, T143), T143).
del101(.(t, T149), .(t, X285)) :- del101(T149, X285).
max150([], f).
max150(.(f, T202), T204) :- max150(T202, T204).
max150(.(t, T212), T214) :- max44(T212, T214).
del203([], []).
del203(.(t, T269), T269).
del203(.(f, T275), .(f, X547)) :- del203(T275, X547).
del15(t, []).
del15(f, []).
del71(t, T110, .(t, T110)).
del71(f, T133, .(t, .(t, X240))) :- del101(T133, X240).
del129(t, T171, .(f, T171)).
del129(f, T181, .(t, X343)) :- del101(.(f, T181), X343).
del173(f, T236, .(f, T236)).
del173(t, T259, .(f, .(f, X500))) :- del203(T259, X500).
del238(f, T313, .(t, T313)).
del238(t, T323, .(f, X623)) :- del203(.(t, T323), X623).
maxsort1([], []).
maxsort1(.(T17, []), .(T17, T18)) :- del15(T17, X14).
maxsort1(.(T17, []), .(T17, T18)) :- ','(del15(T17, T22), maxsort1(T22, T18)).
maxsort1(.(t, .(t, T55)), .(T57, T58)) :- max44(T55, T57).
maxsort1(.(t, .(t, T55)), .(T61, T62)) :- ','(max44(T55, T61), del71(T61, T55, X14)).
maxsort1(.(t, .(t, T55)), .(T61, T62)) :- ','(max44(T55, T61), ','(del71(T61, T55, T95), maxsort1(T95, T62))).
maxsort1(.(t, .(f, T55)), .(T57, T58)) :- max44(T55, T57).
maxsort1(.(t, .(f, T55)), .(T150, T151)) :- ','(max44(T55, T150), del129(T150, T55, X14)).
maxsort1(.(t, .(f, T55)), .(T150, T151)) :- ','(max44(T55, T150), ','(del129(T150, T55, T156), maxsort1(T156, T151))).
maxsort1(.(f, .(f, T55)), .(T57, T58)) :- max150(T55, T57).
maxsort1(.(f, .(f, T55)), .(T187, T188)) :- ','(max150(T55, T187), del173(T187, T55, X14)).
maxsort1(.(f, .(f, T55)), .(T187, T188)) :- ','(max150(T55, T187), ','(del173(T187, T55, T221), maxsort1(T221, T188))).
maxsort1(.(f, .(t, T286)), .(T288, T289)) :- max44(T286, T288).
maxsort1(.(f, .(t, T286)), .(T292, T293)) :- ','(max44(T286, T292), del238(T292, T286, X14)).
maxsort1(.(f, .(t, T286)), .(T292, T293)) :- ','(max44(T286, T292), ','(del238(T292, T286, T298), maxsort1(T298, T293))).
Queries:
maxsort1(g,a).
(3) PrologToPiTRSProof (SOUND transformation)
We use the technique of [LOPSTR]. With regard to the inferred argument filtering the predicates were used in the following modes:
maxsort1_in: (b,f)
max44_in: (b,f)
del71_in: (b,b,f)
del101_in: (b,f)
del129_in: (b,b,f)
max150_in: (b,f)
del173_in: (b,b,f)
del203_in: (b,f)
del238_in: (b,b,f)
Transforming
Prolog into the following
Term Rewriting System:
Pi-finite rewrite system:
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
Infinitary Constructor Rewriting Termination of PiTRS implies Termination of Prolog
(4) Obligation:
Pi-finite rewrite system:
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LOPSTR] we result in the following initial DP problem:
Pi DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U11_GA(T17, T18, del15_in_ga(T17, X14))
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → DEL15_IN_GA(T17, X14)
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → U13_GA(T17, T18, maxsort1_in_ga(T22, T18))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → U14_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAX44_IN_GA(.(t, T76), T78) → U1_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(f, T76), T78) → U2_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U16_GA(T55, T61, T62, del71_in_gga(T61, T55, X14))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → DEL71_IN_GGA(T61, T55, X14)
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → U7_GGA(T133, X240, del101_in_ga(T133, X240))
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → DEL101_IN_GA(T133, X240)
DEL101_IN_GA(.(t, T149), .(t, X285)) → U3_GA(T149, X285, del101_in_ga(T149, X285))
DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_GA(T55, T61, T62, maxsort1_in_ga(T95, T62))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → U19_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U21_GA(T55, T150, T151, del129_in_gga(T150, T55, X14))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → DEL129_IN_GGA(T150, T55, X14)
DEL129_IN_GGA(f, T181, .(t, X343)) → U8_GGA(T181, X343, del101_in_ga(.(f, T181), X343))
DEL129_IN_GGA(f, T181, .(t, X343)) → DEL101_IN_GA(.(f, T181), X343)
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_GA(T55, T150, T151, maxsort1_in_ga(T156, T151))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → U24_GA(T55, T57, T58, max150_in_ga(T55, T57))
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → MAX150_IN_GA(T55, T57)
MAX150_IN_GA(.(f, T202), T204) → U4_GA(T202, T204, max150_in_ga(T202, T204))
MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)
MAX150_IN_GA(.(t, T212), T214) → U5_GA(T212, T214, max44_in_ga(T212, T214))
MAX150_IN_GA(.(t, T212), T214) → MAX44_IN_GA(T212, T214)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U26_GA(T55, T187, T188, del173_in_gga(T187, T55, X14))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → DEL173_IN_GGA(T187, T55, X14)
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → U9_GGA(T259, X500, del203_in_ga(T259, X500))
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → DEL203_IN_GA(T259, X500)
DEL203_IN_GA(.(f, T275), .(f, X547)) → U6_GA(T275, X547, del203_in_ga(T275, X547))
DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_GA(T55, T187, T188, maxsort1_in_ga(T221, T188))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → U29_GA(T286, T288, T289, max44_in_ga(T286, T288))
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → MAX44_IN_GA(T286, T288)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, del238_in_gga(T292, T286, X14))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → DEL238_IN_GGA(T292, T286, X14)
DEL238_IN_GGA(t, T323, .(f, X623)) → U10_GGA(T323, X623, del203_in_ga(.(t, T323), X623))
DEL238_IN_GGA(t, T323, .(f, X623)) → DEL203_IN_GA(.(t, T323), X623)
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_GA(T286, T292, T293, maxsort1_in_ga(T298, T293))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
MAXSORT1_IN_GA(
x1,
x2) =
MAXSORT1_IN_GA(
x1)
U11_GA(
x1,
x2,
x3) =
U11_GA(
x3)
DEL15_IN_GA(
x1,
x2) =
DEL15_IN_GA(
x1)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x3)
U13_GA(
x1,
x2,
x3) =
U13_GA(
x3)
U14_GA(
x1,
x2,
x3,
x4) =
U14_GA(
x4)
MAX44_IN_GA(
x1,
x2) =
MAX44_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x3)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x3)
U15_GA(
x1,
x2,
x3,
x4) =
U15_GA(
x1,
x4)
U16_GA(
x1,
x2,
x3,
x4) =
U16_GA(
x4)
DEL71_IN_GGA(
x1,
x2,
x3) =
DEL71_IN_GGA(
x1,
x2)
U7_GGA(
x1,
x2,
x3) =
U7_GGA(
x3)
DEL101_IN_GA(
x1,
x2) =
DEL101_IN_GA(
x1)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x3)
U17_GA(
x1,
x2,
x3,
x4) =
U17_GA(
x4)
U18_GA(
x1,
x2,
x3,
x4) =
U18_GA(
x4)
U19_GA(
x1,
x2,
x3,
x4) =
U19_GA(
x4)
U20_GA(
x1,
x2,
x3,
x4) =
U20_GA(
x1,
x4)
U21_GA(
x1,
x2,
x3,
x4) =
U21_GA(
x4)
DEL129_IN_GGA(
x1,
x2,
x3) =
DEL129_IN_GGA(
x1,
x2)
U8_GGA(
x1,
x2,
x3) =
U8_GGA(
x3)
U22_GA(
x1,
x2,
x3,
x4) =
U22_GA(
x4)
U23_GA(
x1,
x2,
x3,
x4) =
U23_GA(
x4)
U24_GA(
x1,
x2,
x3,
x4) =
U24_GA(
x4)
MAX150_IN_GA(
x1,
x2) =
MAX150_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x3)
U5_GA(
x1,
x2,
x3) =
U5_GA(
x3)
U25_GA(
x1,
x2,
x3,
x4) =
U25_GA(
x1,
x4)
U26_GA(
x1,
x2,
x3,
x4) =
U26_GA(
x4)
DEL173_IN_GGA(
x1,
x2,
x3) =
DEL173_IN_GGA(
x1,
x2)
U9_GGA(
x1,
x2,
x3) =
U9_GGA(
x3)
DEL203_IN_GA(
x1,
x2) =
DEL203_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x3)
U27_GA(
x1,
x2,
x3,
x4) =
U27_GA(
x4)
U28_GA(
x1,
x2,
x3,
x4) =
U28_GA(
x4)
U29_GA(
x1,
x2,
x3,
x4) =
U29_GA(
x4)
U30_GA(
x1,
x2,
x3,
x4) =
U30_GA(
x1,
x4)
U31_GA(
x1,
x2,
x3,
x4) =
U31_GA(
x4)
DEL238_IN_GGA(
x1,
x2,
x3) =
DEL238_IN_GGA(
x1,
x2)
U10_GGA(
x1,
x2,
x3) =
U10_GGA(
x3)
U32_GA(
x1,
x2,
x3,
x4) =
U32_GA(
x4)
U33_GA(
x1,
x2,
x3,
x4) =
U33_GA(
x4)
We have to consider all (P,R,Pi)-chains
(6) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U11_GA(T17, T18, del15_in_ga(T17, X14))
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → DEL15_IN_GA(T17, X14)
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → U13_GA(T17, T18, maxsort1_in_ga(T22, T18))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → U14_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAX44_IN_GA(.(t, T76), T78) → U1_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(f, T76), T78) → U2_GA(T76, T78, max44_in_ga(T76, T78))
MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U16_GA(T55, T61, T62, del71_in_gga(T61, T55, X14))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → DEL71_IN_GGA(T61, T55, X14)
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → U7_GGA(T133, X240, del101_in_ga(T133, X240))
DEL71_IN_GGA(f, T133, .(t, .(t, X240))) → DEL101_IN_GA(T133, X240)
DEL101_IN_GA(.(t, T149), .(t, X285)) → U3_GA(T149, X285, del101_in_ga(T149, X285))
DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_GA(T55, T61, T62, maxsort1_in_ga(T95, T62))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → U19_GA(T55, T57, T58, max44_in_ga(T55, T57))
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T57, T58)) → MAX44_IN_GA(T55, T57)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U21_GA(T55, T150, T151, del129_in_gga(T150, T55, X14))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → DEL129_IN_GGA(T150, T55, X14)
DEL129_IN_GGA(f, T181, .(t, X343)) → U8_GGA(T181, X343, del101_in_ga(.(f, T181), X343))
DEL129_IN_GGA(f, T181, .(t, X343)) → DEL101_IN_GA(.(f, T181), X343)
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_GA(T55, T150, T151, maxsort1_in_ga(T156, T151))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → U24_GA(T55, T57, T58, max150_in_ga(T55, T57))
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T57, T58)) → MAX150_IN_GA(T55, T57)
MAX150_IN_GA(.(f, T202), T204) → U4_GA(T202, T204, max150_in_ga(T202, T204))
MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)
MAX150_IN_GA(.(t, T212), T214) → U5_GA(T212, T214, max44_in_ga(T212, T214))
MAX150_IN_GA(.(t, T212), T214) → MAX44_IN_GA(T212, T214)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U26_GA(T55, T187, T188, del173_in_gga(T187, T55, X14))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → DEL173_IN_GGA(T187, T55, X14)
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → U9_GGA(T259, X500, del203_in_ga(T259, X500))
DEL173_IN_GGA(t, T259, .(f, .(f, X500))) → DEL203_IN_GA(T259, X500)
DEL203_IN_GA(.(f, T275), .(f, X547)) → U6_GA(T275, X547, del203_in_ga(T275, X547))
DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_GA(T55, T187, T188, maxsort1_in_ga(T221, T188))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → U29_GA(T286, T288, T289, max44_in_ga(T286, T288))
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T288, T289)) → MAX44_IN_GA(T286, T288)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U31_GA(T286, T292, T293, del238_in_gga(T292, T286, X14))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → DEL238_IN_GGA(T292, T286, X14)
DEL238_IN_GGA(t, T323, .(f, X623)) → U10_GGA(T323, X623, del203_in_ga(.(t, T323), X623))
DEL238_IN_GGA(t, T323, .(f, X623)) → DEL203_IN_GA(.(t, T323), X623)
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_GA(T286, T292, T293, maxsort1_in_ga(T298, T293))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
MAXSORT1_IN_GA(
x1,
x2) =
MAXSORT1_IN_GA(
x1)
U11_GA(
x1,
x2,
x3) =
U11_GA(
x3)
DEL15_IN_GA(
x1,
x2) =
DEL15_IN_GA(
x1)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x3)
U13_GA(
x1,
x2,
x3) =
U13_GA(
x3)
U14_GA(
x1,
x2,
x3,
x4) =
U14_GA(
x4)
MAX44_IN_GA(
x1,
x2) =
MAX44_IN_GA(
x1)
U1_GA(
x1,
x2,
x3) =
U1_GA(
x3)
U2_GA(
x1,
x2,
x3) =
U2_GA(
x3)
U15_GA(
x1,
x2,
x3,
x4) =
U15_GA(
x1,
x4)
U16_GA(
x1,
x2,
x3,
x4) =
U16_GA(
x4)
DEL71_IN_GGA(
x1,
x2,
x3) =
DEL71_IN_GGA(
x1,
x2)
U7_GGA(
x1,
x2,
x3) =
U7_GGA(
x3)
DEL101_IN_GA(
x1,
x2) =
DEL101_IN_GA(
x1)
U3_GA(
x1,
x2,
x3) =
U3_GA(
x3)
U17_GA(
x1,
x2,
x3,
x4) =
U17_GA(
x4)
U18_GA(
x1,
x2,
x3,
x4) =
U18_GA(
x4)
U19_GA(
x1,
x2,
x3,
x4) =
U19_GA(
x4)
U20_GA(
x1,
x2,
x3,
x4) =
U20_GA(
x1,
x4)
U21_GA(
x1,
x2,
x3,
x4) =
U21_GA(
x4)
DEL129_IN_GGA(
x1,
x2,
x3) =
DEL129_IN_GGA(
x1,
x2)
U8_GGA(
x1,
x2,
x3) =
U8_GGA(
x3)
U22_GA(
x1,
x2,
x3,
x4) =
U22_GA(
x4)
U23_GA(
x1,
x2,
x3,
x4) =
U23_GA(
x4)
U24_GA(
x1,
x2,
x3,
x4) =
U24_GA(
x4)
MAX150_IN_GA(
x1,
x2) =
MAX150_IN_GA(
x1)
U4_GA(
x1,
x2,
x3) =
U4_GA(
x3)
U5_GA(
x1,
x2,
x3) =
U5_GA(
x3)
U25_GA(
x1,
x2,
x3,
x4) =
U25_GA(
x1,
x4)
U26_GA(
x1,
x2,
x3,
x4) =
U26_GA(
x4)
DEL173_IN_GGA(
x1,
x2,
x3) =
DEL173_IN_GGA(
x1,
x2)
U9_GGA(
x1,
x2,
x3) =
U9_GGA(
x3)
DEL203_IN_GA(
x1,
x2) =
DEL203_IN_GA(
x1)
U6_GA(
x1,
x2,
x3) =
U6_GA(
x3)
U27_GA(
x1,
x2,
x3,
x4) =
U27_GA(
x4)
U28_GA(
x1,
x2,
x3,
x4) =
U28_GA(
x4)
U29_GA(
x1,
x2,
x3,
x4) =
U29_GA(
x4)
U30_GA(
x1,
x2,
x3,
x4) =
U30_GA(
x1,
x4)
U31_GA(
x1,
x2,
x3,
x4) =
U31_GA(
x4)
DEL238_IN_GGA(
x1,
x2,
x3) =
DEL238_IN_GGA(
x1,
x2)
U10_GGA(
x1,
x2,
x3) =
U10_GGA(
x3)
U32_GA(
x1,
x2,
x3,
x4) =
U32_GA(
x4)
U33_GA(
x1,
x2,
x3,
x4) =
U33_GA(
x4)
We have to consider all (P,R,Pi)-chains
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LOPSTR] contains 5 SCCs with 38 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
DEL203_IN_GA(
x1,
x2) =
DEL203_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(10) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(11) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DEL203_IN_GA(.(f, T275), .(f, X547)) → DEL203_IN_GA(T275, X547)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
f =
f
DEL203_IN_GA(
x1,
x2) =
DEL203_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(12) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DEL203_IN_GA(.(f, T275)) → DEL203_IN_GA(T275)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(14) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- DEL203_IN_GA(.(f, T275)) → DEL203_IN_GA(T275)
The graph contains the following edges 1 > 1
(15) YES
(16) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
DEL101_IN_GA(
x1,
x2) =
DEL101_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(17) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(18) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
DEL101_IN_GA(.(t, T149), .(t, X285)) → DEL101_IN_GA(T149, X285)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
t =
t
DEL101_IN_GA(
x1,
x2) =
DEL101_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(19) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(20) Obligation:
Q DP problem:
The TRS P consists of the following rules:
DEL101_IN_GA(.(t, T149)) → DEL101_IN_GA(T149)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(21) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- DEL101_IN_GA(.(t, T149)) → DEL101_IN_GA(T149)
The graph contains the following edges 1 > 1
(22) YES
(23) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
MAX44_IN_GA(
x1,
x2) =
MAX44_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(24) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(25) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAX44_IN_GA(.(f, T76), T78) → MAX44_IN_GA(T76, T78)
MAX44_IN_GA(.(t, T76), T78) → MAX44_IN_GA(T76, T78)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
t =
t
f =
f
MAX44_IN_GA(
x1,
x2) =
MAX44_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(26) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAX44_IN_GA(.(f, T76)) → MAX44_IN_GA(T76)
MAX44_IN_GA(.(t, T76)) → MAX44_IN_GA(T76)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(28) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MAX44_IN_GA(.(f, T76)) → MAX44_IN_GA(T76)
The graph contains the following edges 1 > 1
- MAX44_IN_GA(.(t, T76)) → MAX44_IN_GA(T76)
The graph contains the following edges 1 > 1
(29) YES
(30) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
MAX150_IN_GA(
x1,
x2) =
MAX150_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(31) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(32) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAX150_IN_GA(.(f, T202), T204) → MAX150_IN_GA(T202, T204)
R is empty.
The argument filtering Pi contains the following mapping:
.(
x1,
x2) =
.(
x1,
x2)
f =
f
MAX150_IN_GA(
x1,
x2) =
MAX150_IN_GA(
x1)
We have to consider all (P,R,Pi)-chains
(33) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAX150_IN_GA(.(f, T202)) → MAX150_IN_GA(T202)
R is empty.
Q is empty.
We have to consider all (P,Q,R)-chains.
(35) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MAX150_IN_GA(.(f, T202)) → MAX150_IN_GA(T202)
The graph contains the following edges 1 > 1
(36) YES
(37) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)
The TRS R consists of the following rules:
maxsort1_in_ga([], []) → maxsort1_out_ga([], [])
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U11_ga(T17, T18, del15_in_ga(T17, X14))
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
U11_ga(T17, T18, del15_out_ga(T17, X14)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
maxsort1_in_ga(.(T17, []), .(T17, T18)) → U12_ga(T17, T18, del15_in_ga(T17, T22))
U12_ga(T17, T18, del15_out_ga(T17, T22)) → U13_ga(T17, T18, maxsort1_in_ga(T22, T18))
maxsort1_in_ga(.(t, .(t, T55)), .(T57, T58)) → U14_ga(T55, T57, T58, max44_in_ga(T55, T57))
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U14_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(t, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(t, T55)), .(T61, T62)) → U15_ga(T55, T61, T62, max44_in_ga(T55, T61))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U16_ga(T55, T61, T62, del71_in_gga(T61, T55, X14))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U16_ga(T55, T61, T62, del71_out_gga(T61, T55, X14)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U15_ga(T55, T61, T62, max44_out_ga(T55, T61)) → U17_ga(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_ga(T55, T61, T62, del71_out_gga(T61, T55, T95)) → U18_ga(T55, T61, T62, maxsort1_in_ga(T95, T62))
maxsort1_in_ga(.(t, .(f, T55)), .(T57, T58)) → U19_ga(T55, T57, T58, max44_in_ga(T55, T57))
U19_ga(T55, T57, T58, max44_out_ga(T55, T57)) → maxsort1_out_ga(.(t, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(t, .(f, T55)), .(T150, T151)) → U20_ga(T55, T150, T151, max44_in_ga(T55, T150))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U21_ga(T55, T150, T151, del129_in_gga(T150, T55, X14))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U21_ga(T55, T150, T151, del129_out_gga(T150, T55, X14)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U20_ga(T55, T150, T151, max44_out_ga(T55, T150)) → U22_ga(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_ga(T55, T150, T151, del129_out_gga(T150, T55, T156)) → U23_ga(T55, T150, T151, maxsort1_in_ga(T156, T151))
maxsort1_in_ga(.(f, .(f, T55)), .(T57, T58)) → U24_ga(T55, T57, T58, max150_in_ga(T55, T57))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U24_ga(T55, T57, T58, max150_out_ga(T55, T57)) → maxsort1_out_ga(.(f, .(f, T55)), .(T57, T58))
maxsort1_in_ga(.(f, .(f, T55)), .(T187, T188)) → U25_ga(T55, T187, T188, max150_in_ga(T55, T187))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U26_ga(T55, T187, T188, del173_in_gga(T187, T55, X14))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U26_ga(T55, T187, T188, del173_out_gga(T187, T55, X14)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U25_ga(T55, T187, T188, max150_out_ga(T55, T187)) → U27_ga(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_ga(T55, T187, T188, del173_out_gga(T187, T55, T221)) → U28_ga(T55, T187, T188, maxsort1_in_ga(T221, T188))
maxsort1_in_ga(.(f, .(t, T286)), .(T288, T289)) → U29_ga(T286, T288, T289, max44_in_ga(T286, T288))
U29_ga(T286, T288, T289, max44_out_ga(T286, T288)) → maxsort1_out_ga(.(f, .(t, T286)), .(T288, T289))
maxsort1_in_ga(.(f, .(t, T286)), .(T292, T293)) → U30_ga(T286, T292, T293, max44_in_ga(T286, T292))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U31_ga(T286, T292, T293, del238_in_gga(T292, T286, X14))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
U31_ga(T286, T292, T293, del238_out_gga(T292, T286, X14)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U30_ga(T286, T292, T293, max44_out_ga(T286, T292)) → U32_ga(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_ga(T286, T292, T293, del238_out_gga(T292, T286, T298)) → U33_ga(T286, T292, T293, maxsort1_in_ga(T298, T293))
U33_ga(T286, T292, T293, maxsort1_out_ga(T298, T293)) → maxsort1_out_ga(.(f, .(t, T286)), .(T292, T293))
U28_ga(T55, T187, T188, maxsort1_out_ga(T221, T188)) → maxsort1_out_ga(.(f, .(f, T55)), .(T187, T188))
U23_ga(T55, T150, T151, maxsort1_out_ga(T156, T151)) → maxsort1_out_ga(.(t, .(f, T55)), .(T150, T151))
U18_ga(T55, T61, T62, maxsort1_out_ga(T95, T62)) → maxsort1_out_ga(.(t, .(t, T55)), .(T61, T62))
U13_ga(T17, T18, maxsort1_out_ga(T22, T18)) → maxsort1_out_ga(.(T17, []), .(T17, T18))
The argument filtering Pi contains the following mapping:
maxsort1_in_ga(
x1,
x2) =
maxsort1_in_ga(
x1)
[] =
[]
maxsort1_out_ga(
x1,
x2) =
maxsort1_out_ga
.(
x1,
x2) =
.(
x1,
x2)
U11_ga(
x1,
x2,
x3) =
U11_ga(
x3)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
U12_ga(
x1,
x2,
x3) =
U12_ga(
x3)
U13_ga(
x1,
x2,
x3) =
U13_ga(
x3)
U14_ga(
x1,
x2,
x3,
x4) =
U14_ga(
x4)
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
U15_ga(
x1,
x2,
x3,
x4) =
U15_ga(
x1,
x4)
U16_ga(
x1,
x2,
x3,
x4) =
U16_ga(
x4)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
U17_ga(
x1,
x2,
x3,
x4) =
U17_ga(
x4)
U18_ga(
x1,
x2,
x3,
x4) =
U18_ga(
x4)
U19_ga(
x1,
x2,
x3,
x4) =
U19_ga(
x4)
U20_ga(
x1,
x2,
x3,
x4) =
U20_ga(
x1,
x4)
U21_ga(
x1,
x2,
x3,
x4) =
U21_ga(
x4)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
U22_ga(
x1,
x2,
x3,
x4) =
U22_ga(
x4)
U23_ga(
x1,
x2,
x3,
x4) =
U23_ga(
x4)
U24_ga(
x1,
x2,
x3,
x4) =
U24_ga(
x4)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
U25_ga(
x1,
x2,
x3,
x4) =
U25_ga(
x1,
x4)
U26_ga(
x1,
x2,
x3,
x4) =
U26_ga(
x4)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
U27_ga(
x1,
x2,
x3,
x4) =
U27_ga(
x4)
U28_ga(
x1,
x2,
x3,
x4) =
U28_ga(
x4)
U29_ga(
x1,
x2,
x3,
x4) =
U29_ga(
x4)
U30_ga(
x1,
x2,
x3,
x4) =
U30_ga(
x1,
x4)
U31_ga(
x1,
x2,
x3,
x4) =
U31_ga(
x4)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
U32_ga(
x1,
x2,
x3,
x4) =
U32_ga(
x4)
U33_ga(
x1,
x2,
x3,
x4) =
U33_ga(
x4)
MAXSORT1_IN_GA(
x1,
x2) =
MAXSORT1_IN_GA(
x1)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x3)
U15_GA(
x1,
x2,
x3,
x4) =
U15_GA(
x1,
x4)
U17_GA(
x1,
x2,
x3,
x4) =
U17_GA(
x4)
U20_GA(
x1,
x2,
x3,
x4) =
U20_GA(
x1,
x4)
U22_GA(
x1,
x2,
x3,
x4) =
U22_GA(
x4)
U25_GA(
x1,
x2,
x3,
x4) =
U25_GA(
x1,
x4)
U27_GA(
x1,
x2,
x3,
x4) =
U27_GA(
x4)
U30_GA(
x1,
x2,
x3,
x4) =
U30_GA(
x1,
x4)
U32_GA(
x1,
x2,
x3,
x4) =
U32_GA(
x4)
We have to consider all (P,R,Pi)-chains
(38) UsableRulesProof (EQUIVALENT transformation)
For (infinitary) constructor rewriting [LOPSTR] we can delete all non-usable rules from R.
(39) Obligation:
Pi DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(T17, []), .(T17, T18)) → U12_GA(T17, T18, del15_in_ga(T17, T22))
U12_GA(T17, T18, del15_out_ga(T17, T22)) → MAXSORT1_IN_GA(T22, T18)
MAXSORT1_IN_GA(.(t, .(t, T55)), .(T61, T62)) → U15_GA(T55, T61, T62, max44_in_ga(T55, T61))
U15_GA(T55, T61, T62, max44_out_ga(T55, T61)) → U17_GA(T55, T61, T62, del71_in_gga(T61, T55, T95))
U17_GA(T55, T61, T62, del71_out_gga(T61, T55, T95)) → MAXSORT1_IN_GA(T95, T62)
MAXSORT1_IN_GA(.(t, .(f, T55)), .(T150, T151)) → U20_GA(T55, T150, T151, max44_in_ga(T55, T150))
U20_GA(T55, T150, T151, max44_out_ga(T55, T150)) → U22_GA(T55, T150, T151, del129_in_gga(T150, T55, T156))
U22_GA(T55, T150, T151, del129_out_gga(T150, T55, T156)) → MAXSORT1_IN_GA(T156, T151)
MAXSORT1_IN_GA(.(f, .(f, T55)), .(T187, T188)) → U25_GA(T55, T187, T188, max150_in_ga(T55, T187))
U25_GA(T55, T187, T188, max150_out_ga(T55, T187)) → U27_GA(T55, T187, T188, del173_in_gga(T187, T55, T221))
U27_GA(T55, T187, T188, del173_out_gga(T187, T55, T221)) → MAXSORT1_IN_GA(T221, T188)
MAXSORT1_IN_GA(.(f, .(t, T286)), .(T292, T293)) → U30_GA(T286, T292, T293, max44_in_ga(T286, T292))
U30_GA(T286, T292, T293, max44_out_ga(T286, T292)) → U32_GA(T286, T292, T293, del238_in_gga(T292, T286, T298))
U32_GA(T286, T292, T293, del238_out_gga(T292, T286, T298)) → MAXSORT1_IN_GA(T298, T293)
The TRS R consists of the following rules:
del15_in_ga(t, []) → del15_out_ga(t, [])
del15_in_ga(f, []) → del15_out_ga(f, [])
max44_in_ga([], t) → max44_out_ga([], t)
max44_in_ga(.(t, T76), T78) → U1_ga(T76, T78, max44_in_ga(T76, T78))
max44_in_ga(.(f, T76), T78) → U2_ga(T76, T78, max44_in_ga(T76, T78))
del71_in_gga(t, T110, .(t, T110)) → del71_out_gga(t, T110, .(t, T110))
del71_in_gga(f, T133, .(t, .(t, X240))) → U7_gga(T133, X240, del101_in_ga(T133, X240))
del129_in_gga(t, T171, .(f, T171)) → del129_out_gga(t, T171, .(f, T171))
del129_in_gga(f, T181, .(t, X343)) → U8_gga(T181, X343, del101_in_ga(.(f, T181), X343))
max150_in_ga([], f) → max150_out_ga([], f)
max150_in_ga(.(f, T202), T204) → U4_ga(T202, T204, max150_in_ga(T202, T204))
max150_in_ga(.(t, T212), T214) → U5_ga(T212, T214, max44_in_ga(T212, T214))
del173_in_gga(f, T236, .(f, T236)) → del173_out_gga(f, T236, .(f, T236))
del173_in_gga(t, T259, .(f, .(f, X500))) → U9_gga(T259, X500, del203_in_ga(T259, X500))
del238_in_gga(f, T313, .(t, T313)) → del238_out_gga(f, T313, .(t, T313))
del238_in_gga(t, T323, .(f, X623)) → U10_gga(T323, X623, del203_in_ga(.(t, T323), X623))
U1_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(t, T76), T78)
U2_ga(T76, T78, max44_out_ga(T76, T78)) → max44_out_ga(.(f, T76), T78)
U7_gga(T133, X240, del101_out_ga(T133, X240)) → del71_out_gga(f, T133, .(t, .(t, X240)))
U8_gga(T181, X343, del101_out_ga(.(f, T181), X343)) → del129_out_gga(f, T181, .(t, X343))
U4_ga(T202, T204, max150_out_ga(T202, T204)) → max150_out_ga(.(f, T202), T204)
U5_ga(T212, T214, max44_out_ga(T212, T214)) → max150_out_ga(.(t, T212), T214)
U9_gga(T259, X500, del203_out_ga(T259, X500)) → del173_out_gga(t, T259, .(f, .(f, X500)))
U10_gga(T323, X623, del203_out_ga(.(t, T323), X623)) → del238_out_gga(t, T323, .(f, X623))
del101_in_ga([], []) → del101_out_ga([], [])
del101_in_ga(.(f, T143), T143) → del101_out_ga(.(f, T143), T143)
del101_in_ga(.(t, T149), .(t, X285)) → U3_ga(T149, X285, del101_in_ga(T149, X285))
del203_in_ga([], []) → del203_out_ga([], [])
del203_in_ga(.(t, T269), T269) → del203_out_ga(.(t, T269), T269)
del203_in_ga(.(f, T275), .(f, X547)) → U6_ga(T275, X547, del203_in_ga(T275, X547))
U3_ga(T149, X285, del101_out_ga(T149, X285)) → del101_out_ga(.(t, T149), .(t, X285))
U6_ga(T275, X547, del203_out_ga(T275, X547)) → del203_out_ga(.(f, T275), .(f, X547))
The argument filtering Pi contains the following mapping:
[] =
[]
.(
x1,
x2) =
.(
x1,
x2)
del15_in_ga(
x1,
x2) =
del15_in_ga(
x1)
t =
t
del15_out_ga(
x1,
x2) =
del15_out_ga(
x2)
f =
f
max44_in_ga(
x1,
x2) =
max44_in_ga(
x1)
max44_out_ga(
x1,
x2) =
max44_out_ga(
x2)
U1_ga(
x1,
x2,
x3) =
U1_ga(
x3)
U2_ga(
x1,
x2,
x3) =
U2_ga(
x3)
del71_in_gga(
x1,
x2,
x3) =
del71_in_gga(
x1,
x2)
del71_out_gga(
x1,
x2,
x3) =
del71_out_gga(
x3)
U7_gga(
x1,
x2,
x3) =
U7_gga(
x3)
del101_in_ga(
x1,
x2) =
del101_in_ga(
x1)
del101_out_ga(
x1,
x2) =
del101_out_ga(
x2)
U3_ga(
x1,
x2,
x3) =
U3_ga(
x3)
del129_in_gga(
x1,
x2,
x3) =
del129_in_gga(
x1,
x2)
del129_out_gga(
x1,
x2,
x3) =
del129_out_gga(
x3)
U8_gga(
x1,
x2,
x3) =
U8_gga(
x3)
max150_in_ga(
x1,
x2) =
max150_in_ga(
x1)
max150_out_ga(
x1,
x2) =
max150_out_ga(
x2)
U4_ga(
x1,
x2,
x3) =
U4_ga(
x3)
U5_ga(
x1,
x2,
x3) =
U5_ga(
x3)
del173_in_gga(
x1,
x2,
x3) =
del173_in_gga(
x1,
x2)
del173_out_gga(
x1,
x2,
x3) =
del173_out_gga(
x3)
U9_gga(
x1,
x2,
x3) =
U9_gga(
x3)
del203_in_ga(
x1,
x2) =
del203_in_ga(
x1)
del203_out_ga(
x1,
x2) =
del203_out_ga(
x2)
U6_ga(
x1,
x2,
x3) =
U6_ga(
x3)
del238_in_gga(
x1,
x2,
x3) =
del238_in_gga(
x1,
x2)
del238_out_gga(
x1,
x2,
x3) =
del238_out_gga(
x3)
U10_gga(
x1,
x2,
x3) =
U10_gga(
x3)
MAXSORT1_IN_GA(
x1,
x2) =
MAXSORT1_IN_GA(
x1)
U12_GA(
x1,
x2,
x3) =
U12_GA(
x3)
U15_GA(
x1,
x2,
x3,
x4) =
U15_GA(
x1,
x4)
U17_GA(
x1,
x2,
x3,
x4) =
U17_GA(
x4)
U20_GA(
x1,
x2,
x3,
x4) =
U20_GA(
x1,
x4)
U22_GA(
x1,
x2,
x3,
x4) =
U22_GA(
x4)
U25_GA(
x1,
x2,
x3,
x4) =
U25_GA(
x1,
x4)
U27_GA(
x1,
x2,
x3,
x4) =
U27_GA(
x4)
U30_GA(
x1,
x2,
x3,
x4) =
U30_GA(
x1,
x4)
U32_GA(
x1,
x2,
x3,
x4) =
U32_GA(
x4)
We have to consider all (P,R,Pi)-chains
(40) PiDPToQDPProof (SOUND transformation)
Transforming (infinitary) constructor rewriting Pi-DP problem [LOPSTR] into ordinary QDP problem [LPAR04] by application of Pi.
(41) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(T17, [])) → U12_GA(del15_in_ga(T17))
U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del15_in_ga(t) → del15_out_ga([])
del15_in_ga(f) → del15_out_ga([])
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
del15_in_ga(x0)
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(42) Narrowing (SOUND transformation)
By narrowing [LPAR04] the rule
MAXSORT1_IN_GA(
.(
T17,
[])) →
U12_GA(
del15_in_ga(
T17)) at position [0] we obtained the following new rules [LPAR04]:
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))
(43) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))
The TRS R consists of the following rules:
del15_in_ga(t) → del15_out_ga([])
del15_in_ga(f) → del15_out_ga([])
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
del15_in_ga(x0)
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(44) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(45) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
del15_in_ga(x0)
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(46) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del15_in_ga(x0)
(47) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U12_GA(del15_out_ga(T22)) → MAXSORT1_IN_GA(T22)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(48) Instantiation (EQUIVALENT transformation)
By instantiating [LPAR04] the rule
U12_GA(
del15_out_ga(
T22)) →
MAXSORT1_IN_GA(
T22) we obtained the following new rules [LPAR04]:
U12_GA(del15_out_ga([])) → MAXSORT1_IN_GA([])
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
MAXSORT1_IN_GA(.(t, [])) → U12_GA(del15_out_ga([]))
MAXSORT1_IN_GA(.(f, [])) → U12_GA(del15_out_ga([]))
U12_GA(del15_out_ga([])) → MAXSORT1_IN_GA([])
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(50) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 3 less nodes.
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(52) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U20_GA(T55, max44_out_ga(T150)) → U22_GA(del129_in_gga(T150, T55))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(U15_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(max44_out_ga(x1)) = | | + | | · | x1 |
POL(U17_GA(x1)) = | 0 | + | | · | x1 |
POL(del71_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del71_out_gga(x1)) = | | + | | · | x1 |
POL(MAXSORT1_IN_GA(x1)) = | 0 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(max44_in_ga(x1)) = | | + | | · | x1 |
POL(U20_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(U22_GA(x1)) = | 0 | + | | · | x1 |
POL(del129_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del129_out_gga(x1)) = | | + | | · | x1 |
POL(U25_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(max150_in_ga(x1)) = | | + | | · | x1 |
POL(max150_out_ga(x1)) = | | + | | · | x1 |
POL(U27_GA(x1)) = | 0 | + | | · | x1 |
POL(del173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del173_out_gga(x1)) = | | + | | · | x1 |
POL(U30_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(U32_GA(x1)) = | 0 | + | | · | x1 |
POL(del238_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del238_out_gga(x1)) = | | + | | · | x1 |
POL(del101_in_ga(x1)) = | | + | | · | x1 |
POL(del203_in_ga(x1)) = | | + | | · | x1 |
POL(del203_out_ga(x1)) = | | + | | · | x1 |
POL(del101_out_ga(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
MAXSORT1_IN_GA(.(t, .(f, T55))) → U20_GA(T55, max44_in_ga(T55))
U22_GA(del129_out_gga(T156)) → MAXSORT1_IN_GA(T156)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(54) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(55) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del129_in_gga(t, T171) → del129_out_gga(.(f, T171))
del129_in_gga(f, T181) → U8_gga(del101_in_ga(.(f, T181)))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
U8_gga(del101_out_ga(X343)) → del129_out_gga(.(t, X343))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(56) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(57) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
del129_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U8_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(58) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del129_in_gga(x0, x1)
U8_gga(x0)
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(60) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
U30_GA(T286, max44_out_ga(T292)) → U32_GA(del238_in_gga(T292, T286))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(U17_GA(x1)) = | 0 | + | | · | x1 |
POL(del71_out_gga(x1)) = | | + | | · | x1 |
POL(MAXSORT1_IN_GA(x1)) = | 0 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U15_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(max44_in_ga(x1)) = | | + | | · | x1 |
POL(max44_out_ga(x1)) = | | + | | · | x1 |
POL(del71_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U25_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(max150_in_ga(x1)) = | | + | | · | x1 |
POL(max150_out_ga(x1)) = | | + | | · | x1 |
POL(U27_GA(x1)) = | 0 | + | | · | x1 |
POL(del173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del173_out_gga(x1)) = | | + | | · | x1 |
POL(U30_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(U32_GA(x1)) = | 0 | + | | · | x1 |
POL(del238_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del238_out_gga(x1)) = | | + | | · | x1 |
POL(del101_in_ga(x1)) = | | + | | · | x1 |
POL(del203_in_ga(x1)) = | | + | | · | x1 |
POL(del203_out_ga(x1)) = | | + | | · | x1 |
POL(del101_out_ga(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(t, T286))) → U30_GA(T286, max44_in_ga(T286))
U32_GA(del238_out_gga(T298)) → MAXSORT1_IN_GA(T298)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(62) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
The TRS R consists of the following rules:
del238_in_gga(f, T313) → del238_out_gga(.(t, T313))
del238_in_gga(t, T323) → U10_gga(del203_in_ga(.(t, T323)))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U10_gga(del203_out_ga(X623)) → del238_out_gga(.(f, X623))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(64) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
The TRS R consists of the following rules:
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
del238_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
U10_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(66) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del238_in_gga(x0, x1)
U10_gga(x0)
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
The TRS R consists of the following rules:
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(68) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MAXSORT1_IN_GA(.(t, .(t, T55))) → U15_GA(T55, max44_in_ga(T55))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(MAXSORT1_IN_GA(x1)) = | 0 | + | | · | x1 |
POL(.(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(U15_GA(x1, x2)) = | 1 | + | | · | x1 | + | | · | x2 |
POL(max44_in_ga(x1)) = | | + | | · | x1 |
POL(max44_out_ga(x1)) = | | + | | · | x1 |
POL(U17_GA(x1)) = | 0 | + | | · | x1 |
POL(del71_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del71_out_gga(x1)) = | | + | | · | x1 |
POL(U25_GA(x1, x2)) = | 0 | + | | · | x1 | + | | · | x2 |
POL(max150_in_ga(x1)) = | | + | | · | x1 |
POL(max150_out_ga(x1)) = | | + | | · | x1 |
POL(U27_GA(x1)) = | 0 | + | | · | x1 |
POL(del173_in_gga(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(del173_out_gga(x1)) = | | + | | · | x1 |
POL(del101_in_ga(x1)) = | | + | | · | x1 |
POL(del203_in_ga(x1)) = | | + | | · | x1 |
POL(del203_out_ga(x1)) = | | + | | · | x1 |
POL(del101_out_ga(x1)) = | | + | | · | x1 |
The following usable rules [FROCOS05] were oriented:
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U15_GA(T55, max44_out_ga(T61)) → U17_GA(del71_in_gga(T61, T55))
U17_GA(del71_out_gga(T95)) → MAXSORT1_IN_GA(T95)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
The TRS R consists of the following rules:
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(70) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(71) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del71_in_gga(t, T110) → del71_out_gga(.(t, T110))
del71_in_gga(f, T133) → U7_gga(del101_in_ga(T133))
del101_in_ga(.(f, T143)) → del101_out_ga(T143)
del101_in_ga([]) → del101_out_ga([])
del101_in_ga(.(t, T149)) → U3_ga(del101_in_ga(T149))
U7_gga(del101_out_ga(X240)) → del71_out_gga(.(t, .(t, X240)))
U3_ga(del101_out_ga(X285)) → del101_out_ga(.(t, X285))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(72) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(73) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
max44_in_ga(x0)
del71_in_gga(x0, x1)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U7_gga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del101_in_ga(x0)
del203_in_ga(x0)
U3_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(74) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
del71_in_gga(x0, x1)
U7_gga(x0)
del101_in_ga(x0)
U3_ga(x0)
(75) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
max44_in_ga(x0)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(76) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
max150_in_ga(.(t, T212)) → U5_ga(max44_in_ga(T212))
max44_in_ga([]) → max44_out_ga(t)
max44_in_ga(.(t, T76)) → U1_ga(max44_in_ga(T76))
U5_ga(max44_out_ga(T214)) → max150_out_ga(T214)
U1_ga(max44_out_ga(T78)) → max44_out_ga(T78)
del203_in_ga(.(t, T269)) → del203_out_ga(T269)
U9_gga(del203_out_ga(X500)) → del173_out_gga(.(f, .(f, X500)))
Used ordering: Polynomial interpretation [POLO]:
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(MAXSORT1_IN_GA(x1)) = x1
POL(U1_ga(x1)) = 1 + x1
POL(U25_GA(x1, x2)) = 2·x1 + x2
POL(U27_GA(x1)) = x1
POL(U2_ga(x1)) = x1
POL(U4_ga(x1)) = x1
POL(U5_ga(x1)) = 1 + x1
POL(U6_ga(x1)) = 2·x1
POL(U9_gga(x1)) = 1 + 2·x1
POL([]) = 0
POL(del173_in_gga(x1, x2)) = x1 + 2·x2
POL(del173_out_gga(x1)) = x1
POL(del203_in_ga(x1)) = x1
POL(del203_out_ga(x1)) = 2·x1
POL(f) = 0
POL(max150_in_ga(x1)) = 2·x1
POL(max150_out_ga(x1)) = x1
POL(max44_in_ga(x1)) = 2 + x1
POL(max44_out_ga(x1)) = x1
POL(t) = 1
(77) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
max44_in_ga(.(f, T76)) → U2_ga(max44_in_ga(T76))
U2_ga(max44_out_ga(T78)) → max44_out_ga(T78)
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
max44_in_ga(x0)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(78) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
max44_in_ga(x0)
max150_in_ga(x0)
del173_in_gga(x0, x1)
U1_ga(x0)
U2_ga(x0)
U4_ga(x0)
U5_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(80) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
max44_in_ga(x0)
U1_ga(x0)
U2_ga(x0)
U5_ga(x0)
(81) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(82) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
No dependency pairs are removed.
The following rules are removed from R:
del173_in_gga(t, T259) → U9_gga(del203_in_ga(T259))
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(.(x1, x2)) = 2·x1 + 2·x2
POL(MAXSORT1_IN_GA(x1)) = x1
POL(U25_GA(x1, x2)) = 2·x1 + x2
POL(U27_GA(x1)) = x1
POL(U4_ga(x1)) = x1
POL(U6_ga(x1)) = 2·x1
POL(U9_gga(x1)) = 2 + x1
POL([]) = 0
POL(del173_in_gga(x1, x2)) = x1 + 2·x2
POL(del173_out_gga(x1)) = x1
POL(del203_in_ga(x1)) = x1
POL(del203_out_ga(x1)) = x1
POL(f) = 0
POL(max150_in_ga(x1)) = 2·x1
POL(max150_out_ga(x1)) = 2·x1
POL(t) = 2
(83) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
del203_in_ga([]) → del203_out_ga([])
del203_in_ga(.(f, T275)) → U6_ga(del203_in_ga(T275))
U6_ga(del203_out_ga(X547)) → del203_out_ga(.(f, X547))
The set Q consists of the following terms:
max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(84) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(85) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
The set Q consists of the following terms:
max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
We have to consider all (P,Q,R)-chains.
(86) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
U9_gga(x0)
del203_in_ga(x0)
U6_ga(x0)
(87) Obligation:
Q DP problem:
The TRS P consists of the following rules:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
The set Q consists of the following terms:
max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
We have to consider all (P,Q,R)-chains.
(88) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
U25_GA(T55, max150_out_ga(T187)) → U27_GA(del173_in_gga(T187, T55))
U27_GA(del173_out_gga(T221)) → MAXSORT1_IN_GA(T221)
The following rules are removed from R:
max150_in_ga([]) → max150_out_ga(f)
max150_in_ga(.(f, T202)) → U4_ga(max150_in_ga(T202))
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(.(x1, x2)) = x1 + 2·x2
POL(MAXSORT1_IN_GA(x1)) = x1
POL(U25_GA(x1, x2)) = 2 + 2·x1 + x2
POL(U27_GA(x1)) = 1 + x1
POL(U4_ga(x1)) = x1
POL([]) = 2
POL(del173_in_gga(x1, x2)) = x1 + 2·x2
POL(del173_out_gga(x1)) = x1
POL(f) = 1
POL(max150_in_ga(x1)) = 1 + x1
POL(max150_out_ga(x1)) = 2·x1
(89) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MAXSORT1_IN_GA(.(f, .(f, T55))) → U25_GA(T55, max150_in_ga(T55))
The TRS R consists of the following rules:
U4_ga(max150_out_ga(T204)) → max150_out_ga(T204)
del173_in_gga(f, T236) → del173_out_gga(.(f, T236))
The set Q consists of the following terms:
max150_in_ga(x0)
del173_in_gga(x0, x1)
U4_ga(x0)
We have to consider all (P,Q,R)-chains.
(90) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(91) TRUE