and S is the following TRS.
isort#(Cons(z0,z1),z2) |
→ |
c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) |
(12) |
|
originates from |
isort(Cons(z0,z1),z2) |
→ |
isort(z1,insert(z0,z2)) |
(11) |
|
|
originates from |
|
insert#(z0,Cons(z1,z2)) |
→ |
c7(insert[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) |
(16) |
|
originates from |
insert(z0,Cons(z1,z2)) |
→ |
insert[Ite][False][Ite](<(z0,z1),z0,Cons(z1,z2)) |
(15) |
|
insert#(z0,Nil) |
→ |
c8 |
(18) |
|
originates from |
insert(z0,Nil) |
→ |
Cons(z0,Nil) |
(17) |
|
inssort#(z0) |
→ |
c9(isort#(z0,Nil)) |
(20) |
|
originates from |
inssort(z0) |
→ |
isort(z0,Nil) |
(19) |
|
<#(S(z0),S(z1)) |
→ |
c(<#(z0,z1)) |
(22) |
|
originates from |
<(S(z0),S(z1)) |
→ |
<(z0,z1) |
(21) |
|
|
originates from |
|
|
originates from |
|
insert[Ite][False][Ite]#(False,z0,Cons(z1,z2)) |
→ |
c3(insert#(z0,z2)) |
(28) |
|
originates from |
insert[Ite][False][Ite](False,z0,Cons(z1,z2)) |
→ |
Cons(z1,insert(z0,z2)) |
(27) |
|
insert[Ite][False][Ite]#(True,z0,z1) |
→ |
c4 |
(30) |
|
originates from |
insert[Ite][False][Ite](True,z0,z1) |
→ |
Cons(z0,z1) |
(29) |
|
Moreover, we add the following terms to the innermost strategy.
<#(S(z0),S(z1)) |
→ |
c(<#(z0,z1)) |
(22) |
<#(0,S(z0)) |
→ |
c1 |
(24) |
<#(z0,0) |
→ |
c2 |
(26) |
insert[Ite][False][Ite]#(False,z0,Cons(z1,z2)) |
→ |
c3(insert#(z0,z2)) |
(28) |
insert[Ite][False][Ite]#(True,z0,z1) |
→ |
c4 |
(30) |
isort#(Cons(z0,z1),z2) |
→ |
c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) |
(12) |
isort#(Nil,z0) |
→ |
c6 |
(14) |
insert#(z0,Cons(z1,z2)) |
→ |
c7(insert[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) |
(16) |
insert#(z0,Nil) |
→ |
c8 |
(18) |
inssort#(z0) |
→ |
c9(isort#(z0,Nil)) |
(20) |
<#(S(z0),S(z1)) |
→ |
c(<#(z0,z1)) |
(22) |
<#(0,S(z0)) |
→ |
c1 |
(24) |
<#(z0,0) |
→ |
c2 |
(26) |
insert[Ite][False][Ite]#(False,z0,Cons(z1,z2)) |
→ |
c3(insert#(z0,z2)) |
(28) |
insert[Ite][False][Ite]#(True,z0,z1) |
→ |
c4 |
(30) |
isort#(Cons(z0,z1),z2) |
→ |
c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) |
(12) |
isort#(Nil,z0) |
→ |
c6 |
(14) |
insert#(z0,Cons(z1,z2)) |
→ |
c7(insert[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) |
(16) |
insert#(z0,Nil) |
→ |
c8 |
(18) |
inssort#(z0) |
→ |
c9(isort#(z0,Nil)) |
(20) |
<#(S(z0),S(z1)) |
→ |
c(<#(z0,z1)) |
(22) |
<#(0,S(z0)) |
→ |
c1 |
(24) |
<#(z0,0) |
→ |
c2 |
(26) |
insert[Ite][False][Ite]#(False,z0,Cons(z1,z2)) |
→ |
c3(insert#(z0,z2)) |
(28) |
insert[Ite][False][Ite]#(True,z0,z1) |
→ |
c4 |
(30) |
isort#(Cons(z0,z1),z2) |
→ |
c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) |
(12) |
isort#(Nil,z0) |
→ |
c6 |
(14) |
insert#(z0,Cons(z1,z2)) |
→ |
c7(insert[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) |
(16) |
insert#(z0,Nil) |
→ |
c8 |
(18) |
inssort#(z0) |
→ |
c9(isort#(z0,Nil)) |
(20) |
<#(S(z0),S(z1)) |
→ |
c(<#(z0,z1)) |
(22) |
<#(0,S(z0)) |
→ |
c1 |
(24) |
<#(z0,0) |
→ |
c2 |
(26) |
insert[Ite][False][Ite]#(False,z0,Cons(z1,z2)) |
→ |
c3(insert#(z0,z2)) |
(28) |
insert[Ite][False][Ite]#(True,z0,z1) |
→ |
c4 |
(30) |
isort#(Cons(z0,z1),z2) |
→ |
c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) |
(12) |
isort#(Nil,z0) |
→ |
c6 |
(14) |
insert#(z0,Cons(z1,z2)) |
→ |
c7(insert[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) |
(16) |
insert#(z0,Nil) |
→ |
c8 |
(18) |
inssort#(z0) |
→ |
c9(isort#(z0,Nil)) |
(20) |
<(z0,0) |
→ |
False |
(25) |
<(0,S(z0)) |
→ |
True |
(23) |
<(S(z0),S(z1)) |
→ |
<(z0,z1) |
(21) |
<#(S(z0),S(z1)) |
→ |
c(<#(z0,z1)) |
(22) |
<#(0,S(z0)) |
→ |
c1 |
(24) |
<#(z0,0) |
→ |
c2 |
(26) |
insert[Ite][False][Ite]#(False,z0,Cons(z1,z2)) |
→ |
c3(insert#(z0,z2)) |
(28) |
insert[Ite][False][Ite]#(True,z0,z1) |
→ |
c4 |
(30) |
isort#(Cons(z0,z1),z2) |
→ |
c5(isort#(z1,insert(z0,z2)),insert#(z0,z2)) |
(12) |
isort#(Nil,z0) |
→ |
c6 |
(14) |
insert#(z0,Cons(z1,z2)) |
→ |
c7(insert[Ite][False][Ite]#(<(z0,z1),z0,Cons(z1,z2)),<#(z0,z1)) |
(16) |
insert#(z0,Nil) |
→ |
c8 |
(18) |
inssort#(z0) |
→ |
c9(isort#(z0,Nil)) |
(20) |
insert(z0,Cons(z1,z2)) |
→ |
insert[Ite][False][Ite](<(z0,z1),z0,Cons(z1,z2)) |
(15) |
insert[Ite][False][Ite](False,z0,Cons(z1,z2)) |
→ |
Cons(z1,insert(z0,z2)) |
(27) |
insert(z0,Nil) |
→ |
Cons(z0,Nil) |
(17) |
insert[Ite][False][Ite](True,z0,z1) |
→ |
Cons(z0,z1) |
(29) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).