The rewrite relation of the following TRS is considered.
-(x,0) | → | x | (1) |
-(0,s(y)) | → | 0 | (2) |
-(s(x),s(y)) | → | -(x,y) | (3) |
lt(x,0) | → | false | (4) |
lt(0,s(y)) | → | true | (5) |
lt(s(x),s(y)) | → | lt(x,y) | (6) |
if(true,x,y) | → | x | (7) |
if(false,x,y) | → | y | (8) |
div(x,0) | → | 0 | (9) |
div(0,y) | → | 0 | (10) |
div(s(x),s(y)) | → | if(lt(x,y),0,s(div(-(x,y),s(y)))) | (11) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
-#(z0,0) |
-#(0,s(z0)) |
-#(s(z0),s(z1)) |
lt#(z0,0) |
lt#(0,s(z0)) |
lt#(s(z0),s(z1)) |
if#(true,z0,z1) |
if#(false,z0,z1) |
div#(z0,0) |
div#(0,z0) |
div#(s(z0),s(z1)) |
div(z0,0) | → | 0 | (28) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 1 + 1 · x1 |
[div(x1, x2)] | = | 1 |
[-(x1, x2)] | = | 1 + 1 · x2 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[-#(x1, x2)] | = | 0 |
[lt#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 1 · x2 + 0 |
[div#(x1, x2)] | = | 1 + 1 · x2 |
[0] | = | 0 |
[false] | = | 1 |
[s(x1)] | = | 0 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 1 + 1 · x1 |
[div(x1, x2)] | = | 1 |
[-(x1, x2)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[-#(x1, x2)] | = | 0 |
[lt#(x1, x2)] | = | 1 |
[if#(x1, x2, x3)] | = | 1 · x2 + 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[0] | = | 0 |
[false] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
-(0,s(z0)) | → | 0 | (14) |
-(s(z0),s(z1)) | → | -(z0,z1) | (16) |
-(z0,0) | → | z0 | (12) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[div(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[-(x1, x2)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[-#(x1, x2)] | = | 0 |
[lt#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[0] | = | 1 |
[false] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
-(0,s(z0)) | → | 0 | (14) |
-(s(z0),s(z1)) | → | -(z0,z1) | (16) |
-(z0,0) | → | z0 | (12) |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[div(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[-(x1, x2)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[-#(x1, x2)] | = | 1 |
[lt#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 0 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[0] | = | 1 |
[false] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
-(0,s(z0)) | → | 0 | (14) |
-(s(z0),s(z1)) | → | -(z0,z1) | (16) |
-(z0,0) | → | z0 | (12) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[div(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[-(x1, x2)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 1 + 1 · x1 + 1 · x2 + 1 · x3 |
[-#(x1, x2)] | = | 0 |
[lt#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 1 |
[div#(x1, x2)] | = | 1 · x1 + 0 |
[0] | = | 1 |
[false] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
-(0,s(z0)) | → | 0 | (14) |
-(s(z0),s(z1)) | → | -(z0,z1) | (16) |
-(z0,0) | → | z0 | (12) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 0 |
[div(x1, x2)] | = | 1 · x1 + 0 |
[-(x1, x2)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 2 · x2 + 0 + 1 · x3 + 1 · x2 · x2 |
[-#(x1, x2)] | = | 0 |
[lt#(x1, x2)] | = | 1 · x1 + 0 |
[if#(x1, x2, x3)] | = | 1 · x2 + 0 + 1 · x3 + 1 · x2 · x2 |
[div#(x1, x2)] | = | 1 · x1 · x1 + 0 |
[0] | = | 0 |
[false] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
-(0,s(z0)) | → | 0 | (14) |
-(s(z0),s(z1)) | → | -(z0,z1) | (16) |
div(s(z0),s(z1)) | → | if(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))) | (32) |
if(true,z0,z1) | → | z0 | (24) |
-(z0,0) | → | z0 | (12) |
div(0,z0) | → | 0 | (30) |
if(false,z0,z1) | → | z1 | (26) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
[c] | = | 0 |
[c1] | = | 0 |
[c2(x1)] | = | 1 · x1 + 0 |
[c3] | = | 0 |
[c4] | = | 0 |
[c5(x1)] | = | 1 · x1 + 0 |
[c6] | = | 0 |
[c7] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1,...,x4)] | = | 1 · x1 + 0 + 1 · x2 + 1 · x3 + 1 · x4 |
[lt(x1, x2)] | = | 0 |
[div(x1, x2)] | = | 0 |
[-(x1, x2)] | = | 1 · x1 + 0 |
[if(x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x2 · x2 |
[-#(x1, x2)] | = | 1 · x1 + 0 |
[lt#(x1, x2)] | = | 0 |
[if#(x1, x2, x3)] | = | 2 · x2 + 0 + 2 · x2 · x2 |
[div#(x1, x2)] | = | 1 · x1 · x1 + 0 |
[0] | = | 0 |
[false] | = | 1 |
[s(x1)] | = | 1 + 1 · x1 |
[true] | = | 1 |
-#(z0,0) | → | c | (13) |
-#(0,s(z0)) | → | c1 | (15) |
-#(s(z0),s(z1)) | → | c2(-#(z0,z1)) | (17) |
lt#(z0,0) | → | c3 | (19) |
lt#(0,s(z0)) | → | c4 | (21) |
lt#(s(z0),s(z1)) | → | c5(lt#(z0,z1)) | (23) |
if#(true,z0,z1) | → | c6 | (25) |
if#(false,z0,z1) | → | c7 | (27) |
div#(z0,0) | → | c8 | (29) |
div#(0,z0) | → | c9 | (31) |
div#(s(z0),s(z1)) | → | c10(if#(lt(z0,z1),0,s(div(-(z0,z1),s(z1)))),lt#(z0,z1),div#(-(z0,z1),s(z1)),-#(z0,z1)) | (33) |
-(0,s(z0)) | → | 0 | (14) |
-(s(z0),s(z1)) | → | -(z0,z1) | (16) |
-(z0,0) | → | z0 | (12) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).