a(a(f(

f(a(

f(b(

R

↳Dependency Pair Analysis

A(a(f(x,y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

A(a(f(x,y))) -> A(b(a(b(a(x)))))

A(a(f(x,y))) -> A(b(a(x)))

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

A(a(f(x,y))) -> A(b(a(b(a(y)))))

A(a(f(x,y))) -> A(b(a(y)))

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

F(a(x), a(y)) -> A(f(x,y))

F(a(x), a(y)) -> F(x,y)

F(b(x), b(y)) -> F(x,y)

Furthermore,

R

↳DPs

→DP Problem 1

↳Narrowing Transformation

**F(b( x), b(y)) -> F(x, y)**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

two new Dependency Pairs are created:

F(a(x), a(y)) -> A(f(x,y))

F(a(a(x'')), a(a(y''))) -> A(a(f(x'',y'')))

F(a(b(x'')), a(b(y''))) -> A(b(f(x'',y'')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳Forward Instantiation Transformation

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

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

one new Dependency Pair is created:

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

A(a(f(a(f(x'',y'')),y))) -> A(a(f(x'',y'')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 3

↳Forward Instantiation Transformation

**A(a(f(a(f( x'', y'')), y))) -> A(a(f(x'', y'')))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

two new Dependency Pairs are created:

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

A(a(f(x, a(f(x'',y''))))) -> A(a(f(x'',y'')))

A(a(f(x, a(f(a(f(x'''',y'''')),y''))))) -> A(a(f(a(f(x'''',y'''')),y'')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 4

↳Forward Instantiation Transformation

**A(a(f( x, a(f(a(f(x'''', y'''')), y''))))) -> A(a(f(a(f(x'''', y'''')), y'')))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

three new Dependency Pairs are created:

F(a(x), a(y)) -> F(x,y)

F(a(a(x'')), a(a(y''))) -> F(a(x''), a(y''))

F(a(b(x'')), a(b(y''))) -> F(b(x''), b(y''))

F(a(a(a(x''''))), a(a(a(y'''')))) -> F(a(a(x'''')), a(a(y'''')))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 5

↳Forward Instantiation Transformation

**F(a(a(a( x''''))), a(a(a(y'''')))) -> F(a(a(x'''')), a(a(y'''')))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(b(x), b(y)) -> F(x,y)

F(b(b(x'')), b(b(y''))) -> F(b(x''), b(y''))

F(b(a(a(x''''))), b(a(a(y'''')))) -> F(a(a(x'''')), a(a(y'''')))

F(b(a(b(x''''))), b(a(b(y'''')))) -> F(a(b(x'''')), a(b(y'''')))

F(b(a(a(a(x'''''')))), b(a(a(a(y''''''))))) -> F(a(a(a(x''''''))), a(a(a(y''''''))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 6

↳Forward Instantiation Transformation

**A(a(f( x, a(f(a(f(x'''', y'''')), y''))))) -> A(a(f(a(f(x'''', y'''')), y'')))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(a(b(x'')), a(b(y''))) -> F(b(x''), b(y''))

F(a(b(b(x''''))), a(b(b(y'''')))) -> F(b(b(x'''')), b(b(y'''')))

F(a(b(a(a(x'''''')))), a(b(a(a(y''''''))))) -> F(b(a(a(x''''''))), b(a(a(y''''''))))

F(a(b(a(b(x'''''')))), a(b(a(b(y''''''))))) -> F(b(a(b(x''''''))), b(a(b(y''''''))))

F(a(b(a(a(a(x''''''''))))), a(b(a(a(a(y'''''''')))))) -> F(b(a(a(a(x'''''''')))), b(a(a(a(y'''''''')))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 7

↳Forward Instantiation Transformation

**F(a(b(a(a(a( x''''''''))))), a(b(a(a(a(y'''''''')))))) -> F(b(a(a(a(x'''''''')))), b(a(a(a(y'''''''')))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(b(b(x'')), b(b(y''))) -> F(b(x''), b(y''))

F(b(b(b(x''''))), b(b(b(y'''')))) -> F(b(b(x'''')), b(b(y'''')))

F(b(b(a(a(x'''''')))), b(b(a(a(y''''''))))) -> F(b(a(a(x''''''))), b(a(a(y''''''))))

F(b(b(a(b(x'''''')))), b(b(a(b(y''''''))))) -> F(b(a(b(x''''''))), b(a(b(y''''''))))

F(b(b(a(a(a(x''''''''))))), b(b(a(a(a(y'''''''')))))) -> F(b(a(a(a(x'''''''')))), b(a(a(a(y'''''''')))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 8

↳Polynomial Ordering

**A(a(f( x, a(f(a(f(x'''', y'''')), y''))))) -> A(a(f(a(f(x'''', y'''')), y'')))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

The following dependency pairs can be strictly oriented:

A(a(f(x, a(f(a(f(x'''',y'''')),y''))))) -> A(a(f(a(f(x'''',y'''')),y'')))

A(a(f(x, a(f(x'',y''))))) -> A(a(f(x'',y'')))

A(a(f(a(f(x'',y'')),y))) -> A(a(f(x'',y'')))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

Used ordering: Polynomial ordering with Polynomial interpretation:

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

resulting in one new DP problem.

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 9

↳Forward Instantiation Transformation

**F(b(b(a(a(a( x''''''''))))), b(b(a(a(a(y'''''''')))))) -> F(b(a(a(a(x'''''''')))), b(a(a(a(y'''''''')))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(a(b(b(x''''))), a(b(b(y'''')))) -> F(b(b(x'''')), b(b(y'''')))

F(a(b(b(b(x'''''')))), a(b(b(b(y''''''))))) -> F(b(b(b(x''''''))), b(b(b(y''''''))))

F(a(b(b(a(a(x''''''''))))), a(b(b(a(a(y'''''''')))))) -> F(b(b(a(a(x'''''''')))), b(b(a(a(y'''''''')))))

F(a(b(b(a(b(x''''''''))))), a(b(b(a(b(y'''''''')))))) -> F(b(b(a(b(x'''''''')))), b(b(a(b(y'''''''')))))

F(a(b(b(a(a(a(x'''''''''')))))), a(b(b(a(a(a(y''''''''''))))))) -> F(b(b(a(a(a(x''''''''''))))), b(b(a(a(a(y''''''''''))))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 10

↳Forward Instantiation Transformation

**F(a(b(b(a(a(a( x'''''''''')))))), a(b(b(a(a(a(y''''''''''))))))) -> F(b(b(a(a(a(x''''''''''))))), b(b(a(a(a(y''''''''''))))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(b(b(b(x''''))), b(b(b(y'''')))) -> F(b(b(x'''')), b(b(y'''')))

F(b(b(b(b(x'''''')))), b(b(b(b(y''''''))))) -> F(b(b(b(x''''''))), b(b(b(y''''''))))

F(b(b(b(a(a(x''''''''))))), b(b(b(a(a(y'''''''')))))) -> F(b(b(a(a(x'''''''')))), b(b(a(a(y'''''''')))))

F(b(b(b(a(b(x''''''''))))), b(b(b(a(b(y'''''''')))))) -> F(b(b(a(b(x'''''''')))), b(b(a(b(y'''''''')))))

F(b(b(b(a(a(a(x'''''''''')))))), b(b(b(a(a(a(y''''''''''))))))) -> F(b(b(a(a(a(x''''''''''))))), b(b(a(a(a(y''''''''''))))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 11

↳Forward Instantiation Transformation

**F(a(b(b(a(b( x''''''''))))), a(b(b(a(b(y'''''''')))))) -> F(b(b(a(b(x'''''''')))), b(b(a(b(y'''''''')))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(a(b(b(b(x'''''')))), a(b(b(b(y''''''))))) -> F(b(b(b(x''''''))), b(b(b(y''''''))))

F(a(b(b(b(b(x''''''''))))), a(b(b(b(b(y'''''''')))))) -> F(b(b(b(b(x'''''''')))), b(b(b(b(y'''''''')))))

F(a(b(b(b(a(a(x'''''''''')))))), a(b(b(b(a(a(y''''''''''))))))) -> F(b(b(b(a(a(x''''''''''))))), b(b(b(a(a(y''''''''''))))))

F(a(b(b(b(a(b(x'''''''''')))))), a(b(b(b(a(b(y''''''''''))))))) -> F(b(b(b(a(b(x''''''''''))))), b(b(b(a(b(y''''''''''))))))

F(a(b(b(b(a(a(a(x''''''''''''))))))), a(b(b(b(a(a(a(y'''''''''''')))))))) -> F(b(b(b(a(a(a(x'''''''''''')))))), b(b(b(a(a(a(y'''''''''''')))))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 12

↳Forward Instantiation Transformation

**F(a(b(b(b(a(a(a( x''''''''''''))))))), a(b(b(b(a(a(a(y'''''''''''')))))))) -> F(b(b(b(a(a(a(x'''''''''''')))))), b(b(b(a(a(a(y'''''''''''')))))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(b(b(b(b(x'''''')))), b(b(b(b(y''''''))))) -> F(b(b(b(x''''''))), b(b(b(y''''''))))

F(b(b(b(b(b(x''''''''))))), b(b(b(b(b(y'''''''')))))) -> F(b(b(b(b(x'''''''')))), b(b(b(b(y'''''''')))))

F(b(b(b(b(a(a(x'''''''''')))))), b(b(b(b(a(a(y''''''''''))))))) -> F(b(b(b(a(a(x''''''''''))))), b(b(b(a(a(y''''''''''))))))

F(b(b(b(b(a(b(x'''''''''')))))), b(b(b(b(a(b(y''''''''''))))))) -> F(b(b(b(a(b(x''''''''''))))), b(b(b(a(b(y''''''''''))))))

F(b(b(b(b(a(a(a(x''''''''''''))))))), b(b(b(b(a(a(a(y'''''''''''')))))))) -> F(b(b(b(a(a(a(x'''''''''''')))))), b(b(b(a(a(a(y'''''''''''')))))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 13

↳Forward Instantiation Transformation

**F(a(b(b(b(a(b( x'''''''''')))))), a(b(b(b(a(b(y''''''''''))))))) -> F(b(b(b(a(b(x''''''''''))))), b(b(b(a(b(y''''''''''))))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(a(b(b(b(b(x''''''''))))), a(b(b(b(b(y'''''''')))))) -> F(b(b(b(b(x'''''''')))), b(b(b(b(y'''''''')))))

F(a(b(b(b(b(b(x'''''''''')))))), a(b(b(b(b(b(y''''''''''))))))) -> F(b(b(b(b(b(x''''''''''))))), b(b(b(b(b(y''''''''''))))))

F(a(b(b(b(b(a(a(x''''''''''''))))))), a(b(b(b(b(a(a(y'''''''''''')))))))) -> F(b(b(b(b(a(a(x'''''''''''')))))), b(b(b(b(a(a(y'''''''''''')))))))

F(a(b(b(b(b(a(b(x''''''''''''))))))), a(b(b(b(b(a(b(y'''''''''''')))))))) -> F(b(b(b(b(a(b(x'''''''''''')))))), b(b(b(b(a(b(y'''''''''''')))))))

F(a(b(b(b(b(a(a(a(x'''''''''''''')))))))), a(b(b(b(b(a(a(a(y''''''''''''''))))))))) -> F(b(b(b(b(a(a(a(x''''''''''''''))))))), b(b(b(b(a(a(a(y''''''''''''''))))))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 14

↳Forward Instantiation Transformation

**F(a(b(b(b(b(a(a(a( x'''''''''''''')))))))), a(b(b(b(b(a(a(a(y''''''''''''''))))))))) -> F(b(b(b(b(a(a(a(x''''''''''''''))))))), b(b(b(b(a(a(a(y''''''''''''''))))))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

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

As a result of transforming the rule

four new Dependency Pairs are created:

F(b(b(b(b(b(x''''''''))))), b(b(b(b(b(y'''''''')))))) -> F(b(b(b(b(x'''''''')))), b(b(b(b(y'''''''')))))

F(b(b(b(b(b(b(x'''''''''')))))), b(b(b(b(b(b(y''''''''''))))))) -> F(b(b(b(b(b(x''''''''''))))), b(b(b(b(b(y''''''''''))))))

F(b(b(b(b(b(a(a(x''''''''''''))))))), b(b(b(b(b(a(a(y'''''''''''')))))))) -> F(b(b(b(b(a(a(x'''''''''''')))))), b(b(b(b(a(a(y'''''''''''')))))))

F(b(b(b(b(b(a(b(x''''''''''''))))))), b(b(b(b(b(a(b(y'''''''''''')))))))) -> F(b(b(b(b(a(b(x'''''''''''')))))), b(b(b(b(a(b(y'''''''''''')))))))

F(b(b(b(b(b(a(a(a(x'''''''''''''')))))))), b(b(b(b(b(a(a(a(y''''''''''''''))))))))) -> F(b(b(b(b(a(a(a(x''''''''''''''))))))), b(b(b(b(a(a(a(y''''''''''''''))))))))

The transformation is resulting in one new DP problem:

R

↳DPs

→DP Problem 1

↳Nar

→DP Problem 2

↳FwdInst

...

→DP Problem 15

↳Remaining Obligation(s)

The following remains to be proven:

**F(a(b(b(b(b(a(b( x''''''''''''))))))), a(b(b(b(b(a(b(y'''''''''''')))))))) -> F(b(b(b(b(a(b(x'''''''''''')))))), b(b(b(b(a(b(y'''''''''''')))))))**

a(a(f(x,y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))

f(a(x), a(y)) -> a(f(x,y))

f(b(x), b(y)) -> b(f(x,y))

innermost

Duration:

0:08 minutes