The rewrite relation of the following TRS is considered.
|
originates from |
|
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
|
originates from |
sort#2(Cons(z0,z1)) |
→ |
insert#3(z0,sort#2(z1)) |
(12) |
|
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
|
originates from |
cond_insert_ord_x_ys_1(True,z0,z1,z2) |
→ |
Cons(z0,Cons(z1,z2)) |
(14) |
|
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
|
originates from |
cond_insert_ord_x_ys_1(False,z0,z1,z2) |
→ |
Cons(z1,insert#3(z0,z2)) |
(16) |
|
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
|
originates from |
insert#3(z0,Nil) |
→ |
Cons(z0,Nil) |
(18) |
|
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
|
originates from |
insert#3(z0,Cons(z1,z2)) |
→ |
cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) |
(20) |
|
|
originates from |
|
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
|
originates from |
leq#2(S(z0),0) |
→ |
False |
(24) |
|
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
|
originates from |
leq#2(S(z0),S(z1)) |
→ |
leq#2(z0,z1) |
(26) |
|
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
|
originates from |
main(z0) |
→ |
sort#2(z0) |
(28) |
|
Moreover, we add the following terms to the innermost strategy.
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
leq#2(0,z0) |
→ |
True |
(22) |
leq#2(S(z0),0) |
→ |
False |
(24) |
leq#2(S(z0),S(z1)) |
→ |
leq#2(z0,z1) |
(26) |
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
insert#3(z0,Nil) |
→ |
Cons(z0,Nil) |
(18) |
cond_insert_ord_x_ys_1(True,z0,z1,z2) |
→ |
Cons(z0,Cons(z1,z2)) |
(14) |
cond_insert_ord_x_ys_1(False,z0,z1,z2) |
→ |
Cons(z1,insert#3(z0,z2)) |
(16) |
sort#2(Cons(z0,z1)) |
→ |
insert#3(z0,sort#2(z1)) |
(12) |
sort#2(Nil) |
→ |
Nil |
(1) |
insert#3(z0,Cons(z1,z2)) |
→ |
cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) |
(20) |
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
insert#3(z0,Nil) |
→ |
Cons(z0,Nil) |
(18) |
cond_insert_ord_x_ys_1(True,z0,z1,z2) |
→ |
Cons(z0,Cons(z1,z2)) |
(14) |
cond_insert_ord_x_ys_1(False,z0,z1,z2) |
→ |
Cons(z1,insert#3(z0,z2)) |
(16) |
sort#2(Cons(z0,z1)) |
→ |
insert#3(z0,sort#2(z1)) |
(12) |
sort#2(Nil) |
→ |
Nil |
(1) |
insert#3(z0,Cons(z1,z2)) |
→ |
cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) |
(20) |
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
insert#3(z0,Nil) |
→ |
Cons(z0,Nil) |
(18) |
cond_insert_ord_x_ys_1(True,z0,z1,z2) |
→ |
Cons(z0,Cons(z1,z2)) |
(14) |
cond_insert_ord_x_ys_1(False,z0,z1,z2) |
→ |
Cons(z1,insert#3(z0,z2)) |
(16) |
sort#2(Cons(z0,z1)) |
→ |
insert#3(z0,sort#2(z1)) |
(12) |
sort#2(Nil) |
→ |
Nil |
(1) |
insert#3(z0,Cons(z1,z2)) |
→ |
cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) |
(20) |
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
insert#3(z0,Nil) |
→ |
Cons(z0,Nil) |
(18) |
cond_insert_ord_x_ys_1(True,z0,z1,z2) |
→ |
Cons(z0,Cons(z1,z2)) |
(14) |
cond_insert_ord_x_ys_1(False,z0,z1,z2) |
→ |
Cons(z1,insert#3(z0,z2)) |
(16) |
sort#2(Cons(z0,z1)) |
→ |
insert#3(z0,sort#2(z1)) |
(12) |
sort#2(Nil) |
→ |
Nil |
(1) |
insert#3(z0,Cons(z1,z2)) |
→ |
cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) |
(20) |
sort#2#(Nil) |
→ |
c |
(11) |
sort#2#(Cons(z0,z1)) |
→ |
c1(insert#3#(z0,sort#2(z1)),sort#2#(z1)) |
(13) |
cond_insert_ord_x_ys_1#(True,z0,z1,z2) |
→ |
c2 |
(15) |
cond_insert_ord_x_ys_1#(False,z0,z1,z2) |
→ |
c3(insert#3#(z0,z2)) |
(17) |
insert#3#(z0,Nil) |
→ |
c4 |
(19) |
insert#3#(z0,Cons(z1,z2)) |
→ |
c5(cond_insert_ord_x_ys_1#(leq#2(z0,z1),z0,z1,z2),leq#2#(z0,z1)) |
(21) |
leq#2#(0,z0) |
→ |
c6 |
(23) |
leq#2#(S(z0),0) |
→ |
c7 |
(25) |
leq#2#(S(z0),S(z1)) |
→ |
c8(leq#2#(z0,z1)) |
(27) |
main#(z0) |
→ |
c9(sort#2#(z0)) |
(29) |
insert#3(z0,Nil) |
→ |
Cons(z0,Nil) |
(18) |
leq#2(0,z0) |
→ |
True |
(22) |
cond_insert_ord_x_ys_1(True,z0,z1,z2) |
→ |
Cons(z0,Cons(z1,z2)) |
(14) |
cond_insert_ord_x_ys_1(False,z0,z1,z2) |
→ |
Cons(z1,insert#3(z0,z2)) |
(16) |
sort#2(Cons(z0,z1)) |
→ |
insert#3(z0,sort#2(z1)) |
(12) |
leq#2(S(z0),0) |
→ |
False |
(24) |
leq#2(S(z0),S(z1)) |
→ |
leq#2(z0,z1) |
(26) |
sort#2(Nil) |
→ |
Nil |
(1) |
insert#3(z0,Cons(z1,z2)) |
→ |
cond_insert_ord_x_ys_1(leq#2(z0,z1),z0,z1,z2) |
(20) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).