Termination Proof using AProVE

Term Rewriting System R:
[x, y, u, z]
perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

PERFECTP(s(x)) -> F(x, s(0), s(x), s(x))
F(s(x), 0, z, u) -> F(x, u, minus(z, s(x)), u)
F(s(x), s(y), z, u) -> F(s(x), minus(y, x), z, u)
F(s(x), s(y), z, u) -> F(x, u, z, u)

Furthermore, R contains one SCC.

     ↳DPs

       →DP Problem 1

         ↳Instantiation Transformation

Dependency Pairs:

F(s(x), 0, z, u) -> F(x, u, minus(z, s(x)), u)
F(s(x), s(y), z, u) -> F(x, u, z, u)

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

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

F(s(x), 0, z, u) -> F(x, u, minus(z, s(x)), u)

two new Dependency Pairs are created:

F(s(x''), 0, minus(z'', s(s(x''))), 0) -> F(x'', 0, minus(minus(z'', s(s(x''))), s(x'')), 0)
F(s(x''), 0, z'', 0) -> F(x'', 0, minus(z'', s(x'')), 0)

The transformation is resulting in two new DP problems:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Instantiation Transformation

           →DP Problem 3

             ↳Inst

Dependency Pairs:

F(s(x''), 0, z'', 0) -> F(x'', 0, minus(z'', s(x'')), 0)
F(s(x''), 0, minus(z'', s(s(x''))), 0) -> F(x'', 0, minus(minus(z'', s(s(x''))), s(x'')), 0)

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

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

F(s(x''), 0, z'', 0) -> F(x'', 0, minus(z'', s(x'')), 0)

two new Dependency Pairs are created:

F(s(x''''), 0, minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), 0) -> F(x'''', 0, minus(minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), s(x'''')), 0)
F(s(x''''), 0, minus(z'''', s(s(x''''))), 0) -> F(x'''', 0, minus(minus(z'''', s(s(x''''))), s(x'''')), 0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Inst

...

               →DP Problem 4

                 ↳Instantiation Transformation

           →DP Problem 3

             ↳Inst

Dependency Pairs:

F(s(x''''), 0, minus(z'''', s(s(x''''))), 0) -> F(x'''', 0, minus(minus(z'''', s(s(x''''))), s(x'''')), 0)
F(s(x''''), 0, minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), 0) -> F(x'''', 0, minus(minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), s(x'''')), 0)
F(s(x''), 0, minus(z'', s(s(x''))), 0) -> F(x'', 0, minus(minus(z'', s(s(x''))), s(x'')), 0)

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

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

F(s(x''), 0, minus(z'', s(s(x''))), 0) -> F(x'', 0, minus(minus(z'', s(s(x''))), s(x'')), 0)

three new Dependency Pairs are created:

F(s(x''''), 0, minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), 0) -> F(x'''', 0, minus(minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), s(x'''')), 0)
F(s(x'''), 0, minus(minus(minus(z'''''', s(s(s(s(x'''))))), s(s(s(x''')))), s(s(x'''))), 0) -> F(x''', 0, minus(minus(minus(minus(z'''''', s(s(s(s(x'''))))), s(s(s(x''')))), s(s(x'''))), s(x''')), 0)
F(s(x'''), 0, minus(minus(z'''''', s(s(s(x''')))), s(s(x'''))), 0) -> F(x''', 0, minus(minus(minus(z'''''', s(s(s(x''')))), s(s(x'''))), s(x''')), 0)

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Inst

...

               →DP Problem 6

                 ↳Polynomial Ordering

           →DP Problem 3

             ↳Inst

Dependency Pairs:

F(s(x'''), 0, minus(minus(z'''''', s(s(s(x''')))), s(s(x'''))), 0) -> F(x''', 0, minus(minus(minus(z'''''', s(s(s(x''')))), s(s(x'''))), s(x''')), 0)
F(s(x'''), 0, minus(minus(minus(z'''''', s(s(s(s(x'''))))), s(s(s(x''')))), s(s(x'''))), 0) -> F(x''', 0, minus(minus(minus(minus(z'''''', s(s(s(s(x'''))))), s(s(s(x''')))), s(s(x'''))), s(x''')), 0)
F(s(x''''), 0, minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), 0) -> F(x'''', 0, minus(minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), s(x'''')), 0)
F(s(x''''), 0, minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), 0) -> F(x'''', 0, minus(minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), s(x'''')), 0)
F(s(x''''), 0, minus(z'''', s(s(x''''))), 0) -> F(x'''', 0, minus(minus(z'''', s(s(x''''))), s(x'''')), 0)

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

F(s(x'''), 0, minus(minus(z'''''', s(s(s(x''')))), s(s(x'''))), 0) -> F(x''', 0, minus(minus(minus(z'''''', s(s(s(x''')))), s(s(x'''))), s(x''')), 0)
F(s(x'''), 0, minus(minus(minus(z'''''', s(s(s(s(x'''))))), s(s(s(x''')))), s(s(x'''))), 0) -> F(x''', 0, minus(minus(minus(minus(z'''''', s(s(s(s(x'''))))), s(s(s(x''')))), s(s(x'''))), s(x''')), 0)
F(s(x''''), 0, minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), 0) -> F(x'''', 0, minus(minus(minus(z'''', s(s(s(x'''')))), s(s(x''''))), s(x'''')), 0)
F(s(x''''), 0, minus(z'''', s(s(x''''))), 0) -> F(x'''', 0, minus(minus(z'''', s(s(x''''))), s(x'''')), 0)

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(0) = 0

POL(minus(x₁, x₂)) = x₂

POL(s(x₁)) = 1 + x₁

POL(F(x₁, x₂, x₃, x₄)) = x₂ + x₃

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Inst

...

               →DP Problem 8

                 ↳Dependency Graph

           →DP Problem 3

             ↳Inst

Dependency Pair:

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Inst

           →DP Problem 3

             ↳Instantiation Transformation

Dependency Pair:

F(s(x), s(y), z, u) -> F(x, u, z, u)

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

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

F(s(x), s(y), z, u) -> F(x, u, z, u)

one new Dependency Pair is created:

F(s(x''), s(y'), z'', s(y')) -> F(x'', s(y'), z'', s(y'))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Inst

           →DP Problem 3

             ↳Inst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

Dependency Pair:

F(s(x''), s(y'), z'', s(y')) -> F(x'', s(y'), z'', s(y'))

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

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

F(s(x''), s(y'), z'', s(y')) -> F(x'', s(y'), z'', s(y'))

one new Dependency Pair is created:

F(s(s(x'''')), s(y'0), z'''', s(y'0)) -> F(s(x''''), s(y'0), z'''', s(y'0))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 2

             ↳Inst

           →DP Problem 3

             ↳Inst

...

               →DP Problem 7

                 ↳Polynomial Ordering

Dependency Pair:

F(s(s(x'''')), s(y'0), z'''', s(y'0)) -> F(s(x''''), s(y'0), z'''', s(y'0))

Rules:

perfectp(0) -> false
perfectp(s(x)) -> f(x, s(0), s(x), s(x))
f(0, y, 0, u) -> true
f(0, y, s(z), u) -> false
f(s(x), 0, z, u) -> f(x, u, minus(z, s(x)), u)
f(s(x), s(y), z, u) -> if(le(x, y), f(s(x), minus(y, x), z, u), f(x, u, z, u))

Strategy:

innermost

The following dependency pair can be strictly oriented:

F(s(s(x'''')), s(y'0), z'''', s(y'0)) -> F(s(x''''), s(y'0), z'''', s(y'0))

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(x₁)) = 1 + x₁

POL(F(x₁, x₂, x₃, x₄)) = 1 + x₁

resulting in one new DP problem.

Innermost Termination of R successfully shown.
Duration:
0:02 minutes

POL(0)	= 0
POL(minus(x₁, x₂))	= x₂
POL(s(x₁))	= 1 + x₁
POL(F(x₁, x₂, x₃, x₄))	= x₂ + x₃