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