The relative rewrite relation R/S is considered where R is the following TRS
isort(Cons(x,xs),r) | → | isort(xs,insert(x,r)) | (1) |
isort(Nil,r) | → | Nil | (2) |
insert(S(x),r) | → | insert[Ite](<(S(x),x),S(x),r) | (3) |
inssort(xs) | → | isort(xs,Nil) | (4) |
and S is the following TRS.
<(S(x),S(y)) | → | <(x,y) | (5) |
<(0,S(y)) | → | True | (6) |
<(x,0) | → | False | (7) |
insert[Ite](False,x',Cons(x,xs)) | → | Cons(x,insert(x',xs)) | (8) |
insert[Ite](True,x,r) | → | Cons(x,r) | (9) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
originates from |
|
<#(S(z0),S(z1)) |
<#(0,S(z0)) |
<#(z0,0) |
insert[Ite]#(False,z0,Cons(z1,z2)) |
insert[Ite]#(True,z0,z1) |
isort#(Cons(z0,z1),z2) |
isort#(Nil,z0) |
insert#(S(z0),z1) |
inssort#(z0) |
isort(Cons(z0,z1),z2) | → | isort(z1,insert(z0,z2)) | (10) |
isort(Nil,z0) | → | Nil | (12) |
inssort(z0) | → | isort(z0,Nil) | (16) |
isort#(Nil,z0) | → | c6 | (13) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c6] | = | 0 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c8(x1)] | = | 1 · x1 + 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert[Ite](x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[<(x1, x2)] | = | 1 + 1 · x2 |
[<#(x1, x2)] | = | 0 |
[insert[Ite]#(x1, x2, x3)] | = | 1 · x2 + 0 |
[isort#(x1, x2)] | = | 1 |
[insert#(x1, x2)] | = | 0 |
[inssort#(x1)] | = | 1 |
[S(x1)] | = | 0 |
[0] | = | 1 |
[False] | = | 1 |
[True] | = | 1 |
[Cons(x1, x2)] | = | 1 + 1 · x1 |
[Nil] | = | 1 |
<#(S(z0),S(z1)) | → | c(<#(z0,z1)) | (19) |
<#(0,S(z0)) | → | c1 | (21) |
<#(z0,0) | → | c2 | (23) |
insert[Ite]#(False,z0,Cons(z1,z2)) | → | c3(insert#(z0,z2)) | (25) |
insert[Ite]#(True,z0,z1) | → | c4 | (27) |
isort#(Cons(z0,z1),z2) | → | c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) | (11) |
isort#(Nil,z0) | → | c6 | (13) |
insert#(S(z0),z1) | → | c7(insert[Ite]#(<(S(z0),z0),S(z0),z1),<#(S(z0),z0)) | (15) |
inssort#(z0) | → | c8(isort#(z0,Nil)) | (17) |
inssort#(z0) | → | c8(isort#(z0,Nil)) | (17) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c6] | = | 0 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c8(x1)] | = | 1 · x1 + 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert[Ite](x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[<(x1, x2)] | = | 1 + 1 · x2 |
[<#(x1, x2)] | = | 0 |
[insert[Ite]#(x1, x2, x3)] | = | 1 · x2 + 0 |
[isort#(x1, x2)] | = | 0 |
[insert#(x1, x2)] | = | 0 |
[inssort#(x1)] | = | 1 |
[S(x1)] | = | 0 |
[0] | = | 1 |
[False] | = | 1 |
[True] | = | 1 |
[Cons(x1, x2)] | = | 1 + 1 · x1 |
[Nil] | = | 1 |
<#(S(z0),S(z1)) | → | c(<#(z0,z1)) | (19) |
<#(0,S(z0)) | → | c1 | (21) |
<#(z0,0) | → | c2 | (23) |
insert[Ite]#(False,z0,Cons(z1,z2)) | → | c3(insert#(z0,z2)) | (25) |
insert[Ite]#(True,z0,z1) | → | c4 | (27) |
isort#(Cons(z0,z1),z2) | → | c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) | (11) |
isort#(Nil,z0) | → | c6 | (13) |
insert#(S(z0),z1) | → | c7(insert[Ite]#(<(S(z0),z0),S(z0),z1),<#(S(z0),z0)) | (15) |
inssort#(z0) | → | c8(isort#(z0,Nil)) | (17) |
isort#(Cons(z0,z1),z2) | → | c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) | (11) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c6] | = | 0 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c8(x1)] | = | 1 · x1 + 0 |
[insert(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[insert[Ite](x1, x2, x3)] | = | 1 + 1 · x2 + 1 · x3 |
[<(x1, x2)] | = | 1 + 1 · x2 |
[<#(x1, x2)] | = | 0 |
[insert[Ite]#(x1, x2, x3)] | = | 1 · x2 + 0 |
[isort#(x1, x2)] | = | 1 + 1 · x1 |
[insert#(x1, x2)] | = | 0 |
[inssort#(x1)] | = | 1 + 1 · x1 |
[S(x1)] | = | 0 |
[0] | = | 1 |
[False] | = | 1 |
[True] | = | 1 |
[Cons(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[Nil] | = | 1 |
<#(S(z0),S(z1)) | → | c(<#(z0,z1)) | (19) |
<#(0,S(z0)) | → | c1 | (21) |
<#(z0,0) | → | c2 | (23) |
insert[Ite]#(False,z0,Cons(z1,z2)) | → | c3(insert#(z0,z2)) | (25) |
insert[Ite]#(True,z0,z1) | → | c4 | (27) |
isort#(Cons(z0,z1),z2) | → | c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) | (11) |
isort#(Nil,z0) | → | c6 | (13) |
insert#(S(z0),z1) | → | c7(insert[Ite]#(<(S(z0),z0),S(z0),z1),<#(S(z0),z0)) | (15) |
inssort#(z0) | → | c8(isort#(z0,Nil)) | (17) |
insert#(S(z0),z1) | → | c7(insert[Ite]#(<(S(z0),z0),S(z0),z1),<#(S(z0),z0)) | (15) |
[c(x1)] | = | 1 · x1 + 0 |
[c1] | = | 0 |
[c2] | = | 0 |
[c3(x1)] | = | 1 · x1 + 0 |
[c4] | = | 0 |
[c5(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c6] | = | 0 |
[c7(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[c8(x1)] | = | 1 · x1 + 0 |
[insert(x1, x2)] | = | 2 + 1 · x1 + 1 · x2 |
[insert[Ite](x1, x2, x3)] | = | 2 + 1 · x2 + 1 · x3 |
[<(x1, x2)] | = | 0 |
[<#(x1, x2)] | = | 0 |
[insert[Ite]#(x1, x2, x3)] | = | 2 · x3 + 0 + 1 · x2 · x3 |
[isort#(x1, x2)] | = | 1 · x1 · x2 + 0 + 1 · x1 · x1 |
[insert#(x1, x2)] | = | 2 · x1 + 0 + 2 · x2 + 1 · x1 · x2 |
[inssort#(x1)] | = | 1 + 2 · x1 + 1 · x1 · x1 |
[S(x1)] | = | 2 |
[0] | = | 0 |
[False] | = | 0 |
[True] | = | 0 |
[Cons(x1, x2)] | = | 2 + 1 · x1 + 1 · x2 |
[Nil] | = | 0 |
<#(S(z0),S(z1)) | → | c(<#(z0,z1)) | (19) |
<#(0,S(z0)) | → | c1 | (21) |
<#(z0,0) | → | c2 | (23) |
insert[Ite]#(False,z0,Cons(z1,z2)) | → | c3(insert#(z0,z2)) | (25) |
insert[Ite]#(True,z0,z1) | → | c4 | (27) |
isort#(Cons(z0,z1),z2) | → | c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) | (11) |
isort#(Nil,z0) | → | c6 | (13) |
insert#(S(z0),z1) | → | c7(insert[Ite]#(<(S(z0),z0),S(z0),z1),<#(S(z0),z0)) | (15) |
inssort#(z0) | → | c8(isort#(z0,Nil)) | (17) |
insert[Ite](True,z0,z1) | → | Cons(z0,z1) | (26) |
insert(S(z0),z1) | → | insert[Ite](<(S(z0),z0),S(z0),z1) | (14) |
insert[Ite](False,z0,Cons(z1,z2)) | → | Cons(z1,insert(z0,z2)) | (24) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).