The rewrite relation of the following TRS is considered.
f(0) | → | true | (1) |
f(1) | → | false | (2) |
f(s(x)) | → | f(x) | (3) |
if(true,x,y) | → | x | (4) |
if(false,x,y) | → | y | (5) |
g(s(x),s(y)) | → | if(f(x),s(x),s(y)) | (6) |
g(x,c(y)) | → | g(x,g(s(c(y)),y)) | (7) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
f#(0) |
f#(1) |
f#(s(z0)) |
if#(true,z0,z1) |
if#(false,z0,z1) |
g#(s(z0),s(z1)) |
g#(z0,c(z1)) |
f#(0) | → | c1 | (8) |
f#(1) | → | c2 | (9) |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[f(x1)] | = | 0 |
[if(x1, x2, x3)] | = | 3 |
[g(x1, x2)] | = | 3 |
[f#(x1)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 0 |
[g#(x1, x2)] | = | 2 · x1 + 0 |
[s(x1)] | = | 1 · x1 + 0 |
[c(x1)] | = | 0 |
[0] | = | 3 |
[true] | = | 3 |
[1] | = | 1 |
[false] | = | 3 |
f#(0) | → | c1 | (8) |
f#(1) | → | c2 | (9) |
f#(s(z0)) | → | c3(f#(z0)) | (11) |
if#(true,z0,z1) | → | c4 | (13) |
if#(false,z0,z1) | → | c5 | (15) |
g#(s(z0),s(z1)) | → | c6(if#(f(z0),s(z0),s(z1)),f#(z0)) | (17) |
g#(z0,c(z1)) | → | c7(g#(z0,g(s(c(z1)),z1)),g#(s(c(z1)),z1)) | (19) |
if#(true,z0,z1) | → | c4 | (13) |
if#(false,z0,z1) | → | c5 | (15) |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[f(x1)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[g(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[f#(x1)] | = | 0 |
[if#(x1, x2, x3)] | = | 1 · x1 + 0 |
[g#(x1, x2)] | = | 1 · x1 + 0 |
[s(x1)] | = | 1 · x1 + 0 |
[c(x1)] | = | 0 |
[0] | = | 1 |
[true] | = | 1 |
[1] | = | 1 |
[false] | = | 1 |
f#(0) | → | c1 | (8) |
f#(1) | → | c2 | (9) |
f#(s(z0)) | → | c3(f#(z0)) | (11) |
if#(true,z0,z1) | → | c4 | (13) |
if#(false,z0,z1) | → | c5 | (15) |
g#(s(z0),s(z1)) | → | c6(if#(f(z0),s(z0),s(z1)),f#(z0)) | (17) |
g#(z0,c(z1)) | → | c7(g#(z0,g(s(c(z1)),z1)),g#(s(c(z1)),z1)) | (19) |
f(1) | → | false | (2) |
f(0) | → | true | (1) |
f(s(z0)) | → | f(z0) | (10) |
g#(s(z0),s(z1)) | → | c6(if#(f(z0),s(z0),s(z1)),f#(z0)) | (17) |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[f(x1)] | = | 0 |
[if(x1, x2, x3)] | = | 2 · x2 + 0 + 2 · x3 |
[g(x1, x2)] | = | 0 |
[f#(x1)] | = | 0 |
[if#(x1, x2, x3)] | = | 3 · x2 + 0 + 3 · x3 |
[g#(x1, x2)] | = | 2 + 3 · x1 + 1 · x2 |
[s(x1)] | = | 0 |
[c(x1)] | = | 2 + 1 · x1 |
[0] | = | 3 |
[true] | = | 3 |
[1] | = | 3 |
[false] | = | 3 |
f#(0) | → | c1 | (8) |
f#(1) | → | c2 | (9) |
f#(s(z0)) | → | c3(f#(z0)) | (11) |
if#(true,z0,z1) | → | c4 | (13) |
if#(false,z0,z1) | → | c5 | (15) |
g#(s(z0),s(z1)) | → | c6(if#(f(z0),s(z0),s(z1)),f#(z0)) | (17) |
g#(z0,c(z1)) | → | c7(g#(z0,g(s(c(z1)),z1)),g#(s(c(z1)),z1)) | (19) |
g(s(z0),s(z1)) | → | if(f(z0),s(z0),s(z1)) | (16) |
if(true,z0,z1) | → | z0 | (12) |
g(z0,c(z1)) | → | g(z0,g(s(c(z1)),z1)) | (18) |
if(false,z0,z1) | → | z1 | (14) |
g#(z0,c(z1)) | → | c7(g#(z0,g(s(c(z1)),z1)),g#(s(c(z1)),z1)) | (19) |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5] | = | 0 |
[c6(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[f(x1)] | = | 1 |
[if(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 |
[g(x1, x2)] | = | 0 |
[f#(x1)] | = | 0 |
[if#(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 |
[g#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[s(x1)] | = | 0 |
[c(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
[true] | = | 1 |
[1] | = | 1 |
[false] | = | 1 |
f#(0) | → | c1 | (8) |
f#(1) | → | c2 | (9) |
f#(s(z0)) | → | c3(f#(z0)) | (11) |
if#(true,z0,z1) | → | c4 | (13) |
if#(false,z0,z1) | → | c5 | (15) |
g#(s(z0),s(z1)) | → | c6(if#(f(z0),s(z0),s(z1)),f#(z0)) | (17) |
g#(z0,c(z1)) | → | c7(g#(z0,g(s(c(z1)),z1)),g#(s(c(z1)),z1)) | (19) |
g(s(z0),s(z1)) | → | if(f(z0),s(z0),s(z1)) | (16) |
if(true,z0,z1) | → | z0 | (12) |
g(z0,c(z1)) | → | g(z0,g(s(c(z1)),z1)) | (18) |
if(false,z0,z1) | → | z1 | (14) |
f#(s(z0)) | → | c3(f#(z0)) | (11) |
[g#(x1, x2)] | = |
|
||||||||||||||||||||||||||||
[c1] | = |
|
||||||||||||||||||||||||||||
[c5] | = |
|
||||||||||||||||||||||||||||
[c6(x1, x2)] | = |
|
||||||||||||||||||||||||||||
[c3(x1)] | = |
|
||||||||||||||||||||||||||||
[if#(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||
[c4] | = |
|
||||||||||||||||||||||||||||
[f#(x1)] | = |
|
||||||||||||||||||||||||||||
[c2] | = |
|
||||||||||||||||||||||||||||
[c7(x1, x2)] | = |
|
||||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||||
[true] | = |
|
||||||||||||||||||||||||||||
[c(x1)] | = |
|
||||||||||||||||||||||||||||
[f(x1)] | = |
|
||||||||||||||||||||||||||||
[if(x1, x2, x3)] | = |
|
||||||||||||||||||||||||||||
[0] | = |
|
||||||||||||||||||||||||||||
[1] | = |
|
||||||||||||||||||||||||||||
[g(x1, x2)] | = |
|
||||||||||||||||||||||||||||
[false] | = |
|
f#(0) | → | c1 | (8) |
f#(1) | → | c2 | (9) |
f#(s(z0)) | → | c3(f#(z0)) | (11) |
if#(true,z0,z1) | → | c4 | (13) |
if#(false,z0,z1) | → | c5 | (15) |
g#(s(z0),s(z1)) | → | c6(if#(f(z0),s(z0),s(z1)),f#(z0)) | (17) |
g#(z0,c(z1)) | → | c7(g#(z0,g(s(c(z1)),z1)),g#(s(c(z1)),z1)) | (19) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).