We consider the system AotoYamada_05__016. Alphabet: 0 : [] --> a cons : [a * c] --> c false : [] --> b filter : [a -> b] --> c -> c filtersub : [b * a -> b * c] --> c neq : [a] --> a -> b nil : [] --> c nonzero : [] --> c -> c s : [a] --> a true : [] --> b Rules: neq(0) 0 => false neq(0) s(x) => true neq(s(x)) 0 => true neq(s(x)) s(y) => neq(x) y filter(f) nil => nil filter(f) cons(x, y) => filtersub(f x, f, cons(x, y)) filtersub(true, f, cons(x, y)) => cons(x, filter(f) y) filtersub(false, f, cons(x, y)) => filter(f) y nonzero => filter(neq(0)) This AFS is converted to an AFSM simply by replacing all free variables by meta-variables (with arity 0). We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): neq(0) 0 >? false neq(0) s(X) >? true neq(s(X)) 0 >? true neq(s(X)) s(Y) >? neq(X) Y filter(F) nil >? nil filter(F) cons(X, Y) >? filtersub(F X, F, cons(X, Y)) filtersub(true, F, cons(X, Y)) >? cons(X, filter(F) Y) filtersub(false, F, cons(X, Y)) >? filter(F) Y nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[@_{o -> o}(x_1, x_2)]] = @_{o -> o}(x_2, x_1) [[filtersub(x_1, x_2, x_3)]] = filtersub(x_3, x_2, x_1) [[nil]] = _|_ [[true]] = _|_ We choose Lex = {@_{o -> o}, cons, filtersub} and Mul = {false, filter, neq, nonzero, s}, and the following precedence: nonzero > neq > @_{o -> o} = cons = filtersub > s > filter > false Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(neq(_|_), _|_) >= false @_{o -> o}(neq(_|_), s(X)) >= _|_ @_{o -> o}(neq(s(X)), _|_) > _|_ @_{o -> o}(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y) @_{o -> o}(filter(F), _|_) >= _|_ @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) filtersub(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) filtersub(false, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) nonzero >= filter(neq(_|_)) With these choices, we have: 1] @_{o -> o}(neq(_|_), _|_) >= false because [2], by (Star) 2] @_{o -> o}*(neq(_|_), _|_) >= false because @_{o -> o} > false, by (Copy) 3] @_{o -> o}(neq(_|_), s(X)) >= _|_ by (Bot) 4] @_{o -> o}(neq(s(X)), _|_) > _|_ because [5], by definition 5] @_{o -> o}*(neq(s(X)), _|_) >= _|_ by (Bot) 6] @_{o -> o}(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y) because [7] and [12], by (Fun) 7] neq(s(X)) >= neq(X) because [8], by (Star) 8] neq*(s(X)) >= neq(X) because neq in Mul and [9], by (Stat) 9] s(X) > X because [10], by definition 10] s*(X) >= X because [11], by (Select) 11] X >= X by (Meta) 12] s(Y) >= Y because [13], by (Star) 13] s*(Y) >= Y because [14], by (Select) 14] Y >= Y by (Meta) 15] @_{o -> o}(filter(F), _|_) >= _|_ by (Bot) 16] @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because [17], by (Star) 17] @_{o -> o}*(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because @_{o -> o} = filtersub, [18], [21], [24], [27] and [31], by (Stat) 18] filter(F) > F because [19], by definition 19] filter*(F) >= F because [20], by (Select) 20] F >= F by (Meta) 21] cons(X, Y) >= cons(X, Y) because [22] and [23], by (Fun) 22] X >= X by (Meta) 23] Y >= Y by (Meta) 24] @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X) because [25], [27] and [29], by (Stat) 25] cons(X, Y) > X because [26], by definition 26] cons*(X, Y) >= X because [22], by (Select) 27] @_{o -> o}*(filter(F), cons(X, Y)) >= F because [28], by (Select) 28] filter(F) >= F because [19], by (Star) 29] @_{o -> o}*(filter(F), cons(X, Y)) >= X because [30], by (Select) 30] cons(X, Y) >= X because [26], by (Star) 31] @_{o -> o}*(filter(F), cons(X, Y)) >= cons(X, Y) because [21], by (Select) 32] filtersub(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because [33], by (Star) 33] filtersub*(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because filtersub = cons, [34], [37] and [39], by (Stat) 34] cons(X, Y) > X because [35], by definition 35] cons*(X, Y) >= X because [36], by (Select) 36] X >= X by (Meta) 37] filtersub*(_|_, F, cons(X, Y)) >= X because [38], by (Select) 38] cons(X, Y) >= X because [35], by (Star) 39] filtersub*(_|_, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because filtersub = @_{o -> o}, [40], [43] and [46], by (Stat) 40] cons(X, Y) > Y because [41], by definition 41] cons*(X, Y) >= Y because [42], by (Select) 42] Y >= Y by (Meta) 43] filtersub*(_|_, F, cons(X, Y)) >= filter(F) because filtersub > filter and [44], by (Copy) 44] filtersub*(_|_, F, cons(X, Y)) >= F because [45], by (Select) 45] F >= F by (Meta) 46] filtersub*(_|_, F, cons(X, Y)) >= Y because [47], by (Select) 47] cons(X, Y) >= Y because [41], by (Star) 48] filtersub(false, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because [49], by (Star) 49] filtersub*(false, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because filtersub = @_{o -> o}, [50], [53] and [56], by (Stat) 50] cons(X, Y) > Y because [51], by definition 51] cons*(X, Y) >= Y because [52], by (Select) 52] Y >= Y by (Meta) 53] filtersub*(false, F, cons(X, Y)) >= filter(F) because filtersub > filter and [54], by (Copy) 54] filtersub*(false, F, cons(X, Y)) >= F because [55], by (Select) 55] F >= F by (Meta) 56] filtersub*(false, F, cons(X, Y)) >= Y because [57], by (Select) 57] cons(X, Y) >= Y because [51], by (Star) 58] nonzero >= filter(neq(_|_)) because [59], by (Star) 59] nonzero* >= filter(neq(_|_)) because nonzero > filter and [60], by (Copy) 60] nonzero* >= neq(_|_) because nonzero > neq and [61], by (Copy) 61] nonzero* >= _|_ by (Bot) We can thus remove the following rules: neq(s(X)) 0 => true We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): neq(0) 0 >? false neq(0) s(X) >? true neq(s(X)) s(Y) >? neq(X) Y filter(F) nil >? nil filter(F) cons(X, Y) >? filtersub(F X, F, cons(X, Y)) filtersub(true, F, cons(X, Y)) >? cons(X, filter(F) Y) filtersub(false, F, cons(X, Y)) >? filter(F) Y nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[@_{o -> o}(x_1, x_2)]] = @_{o -> o}(x_2, x_1) [[false]] = _|_ [[filtersub(x_1, x_2, x_3)]] = filtersub(x_3, x_2, x_1) [[nil]] = _|_ [[true]] = _|_ We choose Lex = {@_{o -> o}, filtersub} and Mul = {cons, filter, neq, nonzero, s}, and the following precedence: @_{o -> o} = filtersub > nonzero > cons > filter > neq > s Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(neq(_|_), _|_) >= _|_ @_{o -> o}(neq(_|_), s(X)) >= _|_ @_{o -> o}(neq(s(X)), s(Y)) > @_{o -> o}(neq(X), Y) @_{o -> o}(filter(F), _|_) >= _|_ @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) filtersub(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) filtersub(_|_, F, cons(X, Y)) > @_{o -> o}(filter(F), Y) nonzero >= filter(neq(_|_)) With these choices, we have: 1] @_{o -> o}(neq(_|_), _|_) >= _|_ by (Bot) 2] @_{o -> o}(neq(_|_), s(X)) >= _|_ by (Bot) 3] @_{o -> o}(neq(s(X)), s(Y)) > @_{o -> o}(neq(X), Y) because [4], by definition 4] @_{o -> o}*(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y) because [5], by (Select) 5] neq(s(X)) @_{o -> o}*(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y) because [6] 6] neq*(s(X), @_{o -> o}*(neq(s(X)), s(Y))) >= @_{o -> o}(neq(X), Y) because [7], by (Select) 7] @_{o -> o}*(neq(s(X)), s(Y)) >= @_{o -> o}(neq(X), Y) because [8], [11] and [21], by (Stat) 8] s(Y) > Y because [9], by definition 9] s*(Y) >= Y because [10], by (Select) 10] Y >= Y by (Meta) 11] @_{o -> o}*(neq(s(X)), s(Y)) >= neq(X) because @_{o -> o} > neq and [12], by (Copy) 12] @_{o -> o}*(neq(s(X)), s(Y)) >= X because [13], by (Select) 13] neq(s(X)) @_{o -> o}*(neq(s(X)), s(Y)) >= X because [14] 14] neq*(s(X), @_{o -> o}*(neq(s(X)), s(Y))) >= X because [15], by (Select) 15] @_{o -> o}*(neq(s(X)), s(Y)) >= X because [16], by (Select) 16] neq(s(X)) @_{o -> o}*(neq(s(X)), s(Y)) >= X because [17] 17] neq*(s(X), @_{o -> o}*(neq(s(X)), s(Y))) >= X because [18], by (Select) 18] s(X) >= X because [19], by (Star) 19] s*(X) >= X because [20], by (Select) 20] X >= X by (Meta) 21] @_{o -> o}*(neq(s(X)), s(Y)) >= Y because [22], by (Select) 22] neq(s(X)) @_{o -> o}*(neq(s(X)), s(Y)) >= Y because [23] 23] neq*(s(X), @_{o -> o}*(neq(s(X)), s(Y))) >= Y because [24], by (Select) 24] @_{o -> o}*(neq(s(X)), s(Y)) >= Y because [25], by (Select) 25] s(Y) >= Y because [9], by (Star) 26] @_{o -> o}(filter(F), _|_) >= _|_ by (Bot) 27] @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because [28], by (Star) 28] @_{o -> o}*(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because @_{o -> o} = filtersub, [29], [32], [35], [38] and [45], by (Stat) 29] filter(F) > F because [30], by definition 30] filter*(F) >= F because [31], by (Select) 31] F >= F by (Meta) 32] cons(X, Y) >= cons(X, Y) because cons in Mul, [33] and [34], by (Fun) 33] X >= X by (Meta) 34] Y >= Y by (Meta) 35] @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X) because [29], [36], [38] and [40], by (Stat) 36] cons(X, Y) >= X because [37], by (Star) 37] cons*(X, Y) >= X because [33], by (Select) 38] @_{o -> o}*(filter(F), cons(X, Y)) >= F because [39], by (Select) 39] filter(F) >= F because [30], by (Star) 40] @_{o -> o}*(filter(F), cons(X, Y)) >= X because [41], by (Select) 41] filter(F) @_{o -> o}*(filter(F), cons(X, Y)) >= X because [42] 42] filter*(F, @_{o -> o}*(filter(F), cons(X, Y))) >= X because [43], by (Select) 43] @_{o -> o}*(filter(F), cons(X, Y)) >= X because [44], by (Select) 44] cons(X, Y) >= X because [37], by (Star) 45] @_{o -> o}*(filter(F), cons(X, Y)) >= cons(X, Y) because [32], by (Select) 46] filtersub(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because [47], by (Star) 47] filtersub*(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because filtersub > cons, [48] and [52], by (Copy) 48] filtersub*(_|_, F, cons(X, Y)) >= X because [49], by (Select) 49] cons(X, Y) >= X because [50], by (Star) 50] cons*(X, Y) >= X because [51], by (Select) 51] X >= X by (Meta) 52] filtersub*(_|_, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because filtersub = @_{o -> o}, [53], [56] and [59], by (Stat) 53] cons(X, Y) > Y because [54], by definition 54] cons*(X, Y) >= Y because [55], by (Select) 55] Y >= Y by (Meta) 56] filtersub*(_|_, F, cons(X, Y)) >= filter(F) because filtersub > filter and [57], by (Copy) 57] filtersub*(_|_, F, cons(X, Y)) >= F because [58], by (Select) 58] F >= F by (Meta) 59] filtersub*(_|_, F, cons(X, Y)) >= Y because [60], by (Select) 60] cons(X, Y) >= Y because [54], by (Star) 61] filtersub(_|_, F, cons(X, Y)) > @_{o -> o}(filter(F), Y) because [62], by definition 62] filtersub*(_|_, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because filtersub = @_{o -> o}, [63], [66] and [69], by (Stat) 63] cons(X, Y) > Y because [64], by definition 64] cons*(X, Y) >= Y because [65], by (Select) 65] Y >= Y by (Meta) 66] filtersub*(_|_, F, cons(X, Y)) >= filter(F) because filtersub > filter and [67], by (Copy) 67] filtersub*(_|_, F, cons(X, Y)) >= F because [68], by (Select) 68] F >= F by (Meta) 69] filtersub*(_|_, F, cons(X, Y)) >= Y because [70], by (Select) 70] cons(X, Y) >= Y because [64], by (Star) 71] nonzero >= filter(neq(_|_)) because [72], by (Star) 72] nonzero* >= filter(neq(_|_)) because nonzero > filter and [73], by (Copy) 73] nonzero* >= neq(_|_) because nonzero > neq and [74], by (Copy) 74] nonzero* >= _|_ by (Bot) We can thus remove the following rules: neq(s(X)) s(Y) => neq(X) Y filtersub(false, F, cons(X, Y)) => filter(F) Y We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): neq(0) 0 >? false neq(0) s(X) >? true filter(F) nil >? nil filter(F) cons(X, Y) >? filtersub(F X, F, cons(X, Y)) filtersub(true, F, cons(X, Y)) >? cons(X, filter(F) Y) nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[@_{o -> o}(x_1, x_2)]] = @_{o -> o}(x_2, x_1) [[false]] = _|_ [[filtersub(x_1, x_2, x_3)]] = filtersub(x_3, x_2, x_1) [[true]] = _|_ We choose Lex = {@_{o -> o}, filtersub} and Mul = {cons, filter, neq, nil, nonzero, s}, and the following precedence: @_{o -> o} = filtersub > nonzero > nil > filter > cons > s > neq Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(neq(_|_), _|_) >= _|_ @_{o -> o}(neq(_|_), s(X)) >= _|_ @_{o -> o}(filter(F), nil) > nil @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) filtersub(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) nonzero >= filter(neq(_|_)) With these choices, we have: 1] @_{o -> o}(neq(_|_), _|_) >= _|_ by (Bot) 2] @_{o -> o}(neq(_|_), s(X)) >= _|_ by (Bot) 3] @_{o -> o}(filter(F), nil) > nil because [4], by definition 4] @_{o -> o}*(filter(F), nil) >= nil because [5], by (Select) 5] nil >= nil by (Fun) 6] @_{o -> o}(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because [7], by (Star) 7] @_{o -> o}*(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because @_{o -> o} = filtersub, [8], [11], [14], [17] and [20], by (Stat) 8] filter(F) > F because [9], by definition 9] filter*(F) >= F because [10], by (Select) 10] F >= F by (Meta) 11] cons(X, Y) >= cons(X, Y) because cons in Mul, [12] and [13], by (Fun) 12] X >= X by (Meta) 13] Y >= Y by (Meta) 14] @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X) because [8], [15], [17] and [19], by (Stat) 15] cons(X, Y) >= X because [16], by (Star) 16] cons*(X, Y) >= X because [12], by (Select) 17] @_{o -> o}*(filter(F), cons(X, Y)) >= F because [18], by (Select) 18] filter(F) >= F because [9], by (Star) 19] @_{o -> o}*(filter(F), cons(X, Y)) >= X because [15], by (Select) 20] @_{o -> o}*(filter(F), cons(X, Y)) >= cons(X, Y) because @_{o -> o} > cons, [19] and [21], by (Copy) 21] @_{o -> o}*(filter(F), cons(X, Y)) >= Y because [22], by (Select) 22] cons(X, Y) >= Y because [23], by (Star) 23] cons*(X, Y) >= Y because [13], by (Select) 24] filtersub(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because [25], by (Star) 25] filtersub*(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because filtersub > cons, [26] and [30], by (Copy) 26] filtersub*(_|_, F, cons(X, Y)) >= X because [27], by (Select) 27] cons(X, Y) >= X because [28], by (Star) 28] cons*(X, Y) >= X because [29], by (Select) 29] X >= X by (Meta) 30] filtersub*(_|_, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because filtersub = @_{o -> o}, [31], [34] and [37], by (Stat) 31] cons(X, Y) > Y because [32], by definition 32] cons*(X, Y) >= Y because [33], by (Select) 33] Y >= Y by (Meta) 34] filtersub*(_|_, F, cons(X, Y)) >= filter(F) because filtersub > filter and [35], by (Copy) 35] filtersub*(_|_, F, cons(X, Y)) >= F because [36], by (Select) 36] F >= F by (Meta) 37] filtersub*(_|_, F, cons(X, Y)) >= Y because [38], by (Select) 38] cons(X, Y) >= Y because [32], by (Star) 39] nonzero >= filter(neq(_|_)) because [40], by (Star) 40] nonzero* >= filter(neq(_|_)) because nonzero > filter and [41], by (Copy) 41] nonzero* >= neq(_|_) because nonzero > neq and [42], by (Copy) 42] nonzero* >= _|_ by (Bot) We can thus remove the following rules: filter(F) nil => nil We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): neq(0) 0 >? false neq(0) s(X) >? true filter(F) cons(X, Y) >? filtersub(F X, F, cons(X, Y)) filtersub(true, F, cons(X, Y)) >? cons(X, filter(F) Y) nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[@_{o -> o}(x_1, x_2)]] = @_{o -> o}(x_2, x_1) [[false]] = _|_ [[filtersub(x_1, x_2, x_3)]] = filtersub(x_3, x_2, x_1) [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {@_{o -> o}, filtersub} and Mul = {cons, filter, neq, nonzero}, and the following precedence: nonzero > @_{o -> o} = filtersub > neq > filter > cons Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(neq(_|_), _|_) >= _|_ @_{o -> o}(neq(_|_), X) >= _|_ @_{o -> o}(filter(F), cons(X, Y)) > filtersub(@_{o -> o}(F, X), F, cons(X, Y)) filtersub(_|_, F, cons(X, Y)) > cons(X, @_{o -> o}(filter(F), Y)) nonzero >= filter(neq(_|_)) With these choices, we have: 1] @_{o -> o}(neq(_|_), _|_) >= _|_ by (Bot) 2] @_{o -> o}(neq(_|_), X) >= _|_ by (Bot) 3] @_{o -> o}(filter(F), cons(X, Y)) > filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because [4], by definition 4] @_{o -> o}*(filter(F), cons(X, Y)) >= filtersub(@_{o -> o}(F, X), F, cons(X, Y)) because @_{o -> o} = filtersub, [5], [8], [11], [17] and [20], by (Stat) 5] filter(F) > F because [6], by definition 6] filter*(F) >= F because [7], by (Select) 7] F >= F by (Meta) 8] cons(X, Y) >= cons(X, Y) because cons in Mul, [9] and [10], by (Fun) 9] X >= X by (Meta) 10] Y >= Y by (Meta) 11] @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X) because [12], by (Select) 12] filter(F) @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X) because [13] 13] filter*(F, @_{o -> o}*(filter(F), cons(X, Y))) >= @_{o -> o}(F, X) because [14], by (Select) 14] @_{o -> o}*(filter(F), cons(X, Y)) >= @_{o -> o}(F, X) because [5], [15], [17] and [19], by (Stat) 15] cons(X, Y) >= X because [16], by (Star) 16] cons*(X, Y) >= X because [9], by (Select) 17] @_{o -> o}*(filter(F), cons(X, Y)) >= F because [18], by (Select) 18] filter(F) >= F because [6], by (Star) 19] @_{o -> o}*(filter(F), cons(X, Y)) >= X because [15], by (Select) 20] @_{o -> o}*(filter(F), cons(X, Y)) >= cons(X, Y) because @_{o -> o} > cons, [19] and [21], by (Copy) 21] @_{o -> o}*(filter(F), cons(X, Y)) >= Y because [22], by (Select) 22] cons(X, Y) >= Y because [23], by (Star) 23] cons*(X, Y) >= Y because [10], by (Select) 24] filtersub(_|_, F, cons(X, Y)) > cons(X, @_{o -> o}(filter(F), Y)) because [25], by definition 25] filtersub*(_|_, F, cons(X, Y)) >= cons(X, @_{o -> o}(filter(F), Y)) because filtersub > cons, [26] and [30], by (Copy) 26] filtersub*(_|_, F, cons(X, Y)) >= X because [27], by (Select) 27] cons(X, Y) >= X because [28], by (Star) 28] cons*(X, Y) >= X because [29], by (Select) 29] X >= X by (Meta) 30] filtersub*(_|_, F, cons(X, Y)) >= @_{o -> o}(filter(F), Y) because filtersub = @_{o -> o}, [31], [34] and [37], by (Stat) 31] cons(X, Y) > Y because [32], by definition 32] cons*(X, Y) >= Y because [33], by (Select) 33] Y >= Y by (Meta) 34] filtersub*(_|_, F, cons(X, Y)) >= filter(F) because filtersub > filter and [35], by (Copy) 35] filtersub*(_|_, F, cons(X, Y)) >= F because [36], by (Select) 36] F >= F by (Meta) 37] filtersub*(_|_, F, cons(X, Y)) >= Y because [38], by (Select) 38] cons(X, Y) >= Y because [32], by (Star) 39] nonzero >= filter(neq(_|_)) because [40], by (Star) 40] nonzero* >= filter(neq(_|_)) because nonzero > filter and [41], by (Copy) 41] nonzero* >= neq(_|_) because nonzero > neq and [42], by (Copy) 42] nonzero* >= _|_ by (Bot) We can thus remove the following rules: filter(F) cons(X, Y) => filtersub(F X, F, cons(X, Y)) filtersub(true, F, cons(X, Y)) => cons(X, filter(F) Y) We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): neq(0) 0 >? false neq(0) s(X) >? true nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[false]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, filter, neq, nonzero}, and the following precedence: @_{o -> o} > nonzero > neq > filter Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(neq(_|_), _|_) > _|_ @_{o -> o}(neq(_|_), X) >= _|_ nonzero >= filter(neq(_|_)) With these choices, we have: 1] @_{o -> o}(neq(_|_), _|_) > _|_ because [2], by definition 2] @_{o -> o}*(neq(_|_), _|_) >= _|_ by (Bot) 3] @_{o -> o}(neq(_|_), X) >= _|_ by (Bot) 4] nonzero >= filter(neq(_|_)) because [5], by (Star) 5] nonzero* >= filter(neq(_|_)) because nonzero > filter and [6], by (Copy) 6] nonzero* >= neq(_|_) because nonzero > neq and [7], by (Copy) 7] nonzero* >= _|_ by (Bot) We can thus remove the following rules: neq(0) 0 => false We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): neq(0) s(X) >? true nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[s(x_1)]] = x_1 [[true]] = _|_ We choose Lex = {} and Mul = {@_{o -> o}, filter, neq, nonzero}, and the following precedence: @_{o -> o} > nonzero > neq > filter Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: @_{o -> o}(neq(_|_), X) > _|_ nonzero >= filter(neq(_|_)) With these choices, we have: 1] @_{o -> o}(neq(_|_), X) > _|_ because [2], by definition 2] @_{o -> o}*(neq(_|_), X) >= _|_ by (Bot) 3] nonzero >= filter(neq(_|_)) because [4], by (Star) 4] nonzero* >= filter(neq(_|_)) because nonzero > filter and [5], by (Copy) 5] nonzero* >= neq(_|_) because nonzero > neq and [6], by (Copy) 6] nonzero* >= _|_ by (Bot) We can thus remove the following rules: neq(0) s(X) => true We use rule removal, following [Kop12, Theorem 2.23]. This gives the following requirements (possibly using Theorems 2.25 and 2.26 in [Kop12]): nonzero >? filter(neq(0)) We use a recursive path ordering as defined in [Kop12, Chapter 5]. Argument functions: [[0]] = _|_ [[filter(x_1)]] = x_1 We choose Lex = {} and Mul = {neq, nonzero}, and the following precedence: nonzero > neq Taking the argument function into account, and fixing the greater / greater equal choices, the constraints can be denoted as follows: nonzero > neq(_|_) With these choices, we have: 1] nonzero > neq(_|_) because [2], by definition 2] nonzero* >= neq(_|_) because nonzero > neq and [3], by (Copy) 3] nonzero* >= _|_ by (Bot) We can thus remove the following rules: nonzero => filter(neq(0)) All rules were succesfully removed. Thus, termination of the original system has been reduced to termination of the beta-rule, which is well-known to hold. +++ Citations +++ [Kop12] C. Kop. Higher Order Termination. PhD Thesis, 2012.