Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) -> p(a(x, z), a(y, z))
a(a(x, y), z) -> a(x, a(y, z))
a(id, x) -> x
a(1, id) -> 1
a(t, id) -> t
a(1, p(x, y)) -> x
a(t, p(x, y)) -> y

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

A(lambda(x), y) -> A(x, p(1, a(y, t)))
A(lambda(x), y) -> A(y, t)
A(p(x, y), z) -> A(x, z)
A(p(x, y), z) -> A(y, z)
A(a(x, y), z) -> A(x, a(y, z))
A(a(x, y), z) -> A(y, z)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

Dependency Pairs:

A(a(x, y), z) -> A(y, z)
A(p(x, y), z) -> A(y, z)
A(p(x, y), z) -> A(x, z)
A(lambda(x), y) -> A(y, t)
A(lambda(x), y) -> A(x, p(1, a(y, t)))

Rules:

a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) -> p(a(x, z), a(y, z))
a(a(x, y), z) -> a(x, a(y, z))
a(id, x) -> x
a(1, id) -> 1
a(t, id) -> t
a(1, p(x, y)) -> x
a(t, p(x, y)) -> y

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

A(lambda(x), y) -> A(y, t)

three new Dependency Pairs are created:

A(lambda(x), lambda(x'')) -> A(lambda(x''), t)
A(lambda(x), p(x'', y'')) -> A(p(x'', y''), t)
A(lambda(x), a(x'', y'')) -> A(a(x'', y''), t)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳Forward Instantiation Transformation

Dependency Pairs:

A(lambda(x), a(x'', y'')) -> A(a(x'', y''), t)
A(lambda(x), p(x'', y'')) -> A(p(x'', y''), t)
A(lambda(x), lambda(x'')) -> A(lambda(x''), t)
A(p(x, y), z) -> A(y, z)
A(p(x, y), z) -> A(x, z)
A(lambda(x), y) -> A(x, p(1, a(y, t)))
A(a(x, y), z) -> A(y, z)

Rules:

a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) -> p(a(x, z), a(y, z))
a(a(x, y), z) -> a(x, a(y, z))
a(id, x) -> x
a(1, id) -> 1
a(t, id) -> t
a(1, p(x, y)) -> x
a(t, p(x, y)) -> y

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

A(p(x, y), z) -> A(x, z)

six new Dependency Pairs are created:

A(p(p(x'', y''), y), z'') -> A(p(x'', y''), z'')
A(p(lambda(x''), y), z') -> A(lambda(x''), z')
A(p(a(x'', y''), y), z'') -> A(a(x'', y''), z'')
A(p(lambda(x''), y), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(lambda(x''), y), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(lambda(x''), y), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 3

                 ↳Forward Instantiation Transformation

Dependency Pairs:

A(p(lambda(x''), y), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(p(lambda(x''), y), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(lambda(x''), y), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(a(x'', y''), y), z'') -> A(a(x'', y''), z'')
A(p(lambda(x''), y), z') -> A(lambda(x''), z')
A(p(p(x'', y''), y), z'') -> A(p(x'', y''), z'')
A(lambda(x), p(x'', y'')) -> A(p(x'', y''), t)
A(lambda(x), lambda(x'')) -> A(lambda(x''), t)
A(p(x, y), z) -> A(y, z)
A(lambda(x), y) -> A(x, p(1, a(y, t)))
A(a(x, y), z) -> A(y, z)
A(lambda(x), a(x'', y'')) -> A(a(x'', y''), t)

Rules:

a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) -> p(a(x, z), a(y, z))
a(a(x, y), z) -> a(x, a(y, z))
a(id, x) -> x
a(1, id) -> 1
a(t, id) -> t
a(1, p(x, y)) -> x
a(t, p(x, y)) -> y

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

A(p(x, y), z) -> A(y, z)

12 new Dependency Pairs are created:

A(p(x, p(x'', y'')), z'') -> A(p(x'', y''), z'')
A(p(x, lambda(x'')), z') -> A(lambda(x''), z')
A(p(x, a(x'', y'')), z'') -> A(a(x'', y''), z'')
A(p(x, lambda(x'')), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(x, lambda(x'')), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(x, lambda(x'')), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(p(x, p(p(x'''', y''''), y'')), z') -> A(p(p(x'''', y''''), y''), z')
A(p(x, p(lambda(x''''), y'')), z') -> A(p(lambda(x''''), y''), z')
A(p(x, p(a(x'''', y''''), y'')), z') -> A(p(a(x'''', y''''), y''), z')
A(p(x, p(lambda(x''''), y'')), lambda(x'''''')) -> A(p(lambda(x''''), y''), lambda(x''''''))
A(p(x, p(lambda(x''''), y'')), p(x'''''', y'''''')) -> A(p(lambda(x''''), y''), p(x'''''', y''''''))
A(p(x, p(lambda(x''''), y'')), a(x'''''', y'''''')) -> A(p(lambda(x''''), y''), a(x'''''', y''''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

Dependency Pairs:

A(p(x, p(lambda(x''''), y'')), a(x'''''', y'''''')) -> A(p(lambda(x''''), y''), a(x'''''', y''''''))
A(p(x, p(lambda(x''''), y'')), p(x'''''', y'''''')) -> A(p(lambda(x''''), y''), p(x'''''', y''''''))
A(p(x, p(lambda(x''''), y'')), lambda(x'''''')) -> A(p(lambda(x''''), y''), lambda(x''''''))
A(p(x, p(a(x'''', y''''), y'')), z') -> A(p(a(x'''', y''''), y''), z')
A(p(x, p(lambda(x''''), y'')), z') -> A(p(lambda(x''''), y''), z')
A(p(x, p(p(x'''', y''''), y'')), z') -> A(p(p(x'''', y''''), y''), z')
A(p(x, lambda(x'')), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(p(x, lambda(x'')), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(x, lambda(x'')), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(x, a(x'', y'')), z'') -> A(a(x'', y''), z'')
A(p(x, lambda(x'')), z') -> A(lambda(x''), z')
A(p(x, p(x'', y'')), z'') -> A(p(x'', y''), z'')
A(p(lambda(x''), y), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(lambda(x''), y), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(a(x'', y''), y), z'') -> A(a(x'', y''), z'')
A(lambda(x), a(x'', y'')) -> A(a(x'', y''), t)
A(p(lambda(x''), y), z') -> A(lambda(x''), z')
A(p(p(x'', y''), y), z'') -> A(p(x'', y''), z'')
A(lambda(x), p(x'', y'')) -> A(p(x'', y''), t)
A(lambda(x), lambda(x'')) -> A(lambda(x''), t)
A(a(x, y), z) -> A(y, z)
A(lambda(x), y) -> A(x, p(1, a(y, t)))
A(p(lambda(x''), y), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))

Rules:

a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) -> p(a(x, z), a(y, z))
a(a(x, y), z) -> a(x, a(y, z))
a(id, x) -> x
a(1, id) -> 1
a(t, id) -> t
a(1, p(x, y)) -> x
a(t, p(x, y)) -> y

Strategy:

innermost

On this DP problem, a Forward Instantiation SCC transformation can be performed.
As a result of transforming the rule

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

23 new Dependency Pairs are created:

A(a(x, a(x'', y'')), z'') -> A(a(x'', y''), z'')
A(a(x, lambda(x'')), z') -> A(lambda(x''), z')
A(a(x, lambda(x'')), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(a(x, lambda(x'')), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(a(x, lambda(x'')), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(a(x, p(p(x'''', y''''), y'')), z') -> A(p(p(x'''', y''''), y''), z')
A(a(x, p(lambda(x''''), y'')), z') -> A(p(lambda(x''''), y''), z')
A(a(x, p(a(x'''', y''''), y'')), z') -> A(p(a(x'''', y''''), y''), z')
A(a(x, p(lambda(x''''), y'')), lambda(x'''''')) -> A(p(lambda(x''''), y''), lambda(x''''''))
A(a(x, p(lambda(x''''), y'')), p(x'''''', y'''''')) -> A(p(lambda(x''''), y''), p(x'''''', y''''''))
A(a(x, p(lambda(x''''), y'')), a(x'''''', y'''''')) -> A(p(lambda(x''''), y''), a(x'''''', y''''''))
A(a(x, p(x'', p(x'''', y''''))), z') -> A(p(x'', p(x'''', y'''')), z')
A(a(x, p(x'', lambda(x''''))), z') -> A(p(x'', lambda(x'''')), z')
A(a(x, p(x'', a(x'''', y''''))), z') -> A(p(x'', a(x'''', y'''')), z')
A(a(x, p(x'', lambda(x''''))), lambda(x'''''')) -> A(p(x'', lambda(x'''')), lambda(x''''''))
A(a(x, p(x'', lambda(x''''))), p(x'''''', y'''''')) -> A(p(x'', lambda(x'''')), p(x'''''', y''''''))
A(a(x, p(x'', lambda(x''''))), a(x'''''', y'''''')) -> A(p(x'', lambda(x'''')), a(x'''''', y''''''))
A(a(x, p(x'', p(p(x'''''', y''''''), y''''))), z') -> A(p(x'', p(p(x'''''', y''''''), y'''')), z')
A(a(x, p(x'', p(lambda(x''''''), y''''))), z') -> A(p(x'', p(lambda(x''''''), y'''')), z')
A(a(x, p(x'', p(a(x'''''', y''''''), y''''))), z') -> A(p(x'', p(a(x'''''', y''''''), y'''')), z')
A(a(x, p(x'', p(lambda(x''''''), y''''))), lambda(x'''''''')) -> A(p(x'', p(lambda(x''''''), y'''')), lambda(x''''''''))
A(a(x, p(x'', p(lambda(x''''''), y''''))), p(x'''''''', y'''''''')) -> A(p(x'', p(lambda(x''''''), y'''')), p(x'''''''', y''''''''))
A(a(x, p(x'', p(lambda(x''''''), y''''))), a(x'''''''', y'''''''')) -> A(p(x'', p(lambda(x''''''), y'''')), a(x'''''''', y''''''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 2

             ↳FwdInst

...

               →DP Problem 5

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

A(a(x, p(x'', p(lambda(x''''''), y''''))), a(x'''''''', y'''''''')) -> A(p(x'', p(lambda(x''''''), y'''')), a(x'''''''', y''''''''))
A(a(x, p(x'', p(lambda(x''''''), y''''))), p(x'''''''', y'''''''')) -> A(p(x'', p(lambda(x''''''), y'''')), p(x'''''''', y''''''''))
A(a(x, p(x'', p(lambda(x''''''), y''''))), lambda(x'''''''')) -> A(p(x'', p(lambda(x''''''), y'''')), lambda(x''''''''))
A(a(x, p(x'', p(a(x'''''', y''''''), y''''))), z') -> A(p(x'', p(a(x'''''', y''''''), y'''')), z')
A(a(x, p(x'', p(lambda(x''''''), y''''))), z') -> A(p(x'', p(lambda(x''''''), y'''')), z')
A(a(x, p(x'', p(p(x'''''', y''''''), y''''))), z') -> A(p(x'', p(p(x'''''', y''''''), y'''')), z')
A(a(x, p(x'', lambda(x''''))), a(x'''''', y'''''')) -> A(p(x'', lambda(x'''')), a(x'''''', y''''''))
A(a(x, p(x'', lambda(x''''))), p(x'''''', y'''''')) -> A(p(x'', lambda(x'''')), p(x'''''', y''''''))
A(a(x, p(x'', lambda(x''''))), lambda(x'''''')) -> A(p(x'', lambda(x'''')), lambda(x''''''))
A(a(x, p(x'', a(x'''', y''''))), z') -> A(p(x'', a(x'''', y'''')), z')
A(a(x, p(x'', lambda(x''''))), z') -> A(p(x'', lambda(x'''')), z')
A(a(x, p(x'', p(x'''', y''''))), z') -> A(p(x'', p(x'''', y'''')), z')
A(a(x, p(lambda(x''''), y'')), a(x'''''', y'''''')) -> A(p(lambda(x''''), y''), a(x'''''', y''''''))
A(a(x, p(lambda(x''''), y'')), p(x'''''', y'''''')) -> A(p(lambda(x''''), y''), p(x'''''', y''''''))
A(a(x, p(lambda(x''''), y'')), lambda(x'''''')) -> A(p(lambda(x''''), y''), lambda(x''''''))
A(a(x, p(a(x'''', y''''), y'')), z') -> A(p(a(x'''', y''''), y''), z')
A(p(x, p(lambda(x''''), y'')), p(x'''''', y'''''')) -> A(p(lambda(x''''), y''), p(x'''''', y''''''))
A(p(x, p(lambda(x''''), y'')), lambda(x'''''')) -> A(p(lambda(x''''), y''), lambda(x''''''))
A(p(x, p(a(x'''', y''''), y'')), z') -> A(p(a(x'''', y''''), y''), z')
A(p(x, p(lambda(x''''), y'')), z') -> A(p(lambda(x''''), y''), z')
A(p(x, p(p(x'''', y''''), y'')), z') -> A(p(p(x'''', y''''), y''), z')
A(p(x, lambda(x'')), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(p(x, lambda(x'')), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(x, lambda(x'')), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(a(x, p(lambda(x''''), y'')), z') -> A(p(lambda(x''''), y''), z')
A(a(x, lambda(x'')), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(a(x, lambda(x'')), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(a(x, lambda(x'')), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(x, a(x'', y'')), z'') -> A(a(x'', y''), z'')
A(p(x, lambda(x'')), z') -> A(lambda(x''), z')
A(p(lambda(x''), y), a(x'''', y'''')) -> A(lambda(x''), a(x'''', y''''))
A(p(lambda(x''), y), p(x'''', y'''')) -> A(lambda(x''), p(x'''', y''''))
A(p(lambda(x''), y), lambda(x'''')) -> A(lambda(x''), lambda(x''''))
A(p(x, p(x'', y'')), z'') -> A(p(x'', y''), z'')
A(a(x, p(p(x'''', y''''), y'')), z') -> A(p(p(x'''', y''''), y''), z')
A(lambda(x), a(x'', y'')) -> A(a(x'', y''), t)
A(lambda(x), lambda(x'')) -> A(lambda(x''), t)
A(a(x, lambda(x'')), z') -> A(lambda(x''), z')
A(a(x, a(x'', y'')), z'') -> A(a(x'', y''), z'')
A(p(a(x'', y''), y), z'') -> A(a(x'', y''), z'')
A(p(p(x'', y''), y), z'') -> A(p(x'', y''), z'')
A(lambda(x), p(x'', y'')) -> A(p(x'', y''), t)
A(lambda(x), y) -> A(x, p(1, a(y, t)))
A(p(lambda(x''), y), z') -> A(lambda(x''), z')
A(p(x, p(lambda(x''''), y'')), a(x'''''', y'''''')) -> A(p(lambda(x''''), y''), a(x'''''', y''''''))

Rules:

a(lambda(x), y) -> lambda(a(x, p(1, a(y, t))))
a(p(x, y), z) -> p(a(x, z), a(y, z))
a(a(x, y), z) -> a(x, a(y, z))
a(id, x) -> x
a(1, id) -> 1
a(t, id) -> t
a(1, p(x, y)) -> x
a(t, p(x, y)) -> y

Strategy:

innermost

Innermost Termination of R could not be shown.
Duration:
0:44 minutes