half(0) -> 0

half(s(0)) -> 0

half(s(s(

bits(0) -> 0

bits(s(

TRS

↳Removing Redundant Rules

Removing the following rules from

bits(0) -> 0

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(bits(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(half(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

TRS

↳RRRPolo

→TRS2

↳Dependency Pair Analysis

HALF(s(s(x))) -> HALF(x)

BITS(s(x)) -> BITS(half(s(x)))

BITS(s(x)) -> HALF(s(x))

Furthermore,

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳Non-Overlappingness Check

→DP Problem 2

↳NOC

**HALF(s(s( x))) -> HALF(x)**

half(0) -> 0

half(s(0)) -> 0

half(s(s(x))) -> s(half(x))

bits(s(x)) -> s(bits(half(s(x))))

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.

The transformation is resulting in one subcycle:

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

...

→DP Problem 3

↳Usable Rules (Innermost)

→DP Problem 2

↳NOC

**HALF(s(s( x))) -> HALF(x)**

half(0) -> 0

half(s(0)) -> 0

half(s(s(x))) -> s(half(x))

bits(s(x)) -> s(bits(half(s(x))))

innermost

As we are in the innermost case, we can delete all 4 non-usable-rules.

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

...

→DP Problem 4

↳Modular Removal of Rules

→DP Problem 2

↳NOC

**HALF(s(s( x))) -> HALF(x)**

none

innermost

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(HALF(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {HALF}

The following Dependency Pairs can be deleted as they contain symbols in their lhs which do not occur in D:

HALF(s(s(x))) -> HALF(x)

No Rules can be deleted.

After the removal, there are no SCCs in the dependency graph which results in no DP problems which have to be solved.

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳Non-Overlappingness Check

**BITS(s( x)) -> BITS(half(s(x)))**

half(0) -> 0

half(s(0)) -> 0

half(s(s(x))) -> s(half(x))

bits(s(x)) -> s(bits(half(s(x))))

R does not overlap into P. Moreover, R is locally confluent (all critical pairs are trivially joinable).Hence we can switch to innermost.

The transformation is resulting in one subcycle:

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳NOC

...

→DP Problem 5

↳Usable Rules (Innermost)

**BITS(s( x)) -> BITS(half(s(x)))**

half(0) -> 0

half(s(0)) -> 0

half(s(s(x))) -> s(half(x))

bits(s(x)) -> s(bits(half(s(x))))

innermost

As we are in the innermost case, we can delete all 1 non-usable-rules.

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳NOC

...

→DP Problem 6

↳Modular Removal of Rules

**BITS(s( x)) -> BITS(half(s(x)))**

half(0) -> 0

half(s(0)) -> 0

half(s(s(x))) -> s(half(x))

innermost

We have the following set of usable rules:

To remove rules and DPs from this DP problem we used the following monotonic and C

half(0) -> 0

half(s(0)) -> 0

half(s(s(x))) -> s(half(x))

Polynomial interpretation:

_{ }^{ }POL(BITS(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(0)= 1 _{ }^{ }_{ }^{ }POL(s(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(half(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {BITS, 0, s, half}

No Dependency Pairs can be deleted.

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

half(s(0)) -> 0

The result of this processor delivers one new DP problem.

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳NOC

...

→DP Problem 7

↳Modular Removal of Rules

**BITS(s( x)) -> BITS(half(s(x)))**

half(0) -> 0

half(s(s(x))) -> s(half(x))

innermost

We have the following set of usable rules:

To remove rules and DPs from this DP problem we used the following monotonic and C

half(0) -> 0

half(s(s(x))) -> s(half(x))

Polynomial interpretation:

_{ }^{ }POL(BITS(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(s(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(half(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {BITS, 0, s, half}

No Dependency Pairs can be deleted.

The following rules can be deleted as the lhs is strictly greater than the corresponding rhs:

half(s(s(x))) -> s(half(x))

The result of this processor delivers one new DP problem.

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳NOC

...

→DP Problem 8

↳Modular Removal of Rules

**BITS(s( x)) -> BITS(half(s(x)))**

half(0) -> 0

innermost

We have the following set of usable rules: none

To remove rules and DPs from this DP problem we used the following monotonic and C

Polynomial interpretation:

_{ }^{ }POL(BITS(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(half(x)_{1})= x _{1}_{ }^{ }

We have the following set D of usable symbols: {BITS, s, half}

No Dependency Pairs can be deleted.

1 non usable rules have been deleted.

The result of this processor delivers one new DP problem.

TRS

↳RRRPolo

→TRS2

↳DPs

→DP Problem 1

↳NOC

→DP Problem 2

↳NOC

...

→DP Problem 9

↳Dependency Graph

**BITS(s( x)) -> BITS(half(s(x)))**

none

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:01 minutes