norm(nil) -> 0

norm(g(

f(

f(

rem(nil,

rem(g(

rem(g(

R

↳Removing Redundant Rules

Removing the following rules from

norm(nil) -> 0

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(g(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(rem(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(norm(x)_{1})= 1 + x _{1}_{ }^{ }

Not all Rules of

R

↳RRRPolo

→TRS2

↳Removing Redundant Rules

Removing the following rules from

norm(g(x,y)) -> s(norm(x))

rem(g(x,y), s(z)) -> rem(x,z)

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(g(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(rem(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(s(x)_{1})= x _{1}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(norm(x)_{1})= x _{1}_{ }^{ }

Not all Rules of

R

↳RRRPolo

→TRS2

↳RRRPolo

→TRS3

↳Removing Redundant Rules

Removing the following rules from

rem(nil,y) -> nil

rem(g(x,y), 0) -> g(x,y)

where the Polynomial interpretation:

was used.

_{ }^{ }POL(0)= 0 _{ }^{ }_{ }^{ }POL(g(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 0 _{ }^{ }_{ }^{ }POL(rem(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }

Not all Rules of

R

↳RRRPolo

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS4

↳Removing Redundant Rules

Removing the following rules from

f(x, nil) -> g(nil,x)

where the Polynomial interpretation:

was used.

_{ }^{ }POL(g(x)_{1}, x_{2})= x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(nil)= 1 _{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= x _{1}+ 2·x_{2}_{ }^{ }

Not all Rules of

R

↳RRRPolo

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS5

↳Removing Redundant Rules

Removing the following rules from

f(x, g(y,z)) -> g(f(x,y),z)

where the Polynomial interpretation:

was used.

_{ }^{ }POL(g(x)_{1}, x_{2})= 1 + x _{1}+ x_{2}_{ }^{ }_{ }^{ }POL(f(x)_{1}, x_{2})= x _{1}+ 2·x_{2}_{ }^{ }

All Rules of

R

↳RRRPolo

→TRS2

↳RRRPolo

→TRS3

↳RRRPolo

...

→TRS6

↳Dependency Pair Analysis

Duration:

0:00 minutes