We consider the system sort. Alphabet: 0 : [] --> nat ascending!6220sort : [list] --> list cons : [nat * list] --> list descending!6220sort : [list] --> list insert : [nat * list * nat -> nat -> nat * nat -> nat -> nat] --> list max : [nat * nat] --> nat min : [nat * nat] --> nat nil : [] --> list s : [nat] --> nat sort : [list * nat -> nat -> nat * nat -> nat -> nat] --> list Rules: max(0, x) => x max(x, 0) => x max(s(x), s(y)) => s(max(x, y)) min(0, x) => 0 min(x, 0) => 0 min(s(x), s(y)) => s(min(x, y)) insert(x, nil, f, g) => cons(x, nil) insert(x, cons(y, z), f, g) => cons(f x y, insert(g x y, z, f, g)) sort(nil, f, g) => nil sort(cons(x, y), f, g) => insert(x, sort(y, f, g), f, g) ascending!6220sort(x) => sort(x, /\y./\z.min(y, z), /\u./\v.max(u, v)) descending!6220sort(x) => sort(x, /\y./\z.max(y, z), /\u./\v.min(u, v)) 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] max#(s(X), s(Y)) =#> max#(X, Y) 1] min#(s(X), s(Y)) =#> min#(X, Y) 2] insert#(X, cons(Y, Z), F, G) =#> insert#(G X Y, Z, F, G) 3] sort#(cons(X, Y), F, G) =#> insert#(X, sort(Y, F, G), F, G) 4] sort#(cons(X, Y), F, G) =#> sort#(Y, F, G) 5] ascending!6220sort#(X) =#> sort#(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) 6] ascending!6220sort#(X) =#> min#(Y, Z) 7] ascending!6220sort#(X) =#> max#(Y, Z) 8] descending!6220sort#(X) =#> sort#(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 9] descending!6220sort#(X) =#> max#(Y, Z) 10] descending!6220sort#(X) =#> min#(Y, Z) Rules R_0: max(0, X) => X max(X, 0) => X max(s(X), s(Y)) => s(max(X, Y)) min(0, X) => 0 min(X, 0) => 0 min(s(X), s(Y)) => s(min(X, Y)) insert(X, nil, F, G) => cons(X, nil) insert(X, cons(Y, Z), F, G) => cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) => nil sort(cons(X, Y), F, G) => insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) => sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) => sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) 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: max#(s(X), s(Y)) >? max#(X, Y) min#(s(X), s(Y)) >? min#(X, Y) insert#(X, cons(Y, Z), F, G) >? insert#(G X Y, Z, F, G) sort#(cons(X, Y), F, G) >? insert#(X, sort(Y, F, G), F, G) sort#(cons(X, Y), F, G) >? sort#(Y, F, G) ascending!6220sort#(X) >? sort#(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) ascending!6220sort#(X) >? min#(Y, Z) ascending!6220sort#(X) >? max#(Y, Z) descending!6220sort#(X) >? sort#(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) descending!6220sort#(X) >? max#(Y, Z) descending!6220sort#(X) >? min#(Y, Z) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 1 ascending!6220sort = \y0.0 ascending!6220sort# = \y0.3 + 2y0 cons = \y0y1.0 descending!6220sort = \y0.0 descending!6220sort# = \y0.3 + 2y0 insert = \y0y1G2G3.0 insert# = \y0y1G2G3.0 max = \y0y1.1 + y0 + y1 max# = \y0y1.0 min = \y0y1.2y0 + 2y1 min# = \y0y1.0 nil = 0 s = \y0.2 sort = \y0G1G2.2G1(0,0) + 2G1(y0,y0) + 2G2(0,0) sort# = \y0G1G2.G1(0,0) Using this interpretation, the requirements translate to: [[max#(s(_x0), s(_x1))]] = 0 >= 0 = [[max#(_x0, _x1)]] [[min#(s(_x0), s(_x1))]] = 0 >= 0 = [[min#(_x0, _x1)]] [[insert#(_x0, cons(_x1, _x2), _F3, _F4)]] = 0 >= 0 = [[insert#(_F4 _x0 _x1, _x2, _F3, _F4)]] [[sort#(cons(_x0, _x1), _F2, _F3)]] = F2(0,0) >= 0 = [[insert#(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[sort#(cons(_x0, _x1), _F2, _F3)]] = F2(0,0) >= F2(0,0) = [[sort#(_x1, _F2, _F3)]] [[ascending!6220sort#(_x0)]] = 3 + 2x0 > 0 = [[sort#(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[ascending!6220sort#(_x0)]] = 3 + 2x0 > 0 = [[min#(_x1, _x2)]] [[ascending!6220sort#(_x0)]] = 3 + 2x0 > 0 = [[max#(_x1, _x2)]] [[descending!6220sort#(_x0)]] = 3 + 2x0 > 1 = [[sort#(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] [[descending!6220sort#(_x0)]] = 3 + 2x0 > 0 = [[max#(_x1, _x2)]] [[descending!6220sort#(_x0)]] = 3 + 2x0 > 0 = [[min#(_x1, _x2)]] [[max(0, _x0)]] = 2 + x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 2 + x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 5 >= 2 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 2 + 2x0 >= 1 = [[0]] [[min(_x0, 0)]] = 2 + 2x0 >= 1 = [[0]] [[min(s(_x0), s(_x1))]] = 8 >= 2 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 0 >= 0 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 0 >= 0 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 2F1(0,0) + 4F0(0,0) >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 2F3(0,0) + 4F2(0,0) >= 0 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 5 + 8x0 >= 2 + 8x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 7 + 4x0 >= 4 + 4x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] 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: max#(s(X), s(Y)) =#> max#(X, Y) min#(s(X), s(Y)) =#> min#(X, Y) insert#(X, cons(Y, Z), F, G) =#> insert#(G X Y, Z, F, G) sort#(cons(X, Y), F, G) =#> insert#(X, sort(Y, F, G), F, G) sort#(cons(X, Y), F, G) =#> sort#(Y, F, G) 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: max#(s(X), s(Y)) >? max#(X, Y) min#(s(X), s(Y)) >? min#(X, Y) insert#(X, cons(Y, Z), F, G) >? insert#(G X Y, Z, F, G) sort#(cons(X, Y), F, G) >? insert#(X, sort(Y, F, G), F, G) sort#(cons(X, Y), F, G) >? sort#(Y, F, G) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 1 ascending!6220sort = \y0.0 cons = \y0y1.1 descending!6220sort = \y0.0 insert = \y0y1G2G3.1 + 2G3(0,0) insert# = \y0y1G2G3.0 max = \y0y1.3 + 3y0 + 3y1 max# = \y0y1.y0 + y1 min = \y0y1.1 + y0 + y1 min# = \y0y1.y0 + y1 nil = 0 s = \y0.1 + 2y0 sort = \y0G1G2.3 + y0 + 2G2(y0,y0) sort# = \y0G1G2.3 + 2G1(0,0) + 2G2(0,0) Using this interpretation, the requirements translate to: [[max#(s(_x0), s(_x1))]] = 2 + 2x0 + 2x1 > x0 + x1 = [[max#(_x0, _x1)]] [[min#(s(_x0), s(_x1))]] = 2 + 2x0 + 2x1 > x0 + x1 = [[min#(_x0, _x1)]] [[insert#(_x0, cons(_x1, _x2), _F3, _F4)]] = 0 >= 0 = [[insert#(_F4 _x0 _x1, _x2, _F3, _F4)]] [[sort#(cons(_x0, _x1), _F2, _F3)]] = 3 + 2F2(0,0) + 2F3(0,0) > 0 = [[insert#(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[sort#(cons(_x0, _x1), _F2, _F3)]] = 3 + 2F2(0,0) + 2F3(0,0) >= 3 + 2F2(0,0) + 2F3(0,0) = [[sort#(_x1, _F2, _F3)]] [[max(0, _x0)]] = 6 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 6 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 9 + 6x0 + 6x1 >= 7 + 6x0 + 6x1 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 2 + x0 >= 1 = [[0]] [[min(_x0, 0)]] = 2 + x0 >= 1 = [[0]] [[min(s(_x0), s(_x1))]] = 3 + 2x0 + 2x1 >= 3 + 2x0 + 2x1 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 1 + 2F2(0,0) >= 1 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 1 + 2F4(0,0) >= 1 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 3 + 2F1(0,0) >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 4 + 2F3(1,1) >= 1 + 2F3(0,0) = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 12 + 13x0 >= 9 + 13x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 8 + 5x0 >= 5 + 5x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] 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: insert#(X, cons(Y, Z), F, G) =#> insert#(G X Y, Z, F, G) sort#(cons(X, Y), F, G) =#> sort#(Y, F, G) 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: insert#(X, cons(Y, Z), F, G) >? insert#(G X Y, Z, F, G) sort#(cons(X, Y), F, G) >? sort#(Y, F, G) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 0 ascending!6220sort = \y0.0 cons = \y0y1.1 + y1 descending!6220sort = \y0.0 insert = \y0y1G2G3.1 + y1 insert# = \y0y1G2G3.y1 max = \y0y1.3 + 3y0 + 3y1 min = \y0y1.3 nil = 0 s = \y0.0 sort = \y0G1G2.2y0 sort# = \y0G1G2.0 Using this interpretation, the requirements translate to: [[insert#(_x0, cons(_x1, _x2), _F3, _F4)]] = 1 + x2 > x2 = [[insert#(_F4 _x0 _x1, _x2, _F3, _F4)]] [[sort#(cons(_x0, _x1), _F2, _F3)]] = 0 >= 0 = [[sort#(_x1, _F2, _F3)]] [[max(0, _x0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 3 >= 0 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 3 >= 0 = [[0]] [[min(_x0, 0)]] = 3 >= 0 = [[0]] [[min(s(_x0), s(_x1))]] = 3 >= 0 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 1 >= 1 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 2 + x2 >= 2 + x2 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 0 >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 2 + 2x1 >= 1 + 2x1 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 3 + 2x0 >= 2x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 3 + 2x0 >= 2x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] 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: sort#(cons(X, Y), F, G) =#> sort#(Y, F, G) 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: sort#(cons(X, Y), F, G) >? sort#(Y, F, G) max(0, X) >= X max(X, 0) >= X max(s(X), s(Y)) >= s(max(X, Y)) min(0, X) >= 0 min(X, 0) >= 0 min(s(X), s(Y)) >= s(min(X, Y)) insert(X, nil, F, G) >= cons(X, nil) insert(X, cons(Y, Z), F, G) >= cons(F X Y, insert(G X Y, Z, F, G)) sort(nil, F, G) >= nil sort(cons(X, Y), F, G) >= insert(X, sort(Y, F, G), F, G) ascending!6220sort(X) >= sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u)) descending!6220sort(X) >= sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u)) We apply [Kop12, Thm. 6.75] and use the following argument functions: pi( ascending!6220sort(X) ) = #argfun-ascending!6220sort#(sort(X, /\x./\y.min(x, y), /\z./\u.max(z, u))) pi( descending!6220sort(X) ) = #argfun-descending!6220sort#(sort(X, /\x./\y.max(x, y), /\z./\u.min(z, u))) We orient these requirements with a polynomial interpretation in the natural numbers. The following interpretation satisfies the requirements: #argfun-ascending!6220sort# = \y0.3 + y0 #argfun-descending!6220sort# = \y0.3 + y0 0 = 0 ascending!6220sort = \y0.0 cons = \y0y1.1 + y1 descending!6220sort = \y0.0 insert = \y0y1G2G3.1 + y1 max = \y0y1.3 + 3y0 + 3y1 min = \y0y1.3 nil = 0 s = \y0.0 sort = \y0G1G2.2 + 2y0 sort# = \y0G1G2.y0 Using this interpretation, the requirements translate to: [[sort#(cons(_x0, _x1), _F2, _F3)]] = 1 + x1 > x1 = [[sort#(_x1, _F2, _F3)]] [[max(0, _x0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(_x0, 0)]] = 3 + 3x0 >= x0 = [[_x0]] [[max(s(_x0), s(_x1))]] = 3 >= 0 = [[s(max(_x0, _x1))]] [[min(0, _x0)]] = 3 >= 0 = [[0]] [[min(_x0, 0)]] = 3 >= 0 = [[0]] [[min(s(_x0), s(_x1))]] = 3 >= 0 = [[s(min(_x0, _x1))]] [[insert(_x0, nil, _F1, _F2)]] = 1 >= 1 = [[cons(_x0, nil)]] [[insert(_x0, cons(_x1, _x2), _F3, _F4)]] = 2 + x2 >= 2 + x2 = [[cons(_F3 _x0 _x1, insert(_F4 _x0 _x1, _x2, _F3, _F4))]] [[sort(nil, _F0, _F1)]] = 2 >= 0 = [[nil]] [[sort(cons(_x0, _x1), _F2, _F3)]] = 4 + 2x1 >= 3 + 2x1 = [[insert(_x0, sort(_x1, _F2, _F3), _F2, _F3)]] [[#argfun-ascending!6220sort#(sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u)))]] = 5 + 2x0 >= 2 + 2x0 = [[sort(_x0, /\x./\y.min(x, y), /\z./\u.max(z, u))]] [[#argfun-descending!6220sort#(sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u)))]] = 5 + 2x0 >= 2 + 2x0 = [[sort(_x0, /\x./\y.max(x, y), /\z./\u.min(z, u))]] By the observations in [Kop12, Sec. 6.6], this reduction pair suffices; we may thus replace a dependency pair problem (P_3, 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.