We consider the system Applicative_first_order_05__#3.55. Alphabet: 0 : [] --> b add : [b * c] --> c app : [c * c] --> c false : [] --> a filter : [b -> a * c] --> c filter2 : [a * b -> a * b * c] --> c high : [b * c] --> c if!fac6220high : [a * b * c] --> c if!fac6220low : [a * b * c] --> c le : [b * b] --> a low : [b * c] --> c map : [b -> b * c] --> c minus : [b * b] --> b nil : [] --> c quicksort : [c] --> c quot : [b * b] --> b s : [b] --> b true : [] --> a Rules: minus(x, 0) => x minus(s(x), s(y)) => minus(x, y) quot(0, s(x)) => 0 quot(s(x), s(y)) => s(quot(minus(x, y), s(y))) le(0, x) => true le(s(x), 0) => false le(s(x), s(y)) => le(x, y) app(nil, x) => x app(add(x, y), z) => add(x, app(y, z)) low(x, nil) => nil low(x, add(y, z)) => if!fac6220low(le(y, x), x, add(y, z)) if!fac6220low(true, x, add(y, z)) => add(y, low(x, z)) if!fac6220low(false, x, add(y, z)) => low(x, z) high(x, nil) => nil high(x, add(y, z)) => if!fac6220high(le(y, x), x, add(y, z)) if!fac6220high(true, x, add(y, z)) => high(x, z) if!fac6220high(false, x, add(y, z)) => add(y, high(x, z)) quicksort(nil) => nil quicksort(add(x, y)) => app(quicksort(low(x, y)), add(x, quicksort(high(x, y)))) map(f, nil) => nil map(f, add(x, y)) => add(f x, map(f, y)) filter(f, nil) => nil filter(f, add(x, y)) => filter2(f x, f, x, y) filter2(true, f, x, y) => add(x, filter(f, y)) filter2(false, f, x, y) => filter(f, y) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use the dependency pair framework as described in [Kop12, Ch. 6/7], with static dependency pairs (see [KusIsoSakBla09] and the adaptation for AFSMs and accessible arguments in [Kop13]). We thus obtain the following dependency pair problem (P_0, R_0, static, formative): Dependency Pairs P_0: 0] minus#(s(X), s(Y)) =#> minus#(X, Y) 1] quot#(s(X), s(Y)) =#> quot#(minus(X, Y), s(Y)) 2] quot#(s(X), s(Y)) =#> minus#(X, Y) 3] le#(s(X), s(Y)) =#> le#(X, Y) 4] app#(add(X, Y), Z) =#> app#(Y, Z) 5] low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) 6] low#(X, add(Y, Z)) =#> le#(Y, X) 7] if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) 8] if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) 9] high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) 10] high#(X, add(Y, Z)) =#> le#(Y, X) 11] if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) 12] if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) 13] quicksort#(add(X, Y)) =#> app#(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) 14] quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) 15] quicksort#(add(X, Y)) =#> low#(X, Y) 16] quicksort#(add(X, Y)) =#> quicksort#(high(X, Y)) 17] quicksort#(add(X, Y)) =#> high#(X, Y) 18] map#(F, add(X, Y)) =#> map#(F, Y) 19] filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) 20] filter2#(true, F, X, Y) =#> filter#(F, Y) 21] filter2#(false, F, X, Y) =#> filter#(F, Y) Rules R_0: minus(X, 0) => X minus(s(X), s(Y)) => minus(X, Y) quot(0, s(X)) => 0 quot(s(X), s(Y)) => s(quot(minus(X, Y), s(Y))) le(0, X) => true le(s(X), 0) => false le(s(X), s(Y)) => le(X, Y) app(nil, X) => X app(add(X, Y), Z) => add(X, app(Y, Z)) low(X, nil) => nil low(X, add(Y, Z)) => if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) => add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) => low(X, Z) high(X, nil) => nil high(X, add(Y, Z)) => if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) => high(X, Z) if!fac6220high(false, X, add(Y, Z)) => add(Y, high(X, Z)) quicksort(nil) => nil quicksort(add(X, Y)) => app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) => nil map(F, add(X, Y)) => add(F X, map(F, Y)) filter(F, nil) => nil filter(F, add(X, Y)) => filter2(F X, F, X, Y) filter2(true, F, X, Y) => add(X, filter(F, Y)) filter2(false, F, X, Y) => filter(F, Y) Thus, the original system is terminating if (P_0, R_0, static, formative) is finite. We consider the dependency pair problem (P_0, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: minus#(s(X), s(Y)) >? minus#(X, Y) quot#(s(X), s(Y)) >? quot#(minus(X, Y), s(Y)) quot#(s(X), s(Y)) >? minus#(X, Y) le#(s(X), s(Y)) >? le#(X, Y) app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) low#(X, add(Y, Z)) >? le#(Y, X) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) >? le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? app#(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? low#(X, Y) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) quicksort#(add(X, Y)) >? high#(X, Y) map#(F, add(X, Y)) >? map#(F, Y) filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.2 + y1 app# = \y0y1.0 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.0 filter# = \G0y1.0 high = \y0y1.0 high# = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.1 le = \y0y1.0 le# = \y0y1.0 low = \y0y1.0 low# = \y0y1.1 map = \G0y1.2G0(y1) map# = \G0y1.0 minus = \y0y1.y0 minus# = \y0y1.0 nil = 0 quicksort = \y0.2 quicksort# = \y0.3 quot = \y0y1.0 quot# = \y0y1.3 s = \y0.y0 true = 0 Using this interpretation, the requirements translate to: [[minus#(s(_x0), s(_x1))]] = 0 >= 0 = [[minus#(_x0, _x1)]] [[quot#(s(_x0), s(_x1))]] = 3 >= 3 = [[quot#(minus(_x0, _x1), s(_x1))]] [[quot#(s(_x0), s(_x1))]] = 3 > 0 = [[minus#(_x0, _x1)]] [[le#(s(_x0), s(_x1))]] = 0 >= 0 = [[le#(_x0, _x1)]] [[app#(add(_x0, _x1), _x2)]] = 0 >= 0 = [[app#(_x1, _x2)]] [[low#(_x0, add(_x1, _x2))]] = 1 >= 1 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[low#(_x0, add(_x1, _x2))]] = 1 > 0 = [[le#(_x1, _x0)]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 1 >= 1 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 1 >= 1 = [[low#(_x0, _x2)]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[le#(_x1, _x0)]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[quicksort#(add(_x0, _x1))]] = 3 > 0 = [[app#(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[quicksort#(add(_x0, _x1))]] = 3 >= 3 = [[quicksort#(low(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 3 > 1 = [[low#(_x0, _x1)]] [[quicksort#(add(_x0, _x1))]] = 3 >= 3 = [[quicksort#(high(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 3 > 0 = [[high#(_x0, _x1)]] [[map#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[filter2#(true, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 0 >= 0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = 2 + x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = 2 + x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 2 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 2 >= 2 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 2F0(0) >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 2F0(0) >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_0, R_0, static, formative) by (P_1, R_0, static, formative), where P_1 consists of: minus#(s(X), s(Y)) =#> minus#(X, Y) quot#(s(X), s(Y)) =#> quot#(minus(X, Y), s(Y)) le#(s(X), s(Y)) =#> le#(X, Y) app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) =#> le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) quicksort#(add(X, Y)) =#> quicksort#(high(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) filter2#(true, F, X, Y) =#> filter#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if (P_1, R_0, static, formative) is finite. We consider the dependency pair problem (P_1, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: minus#(s(X), s(Y)) >? minus#(X, Y) quot#(s(X), s(Y)) >? quot#(minus(X, Y), s(Y)) le#(s(X), s(Y)) >? le#(X, Y) app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) >? le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 app# = \y0y1.0 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.0 filter# = \G0y1.0 high = \y0y1.0 high# = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.0 le = \y0y1.0 le# = \y0y1.0 low = \y0y1.0 low# = \y0y1.0 map = \G0y1.2G0(y1) map# = \G0y1.0 minus = \y0y1.y0 minus# = \y0y1.y1 nil = 0 quicksort = \y0.2 quicksort# = \y0.0 quot = \y0y1.2y0 quot# = \y0y1.0 s = \y0.2 + y0 true = 0 Using this interpretation, the requirements translate to: [[minus#(s(_x0), s(_x1))]] = 2 + x1 > x1 = [[minus#(_x0, _x1)]] [[quot#(s(_x0), s(_x1))]] = 0 >= 0 = [[quot#(minus(_x0, _x1), s(_x1))]] [[le#(s(_x0), s(_x1))]] = 0 >= 0 = [[le#(_x0, _x1)]] [[app#(add(_x0, _x1), _x2)]] = 0 >= 0 = [[app#(_x1, _x2)]] [[low#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[le#(_x1, _x0)]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(low(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(high(_x0, _x1))]] [[map#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[filter2#(true, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 2 + x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 4 + 2x0 >= 2 + 2x0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 2 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 2 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 2F0(0) >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 2F0(0) >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_1, R_0, static, formative) by (P_2, R_0, static, formative), where P_2 consists of: quot#(s(X), s(Y)) =#> quot#(minus(X, Y), s(Y)) le#(s(X), s(Y)) =#> le#(X, Y) app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) =#> le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) quicksort#(add(X, Y)) =#> quicksort#(high(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) filter2#(true, F, X, Y) =#> filter#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if (P_2, R_0, static, formative) is finite. We consider the dependency pair problem (P_2, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: quot#(s(X), s(Y)) >? quot#(minus(X, Y), s(Y)) le#(s(X), s(Y)) >? le#(X, Y) app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) >? le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 app# = \y0y1.0 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.0 filter# = \G0y1.0 high = \y0y1.0 high# = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.0 le = \y0y1.0 le# = \y0y1.0 low = \y0y1.0 low# = \y0y1.0 map = \G0y1.0 map# = \G0y1.0 minus = \y0y1.y0 nil = 0 quicksort = \y0.0 quicksort# = \y0.0 quot = \y0y1.y0 quot# = \y0y1.y0 s = \y0.2 + y0 true = 0 Using this interpretation, the requirements translate to: [[quot#(s(_x0), s(_x1))]] = 2 + x0 > x0 = [[quot#(minus(_x0, _x1), s(_x1))]] [[le#(s(_x0), s(_x1))]] = 0 >= 0 = [[le#(_x0, _x1)]] [[app#(add(_x0, _x1), _x2)]] = 0 >= 0 = [[app#(_x1, _x2)]] [[low#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[le#(_x1, _x0)]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(low(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(high(_x0, _x1))]] [[map#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[filter2#(true, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 2 + x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 2 + x0 >= 2 + x0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_2, R_0, static, formative) by (P_3, R_0, static, formative), where P_3 consists of: le#(s(X), s(Y)) =#> le#(X, Y) app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) =#> le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) quicksort#(add(X, Y)) =#> quicksort#(high(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) filter2#(true, F, X, Y) =#> filter#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if (P_3, R_0, static, formative) is finite. We consider the dependency pair problem (P_3, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: le#(s(X), s(Y)) >? le#(X, Y) app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) >? le#(Y, X) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 app# = \y0y1.0 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.0 filter# = \G0y1.0 high = \y0y1.0 high# = \y0y1.1 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.1 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.0 le = \y0y1.0 le# = \y0y1.0 low = \y0y1.0 low# = \y0y1.0 map = \G0y1.0 map# = \G0y1.0 minus = \y0y1.2y0 nil = 0 quicksort = \y0.2 quicksort# = \y0.0 quot = \y0y1.0 s = \y0.2y0 true = 0 Using this interpretation, the requirements translate to: [[le#(s(_x0), s(_x1))]] = 0 >= 0 = [[le#(_x0, _x1)]] [[app#(add(_x0, _x1), _x2)]] = 0 >= 0 = [[app#(_x1, _x2)]] [[low#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[high#(_x0, add(_x1, _x2))]] = 1 >= 1 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[high#(_x0, add(_x1, _x2))]] = 1 > 0 = [[le#(_x1, _x0)]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 1 >= 1 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 1 >= 1 = [[high#(_x0, _x2)]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(low(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(high(_x0, _x1))]] [[map#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[filter2#(true, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[minus(_x0, 0)]] = 2x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 4x0 >= 2x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 0 >= 0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 2 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 2 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_3, R_0, static, formative) by (P_4, R_0, static, formative), where P_4 consists of: le#(s(X), s(Y)) =#> le#(X, Y) app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) quicksort#(add(X, Y)) =#> quicksort#(high(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) filter2#(true, F, X, Y) =#> filter#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if (P_4, R_0, static, formative) is finite. We consider the dependency pair problem (P_4, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: le#(s(X), s(Y)) >? le#(X, Y) app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.2y1 app# = \y0y1.0 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.0 filter# = \G0y1.0 high = \y0y1.0 high# = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.0 le = \y0y1.0 le# = \y0y1.y1 low = \y0y1.0 low# = \y0y1.0 map = \G0y1.0 map# = \G0y1.0 minus = \y0y1.y0 nil = 0 quicksort = \y0.0 quicksort# = \y0.0 quot = \y0y1.y0 s = \y0.1 + y0 true = 0 Using this interpretation, the requirements translate to: [[le#(s(_x0), s(_x1))]] = 1 + x1 > x1 = [[le#(_x0, _x1)]] [[app#(add(_x0, _x1), _x2)]] = 0 >= 0 = [[app#(_x1, _x2)]] [[low#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(low(_x0, _x1))]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(high(_x0, _x1))]] [[map#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2#(_F0 _x1, _F0, _x1, _x2)]] [[filter2#(true, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter#(_F0, _x2)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 1 + x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 1 + x0 >= 1 + x0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = 2x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = 2x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_4, R_0, static, formative) by (P_5, R_0, static, formative), where P_5 consists of: app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) quicksort#(add(X, Y)) =#> quicksort#(high(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) filter#(F, add(X, Y)) =#> filter2#(F X, F, X, Y) filter2#(true, F, X, Y) =#> filter#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if (P_5, R_0, static, formative) is finite. We consider the dependency pair problem (P_5, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) quicksort#(add(X, Y)) >? quicksort#(high(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) filter#(F, add(X, Y)) >? filter2#(F X, F, X, Y) filter2#(true, F, X, Y) >? filter#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[app#(x_1, x_2)]] = x_2 [[false]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_1, x_3) [[filter2#(x_1, x_2, x_3, x_4)]] = filter2#(x_2, x_4, x_1) [[high(x_1, x_2)]] = x_2 [[if!fac6220high(x_1, x_2, x_3)]] = x_3 [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_2, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = x_3 [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[low(x_1, x_2)]] = x_2 [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = x_1 [[true]] = _|_ We choose Lex = {@_{o -> o}, filter, filter2, filter2#, filter#} and Mul = {add, app, high#, if!fac6220high#, if!fac6220low#, le, low#, map, map#, quicksort, quicksort#, s}, and the following precedence: if!fac6220low# = low# > quicksort > map > filter = filter2 > app > add > high# = if!fac6220high# > quicksort# > s > le > map# > @_{o -> o} = filter2# = filter# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: X >= X low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) quicksort#(add(X, Y)) >= quicksort#(Y) quicksort#(add(X, Y)) > quicksort#(Y) map#(F, add(X, Y)) >= map#(F, Y) filter#(F, add(X, Y)) > filter2#(@_{o -> o}(F, X), F, X, Y) filter2#(_|_, F, X, Y) > filter#(F, Y) filter2#(_|_, F, X, Y) >= filter#(F, Y) X >= X s(X) >= X _|_ >= _|_ s(X) >= s(X) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= add(X, Y) add(X, Y) >= Y _|_ >= _|_ add(X, Y) >= add(X, Y) add(X, Y) >= Y add(X, Y) >= add(X, Y) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(Y))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) filter2(_|_, F, X, Y) >= filter(F, Y) With these choices, we have: 1] X >= X by (Meta) 2] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [3] and [4], by (Fun) 3] X >= X by (Meta) 4] add(Y, Z) >= add(Y, Z) because add in Mul, [5] and [6], by (Fun) 5] Y >= Y by (Meta) 6] Z >= Z by (Meta) 7] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [8] and [9], by (Fun) 8] X >= X by (Meta) 9] add(Y, Z) >= Z because [10], by (Star) 10] add*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [13] and [14], by (Fun) 13] X >= X by (Meta) 14] add(Y, Z) >= Z because [15], by (Star) 15] add*(Y, Z) >= Z because [16], by (Select) 16] Z >= Z by (Meta) 17] high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) because high# = if!fac6220high#, high# in Mul, [18] and [19], by (Fun) 18] X >= X by (Meta) 19] add(Y, Z) >= add(Y, Z) because add in Mul, [20] and [21], by (Fun) 20] Y >= Y by (Meta) 21] Z >= Z by (Meta) 22] if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [23] and [24], by (Fun) 23] X >= X by (Meta) 24] add(Y, Z) >= Z because [25], by (Star) 25] add*(Y, Z) >= Z because [26], by (Select) 26] Z >= Z by (Meta) 27] if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [28] and [29], by (Fun) 28] X >= X by (Meta) 29] add(Y, Z) >= Z because [30], by (Star) 30] add*(Y, Z) >= Z because [31], by (Select) 31] Z >= Z by (Meta) 32] quicksort#(add(X, Y)) >= quicksort#(Y) because [33], by (Star) 33] quicksort#*(add(X, Y)) >= quicksort#(Y) because [34], by (Select) 34] add(X, Y) >= quicksort#(Y) because [35], by (Star) 35] add*(X, Y) >= quicksort#(Y) because add > quicksort# and [36], by (Copy) 36] add*(X, Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] quicksort#(add(X, Y)) > quicksort#(Y) because [39], by definition 39] quicksort#*(add(X, Y)) >= quicksort#(Y) because [40], by (Select) 40] add(X, Y) >= quicksort#(Y) because [41], by (Star) 41] add*(X, Y) >= quicksort#(Y) because add > quicksort# and [42], by (Copy) 42] add*(X, Y) >= Y because [37], by (Select) 43] map#(F, add(X, Y)) >= map#(F, Y) because map# in Mul, [44] and [45], by (Fun) 44] F >= F by (Meta) 45] add(X, Y) >= Y because [46], by (Star) 46] add*(X, Y) >= Y because [47], by (Select) 47] Y >= Y by (Meta) 48] filter#(F, add(X, Y)) > filter2#(@_{o -> o}(F, X), F, X, Y) because [49], by definition 49] filter#*(F, add(X, Y)) >= filter2#(@_{o -> o}(F, X), F, X, Y) because filter# = filter2#, [50], [51], [54], [58] and [61], by (Stat) 50] F >= F by (Meta) 51] add(X, Y) > Y because [52], by definition 52] add*(X, Y) >= Y because [53], by (Select) 53] Y >= Y by (Meta) 54] filter#*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter# = @_{o -> o}, [50], [55], [58] and [59], by (Stat) 55] add(X, Y) > X because [56], by definition 56] add*(X, Y) >= X because [57], by (Select) 57] X >= X by (Meta) 58] filter#*(F, add(X, Y)) >= F because [50], by (Select) 59] filter#*(F, add(X, Y)) >= X because [60], by (Select) 60] add(X, Y) >= X because [56], by (Star) 61] filter#*(F, add(X, Y)) >= Y because [62], by (Select) 62] add(X, Y) >= Y because [52], by (Star) 63] filter2#(_|_, F, X, Y) > filter#(F, Y) because [64], by definition 64] filter2#*(_|_, F, X, Y) >= filter#(F, Y) because filter2# = filter#, [65], [66], [67] and [68], by (Stat) 65] F >= F by (Meta) 66] Y >= Y by (Meta) 67] filter2#*(_|_, F, X, Y) >= F because [65], by (Select) 68] filter2#*(_|_, F, X, Y) >= Y because [66], by (Select) 69] filter2#(_|_, F, X, Y) >= filter#(F, Y) because [70], by (Star) 70] filter2#*(_|_, F, X, Y) >= filter#(F, Y) because filter2# = filter#, [71], [72], [73] and [74], by (Stat) 71] F >= F by (Meta) 72] Y >= Y by (Meta) 73] filter2#*(_|_, F, X, Y) >= F because [71], by (Select) 74] filter2#*(_|_, F, X, Y) >= Y because [72], by (Select) 75] X >= X by (Meta) 76] s(X) >= X because [77], by (Star) 77] s*(X) >= X because [78], by (Select) 78] X >= X by (Meta) 79] _|_ >= _|_ by (Bot) 80] s(X) >= s(X) because s in Mul and [81], by (Fun) 81] X >= X by (Meta) 82] le(_|_, X) >= _|_ by (Bot) 83] le(s(X), _|_) >= _|_ by (Bot) 84] le(s(X), s(Y)) >= le(X, Y) because [85], by (Star) 85] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [86] and [89], by (Stat) 86] s(X) > X because [87], by definition 87] s*(X) >= X because [88], by (Select) 88] X >= X by (Meta) 89] s(Y) >= Y because [90], by (Star) 90] s*(Y) >= Y because [91], by (Select) 91] Y >= Y by (Meta) 92] app(_|_, X) >= X because [93], by (Star) 93] app*(_|_, X) >= X because [94], by (Select) 94] X >= X by (Meta) 95] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [96], by (Star) 96] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [97] and [101], by (Copy) 97] app*(add(X, Y), Z) >= X because [98], by (Select) 98] add(X, Y) >= X because [99], by (Star) 99] add*(X, Y) >= X because [100], by (Select) 100] X >= X by (Meta) 101] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [102] and [105], by (Stat) 102] add(X, Y) > Y because [103], by definition 103] add*(X, Y) >= Y because [104], by (Select) 104] Y >= Y by (Meta) 105] Z >= Z by (Meta) 106] _|_ >= _|_ by (Bot) 107] add(X, Y) >= add(X, Y) because add in Mul, [5] and [6], by (Fun) 108] add(X, Y) >= add(X, Y) because add in Mul, [109] and [110], by (Fun) 109] X >= X by (Meta) 110] Y >= Y by (Meta) 111] add(X, Y) >= Y because [15], by (Star) 112] _|_ >= _|_ by (Bot) 113] add(X, Y) >= add(X, Y) because add in Mul, [20] and [21], by (Fun) 114] add(X, Y) >= Y because [25], by (Star) 115] add(X, Y) >= add(X, Y) because add in Mul, [116] and [117], by (Fun) 116] X >= X by (Meta) 117] Y >= Y by (Meta) 118] quicksort(_|_) >= _|_ by (Bot) 119] quicksort(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(Y))) because [120], by (Star) 120] quicksort*(add(X, Y)) >= app(quicksort(Y), add(X, quicksort(Y))) because quicksort > app, [121] and [123], by (Copy) 121] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [122], by (Stat) 122] add(X, Y) > Y because [36], by definition 123] quicksort*(add(X, Y)) >= add(X, quicksort(Y)) because quicksort > add, [124] and [128], by (Copy) 124] quicksort*(add(X, Y)) >= X because [125], by (Select) 125] add(X, Y) >= X because [126], by (Star) 126] add*(X, Y) >= X because [127], by (Select) 127] X >= X by (Meta) 128] quicksort*(add(X, Y)) >= quicksort(Y) because quicksort in Mul and [129], by (Stat) 129] add(X, Y) > Y because [42], by definition 130] map(F, _|_) >= _|_ by (Bot) 131] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [132], by (Star) 132] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [133] and [139], by (Copy) 133] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [134] and [135], by (Copy) 134] map*(F, add(X, Y)) >= F because [44], by (Select) 135] map*(F, add(X, Y)) >= X because [136], by (Select) 136] add(X, Y) >= X because [137], by (Star) 137] add*(X, Y) >= X because [138], by (Select) 138] X >= X by (Meta) 139] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [44] and [140], by (Stat) 140] add(X, Y) > Y because [141], by definition 141] add*(X, Y) >= Y because [47], by (Select) 142] filter(F, _|_) >= _|_ by (Bot) 143] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [144], by (Star) 144] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [50], [51], [145], [146], [147] and [148], by (Stat) 145] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [146] and [147], by (Copy) 146] filter*(F, add(X, Y)) >= F because [50], by (Select) 147] filter*(F, add(X, Y)) >= X because [60], by (Select) 148] filter*(F, add(X, Y)) >= Y because [62], by (Select) 149] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [150], by (Star) 150] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [151] and [153], by (Copy) 151] filter2*(_|_, F, X, Y) >= X because [152], by (Select) 152] X >= X by (Meta) 153] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [65], [66], [154] and [155], by (Stat) 154] filter2*(_|_, F, X, Y) >= F because [65], by (Select) 155] filter2*(_|_, F, X, Y) >= Y because [66], by (Select) 156] filter2(_|_, F, X, Y) >= filter(F, Y) because [157], by (Star) 157] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [71], [72], [158] and [159], by (Stat) 158] filter2*(_|_, F, X, Y) >= F because [71], by (Select) 159] filter2*(_|_, F, X, Y) >= Y because [72], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_5, R_0, static, formative) by (P_6, R_0, static, formative), where P_6 consists of: app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) filter2#(false, F, X, Y) =#> filter#(F, Y) Thus, the original system is terminating if (P_6, R_0, static, formative) is finite. We consider the dependency pair problem (P_6, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) filter2#(false, F, X, Y) >? filter#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 app# = \y0y1.0 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 filter2# = \y0G1y2y3.3 filter# = \G0y1.0 high = \y0y1.0 high# = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.0 le = \y0y1.0 low = \y0y1.0 low# = \y0y1.0 map = \G0y1.0 map# = \G0y1.0 minus = \y0y1.y0 nil = 0 quicksort = \y0.2 quicksort# = \y0.0 quot = \y0y1.0 s = \y0.2y0 true = 0 Using this interpretation, the requirements translate to: [[app#(add(_x0, _x1), _x2)]] = 0 >= 0 = [[app#(_x1, _x2)]] [[low#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[if!fac6220low#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low#(_x0, _x2)]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high#(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[quicksort#(add(_x0, _x1))]] = 0 >= 0 = [[quicksort#(low(_x0, _x1))]] [[map#(_F0, add(_x1, _x2))]] = 0 >= 0 = [[map#(_F0, _x2)]] [[filter2#(false, _F0, _x1, _x2)]] = 3 > 0 = [[filter#(_F0, _x2)]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 2x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 0 >= 0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 2 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 2 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_6, R_0, static, formative) by (P_7, R_0, static, formative), where P_7 consists of: app#(add(X, Y), Z) =#> app#(Y, Z) low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) Thus, the original system is terminating if (P_7, R_0, static, formative) is finite. We consider the dependency pair problem (P_7, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: app#(add(X, Y), Z) >? app#(Y, Z) low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[add(x_1, x_2)]] = add(x_2) [[false]] = _|_ [[filter(x_1, x_2)]] = x_2 [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_4) [[high(x_1, x_2)]] = x_2 [[high#(x_1, x_2)]] = _|_ [[if!fac6220high(x_1, x_2, x_3)]] = x_3 [[if!fac6220high#(x_1, x_2, x_3)]] = _|_ [[if!fac6220low(x_1, x_2, x_3)]] = x_3 [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2) [[low(x_1, x_2)]] = x_2 [[low#(x_1, x_2)]] = low#(x_1) [[map(x_1, x_2)]] = map(x_2) [[map#(x_1, x_2)]] = _|_ [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, app#, filter2, if!fac6220low#, le, low#, map, quicksort, quicksort#, quot, s}, and the following precedence: app# > if!fac6220low# = low# > @_{o -> o} > quicksort > app > quicksort# > le > add = filter2 = map > quot = s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: app#(add(X), Y) > app#(X, Y) low#(X) >= if!fac6220low#(X) if!fac6220low#(X) >= low#(X) if!fac6220low#(X) >= low#(X) _|_ >= _|_ _|_ >= _|_ _|_ >= _|_ quicksort#(add(X)) >= quicksort#(X) _|_ >= _|_ X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X), Y) >= add(app(X, Y)) _|_ >= _|_ add(X) >= add(X) add(X) >= add(X) add(X) >= X _|_ >= _|_ add(X) >= add(X) add(X) >= X add(X) >= add(X) quicksort(_|_) >= _|_ quicksort(add(X)) >= app(quicksort(X), add(quicksort(X))) map(_|_) >= _|_ map(add(X)) >= add(map(X)) _|_ >= _|_ add(X) >= filter2(X) filter2(X) >= add(X) filter2(X) >= X With these choices, we have: 1] app#(add(X), Y) > app#(X, Y) because [2], by definition 2] app#*(add(X), Y) >= app#(X, Y) because app# in Mul, [3] and [6], by (Stat) 3] add(X) > X because [4], by definition 4] add*(X) >= X because [5], by (Select) 5] X >= X by (Meta) 6] Y >= Y by (Meta) 7] low#(X) >= if!fac6220low#(X) because low# = if!fac6220low#, low# in Mul and [8], by (Fun) 8] X >= X by (Meta) 9] if!fac6220low#(X) >= low#(X) because if!fac6220low# = low#, if!fac6220low# in Mul and [10], by (Fun) 10] X >= X by (Meta) 11] if!fac6220low#(X) >= low#(X) because if!fac6220low# = low#, if!fac6220low# in Mul and [12], by (Fun) 12] X >= X by (Meta) 13] _|_ >= _|_ by (Bot) 14] _|_ >= _|_ by (Bot) 15] _|_ >= _|_ by (Bot) 16] quicksort#(add(X)) >= quicksort#(X) because quicksort# in Mul and [17], by (Fun) 17] add(X) >= X because [18], by (Star) 18] add*(X) >= X because [19], by (Select) 19] X >= X by (Meta) 20] _|_ >= _|_ by (Bot) 21] X >= X by (Meta) 22] s(X) >= X because [23], by (Star) 23] s*(X) >= X because [24], by (Select) 24] X >= X by (Meta) 25] quot(_|_) >= _|_ by (Bot) 26] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [27], by (Fun) 27] s(X) >= quot(X) because s = quot, s in Mul and [28], by (Fun) 28] X >= X by (Meta) 29] le(_|_, X) >= _|_ by (Bot) 30] le(s(X), _|_) >= _|_ by (Bot) 31] le(s(X), s(Y)) >= le(X, Y) because [32], by (Star) 32] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [33] and [36], by (Stat) 33] s(X) > X because [34], by definition 34] s*(X) >= X because [35], by (Select) 35] X >= X by (Meta) 36] s(Y) >= Y because [37], by (Star) 37] s*(Y) >= Y because [38], by (Select) 38] Y >= Y by (Meta) 39] app(_|_, X) >= X because [40], by (Star) 40] app*(_|_, X) >= X because [41], by (Select) 41] X >= X by (Meta) 42] app(add(X), Y) >= add(app(X, Y)) because [43], by (Star) 43] app*(add(X), Y) >= add(app(X, Y)) because app > add and [44], by (Copy) 44] app*(add(X), Y) >= app(X, Y) because app in Mul, [3] and [6], by (Stat) 45] _|_ >= _|_ by (Bot) 46] add(X) >= add(X) because add in Mul and [47], by (Fun) 47] X >= X by (Meta) 48] add(X) >= add(X) because add in Mul and [49], by (Fun) 49] X >= X by (Meta) 50] add(X) >= X because [51], by (Star) 51] add*(X) >= X because [52], by (Select) 52] X >= X by (Meta) 53] _|_ >= _|_ by (Bot) 54] add(X) >= add(X) because add in Mul and [55], by (Fun) 55] X >= X by (Meta) 56] add(X) >= X because [57], by (Star) 57] add*(X) >= X because [58], by (Select) 58] X >= X by (Meta) 59] add(X) >= add(X) because add in Mul and [60], by (Fun) 60] X >= X by (Meta) 61] quicksort(_|_) >= _|_ by (Bot) 62] quicksort(add(X)) >= app(quicksort(X), add(quicksort(X))) because [63], by (Star) 63] quicksort*(add(X)) >= app(quicksort(X), add(quicksort(X))) because quicksort > app, [64] and [67], by (Copy) 64] quicksort*(add(X)) >= quicksort(X) because quicksort in Mul and [65], by (Stat) 65] add(X) > X because [66], by definition 66] add*(X) >= X because [19], by (Select) 67] quicksort*(add(X)) >= add(quicksort(X)) because quicksort > add and [68], by (Copy) 68] quicksort*(add(X)) >= quicksort(X) because quicksort in Mul and [69], by (Stat) 69] add(X) > X because [70], by definition 70] add*(X) >= X because [19], by (Select) 71] map(_|_) >= _|_ by (Bot) 72] map(add(X)) >= add(map(X)) because map = add, map in Mul and [73], by (Fun) 73] add(X) >= map(X) because add = map, add in Mul and [74], by (Fun) 74] X >= X by (Meta) 75] _|_ >= _|_ by (Bot) 76] add(X) >= filter2(X) because add = filter2, add in Mul and [77], by (Fun) 77] X >= X by (Meta) 78] filter2(X) >= add(X) because filter2 = add, filter2 in Mul and [79], by (Fun) 79] X >= X by (Meta) 80] filter2(X) >= X because [81], by (Star) 81] filter2*(X) >= X because [82], by (Select) 82] X >= X by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_7, R_0, static, formative) by (P_8, R_0, static, formative), where P_8 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) map#(F, add(X, Y)) =#> map#(F, Y) Thus, the original system is terminating if (P_8, R_0, static, formative) is finite. We consider the dependency pair problem (P_8, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) map#(F, add(X, Y)) >? map#(F, Y) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_4, x_1, x_3) [[high(x_1, x_2)]] = high(x_2) [[high#(x_1, x_2)]] = _|_ [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = _|_ [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quicksort#(x_1)]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {@_{o -> o}, filter, filter2} and Mul = {add, app, high, if!fac6220high, if!fac6220low, if!fac6220low#, le, low, low#, map, map#, quicksort, quot, s}, and the following precedence: le > if!fac6220low# = low# > map > @_{o -> o} = filter = filter2 > map# > quicksort > app > quot = s > add = high = if!fac6220high = if!fac6220low = low Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) _|_ >= _|_ _|_ >= _|_ _|_ >= _|_ _|_ >= _|_ map#(F, add(X, Y)) > map#(F, Y) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(_|_) >= _|_ low(add(X, Y)) >= if!fac6220low(add(X, Y)) if!fac6220low(add(X, Y)) >= add(X, low(Y)) if!fac6220low(add(X, Y)) >= low(Y) high(_|_) >= _|_ high(add(X, Y)) >= if!fac6220high(add(X, Y)) if!fac6220high(add(X, Y)) >= high(Y) if!fac6220high(add(X, Y)) >= add(X, high(Y)) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) filter2(_|_, F, X, Y) >= filter(F, Y) With these choices, we have: 1] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [7] and [8], by (Fun) 7] X >= X by (Meta) 8] add(Y, Z) >= Z because [9], by (Star) 9] add*(Y, Z) >= Z because [10], by (Select) 10] Z >= Z by (Meta) 11] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [12] and [13], by (Fun) 12] X >= X by (Meta) 13] add(Y, Z) >= Z because [14], by (Star) 14] add*(Y, Z) >= Z because [15], by (Select) 15] Z >= Z by (Meta) 16] _|_ >= _|_ by (Bot) 17] _|_ >= _|_ by (Bot) 18] _|_ >= _|_ by (Bot) 19] _|_ >= _|_ by (Bot) 20] map#(F, add(X, Y)) > map#(F, Y) because [21], by definition 21] map#*(F, add(X, Y)) >= map#(F, Y) because map# in Mul, [22] and [23], by (Stat) 22] F >= F by (Meta) 23] add(X, Y) > Y because [24], by definition 24] add*(X, Y) >= Y because [25], by (Select) 25] Y >= Y by (Meta) 26] X >= X by (Meta) 27] s(X) >= X because [28], by (Star) 28] s*(X) >= X because [29], by (Select) 29] X >= X by (Meta) 30] quot(_|_) >= _|_ by (Bot) 31] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [32], by (Fun) 32] s(X) >= quot(X) because s = quot, s in Mul and [33], by (Fun) 33] X >= X by (Meta) 34] le(_|_, X) >= _|_ by (Bot) 35] le(s(X), _|_) >= _|_ by (Bot) 36] le(s(X), s(Y)) >= le(X, Y) because le in Mul, [37] and [40], by (Fun) 37] s(X) >= X because [38], by (Star) 38] s*(X) >= X because [39], by (Select) 39] X >= X by (Meta) 40] s(Y) >= Y because [41], by (Star) 41] s*(Y) >= Y because [42], by (Select) 42] Y >= Y by (Meta) 43] app(_|_, X) >= X because [44], by (Star) 44] app*(_|_, X) >= X because [45], by (Select) 45] X >= X by (Meta) 46] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [47], by (Star) 47] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [48] and [52], by (Copy) 48] app*(add(X, Y), Z) >= X because [49], by (Select) 49] add(X, Y) >= X because [50], by (Star) 50] add*(X, Y) >= X because [51], by (Select) 51] X >= X by (Meta) 52] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [53] and [56], by (Stat) 53] add(X, Y) > Y because [54], by definition 54] add*(X, Y) >= Y because [55], by (Select) 55] Y >= Y by (Meta) 56] Z >= Z by (Meta) 57] low(_|_) >= _|_ by (Bot) 58] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [3], by (Fun) 59] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [60], by (Star) 60] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [61] and [64], by (Stat) 61] add(X, Y) > X because [62], by definition 62] add*(X, Y) >= X because [63], by (Select) 63] X >= X by (Meta) 64] add(X, Y) > low(Y) because [65], by definition 65] add*(X, Y) >= low(Y) because add = low, add in Mul and [66], by (Stat) 66] Y >= Y by (Meta) 67] if!fac6220low(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [13], by (Fun) 68] high(_|_) >= _|_ by (Bot) 69] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [70], by (Fun) 70] add(X, Y) >= add(X, Y) because add in Mul, [71] and [72], by (Fun) 71] X >= X by (Meta) 72] Y >= Y by (Meta) 73] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [74], by (Fun) 74] add(X, Y) >= Y because [75], by (Star) 75] add*(X, Y) >= Y because [76], by (Select) 76] Y >= Y by (Meta) 77] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [78], by (Star) 78] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [79] and [82], by (Stat) 79] add(X, Y) > X because [80], by definition 80] add*(X, Y) >= X because [81], by (Select) 81] X >= X by (Meta) 82] add(X, Y) > high(Y) because [83], by definition 83] add*(X, Y) >= high(Y) because add = high, add in Mul and [84], by (Stat) 84] Y >= Y by (Meta) 85] quicksort(_|_) >= _|_ by (Bot) 86] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [87], by (Star) 87] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [88] and [92], by (Copy) 88] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [89], by (Stat) 89] add(X, Y) > low(Y) because [90], by definition 90] add*(X, Y) >= low(Y) because add = low, add in Mul and [91], by (Stat) 91] Y >= Y by (Meta) 92] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [93] and [97], by (Copy) 93] quicksort*(add(X, Y)) >= X because [94], by (Select) 94] add(X, Y) >= X because [95], by (Star) 95] add*(X, Y) >= X because [96], by (Select) 96] X >= X by (Meta) 97] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [98], by (Stat) 98] add(X, Y) > high(Y) because [99], by definition 99] add*(X, Y) >= high(Y) because add = high, add in Mul and [91], by (Stat) 100] map(F, _|_) >= _|_ by (Bot) 101] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [102], by (Star) 102] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [103] and [109], by (Copy) 103] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [104] and [105], by (Copy) 104] map*(F, add(X, Y)) >= F because [22], by (Select) 105] map*(F, add(X, Y)) >= X because [106], by (Select) 106] add(X, Y) >= X because [107], by (Star) 107] add*(X, Y) >= X because [108], by (Select) 108] X >= X by (Meta) 109] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [22] and [23], by (Stat) 110] filter(F, _|_) >= _|_ by (Bot) 111] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [112], by (Star) 112] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [113], [114], [117], [121], [122] and [124], by (Stat) 113] F >= F by (Meta) 114] add(X, Y) > Y because [115], by definition 115] add*(X, Y) >= Y because [116], by (Select) 116] Y >= Y by (Meta) 117] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter = @_{o -> o}, [113], [118], [121] and [122], by (Stat) 118] add(X, Y) > X because [119], by definition 119] add*(X, Y) >= X because [120], by (Select) 120] X >= X by (Meta) 121] filter*(F, add(X, Y)) >= F because [113], by (Select) 122] filter*(F, add(X, Y)) >= X because [123], by (Select) 123] add(X, Y) >= X because [119], by (Star) 124] filter*(F, add(X, Y)) >= Y because [125], by (Select) 125] add(X, Y) >= Y because [115], by (Star) 126] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [127], by (Star) 127] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [128] and [130], by (Copy) 128] filter2*(_|_, F, X, Y) >= X because [129], by (Select) 129] X >= X by (Meta) 130] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [131], [132], [133] and [134], by (Stat) 131] F >= F by (Meta) 132] Y >= Y by (Meta) 133] filter2*(_|_, F, X, Y) >= F because [131], by (Select) 134] filter2*(_|_, F, X, Y) >= Y because [132], by (Select) 135] filter2(_|_, F, X, Y) >= filter(F, Y) because [136], by (Star) 136] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [137], [138], [139] and [140], by (Stat) 137] F >= F by (Meta) 138] Y >= Y by (Meta) 139] filter2*(_|_, F, X, Y) >= F because [137], by (Select) 140] filter2*(_|_, F, X, Y) >= Y because [138], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_8, R_0, static, formative) by (P_9, R_0, static, formative), where P_9 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) quicksort#(add(X, Y)) =#> quicksort#(low(X, Y)) Thus, the original system is terminating if (P_9, R_0, static, formative) is finite. We consider the dependency pair problem (P_9, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) quicksort#(add(X, Y)) >? quicksort#(low(X, Y)) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_3, x_4) [[high(x_1, x_2)]] = high(x_2) [[high#(x_1, x_2)]] = _|_ [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = _|_ [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[le(x_1, x_2)]] = le(x_1) [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quicksort#(x_1)]] = x_1 [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter, filter2, high, if!fac6220high, if!fac6220low, if!fac6220low#, le, low, low#, map, quicksort, quot, s}, and the following precedence: filter = filter2 > map > @_{o -> o} > quicksort > app > le > if!fac6220low# = low# > add = high = if!fac6220high = if!fac6220low = low > quot = s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) _|_ >= _|_ _|_ >= _|_ _|_ >= _|_ add(X, Y) > low(Y) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_) >= _|_ le(s(X)) >= _|_ le(s(X)) >= le(X) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(_|_) >= _|_ low(add(X, Y)) >= if!fac6220low(add(X, Y)) if!fac6220low(add(X, Y)) >= add(X, low(Y)) if!fac6220low(add(X, Y)) >= low(Y) high(_|_) >= _|_ high(add(X, Y)) >= if!fac6220high(add(X, Y)) if!fac6220high(add(X, Y)) >= high(Y) if!fac6220high(add(X, Y)) >= add(X, high(Y)) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(F, X, Y) filter2(F, X, Y) >= add(X, filter(F, Y)) filter2(F, X, Y) >= filter(F, Y) With these choices, we have: 1] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [7] and [8], by (Fun) 7] X >= X by (Meta) 8] add(Y, Z) >= Z because [9], by (Star) 9] add*(Y, Z) >= Z because [10], by (Select) 10] Z >= Z by (Meta) 11] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [12] and [13], by (Fun) 12] X >= X by (Meta) 13] add(Y, Z) >= Z because [14], by (Star) 14] add*(Y, Z) >= Z because [15], by (Select) 15] Z >= Z by (Meta) 16] _|_ >= _|_ by (Bot) 17] _|_ >= _|_ by (Bot) 18] _|_ >= _|_ by (Bot) 19] add(X, Y) > low(Y) because [20], by definition 20] add*(X, Y) >= low(Y) because add = low, add in Mul and [21], by (Stat) 21] Y >= Y by (Meta) 22] X >= X by (Meta) 23] s(X) >= X because [24], by (Star) 24] s*(X) >= X because [25], by (Select) 25] X >= X by (Meta) 26] quot(_|_) >= _|_ by (Bot) 27] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [28], by (Fun) 28] s(X) >= quot(X) because s = quot, s in Mul and [29], by (Fun) 29] X >= X by (Meta) 30] le(_|_) >= _|_ by (Bot) 31] le(s(X)) >= _|_ by (Bot) 32] le(s(X)) >= le(X) because le in Mul and [33], by (Fun) 33] s(X) >= X because [34], by (Star) 34] s*(X) >= X because [35], by (Select) 35] X >= X by (Meta) 36] app(_|_, X) >= X because [37], by (Star) 37] app*(_|_, X) >= X because [38], by (Select) 38] X >= X by (Meta) 39] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [40], by (Star) 40] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [41] and [45], by (Copy) 41] app*(add(X, Y), Z) >= X because [42], by (Select) 42] add(X, Y) >= X because [43], by (Star) 43] add*(X, Y) >= X because [44], by (Select) 44] X >= X by (Meta) 45] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [46] and [49], by (Stat) 46] add(X, Y) > Y because [47], by definition 47] add*(X, Y) >= Y because [48], by (Select) 48] Y >= Y by (Meta) 49] Z >= Z by (Meta) 50] low(_|_) >= _|_ by (Bot) 51] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [3], by (Fun) 52] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [53], by (Star) 53] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [54] and [57], by (Stat) 54] add(X, Y) > X because [55], by definition 55] add*(X, Y) >= X because [56], by (Select) 56] X >= X by (Meta) 57] add(X, Y) > low(Y) because [58], by definition 58] add*(X, Y) >= low(Y) because add = low, add in Mul and [59], by (Stat) 59] Y >= Y by (Meta) 60] if!fac6220low(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [13], by (Fun) 61] high(_|_) >= _|_ by (Bot) 62] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [63], by (Fun) 63] add(X, Y) >= add(X, Y) because add in Mul, [64] and [65], by (Fun) 64] X >= X by (Meta) 65] Y >= Y by (Meta) 66] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [67], by (Fun) 67] add(X, Y) >= Y because [68], by (Star) 68] add*(X, Y) >= Y because [69], by (Select) 69] Y >= Y by (Meta) 70] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [71], by (Star) 71] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [72] and [75], by (Stat) 72] add(X, Y) > X because [73], by definition 73] add*(X, Y) >= X because [74], by (Select) 74] X >= X by (Meta) 75] add(X, Y) > high(Y) because [76], by definition 76] add*(X, Y) >= high(Y) because add = high, add in Mul and [77], by (Stat) 77] Y >= Y by (Meta) 78] quicksort(_|_) >= _|_ by (Bot) 79] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [80], by (Star) 80] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [81] and [83], by (Copy) 81] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [82], by (Stat) 82] add(X, Y) > low(Y) because [20], by definition 83] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [84] and [88], by (Copy) 84] quicksort*(add(X, Y)) >= X because [85], by (Select) 85] add(X, Y) >= X because [86], by (Star) 86] add*(X, Y) >= X because [87], by (Select) 87] X >= X by (Meta) 88] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [89], by (Stat) 89] add(X, Y) > high(Y) because [90], by definition 90] add*(X, Y) >= high(Y) because add = high, add in Mul and [21], by (Stat) 91] map(F, _|_) >= _|_ by (Bot) 92] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [93], by (Star) 93] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [94] and [101], by (Copy) 94] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [95] and [97], by (Copy) 95] map*(F, add(X, Y)) >= F because [96], by (Select) 96] F >= F by (Meta) 97] map*(F, add(X, Y)) >= X because [98], by (Select) 98] add(X, Y) >= X because [99], by (Star) 99] add*(X, Y) >= X because [100], by (Select) 100] X >= X by (Meta) 101] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [102] and [103], by (Stat) 102] F >= F by (Meta) 103] add(X, Y) > Y because [104], by definition 104] add*(X, Y) >= Y because [105], by (Select) 105] Y >= Y by (Meta) 106] filter(F, _|_) >= _|_ by (Bot) 107] filter(F, add(X, Y)) >= filter2(F, X, Y) because [108], by (Star) 108] filter*(F, add(X, Y)) >= filter2(F, X, Y) because filter = filter2, filter in Mul, [109], [110] and [113], by (Stat) 109] F >= F by (Meta) 110] add(X, Y) > X because [111], by definition 111] add*(X, Y) >= X because [112], by (Select) 112] X >= X by (Meta) 113] add(X, Y) > Y because [114], by definition 114] add*(X, Y) >= Y because [115], by (Select) 115] Y >= Y by (Meta) 116] filter2(F, X, Y) >= add(X, filter(F, Y)) because [117], by (Star) 117] filter2*(F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [118] and [120], by (Copy) 118] filter2*(F, X, Y) >= X because [119], by (Select) 119] X >= X by (Meta) 120] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [121] and [122], by (Stat) 121] F >= F by (Meta) 122] Y >= Y by (Meta) 123] filter2(F, X, Y) >= filter(F, Y) because [124], by (Star) 124] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [125] and [126], by (Stat) 125] F >= F by (Meta) 126] Y >= Y by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_9, R_0, static, formative) by (P_10, R_0, static, formative), where P_10 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) =#> high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) Thus, the original system is terminating if (P_10, R_0, static, formative) is finite. We consider the dependency pair problem (P_10, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(true, X, add(Y, Z)) >? high#(X, Z) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[filter(x_1, x_2)]] = x_2 [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_3, x_4) [[high(x_1, x_2)]] = high(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_2, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter2, high, high#, if!fac6220high, if!fac6220high#, if!fac6220low, if!fac6220low#, le, low, low#, map, quicksort, s}, and the following precedence: quicksort > app > s > le > if!fac6220low# = low# > high# = if!fac6220high# > map > @_{o -> o} > add = filter2 = high = if!fac6220high = if!fac6220low = low Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) if!fac6220high#(X, add(Y, Z)) > high#(X, Z) if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) X >= X s(X) >= X _|_ >= _|_ s(X) >= s(X) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(_|_) >= _|_ low(add(X, Y)) >= if!fac6220low(add(X, Y)) if!fac6220low(add(X, Y)) >= add(X, low(Y)) if!fac6220low(add(X, Y)) >= low(Y) high(_|_) >= _|_ high(add(X, Y)) >= if!fac6220high(add(X, Y)) if!fac6220high(add(X, Y)) >= high(Y) if!fac6220high(add(X, Y)) >= add(X, high(Y)) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) _|_ >= _|_ add(X, Y) >= filter2(X, Y) filter2(X, Y) >= add(X, Y) filter2(X, Y) >= Y With these choices, we have: 1] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because [7], by (Star) 7] if!fac6220low#*(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [8] and [9], by (Stat) 8] X >= X by (Meta) 9] add(Y, Z) > Z because [10], by definition 10] add*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [13] and [14], by (Fun) 13] X >= X by (Meta) 14] add(Y, Z) >= Z because [15], by (Star) 15] add*(Y, Z) >= Z because [16], by (Select) 16] Z >= Z by (Meta) 17] high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) because high# = if!fac6220high#, high# in Mul, [18] and [19], by (Fun) 18] X >= X by (Meta) 19] add(Y, Z) >= add(Y, Z) because add in Mul, [20] and [21], by (Fun) 20] Y >= Y by (Meta) 21] Z >= Z by (Meta) 22] if!fac6220high#(X, add(Y, Z)) > high#(X, Z) because [23], by definition 23] if!fac6220high#*(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [24] and [25], by (Stat) 24] X >= X by (Meta) 25] add(Y, Z) > Z because [26], by definition 26] add*(Y, Z) >= Z because [27], by (Select) 27] Z >= Z by (Meta) 28] if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [29] and [30], by (Fun) 29] X >= X by (Meta) 30] add(Y, Z) >= Z because [31], by (Star) 31] add*(Y, Z) >= Z because [32], by (Select) 32] Z >= Z by (Meta) 33] X >= X by (Meta) 34] s(X) >= X because [35], by (Star) 35] s*(X) >= X because [36], by (Select) 36] X >= X by (Meta) 37] _|_ >= _|_ by (Bot) 38] s(X) >= s(X) because s in Mul and [39], by (Fun) 39] X >= X by (Meta) 40] le(_|_, X) >= _|_ by (Bot) 41] le(s(X), _|_) >= _|_ by (Bot) 42] le(s(X), s(Y)) >= le(X, Y) because le in Mul, [43] and [46], by (Fun) 43] s(X) >= X because [44], by (Star) 44] s*(X) >= X because [45], by (Select) 45] X >= X by (Meta) 46] s(Y) >= Y because [47], by (Star) 47] s*(Y) >= Y because [48], by (Select) 48] Y >= Y by (Meta) 49] app(_|_, X) >= X because [50], by (Star) 50] app*(_|_, X) >= X because [51], by (Select) 51] X >= X by (Meta) 52] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [53], by (Star) 53] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [54] and [58], by (Copy) 54] app*(add(X, Y), Z) >= X because [55], by (Select) 55] add(X, Y) >= X because [56], by (Star) 56] add*(X, Y) >= X because [57], by (Select) 57] X >= X by (Meta) 58] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [59] and [62], by (Stat) 59] add(X, Y) > Y because [60], by definition 60] add*(X, Y) >= Y because [61], by (Select) 61] Y >= Y by (Meta) 62] Z >= Z by (Meta) 63] low(_|_) >= _|_ by (Bot) 64] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [3], by (Fun) 65] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [66], by (Star) 66] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [67] and [70], by (Stat) 67] add(X, Y) > X because [68], by definition 68] add*(X, Y) >= X because [69], by (Select) 69] X >= X by (Meta) 70] add(X, Y) > low(Y) because [71], by definition 71] add*(X, Y) >= low(Y) because add = low, add in Mul and [72], by (Stat) 72] Y >= Y by (Meta) 73] if!fac6220low(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [14], by (Fun) 74] high(_|_) >= _|_ by (Bot) 75] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [19], by (Fun) 76] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [77], by (Fun) 77] add(X, Y) >= Y because [26], by (Star) 78] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [79], by (Star) 79] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [80] and [83], by (Stat) 80] add(X, Y) > X because [81], by definition 81] add*(X, Y) >= X because [82], by (Select) 82] X >= X by (Meta) 83] add(X, Y) > high(Y) because [84], by definition 84] add*(X, Y) >= high(Y) because add = high, add in Mul and [85], by (Stat) 85] Y >= Y by (Meta) 86] quicksort(_|_) >= _|_ by (Bot) 87] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [88], by (Star) 88] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [89] and [93], by (Copy) 89] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [90], by (Stat) 90] add(X, Y) > low(Y) because [91], by definition 91] add*(X, Y) >= low(Y) because add = low, add in Mul and [92], by (Stat) 92] Y >= Y by (Meta) 93] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [94] and [98], by (Copy) 94] quicksort*(add(X, Y)) >= X because [95], by (Select) 95] add(X, Y) >= X because [96], by (Star) 96] add*(X, Y) >= X because [97], by (Select) 97] X >= X by (Meta) 98] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [99], by (Stat) 99] add(X, Y) > high(Y) because [100], by definition 100] add*(X, Y) >= high(Y) because add = high, add in Mul and [92], by (Stat) 101] map(F, _|_) >= _|_ by (Bot) 102] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [103], by (Star) 103] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [104] and [111], by (Copy) 104] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [105] and [107], by (Copy) 105] map*(F, add(X, Y)) >= F because [106], by (Select) 106] F >= F by (Meta) 107] map*(F, add(X, Y)) >= X because [108], by (Select) 108] add(X, Y) >= X because [109], by (Star) 109] add*(X, Y) >= X because [110], by (Select) 110] X >= X by (Meta) 111] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [112] and [113], by (Stat) 112] F >= F by (Meta) 113] add(X, Y) > Y because [114], by definition 114] add*(X, Y) >= Y because [115], by (Select) 115] Y >= Y by (Meta) 116] _|_ >= _|_ by (Bot) 117] add(X, Y) >= filter2(X, Y) because add = filter2, add in Mul, [118] and [119], by (Fun) 118] X >= X by (Meta) 119] Y >= Y by (Meta) 120] filter2(X, Y) >= add(X, Y) because filter2 = add, filter2 in Mul, [121] and [122], by (Fun) 121] X >= X by (Meta) 122] Y >= Y by (Meta) 123] filter2(X, Y) >= Y because [124], by (Star) 124] filter2*(X, Y) >= Y because [125], by (Select) 125] Y >= Y by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_10, R_0, static, formative) by (P_11, R_0, static, formative), where P_11 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) =#> low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) Thus, the original system is terminating if (P_11, R_0, static, formative) is finite. We consider the dependency pair problem (P_11, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(true, X, add(Y, Z)) >? low#(X, Z) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_3, x_4) [[high(x_1, x_2)]] = high(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_2, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[quot(x_1, x_2)]] = quot(x_1) [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter, filter2, high, high#, if!fac6220high, if!fac6220high#, if!fac6220low, if!fac6220low#, le, low, low#, map, quicksort, quot, s}, and the following precedence: le > high# = if!fac6220high# > @_{o -> o} = map > filter = filter2 > if!fac6220low# = low# > quicksort > app > add = high = if!fac6220high = if!fac6220low = low > quot = s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) > low#(X, Z) if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) X >= X s(X) >= X quot(_|_) >= _|_ quot(s(X)) >= s(quot(X)) le(_|_, X) >= _|_ le(s(X), _|_) >= _|_ le(s(X), s(Y)) >= le(X, Y) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(_|_) >= _|_ low(add(X, Y)) >= if!fac6220low(add(X, Y)) if!fac6220low(add(X, Y)) >= add(X, low(Y)) if!fac6220low(add(X, Y)) >= low(Y) high(_|_) >= _|_ high(add(X, Y)) >= if!fac6220high(add(X, Y)) if!fac6220high(add(X, Y)) >= high(Y) if!fac6220high(add(X, Y)) >= add(X, high(Y)) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(F, X, Y) filter2(F, X, Y) >= add(X, filter(F, Y)) filter2(F, X, Y) >= filter(F, Y) With these choices, we have: 1] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) > low#(X, Z) because [7], by definition 7] if!fac6220low#*(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [8] and [9], by (Stat) 8] X >= X by (Meta) 9] add(Y, Z) > Z because [10], by definition 10] add*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] if!fac6220low#(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [13] and [14], by (Fun) 13] X >= X by (Meta) 14] add(Y, Z) >= Z because [15], by (Star) 15] add*(Y, Z) >= Z because [16], by (Select) 16] Z >= Z by (Meta) 17] high#(X, add(Y, Z)) >= if!fac6220high#(X, add(Y, Z)) because high# = if!fac6220high#, high# in Mul, [18] and [19], by (Fun) 18] X >= X by (Meta) 19] add(Y, Z) >= add(Y, Z) because add in Mul, [20] and [21], by (Fun) 20] Y >= Y by (Meta) 21] Z >= Z by (Meta) 22] if!fac6220high#(X, add(Y, Z)) >= high#(X, Z) because if!fac6220high# = high#, if!fac6220high# in Mul, [23] and [24], by (Fun) 23] X >= X by (Meta) 24] add(Y, Z) >= Z because [25], by (Star) 25] add*(Y, Z) >= Z because [26], by (Select) 26] Z >= Z by (Meta) 27] X >= X by (Meta) 28] s(X) >= X because [29], by (Star) 29] s*(X) >= X because [30], by (Select) 30] X >= X by (Meta) 31] quot(_|_) >= _|_ by (Bot) 32] quot(s(X)) >= s(quot(X)) because quot = s, quot in Mul and [33], by (Fun) 33] s(X) >= quot(X) because s = quot, s in Mul and [34], by (Fun) 34] X >= X by (Meta) 35] le(_|_, X) >= _|_ by (Bot) 36] le(s(X), _|_) >= _|_ by (Bot) 37] le(s(X), s(Y)) >= le(X, Y) because [38], by (Star) 38] le*(s(X), s(Y)) >= le(X, Y) because le in Mul, [39] and [42], by (Stat) 39] s(X) > X because [40], by definition 40] s*(X) >= X because [41], by (Select) 41] X >= X by (Meta) 42] s(Y) >= Y because [43], by (Star) 43] s*(Y) >= Y because [44], by (Select) 44] Y >= Y by (Meta) 45] app(_|_, X) >= X because [46], by (Star) 46] app*(_|_, X) >= X because [47], by (Select) 47] X >= X by (Meta) 48] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [49], by (Star) 49] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [50] and [54], by (Copy) 50] app*(add(X, Y), Z) >= X because [51], by (Select) 51] add(X, Y) >= X because [52], by (Star) 52] add*(X, Y) >= X because [53], by (Select) 53] X >= X by (Meta) 54] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [55] and [58], by (Stat) 55] add(X, Y) > Y because [56], by definition 56] add*(X, Y) >= Y because [57], by (Select) 57] Y >= Y by (Meta) 58] Z >= Z by (Meta) 59] low(_|_) >= _|_ by (Bot) 60] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [3], by (Fun) 61] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [62], by (Star) 62] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [63] and [66], by (Stat) 63] add(X, Y) > X because [64], by definition 64] add*(X, Y) >= X because [65], by (Select) 65] X >= X by (Meta) 66] add(X, Y) > low(Y) because [67], by definition 67] add*(X, Y) >= low(Y) because add = low, add in Mul and [68], by (Stat) 68] Y >= Y by (Meta) 69] if!fac6220low(add(X, Y)) >= low(Y) because [70], by (Star) 70] if!fac6220low*(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [71], by (Stat) 71] add(X, Y) > Y because [72], by definition 72] add*(X, Y) >= Y because [16], by (Select) 73] high(_|_) >= _|_ by (Bot) 74] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [19], by (Fun) 75] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [76], by (Fun) 76] add(X, Y) >= Y because [77], by (Star) 77] add*(X, Y) >= Y because [78], by (Select) 78] Y >= Y by (Meta) 79] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [80], by (Star) 80] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [81] and [84], by (Stat) 81] add(X, Y) > X because [82], by definition 82] add*(X, Y) >= X because [83], by (Select) 83] X >= X by (Meta) 84] add(X, Y) > high(Y) because [85], by definition 85] add*(X, Y) >= high(Y) because add = high, add in Mul and [86], by (Stat) 86] Y >= Y by (Meta) 87] quicksort(_|_) >= _|_ by (Bot) 88] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [89], by (Star) 89] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [90] and [94], by (Copy) 90] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [91], by (Stat) 91] add(X, Y) > low(Y) because [92], by definition 92] add*(X, Y) >= low(Y) because add = low, add in Mul and [93], by (Stat) 93] Y >= Y by (Meta) 94] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [95] and [99], by (Copy) 95] quicksort*(add(X, Y)) >= X because [96], by (Select) 96] add(X, Y) >= X because [97], by (Star) 97] add*(X, Y) >= X because [98], by (Select) 98] X >= X by (Meta) 99] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [100], by (Stat) 100] add(X, Y) > high(Y) because [101], by definition 101] add*(X, Y) >= high(Y) because add = high, add in Mul and [93], by (Stat) 102] map(F, _|_) >= _|_ by (Bot) 103] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [104], by (Star) 104] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [105] and [110], by (Copy) 105] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map = @_{o -> o}, map in Mul, [106] and [107], by (Stat) 106] F >= F by (Meta) 107] add(X, Y) > X because [108], by definition 108] add*(X, Y) >= X because [109], by (Select) 109] X >= X by (Meta) 110] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [106] and [111], by (Stat) 111] add(X, Y) > Y because [112], by definition 112] add*(X, Y) >= Y because [113], by (Select) 113] Y >= Y by (Meta) 114] filter(F, _|_) >= _|_ by (Bot) 115] filter(F, add(X, Y)) >= filter2(F, X, Y) because [116], by (Star) 116] filter*(F, add(X, Y)) >= filter2(F, X, Y) because filter = filter2, filter in Mul, [117], [118] and [121], by (Stat) 117] F >= F by (Meta) 118] add(X, Y) > X because [119], by definition 119] add*(X, Y) >= X because [120], by (Select) 120] X >= X by (Meta) 121] add(X, Y) > Y because [122], by definition 122] add*(X, Y) >= Y because [123], by (Select) 123] Y >= Y by (Meta) 124] filter2(F, X, Y) >= add(X, filter(F, Y)) because [125], by (Star) 125] filter2*(F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [126] and [128], by (Copy) 126] filter2*(F, X, Y) >= X because [127], by (Select) 127] X >= X by (Meta) 128] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [129] and [130], by (Stat) 129] F >= F by (Meta) 130] Y >= Y by (Meta) 131] filter2(F, X, Y) >= filter(F, Y) because [132], by (Star) 132] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [133] and [134], by (Stat) 133] F >= F by (Meta) 134] Y >= Y by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_11, R_0, static, formative) by (P_12, R_0, static, formative), where P_12 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(false, X, add(Y, Z)) =#> low#(X, Z) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) Thus, the original system is terminating if (P_12, R_0, static, formative) is finite. We consider the dependency pair problem (P_12, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) if!fac6220low#(false, X, add(Y, Z)) >? low#(X, Z) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_2, x_3, x_4) [[high(x_1, x_2)]] = high(x_2) [[high#(x_1, x_2)]] = high#(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_1, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[if!fac6220low#(x_1, x_2, x_3)]] = if!fac6220low#(x_2, x_3) [[le(x_1, x_2)]] = le(x_1) [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, add, app, filter, filter2, high, high#, if!fac6220high, if!fac6220high#, if!fac6220low, if!fac6220low#, le, low, low#, map, quicksort, quot}, and the following precedence: if!fac6220low# = low# > map > @_{o -> o} > quicksort > app > quot > filter = filter2 > add = high = if!fac6220high = if!fac6220low = low > high# = le > if!fac6220high# Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) if!fac6220low#(X, add(Y, Z)) > low#(X, Z) high#(add(X, Y)) >= if!fac6220high#(le(X), add(X, Y)) if!fac6220high#(_|_, add(X, Y)) >= high#(Y) X >= X X >= X quot(_|_, X) >= _|_ quot(X, Y) >= quot(X, Y) le(_|_) >= _|_ le(X) >= _|_ le(X) >= le(X) app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(_|_) >= _|_ low(add(X, Y)) >= if!fac6220low(add(X, Y)) if!fac6220low(add(X, Y)) >= add(X, low(Y)) if!fac6220low(add(X, Y)) >= low(Y) high(_|_) >= _|_ high(add(X, Y)) >= if!fac6220high(add(X, Y)) if!fac6220high(add(X, Y)) >= high(Y) if!fac6220high(add(X, Y)) >= add(X, high(Y)) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(F, X, Y) filter2(F, X, Y) >= add(X, filter(F, Y)) filter2(F, X, Y) >= filter(F, Y) With these choices, we have: 1] low#(X, add(Y, Z)) >= if!fac6220low#(X, add(Y, Z)) because low# = if!fac6220low#, low# in Mul, [2] and [3], by (Fun) 2] X >= X by (Meta) 3] add(Y, Z) >= add(Y, Z) because add in Mul, [4] and [5], by (Fun) 4] Y >= Y by (Meta) 5] Z >= Z by (Meta) 6] if!fac6220low#(X, add(Y, Z)) > low#(X, Z) because [7], by definition 7] if!fac6220low#*(X, add(Y, Z)) >= low#(X, Z) because if!fac6220low# = low#, if!fac6220low# in Mul, [8] and [9], by (Stat) 8] X >= X by (Meta) 9] add(Y, Z) > Z because [10], by definition 10] add*(Y, Z) >= Z because [11], by (Select) 11] Z >= Z by (Meta) 12] high#(add(X, Y)) >= if!fac6220high#(le(X), add(X, Y)) because [13], by (Star) 13] high#*(add(X, Y)) >= if!fac6220high#(le(X), add(X, Y)) because high# > if!fac6220high#, [14] and [18], by (Copy) 14] high#*(add(X, Y)) >= le(X) because high# = le, high# in Mul and [15], by (Stat) 15] add(X, Y) > X because [16], by definition 16] add*(X, Y) >= X because [17], by (Select) 17] X >= X by (Meta) 18] high#*(add(X, Y)) >= add(X, Y) because [19], by (Select) 19] add(X, Y) >= add(X, Y) because add in Mul, [20] and [21], by (Fun) 20] X >= X by (Meta) 21] Y >= Y by (Meta) 22] if!fac6220high#(_|_, add(X, Y)) >= high#(Y) because [23], by (Star) 23] if!fac6220high#*(_|_, add(X, Y)) >= high#(Y) because [24], by (Select) 24] add(X, Y) >= high#(Y) because [25], by (Star) 25] add*(X, Y) >= high#(Y) because add > high# and [26], by (Copy) 26] add*(X, Y) >= Y because [27], by (Select) 27] Y >= Y by (Meta) 28] X >= X by (Meta) 29] X >= X by (Meta) 30] quot(_|_, X) >= _|_ by (Bot) 31] quot(X, Y) >= quot(X, Y) because quot in Mul, [32] and [33], by (Fun) 32] X >= X by (Meta) 33] Y >= Y by (Meta) 34] le(_|_) >= _|_ by (Bot) 35] le(X) >= _|_ by (Bot) 36] le(X) >= le(X) because le in Mul and [37], by (Fun) 37] X >= X by (Meta) 38] app(_|_, X) >= X because [39], by (Star) 39] app*(_|_, X) >= X because [40], by (Select) 40] X >= X by (Meta) 41] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [42], by (Star) 42] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [43] and [47], by (Copy) 43] app*(add(X, Y), Z) >= X because [44], by (Select) 44] add(X, Y) >= X because [45], by (Star) 45] add*(X, Y) >= X because [46], by (Select) 46] X >= X by (Meta) 47] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [48] and [51], by (Stat) 48] add(X, Y) > Y because [49], by definition 49] add*(X, Y) >= Y because [50], by (Select) 50] Y >= Y by (Meta) 51] Z >= Z by (Meta) 52] low(_|_) >= _|_ by (Bot) 53] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [3], by (Fun) 54] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [55], by (Star) 55] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [56] and [59], by (Stat) 56] add(X, Y) > X because [57], by definition 57] add*(X, Y) >= X because [58], by (Select) 58] X >= X by (Meta) 59] add(X, Y) > low(Y) because [60], by definition 60] add*(X, Y) >= low(Y) because add = low, add in Mul and [61], by (Stat) 61] Y >= Y by (Meta) 62] if!fac6220low(add(X, Y)) >= low(Y) because [63], by (Star) 63] if!fac6220low*(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [9], by (Stat) 64] high(_|_) >= _|_ by (Bot) 65] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [66], by (Fun) 66] add(X, Y) >= add(X, Y) because add in Mul, [20] and [21], by (Fun) 67] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [68], by (Fun) 68] add(X, Y) >= Y because [69], by (Star) 69] add*(X, Y) >= Y because [70], by (Select) 70] Y >= Y by (Meta) 71] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [72], by (Star) 72] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [73] and [76], by (Stat) 73] add(X, Y) > X because [74], by definition 74] add*(X, Y) >= X because [75], by (Select) 75] X >= X by (Meta) 76] add(X, Y) > high(Y) because [77], by definition 77] add*(X, Y) >= high(Y) because add = high, add in Mul and [78], by (Stat) 78] Y >= Y by (Meta) 79] quicksort(_|_) >= _|_ by (Bot) 80] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [81], by (Star) 81] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [82] and [86], by (Copy) 82] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [83], by (Stat) 83] add(X, Y) > low(Y) because [84], by definition 84] add*(X, Y) >= low(Y) because add = low, add in Mul and [85], by (Stat) 85] Y >= Y by (Meta) 86] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [87] and [91], by (Copy) 87] quicksort*(add(X, Y)) >= X because [88], by (Select) 88] add(X, Y) >= X because [89], by (Star) 89] add*(X, Y) >= X because [90], by (Select) 90] X >= X by (Meta) 91] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [92], by (Stat) 92] add(X, Y) > high(Y) because [93], by definition 93] add*(X, Y) >= high(Y) because add = high, add in Mul and [85], by (Stat) 94] map(F, _|_) >= _|_ by (Bot) 95] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [96], by (Star) 96] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [97] and [104], by (Copy) 97] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [98] and [100], by (Copy) 98] map*(F, add(X, Y)) >= F because [99], by (Select) 99] F >= F by (Meta) 100] map*(F, add(X, Y)) >= X because [101], by (Select) 101] add(X, Y) >= X because [102], by (Star) 102] add*(X, Y) >= X because [103], by (Select) 103] X >= X by (Meta) 104] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [105] and [106], by (Stat) 105] F >= F by (Meta) 106] add(X, Y) > Y because [107], by definition 107] add*(X, Y) >= Y because [108], by (Select) 108] Y >= Y by (Meta) 109] filter(F, _|_) >= _|_ by (Bot) 110] filter(F, add(X, Y)) >= filter2(F, X, Y) because [111], by (Star) 111] filter*(F, add(X, Y)) >= filter2(F, X, Y) because filter = filter2, filter in Mul, [112], [113] and [116], by (Stat) 112] F >= F by (Meta) 113] add(X, Y) > X because [114], by definition 114] add*(X, Y) >= X because [115], by (Select) 115] X >= X by (Meta) 116] add(X, Y) > Y because [117], by definition 117] add*(X, Y) >= Y because [118], by (Select) 118] Y >= Y by (Meta) 119] filter2(F, X, Y) >= add(X, filter(F, Y)) because [120], by (Star) 120] filter2*(F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [121] and [123], by (Copy) 121] filter2*(F, X, Y) >= X because [122], by (Select) 122] X >= X by (Meta) 123] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [124] and [125], by (Stat) 124] F >= F by (Meta) 125] Y >= Y by (Meta) 126] filter2(F, X, Y) >= filter(F, Y) because [127], by (Star) 127] filter2*(F, X, Y) >= filter(F, Y) because filter2 = filter, filter2 in Mul, [128] and [129], by (Stat) 128] F >= F by (Meta) 129] Y >= Y by (Meta) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_12, R_0, static, formative) by (P_13, R_0, static, formative), where P_13 consists of: low#(X, add(Y, Z)) =#> if!fac6220low#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) Thus, the original system is terminating if (P_13, R_0, static, formative) is finite. We consider the dependency pair problem (P_13, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: low#(X, add(Y, Z)) >? if!fac6220low#(le(Y, X), X, add(Y, Z)) high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 false = 0 filter = \G0y1.2 filter2 = \y0G1y2y3.2 high = \y0y1.0 high# = \y0y1.0 if!fac6220high = \y0y1y2.0 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 if!fac6220low# = \y0y1y2.0 le = \y0y1.0 low = \y0y1.0 low# = \y0y1.3 map = \G0y1.0 minus = \y0y1.2y0 nil = 0 quicksort = \y0.0 quot = \y0y1.0 s = \y0.y0 true = 0 Using this interpretation, the requirements translate to: [[low#(_x0, add(_x1, _x2))]] = 3 > 0 = [[if!fac6220low#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[high#(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high#(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high#(_x0, _x2)]] [[minus(_x0, 0)]] = 2x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = 2x0 >= 2x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 0 >= 0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 2 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 2 >= 2 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 2 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 2 >= 2 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_13, R_0, static, formative) by (P_14, R_0, static, formative), where P_14 consists of: high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) =#> high#(X, Z) Thus, the original system is terminating if (P_14, R_0, static, formative) is finite. We consider the dependency pair problem (P_14, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) if!fac6220high#(false, X, add(Y, Z)) >? high#(X, Z) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) Since this representation is not advantageous for the higher-order recursive path ordering, we present the strict requirements in their unextended form, which is not problematic since for any F, s and substituion gamma: (F s)gamma beta-reduces to F(s)gamma.) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[filter(x_1, x_2)]] = filter(x_2, x_1) [[filter2(x_1, x_2, x_3, x_4)]] = filter2(x_4, x_2, x_3, x_1) [[high(x_1, x_2)]] = high(x_2) [[high#(x_1, x_2)]] = high#(x_2) [[if!fac6220high(x_1, x_2, x_3)]] = if!fac6220high(x_3) [[if!fac6220high#(x_1, x_2, x_3)]] = if!fac6220high#(x_1, x_3) [[if!fac6220low(x_1, x_2, x_3)]] = if!fac6220low(x_3) [[le(x_1, x_2)]] = x_1 [[low(x_1, x_2)]] = low(x_2) [[minus(x_1, x_2)]] = x_1 [[nil]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {filter, filter2} and Mul = {@_{o -> o}, add, app, high, high#, if!fac6220high, if!fac6220high#, if!fac6220low, low, map, quicksort, quot}, and the following precedence: map > quicksort > filter = filter2 > app > add = high = high# = if!fac6220high = if!fac6220low = low > if!fac6220high# > @_{o -> o} > quot Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: high#(add(X, Y)) >= if!fac6220high#(X, add(X, Y)) if!fac6220high#(_|_, add(X, Y)) > high#(Y) X >= X X >= X quot(_|_, X) >= _|_ quot(X, Y) >= quot(X, Y) _|_ >= _|_ X >= _|_ X >= X app(_|_, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(_|_) >= _|_ low(add(X, Y)) >= if!fac6220low(add(X, Y)) if!fac6220low(add(X, Y)) >= add(X, low(Y)) if!fac6220low(add(X, Y)) >= low(Y) high(_|_) >= _|_ high(add(X, Y)) >= if!fac6220high(add(X, Y)) if!fac6220high(add(X, Y)) >= high(Y) if!fac6220high(add(X, Y)) >= add(X, high(Y)) quicksort(_|_) >= _|_ quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) map(F, _|_) >= _|_ map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) filter(F, _|_) >= _|_ filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) filter2(_|_, F, X, Y) >= filter(F, Y) With these choices, we have: 1] high#(add(X, Y)) >= if!fac6220high#(X, add(X, Y)) because [2], by (Star) 2] high#*(add(X, Y)) >= if!fac6220high#(X, add(X, Y)) because high# > if!fac6220high#, [3] and [7], by (Copy) 3] high#*(add(X, Y)) >= X because [4], by (Select) 4] add(X, Y) >= X because [5], by (Star) 5] add*(X, Y) >= X because [6], by (Select) 6] X >= X by (Meta) 7] high#*(add(X, Y)) >= add(X, Y) because [8], by (Select) 8] add(X, Y) >= add(X, Y) because add in Mul, [9] and [10], by (Fun) 9] X >= X by (Meta) 10] Y >= Y by (Meta) 11] if!fac6220high#(_|_, add(X, Y)) > high#(Y) because [12], by definition 12] if!fac6220high#*(_|_, add(X, Y)) >= high#(Y) because [13], by (Select) 13] add(X, Y) >= high#(Y) because [14], by (Star) 14] add*(X, Y) >= high#(Y) because add = high#, add in Mul and [15], by (Stat) 15] Y >= Y by (Meta) 16] X >= X by (Meta) 17] X >= X by (Meta) 18] quot(_|_, X) >= _|_ by (Bot) 19] quot(X, Y) >= quot(X, Y) because quot in Mul, [20] and [21], by (Fun) 20] X >= X by (Meta) 21] Y >= Y by (Meta) 22] _|_ >= _|_ by (Bot) 23] X >= _|_ by (Bot) 24] X >= X by (Meta) 25] app(_|_, X) >= X because [26], by (Star) 26] app*(_|_, X) >= X because [27], by (Select) 27] X >= X by (Meta) 28] app(add(X, Y), Z) >= add(X, app(Y, Z)) because [29], by (Star) 29] app*(add(X, Y), Z) >= add(X, app(Y, Z)) because app > add, [30] and [34], by (Copy) 30] app*(add(X, Y), Z) >= X because [31], by (Select) 31] add(X, Y) >= X because [32], by (Star) 32] add*(X, Y) >= X because [33], by (Select) 33] X >= X by (Meta) 34] app*(add(X, Y), Z) >= app(Y, Z) because app in Mul, [35] and [38], by (Stat) 35] add(X, Y) > Y because [36], by definition 36] add*(X, Y) >= Y because [37], by (Select) 37] Y >= Y by (Meta) 38] Z >= Z by (Meta) 39] low(_|_) >= _|_ by (Bot) 40] low(add(X, Y)) >= if!fac6220low(add(X, Y)) because low = if!fac6220low, low in Mul and [41], by (Fun) 41] add(X, Y) >= add(X, Y) because add in Mul, [42] and [43], by (Fun) 42] X >= X by (Meta) 43] Y >= Y by (Meta) 44] if!fac6220low(add(X, Y)) >= add(X, low(Y)) because [45], by (Star) 45] if!fac6220low*(add(X, Y)) >= add(X, low(Y)) because if!fac6220low = add, if!fac6220low in Mul, [46] and [49], by (Stat) 46] add(X, Y) > X because [47], by definition 47] add*(X, Y) >= X because [48], by (Select) 48] X >= X by (Meta) 49] add(X, Y) > low(Y) because [50], by definition 50] add*(X, Y) >= low(Y) because add = low, add in Mul and [51], by (Stat) 51] Y >= Y by (Meta) 52] if!fac6220low(add(X, Y)) >= low(Y) because if!fac6220low = low, if!fac6220low in Mul and [53], by (Fun) 53] add(X, Y) >= Y because [54], by (Star) 54] add*(X, Y) >= Y because [55], by (Select) 55] Y >= Y by (Meta) 56] high(_|_) >= _|_ by (Bot) 57] high(add(X, Y)) >= if!fac6220high(add(X, Y)) because high = if!fac6220high, high in Mul and [58], by (Fun) 58] add(X, Y) >= add(X, Y) because add in Mul, [9] and [10], by (Fun) 59] if!fac6220high(add(X, Y)) >= high(Y) because if!fac6220high = high, if!fac6220high in Mul and [60], by (Fun) 60] add(X, Y) >= Y because [61], by (Star) 61] add*(X, Y) >= Y because [62], by (Select) 62] Y >= Y by (Meta) 63] if!fac6220high(add(X, Y)) >= add(X, high(Y)) because [64], by (Star) 64] if!fac6220high*(add(X, Y)) >= add(X, high(Y)) because if!fac6220high = add, if!fac6220high in Mul, [65] and [68], by (Stat) 65] add(X, Y) > X because [66], by definition 66] add*(X, Y) >= X because [67], by (Select) 67] X >= X by (Meta) 68] add(X, Y) > high(Y) because [69], by definition 69] add*(X, Y) >= high(Y) because add = high, add in Mul and [15], by (Stat) 70] quicksort(_|_) >= _|_ by (Bot) 71] quicksort(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because [72], by (Star) 72] quicksort*(add(X, Y)) >= app(quicksort(low(Y)), add(X, quicksort(high(Y)))) because quicksort > app, [73] and [77], by (Copy) 73] quicksort*(add(X, Y)) >= quicksort(low(Y)) because quicksort in Mul and [74], by (Stat) 74] add(X, Y) > low(Y) because [75], by definition 75] add*(X, Y) >= low(Y) because add = low, add in Mul and [76], by (Stat) 76] Y >= Y by (Meta) 77] quicksort*(add(X, Y)) >= add(X, quicksort(high(Y))) because quicksort > add, [78] and [82], by (Copy) 78] quicksort*(add(X, Y)) >= X because [79], by (Select) 79] add(X, Y) >= X because [80], by (Star) 80] add*(X, Y) >= X because [81], by (Select) 81] X >= X by (Meta) 82] quicksort*(add(X, Y)) >= quicksort(high(Y)) because quicksort in Mul and [83], by (Stat) 83] add(X, Y) > high(Y) because [84], by definition 84] add*(X, Y) >= high(Y) because add = high, add in Mul and [76], by (Stat) 85] map(F, _|_) >= _|_ by (Bot) 86] map(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because [87], by (Star) 87] map*(F, add(X, Y)) >= add(@_{o -> o}(F, X), map(F, Y)) because map > add, [88] and [95], by (Copy) 88] map*(F, add(X, Y)) >= @_{o -> o}(F, X) because map > @_{o -> o}, [89] and [91], by (Copy) 89] map*(F, add(X, Y)) >= F because [90], by (Select) 90] F >= F by (Meta) 91] map*(F, add(X, Y)) >= X because [92], by (Select) 92] add(X, Y) >= X because [93], by (Star) 93] add*(X, Y) >= X because [94], by (Select) 94] X >= X by (Meta) 95] map*(F, add(X, Y)) >= map(F, Y) because map in Mul, [96] and [97], by (Stat) 96] F >= F by (Meta) 97] add(X, Y) > Y because [98], by definition 98] add*(X, Y) >= Y because [99], by (Select) 99] Y >= Y by (Meta) 100] filter(F, _|_) >= _|_ by (Bot) 101] filter(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because [102], by (Star) 102] filter*(F, add(X, Y)) >= filter2(@_{o -> o}(F, X), F, X, Y) because filter = filter2, [103], [106], [107], [109] and [113], by (Stat) 103] add(X, Y) > Y because [104], by definition 104] add*(X, Y) >= Y because [105], by (Select) 105] Y >= Y by (Meta) 106] filter*(F, add(X, Y)) >= @_{o -> o}(F, X) because filter > @_{o -> o}, [107] and [109], by (Copy) 107] filter*(F, add(X, Y)) >= F because [108], by (Select) 108] F >= F by (Meta) 109] filter*(F, add(X, Y)) >= X because [110], by (Select) 110] add(X, Y) >= X because [111], by (Star) 111] add*(X, Y) >= X because [112], by (Select) 112] X >= X by (Meta) 113] filter*(F, add(X, Y)) >= Y because [114], by (Select) 114] add(X, Y) >= Y because [104], by (Star) 115] filter2(_|_, F, X, Y) >= add(X, filter(F, Y)) because [116], by (Star) 116] filter2*(_|_, F, X, Y) >= add(X, filter(F, Y)) because filter2 > add, [117] and [119], by (Copy) 117] filter2*(_|_, F, X, Y) >= X because [118], by (Select) 118] X >= X by (Meta) 119] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [120], [121], [122] and [123], by (Stat) 120] F >= F by (Meta) 121] Y >= Y by (Meta) 122] filter2*(_|_, F, X, Y) >= F because [120], by (Select) 123] filter2*(_|_, F, X, Y) >= Y because [121], by (Select) 124] filter2(_|_, F, X, Y) >= filter(F, Y) because [125], by (Star) 125] filter2*(_|_, F, X, Y) >= filter(F, Y) because filter2 = filter, [126], [127], [128] and [129], by (Stat) 126] F >= F by (Meta) 127] Y >= Y by (Meta) 128] filter2*(_|_, F, X, Y) >= F because [126], by (Select) 129] filter2*(_|_, F, X, Y) >= Y because [127], by (Select) By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace the dependency pair problem (P_14, R_0, static, formative) by (P_15, R_0, static, formative), where P_15 consists of: high#(X, add(Y, Z)) =#> if!fac6220high#(le(Y, X), X, add(Y, Z)) Thus, the original system is terminating if (P_15, R_0, static, formative) is finite. We consider the dependency pair problem (P_15, R_0, static, formative). We will use the reduction pair processor [Kop12, Thm. 7.16]. It suffices to find a standard reduction pair [Kop12, Def. 6.69]. Thus, we must orient: high#(X, add(Y, Z)) >? if!fac6220high#(le(Y, X), X, add(Y, Z)) minus(X, 0) >= X minus(s(X), s(Y)) >= minus(X, Y) quot(0, s(X)) >= 0 quot(s(X), s(Y)) >= s(quot(minus(X, Y), s(Y))) le(0, X) >= true le(s(X), 0) >= false le(s(X), s(Y)) >= le(X, Y) app(nil, X) >= X app(add(X, Y), Z) >= add(X, app(Y, Z)) low(X, nil) >= nil low(X, add(Y, Z)) >= if!fac6220low(le(Y, X), X, add(Y, Z)) if!fac6220low(true, X, add(Y, Z)) >= add(Y, low(X, Z)) if!fac6220low(false, X, add(Y, Z)) >= low(X, Z) high(X, nil) >= nil high(X, add(Y, Z)) >= if!fac6220high(le(Y, X), X, add(Y, Z)) if!fac6220high(true, X, add(Y, Z)) >= high(X, Z) if!fac6220high(false, X, add(Y, Z)) >= add(Y, high(X, Z)) quicksort(nil) >= nil quicksort(add(X, Y)) >= app(quicksort(low(X, Y)), add(X, quicksort(high(X, Y)))) map(F, nil) >= nil map(F, add(X, Y)) >= add(F X, map(F, Y)) filter(F, nil) >= nil filter(F, add(X, Y)) >= filter2(F X, F, X, Y) filter2(true, F, X, Y) >= add(X, filter(F, Y)) filter2(false, F, X, Y) >= filter(F, Y) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: 0 = 0 add = \y0y1.0 app = \y0y1.y1 false = 0 filter = \G0y1.0 filter2 = \y0G1y2y3.0 high = \y0y1.2y0 high# = \y0y1.3 if!fac6220high = \y0y1y2.2y1 if!fac6220high# = \y0y1y2.0 if!fac6220low = \y0y1y2.0 le = \y0y1.0 low = \y0y1.0 map = \G0y1.0 minus = \y0y1.y0 nil = 0 quicksort = \y0.0 quot = \y0y1.0 s = \y0.y0 true = 0 Using this interpretation, the requirements translate to: [[high#(_x0, add(_x1, _x2))]] = 3 > 0 = [[if!fac6220high#(le(_x1, _x0), _x0, add(_x1, _x2))]] [[minus(_x0, 0)]] = x0 >= x0 = [[_x0]] [[minus(s(_x0), s(_x1))]] = x0 >= x0 = [[minus(_x0, _x1)]] [[quot(0, s(_x0))]] = 0 >= 0 = [[0]] [[quot(s(_x0), s(_x1))]] = 0 >= 0 = [[s(quot(minus(_x0, _x1), s(_x1)))]] [[le(0, _x0)]] = 0 >= 0 = [[true]] [[le(s(_x0), 0)]] = 0 >= 0 = [[false]] [[le(s(_x0), s(_x1))]] = 0 >= 0 = [[le(_x0, _x1)]] [[app(nil, _x0)]] = x0 >= x0 = [[_x0]] [[app(add(_x0, _x1), _x2)]] = x2 >= 0 = [[add(_x0, app(_x1, _x2))]] [[low(_x0, nil)]] = 0 >= 0 = [[nil]] [[low(_x0, add(_x1, _x2))]] = 0 >= 0 = [[if!fac6220low(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220low(true, _x0, add(_x1, _x2))]] = 0 >= 0 = [[add(_x1, low(_x0, _x2))]] [[if!fac6220low(false, _x0, add(_x1, _x2))]] = 0 >= 0 = [[low(_x0, _x2)]] [[high(_x0, nil)]] = 2x0 >= 0 = [[nil]] [[high(_x0, add(_x1, _x2))]] = 2x0 >= 2x0 = [[if!fac6220high(le(_x1, _x0), _x0, add(_x1, _x2))]] [[if!fac6220high(true, _x0, add(_x1, _x2))]] = 2x0 >= 2x0 = [[high(_x0, _x2)]] [[if!fac6220high(false, _x0, add(_x1, _x2))]] = 2x0 >= 0 = [[add(_x1, high(_x0, _x2))]] [[quicksort(nil)]] = 0 >= 0 = [[nil]] [[quicksort(add(_x0, _x1))]] = 0 >= 0 = [[app(quicksort(low(_x0, _x1)), add(_x0, quicksort(high(_x0, _x1))))]] [[map(_F0, nil)]] = 0 >= 0 = [[nil]] [[map(_F0, add(_x1, _x2))]] = 0 >= 0 = [[add(_F0 _x1, map(_F0, _x2))]] [[filter(_F0, nil)]] = 0 >= 0 = [[nil]] [[filter(_F0, add(_x1, _x2))]] = 0 >= 0 = [[filter2(_F0 _x1, _F0, _x1, _x2)]] [[filter2(true, _F0, _x1, _x2)]] = 0 >= 0 = [[add(_x1, filter(_F0, _x2))]] [[filter2(false, _F0, _x1, _x2)]] = 0 >= 0 = [[filter(_F0, _x2)]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_15, R_0) by ({}, R_0). By the empty set processor [Kop12, Thm. 7.15] this problem may be immediately removed. As all dependency pair problems were succesfully simplified with sound (and complete) processors until nothing remained, we conclude termination. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012. [Kop13] C. Kop. Static Dependency Pairs with Accessibility. Unpublished manuscript, http://cl-informatik.uibk.ac.at/users/kop/static.pdf, 2013. [KusIsoSakBla09] K. Kusakari, Y. Isogai, M. Sakai, and F. Blanqui. Static Dependency Pair Method Based On Strong Computability for Higher-Order Rewrite Systems. In volume 92(10) of IEICE Transactions on Information and Systems. 2007--2015, 2009.