a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,

a(f, a(s,

a(p, a(s,

R

↳Dependency Pair Analysis

A(f, 0) -> A(s, 0)

A(d, a(s,x)) -> A(s, a(s, a(d, a(p, a(s,x)))))

A(d, a(s,x)) -> A(s, a(d, a(p, a(s,x))))

A(d, a(s,x)) -> A(d, a(p, a(s,x)))

A(d, a(s,x)) -> A(p, a(s,x))

A(f, a(s,x)) -> A(d, a(f, a(p, a(s,x))))

A(f, a(s,x)) -> A(f, a(p, a(s,x)))

A(f, a(s,x)) -> A(p, a(s,x))

Furthermore,

R

↳DPs

→DP Problem 1

↳Rewriting Transformation

→DP Problem 2

↳Rw

**A(d, a(s, x)) -> A(d, a(p, a(s, x)))**

a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,x)) -> a(s, a(s, a(d, a(p, a(s,x)))))

a(f, a(s,x)) -> a(d, a(f, a(p, a(s,x))))

a(p, a(s,x)) ->x

innermost

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

A(d, a(s,x)) -> A(d, a(p, a(s,x)))

A(d, a(s,x)) -> A(d,x)

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 3

↳Polynomial Ordering

→DP Problem 2

↳Rw

**A(d, a(s, x)) -> A(d, x)**

a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,x)) -> a(s, a(s, a(d, a(p, a(s,x)))))

a(f, a(s,x)) -> a(d, a(f, a(p, a(s,x))))

a(p, a(s,x)) ->x

innermost

The following dependency pair can be strictly oriented:

A(d, a(s,x)) -> A(d,x)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(d)= 0 _{ }^{ }_{ }^{ }POL(s)= 0 _{ }^{ }_{ }^{ }POL(a(x)_{1}, x_{2})= 1 + x _{2}_{ }^{ }_{ }^{ }POL(A(x)_{1}, x_{2})= x _{2}_{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 3

↳Polo

...

→DP Problem 4

↳Dependency Graph

→DP Problem 2

↳Rw

a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,x)) -> a(s, a(s, a(d, a(p, a(s,x)))))

a(f, a(s,x)) -> a(d, a(f, a(p, a(s,x))))

a(p, a(s,x)) ->x

innermost

Using the Dependency Graph resulted in no new DP problems.

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rewriting Transformation

**A(f, a(s, x)) -> A(f, a(p, a(s, x)))**

a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,x)) -> a(s, a(s, a(d, a(p, a(s,x)))))

a(f, a(s,x)) -> a(d, a(f, a(p, a(s,x))))

a(p, a(s,x)) ->x

innermost

On this DP problem, a Rewriting SCC transformation can be performed.

As a result of transforming the rule

one new Dependency Pair is created:

A(f, a(s,x)) -> A(f, a(p, a(s,x)))

A(f, a(s,x)) -> A(f,x)

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rw

→DP Problem 5

↳Polynomial Ordering

**A(f, a(s, x)) -> A(f, x)**

a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,x)) -> a(s, a(s, a(d, a(p, a(s,x)))))

a(f, a(s,x)) -> a(d, a(f, a(p, a(s,x))))

a(p, a(s,x)) ->x

innermost

The following dependency pair can be strictly oriented:

A(f, a(s,x)) -> A(f,x)

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

_{ }^{ }POL(s)= 0 _{ }^{ }_{ }^{ }POL(a(x)_{1}, x_{2})= 1 + x _{2}_{ }^{ }_{ }^{ }POL(A(x)_{1}, x_{2})= x _{2}_{ }^{ }_{ }^{ }POL(f)= 0 _{ }^{ }

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Rw

→DP Problem 2

↳Rw

→DP Problem 5

↳Polo

...

→DP Problem 6

↳Dependency Graph

a(f, 0) -> a(s, 0)

a(d, 0) -> 0

a(d, a(s,x)) -> a(s, a(s, a(d, a(p, a(s,x)))))

a(f, a(s,x)) -> a(d, a(f, a(p, a(s,x))))

a(p, a(s,x)) ->x

innermost

Using the Dependency Graph resulted in no new DP problems.

Duration:

0:00 minutes