The relative rewrite relation R/S is considered where R is the following TRS
ordered(Cons(x',Cons(x,xs))) | → | ordered[Ite](<(x',x),Cons(x',Cons(x,xs))) | (1) |
ordered(Cons(x,Nil)) | → | True | (2) |
ordered(Nil) | → | True | (3) |
notEmpty(Cons(x,xs)) | → | True | (4) |
notEmpty(Nil) | → | False | (5) |
goal(xs) | → | ordered(xs) | (6) |
and S is the following TRS.
<(S(x),S(y)) | → | <(x,y) | (7) |
<(0,S(y)) | → | True | (8) |
<(x,0) | → | False | (9) |
ordered[Ite](True,Cons(x,xs)) | → | ordered(xs) | (10) |
ordered[Ite](False,xs) | → | False | (11) |
|
originates from |
|
||||||||
|
originates from |
|
||||||||
|
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) |
ordered[Ite]#(True,Cons(z0,z1)) |
ordered[Ite]#(False,z0) |
ordered#(Cons(z0,Cons(z1,z2))) |
ordered#(Cons(z0,Nil)) |
ordered#(Nil) |
notEmpty#(Cons(z0,z1)) |
notEmpty#(Nil) |
goal#(z0) |
ordered[Ite](True,Cons(z0,z1)) | → | ordered(z1) | (28) |
ordered[Ite](False,z0) | → | False | (30) |
ordered(Cons(z0,Cons(z1,z2))) | → | ordered[Ite](<(z0,z1),Cons(z0,Cons(z1,z2))) | (12) |
ordered(Cons(z0,Nil)) | → | True | (14) |
ordered(Nil) | → | True | (3) |
notEmpty(Cons(z0,z1)) | → | True | (17) |
notEmpty(Nil) | → | False | (5) |
goal(z0) | → | ordered(z0) | (20) |
ordered#(Cons(z0,Nil)) | → | c6 | (15) |
ordered#(Nil) | → | c7 | (16) |
notEmpty#(Cons(z0,z1)) | → | c8 | (18) |
notEmpty#(Nil) | → | c9 | (19) |
goal#(z0) | → | c10(ordered#(z0)) | (21) |
[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] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1)] | = | 1 · x1 + 0 |
[<(x1, x2)] | = | 0 |
[<#(x1, x2)] | = | 0 |
[ordered[Ite]#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[ordered#(x1)] | = | 1 · x1 + 0 |
[notEmpty#(x1)] | = | 1 + 1 · x1 |
[goal#(x1)] | = | 1 + 1 · x1 |
[S(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
[True] | = | 0 |
[False] | = | 0 |
[Cons(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[Nil] | = | 1 |
<#(S(z0),S(z1)) | → | c(<#(z0,z1)) | (23) |
<#(0,S(z0)) | → | c1 | (25) |
<#(z0,0) | → | c2 | (27) |
ordered[Ite]#(True,Cons(z0,z1)) | → | c3(ordered#(z1)) | (29) |
ordered[Ite]#(False,z0) | → | c4 | (31) |
ordered#(Cons(z0,Cons(z1,z2))) | → | c5(ordered[Ite]#(<(z0,z1),Cons(z0,Cons(z1,z2))),<#(z0,z1)) | (13) |
ordered#(Cons(z0,Nil)) | → | c6 | (15) |
ordered#(Nil) | → | c7 | (16) |
notEmpty#(Cons(z0,z1)) | → | c8 | (18) |
notEmpty#(Nil) | → | c9 | (19) |
goal#(z0) | → | c10(ordered#(z0)) | (21) |
<(z0,0) | → | False | (26) |
<(0,S(z0)) | → | True | (24) |
<(S(z0),S(z1)) | → | <(z0,z1) | (22) |
ordered#(Cons(z0,Cons(z1,z2))) | → | c5(ordered[Ite]#(<(z0,z1),Cons(z0,Cons(z1,z2))),<#(z0,z1)) | (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] | = | 0 |
[c8] | = | 0 |
[c9] | = | 0 |
[c10(x1)] | = | 1 · x1 + 0 |
[<(x1, x2)] | = | 0 |
[<#(x1, x2)] | = | 0 |
[ordered[Ite]#(x1, x2)] | = | 1 · x1 + 0 + 1 · x2 |
[ordered#(x1)] | = | 1 + 1 · x1 |
[notEmpty#(x1)] | = | 0 |
[goal#(x1)] | = | 1 + 1 · x1 |
[S(x1)] | = | 1 + 1 · x1 |
[0] | = | 1 |
[True] | = | 0 |
[False] | = | 0 |
[Cons(x1, x2)] | = | 1 + 1 · x1 + 1 · x2 |
[Nil] | = | 0 |
<#(S(z0),S(z1)) | → | c(<#(z0,z1)) | (23) |
<#(0,S(z0)) | → | c1 | (25) |
<#(z0,0) | → | c2 | (27) |
ordered[Ite]#(True,Cons(z0,z1)) | → | c3(ordered#(z1)) | (29) |
ordered[Ite]#(False,z0) | → | c4 | (31) |
ordered#(Cons(z0,Cons(z1,z2))) | → | c5(ordered[Ite]#(<(z0,z1),Cons(z0,Cons(z1,z2))),<#(z0,z1)) | (13) |
ordered#(Cons(z0,Nil)) | → | c6 | (15) |
ordered#(Nil) | → | c7 | (16) |
notEmpty#(Cons(z0,z1)) | → | c8 | (18) |
notEmpty#(Nil) | → | c9 | (19) |
goal#(z0) | → | c10(ordered#(z0)) | (21) |
<(z0,0) | → | False | (26) |
<(0,S(z0)) | → | True | (24) |
<(S(z0),S(z1)) | → | <(z0,z1) | (22) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).