The rewrite relation of the following TRS is considered.
minus(0,Y) | → | 0 | (1) |
minus(s(X),s(Y)) | → | minus(X,Y) | (2) |
geq(X,0) | → | true | (3) |
geq(0,s(Y)) | → | false | (4) |
geq(s(X),s(Y)) | → | geq(X,Y) | (5) |
div(0,s(Y)) | → | 0 | (6) |
div(s(X),s(Y)) | → | if(geq(X,Y),s(div(minus(X,Y),s(Y))),0) | (7) |
if(true,X,Y) | → | X | (8) |
if(false,X,Y) | → | Y | (9) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
minus#(0,z0) |
minus#(s(z0),s(z1)) |
geq#(z0,0) |
geq#(0,s(z0)) |
geq#(s(z0),s(z1)) |
div#(0,s(z0)) |
div#(s(z0),s(z1)) |
if#(true,z0,z1) |
if#(false,z0,z1) |
div#(0,s(z0)) | → | c5 | (21) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c7] | = | 0 |
[c8] | = | 0 |
[minus(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 0 |
[div(x1, x2)] | = | 1 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[minus#(x1, x2)] | = | 0 |
[geq#(x1, x2)] | = | 0 |
[div#(x1, x2)] | = | 1 + 1 · x2 |
[if#(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 |
[0] | = | 0 |
[true] | = | 1 |
[s(x1)] | = | 0 |
[false] | = | 1 |
minus#(0,z0) | → | c | (11) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(0,s(z0)) | → | c5 | (21) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c7] | = | 0 |
[c8] | = | 0 |
[minus(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 0 |
[div(x1, x2)] | = | 1 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[minus#(x1, x2)] | = | 0 |
[geq#(x1, x2)] | = | 1 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 1 · x3 + 0 |
[0] | = | 0 |
[true] | = | 1 |
[s(x1)] | = | 1 |
[false] | = | 1 |
minus#(0,z0) | → | c | (11) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(0,s(z0)) | → | c5 | (21) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
minus(s(z0),s(z1)) | → | minus(z0,z1) | (12) |
minus(0,z0) | → | 0 | (10) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c7] | = | 0 |
[c8] | = | 0 |
[minus(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 1 · x1 + 0 |
[div(x1, x2)] | = | 1 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[minus#(x1, x2)] | = | 0 |
[geq#(x1, x2)] | = | 1 · x1 + 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 1 · x3 + 0 |
[0] | = | 0 |
[true] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[false] | = | 1 |
minus#(0,z0) | → | c | (11) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(0,s(z0)) | → | c5 | (21) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
minus(s(z0),s(z1)) | → | minus(z0,z1) | (12) |
minus(0,z0) | → | 0 | (10) |
minus#(0,z0) | → | c | (11) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c7] | = | 0 |
[c8] | = | 0 |
[minus(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 1 · x1 + 0 |
[div(x1, x2)] | = | 1 + 1 · x1 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[minus#(x1, x2)] | = | 1 |
[geq#(x1, x2)] | = | 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 1 · x3 + 0 |
[0] | = | 0 |
[true] | = | 1 |
[s(x1)] | = | 1 |
[false] | = | 1 |
minus#(0,z0) | → | c | (11) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(0,s(z0)) | → | c5 | (21) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
minus(s(z0),s(z1)) | → | minus(z0,z1) | (12) |
minus(0,z0) | → | 0 | (10) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c7] | = | 0 |
[c8] | = | 0 |
[minus(x1, x2)] | = | 0 |
[geq(x1, x2)] | = | 0 |
[div(x1, x2)] | = | 1 + 1 · x1 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[minus#(x1, x2)] | = | 0 |
[geq#(x1, x2)] | = | 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 1 + 1 · x3 |
[0] | = | 0 |
[true] | = | 0 |
[s(x1)] | = | 1 |
[false] | = | 0 |
minus#(0,z0) | → | c | (11) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(0,s(z0)) | → | c5 | (21) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
minus(s(z0),s(z1)) | → | minus(z0,z1) | (12) |
minus(0,z0) | → | 0 | (10) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
[c] | = | 0 |
[c1(x1)] | = | 1 · x1 + 0 |
[c2] | = | 0 |
[c3] | = | 0 |
[c4(x1)] | = | 1 · x1 + 0 |
[c5] | = | 0 |
[c6(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[c7] | = | 0 |
[c8] | = | 0 |
[minus(x1, x2)] | = | 1 |
[geq(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[div(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[minus#(x1, x2)] | = | 1 · x1 + 0 |
[geq#(x1, x2)] | = | 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 0 |
[0] | = | 1 |
[true] | = | 0 |
[s(x1)] | = | 1 + 1 · x1 |
[false] | = | 1 |
minus#(0,z0) | → | c | (11) |
minus#(s(z0),s(z1)) | → | c1(minus#(z0,z1)) | (13) |
geq#(z0,0) | → | c2 | (15) |
geq#(0,s(z0)) | → | c3 | (17) |
geq#(s(z0),s(z1)) | → | c4(geq#(z0,z1)) | (19) |
div#(0,s(z0)) | → | c5 | (21) |
div#(s(z0),s(z1)) | → | c6(if#(geq(z0,z1),s(div(minus(z0,z1),s(z1))),0),geq#(z0,z1),div#(minus(z0,z1),s(z1)),minus#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c7 | (25) |
if#(false,z0,z1) | → | c8 | (27) |
minus(s(z0),s(z1)) | → | minus(z0,z1) | (12) |
minus(0,z0) | → | 0 | (10) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).