rec(rec(

rec(sent(

rec(no(

rec(bot) -> up(sent(bot))

rec(up(

sent(up(

no(up(

top(rec(up(

top(sent(up(

top(no(up(

check(up(

check(sent(

check(rec(

check(no(

check(no(

R

↳Removing Redundant Rules for Innermost Termination

Removing the following rules from

top(rec(up(x))) -> top(check(rec(x)))

top(sent(up(x))) -> top(check(rec(x)))

top(no(up(x))) -> top(check(rec(x)))

R

↳RRRI

→TRS2

↳Removing Redundant Rules

Removing the following rules from

rec(bot) -> up(sent(bot))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(no(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(bot)= 1 _{ }^{ }_{ }^{ }POL(up(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳Removing Redundant Rules

Removing the following rules from

rec(no(x)) -> sent(rec(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(no(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(up(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS4

↳Removing Redundant Rules

Removing the following rules from

check(no(x)) -> no(check(x))

check(no(x)) -> no(x)

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(no(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(up(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS5

↳Removing Redundant Rules

Removing the following rules from

no(up(x)) -> up(no(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(no(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(up(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS6

↳Removing Redundant Rules

Removing the following rules from

check(up(x)) -> up(check(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(up(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS7

↳Removing Redundant Rules

Removing the following rules from

rec(up(x)) -> up(rec(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(up(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS8

↳Removing Redundant Rules

Removing the following rules from

sent(up(x)) -> up(sent(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(up(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= 2·x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS9

↳Removing Redundant Rules

Removing the following rules from

rec(rec(x)) -> sent(rec(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS10

↳Removing Redundant Rules

Removing the following rules from

check(rec(x)) -> rec(check(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= 1 + x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS11

↳Removing Redundant Rules

Removing the following rules from

check(sent(x)) -> sent(check(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(check(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= 1 + x _{1}_{ }^{ }

Not all Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS12

↳Removing Redundant Rules

Removing the following rules from

rec(sent(x)) -> sent(rec(x))

where the Polynomial interpretation:

was used.

_{ }^{ }POL(rec(x)_{1})= 2·x _{1}_{ }^{ }_{ }^{ }POL(sent(x)_{1})= 1 + x _{1}_{ }^{ }

All Rules of

R

↳RRRI

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS13

↳Dependency Pair Analysis

Duration:

0:00 minutes