The rewrite relation of the following TRS is considered.
half(0) | → | 0 | (1) |
half(s(0)) | → | 0 | (2) |
half(s(s(x))) | → | s(half(x)) | (3) |
bits(0) | → | 0 | (4) |
bits(s(x)) | → | s(bits(half(s(x)))) | (5) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
half#(0) |
half#(s(0)) |
half#(s(s(z0))) |
bits#(0) |
bits#(s(z0)) |
bits(0) | → | 0 | (4) |
bits(s(z0)) | → | s(bits(half(s(z0)))) | (11) |
bits#(0) | → | c3 | (10) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[half(x1)] | = | 1 + 1 · x1 |
[half#(x1)] | = | 0 |
[bits#(x1)] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
half#(0) | → | c | (6) |
half#(s(0)) | → | c1 | (7) |
half#(s(s(z0))) | → | c2(half#(z0)) | (9) |
bits#(0) | → | c3 | (10) |
bits#(s(z0)) | → | c4(bits#(half(s(z0))),half#(s(z0))) | (12) |
bits#(s(z0)) | → | c4(bits#(half(s(z0))),half#(s(z0))) | (12) |
[c] | = |
|
|||||||||||||||||||||
[c1] | = |
|
|||||||||||||||||||||
[bits#(x1)] | = |
|
|||||||||||||||||||||
[c3] | = |
|
|||||||||||||||||||||
[c4(x1, x2)] | = |
|
|||||||||||||||||||||
[c2(x1)] | = |
|
|||||||||||||||||||||
[half#(x1)] | = |
|
|||||||||||||||||||||
[s(x1)] | = |
|
|||||||||||||||||||||
[half(x1)] | = |
|
|||||||||||||||||||||
[0] | = |
|
half#(0) | → | c | (6) |
half#(s(0)) | → | c1 | (7) |
half#(s(s(z0))) | → | c2(half#(z0)) | (9) |
bits#(0) | → | c3 | (10) |
bits#(s(z0)) | → | c4(bits#(half(s(z0))),half#(s(z0))) | (12) |
half(s(0)) | → | 0 | (2) |
half(s(s(z0))) | → | s(half(z0)) | (8) |
half(0) | → | 0 | (1) |
half#(0) | → | c | (6) |
half#(s(0)) | → | c1 | (7) |
[c] | = |
|
|||||||||||||||||||||
[c1] | = |
|
|||||||||||||||||||||
[bits#(x1)] | = |
|
|||||||||||||||||||||
[c3] | = |
|
|||||||||||||||||||||
[c4(x1, x2)] | = |
|
|||||||||||||||||||||
[c2(x1)] | = |
|
|||||||||||||||||||||
[half#(x1)] | = |
|
|||||||||||||||||||||
[s(x1)] | = |
|
|||||||||||||||||||||
[half(x1)] | = |
|
|||||||||||||||||||||
[0] | = |
|
half#(0) | → | c | (6) |
half#(s(0)) | → | c1 | (7) |
half#(s(s(z0))) | → | c2(half#(z0)) | (9) |
bits#(0) | → | c3 | (10) |
bits#(s(z0)) | → | c4(bits#(half(s(z0))),half#(s(z0))) | (12) |
half(s(0)) | → | 0 | (2) |
half(s(s(z0))) | → | s(half(z0)) | (8) |
half(0) | → | 0 | (1) |
half#(s(s(z0))) | → | c2(half#(z0)) | (9) |
[c] | = |
|
||||||||||||||||||||||||||||||||||||
[c1] | = |
|
||||||||||||||||||||||||||||||||||||
[bits#(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[c3] | = |
|
||||||||||||||||||||||||||||||||||||
[c4(x1, x2)] | = |
|
||||||||||||||||||||||||||||||||||||
[c2(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[half#(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[half(x1)] | = |
|
||||||||||||||||||||||||||||||||||||
[0] | = |
|
half#(0) | → | c | (6) |
half#(s(0)) | → | c1 | (7) |
half#(s(s(z0))) | → | c2(half#(z0)) | (9) |
bits#(0) | → | c3 | (10) |
bits#(s(z0)) | → | c4(bits#(half(s(z0))),half#(s(z0))) | (12) |
half(s(0)) | → | 0 | (2) |
half(s(s(z0))) | → | s(half(z0)) | (8) |
half(0) | → | 0 | (1) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).