The rewrite relation of the following TRS is considered.
minus_active#(0,z0) |
→ |
c |
(21) |
|
originates from |
minus_active(0,z0) |
→ |
0 |
(20) |
|
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
|
originates from |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
|
minus_active#(z0,z1) |
→ |
c2 |
(25) |
|
originates from |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
|
|
originates from |
|
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
|
originates from |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
|
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
|
originates from |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
|
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
|
originates from |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
|
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
|
originates from |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
|
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
|
originates from |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
|
ge_active#(z0,0) |
→ |
c9 |
(38) |
|
originates from |
ge_active(z0,0) |
→ |
true |
(37) |
|
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
|
originates from |
ge_active(0,s(z0)) |
→ |
false |
(39) |
|
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
|
originates from |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
|
ge_active#(z0,z1) |
→ |
c12 |
(44) |
|
originates from |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
|
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
|
originates from |
div_active(0,s(z0)) |
→ |
0 |
(45) |
|
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
|
originates from |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
|
div_active#(z0,z1) |
→ |
c15 |
(50) |
|
originates from |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
|
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
|
originates from |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
|
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
|
originates from |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
|
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
|
originates from |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
|
Moreover, we add the following terms to the innermost strategy.
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
[c] |
= |
|
[c1(x1)] |
= |
+ · x1
|
[c12] |
= |
|
[mark#(x1)] |
= |
+ · x1
|
[c8(x1, x2)] |
= |
+ · x1 + · x2
|
[c14(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active#(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[c5(x1)] |
= |
+ · x1
|
[c16(x1)] |
= |
+ · x1
|
[c17(x1)] |
= |
+ · x1
|
[c6(x1)] |
= |
+ · x1
|
[ge_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c2] |
= |
|
[c9] |
= |
|
[c10] |
= |
|
[c13] |
= |
|
[c11(x1)] |
= |
+ · x1
|
[div_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c3] |
= |
|
[c4(x1)] |
= |
+ · x1
|
[c18] |
= |
|
[minus_active#(x1, x2)] |
= |
+ · x1 + · x2
|
[c7(x1, x2)] |
= |
+ · x1 + · x2
|
[c15] |
= |
|
[true] |
= |
|
[minus_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[ge(x1, x2)] |
= |
+ · x1 + · x2
|
[ge_active(x1, x2)] |
= |
+ · x1 + · x2
|
[if_active(x1, x2, x3)] |
= |
+ · x1 + · x2 + · x3
|
[false] |
= |
|
[s(x1)] |
= |
+ · x1
|
[div(x1, x2)] |
= |
+ · x1 + · x2
|
[0] |
= |
|
[minus(x1, x2)] |
= |
+ · x1 + · x2
|
[div_active(x1, x2)] |
= |
+ · x1 + · x2
|
[mark(x1)] |
= |
+ · x1
|
which has the intended complexity.
Here, only the following usable rules have been considered:
minus_active#(0,z0) |
→ |
c |
(21) |
minus_active#(s(z0),s(z1)) |
→ |
c1(minus_active#(z0,z1)) |
(23) |
minus_active#(z0,z1) |
→ |
c2 |
(25) |
mark#(0) |
→ |
c3 |
(26) |
mark#(s(z0)) |
→ |
c4(mark#(z0)) |
(28) |
mark#(minus(z0,z1)) |
→ |
c5(minus_active#(z0,z1)) |
(30) |
mark#(ge(z0,z1)) |
→ |
c6(ge_active#(z0,z1)) |
(32) |
mark#(div(z0,z1)) |
→ |
c7(div_active#(mark(z0),z1),mark#(z0)) |
(34) |
mark#(if(z0,z1,z2)) |
→ |
c8(if_active#(mark(z0),z1,z2),mark#(z0)) |
(36) |
ge_active#(z0,0) |
→ |
c9 |
(38) |
ge_active#(0,s(z0)) |
→ |
c10 |
(40) |
ge_active#(s(z0),s(z1)) |
→ |
c11(ge_active#(z0,z1)) |
(42) |
ge_active#(z0,z1) |
→ |
c12 |
(44) |
div_active#(0,s(z0)) |
→ |
c13 |
(46) |
div_active#(s(z0),s(z1)) |
→ |
c14(if_active#(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0),ge_active#(z0,z1)) |
(48) |
div_active#(z0,z1) |
→ |
c15 |
(50) |
if_active#(true,z0,z1) |
→ |
c16(mark#(z0)) |
(52) |
if_active#(false,z0,z1) |
→ |
c17(mark#(z1)) |
(54) |
if_active#(z0,z1,z2) |
→ |
c18 |
(56) |
if_active(false,z0,z1) |
→ |
mark(z1) |
(53) |
ge_active(s(z0),s(z1)) |
→ |
ge_active(z0,z1) |
(41) |
minus_active(z0,z1) |
→ |
minus(z0,z1) |
(24) |
ge_active(z0,0) |
→ |
true |
(37) |
mark(0) |
→ |
0 |
(2) |
mark(if(z0,z1,z2)) |
→ |
if_active(mark(z0),z1,z2) |
(35) |
ge_active(0,s(z0)) |
→ |
false |
(39) |
minus_active(0,z0) |
→ |
0 |
(20) |
mark(s(z0)) |
→ |
s(mark(z0)) |
(27) |
ge_active(z0,z1) |
→ |
ge(z0,z1) |
(43) |
div_active(0,s(z0)) |
→ |
0 |
(45) |
div_active(s(z0),s(z1)) |
→ |
if_active(ge_active(z0,z1),s(div(minus(z0,z1),s(z1))),0) |
(47) |
div_active(z0,z1) |
→ |
div(z0,z1) |
(49) |
mark(minus(z0,z1)) |
→ |
minus_active(z0,z1) |
(29) |
mark(ge(z0,z1)) |
→ |
ge_active(z0,z1) |
(31) |
mark(div(z0,z1)) |
→ |
div_active(mark(z0),z1) |
(33) |
if_active(z0,z1,z2) |
→ |
if(z0,z1,z2) |
(55) |
minus_active(s(z0),s(z1)) |
→ |
minus_active(z0,z1) |
(22) |
if_active(true,z0,z1) |
→ |
mark(z0) |
(51) |
There are no rules in the TRS R. Hence, R/S has complexity O(1).