Term Rewriting System R:
[x, y, z]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(minus(x, y), z) -> PLUS(y, z)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
PLUS(s(x), y) -> PLUS(x, y)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Forward Instantiation Transformation
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:

PLUS(s(x), y) -> PLUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

PLUS(s(x), y) -> PLUS(x, y)
one new Dependency Pair is created:

PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
Forward Instantiation Transformation
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:

PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

PLUS(s(s(x'')), y'') -> PLUS(s(x''), y'')
one new Dependency Pair is created:

PLUS(s(s(s(x''''))), y'''') -> PLUS(s(s(x'''')), y'''')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 5
Polynomial Ordering
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:

PLUS(s(s(s(x''''))), y'''') -> PLUS(s(s(x'''')), y'''')


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

PLUS(s(s(s(x''''))), y'''') -> PLUS(s(s(x'''')), y'''')


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(PLUS(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 6
Dependency Graph
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Narrowing Transformation
       →DP Problem 3
Nar


Dependency Pairs:

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
one new Dependency Pair is created:

MINUS(minus(x, s(x'')), z') -> MINUS(x, s(plus(x'', z')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pair:

MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

MINUS(s(x), s(y)) -> MINUS(x, y)
one new Dependency Pair is created:

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
FwdInst
             ...
               →DP Problem 8
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pair:

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))
one new Dependency Pair is created:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
FwdInst
             ...
               →DP Problem 9
Polynomial Ordering
       →DP Problem 3
Nar


Dependency Pair:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))


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(MINUS(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
FwdInst
             ...
               →DP Problem 10
Dependency Graph
       →DP Problem 3
Nar


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Narrowing Transformation


Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
three new Dependency Pairs are created:

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))
QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
Narrowing Transformation


Dependency Pairs:

QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))
QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))
QUOT(s(x''), s(0)) -> QUOT(x'', s(0))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

QUOT(s(s(x'')), s(s(y''))) -> QUOT(minus(x'', y''), s(s(y'')))
three new Dependency Pairs are created:

QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
Nar
             ...
               →DP Problem 12
Narrowing Transformation


Dependency Pairs:

QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

QUOT(s(minus(x'', y'')), s(y0)) -> QUOT(minus(x'', plus(y'', y0)), s(y0))
one new Dependency Pair is created:

QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
Nar
             ...
               →DP Problem 13
Forward Instantiation Transformation


Dependency Pairs:

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




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

QUOT(s(x''), s(0)) -> QUOT(x'', s(0))
two new Dependency Pairs are created:

QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))
QUOT(s(s(minus(x'''', s(x'0')))), s(0)) -> QUOT(s(minus(x'''', s(x'0'))), s(0))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
Nar
             ...
               →DP Problem 14
Polynomial Ordering


Dependency Pairs:

QUOT(s(s(minus(x'''', s(x'0')))), s(0)) -> QUOT(s(minus(x'''', s(x'0'))), s(0))
QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

QUOT(s(s(minus(x'''', s(x'0')))), s(0)) -> QUOT(s(minus(x'''', s(x'0'))), s(0))
QUOT(s(s(x'''')), s(0)) -> QUOT(s(x''''), s(0))
QUOT(s(s(s(x'))), s(s(s(y')))) -> QUOT(minus(x', y'), s(s(s(y'))))
QUOT(s(s(minus(x', y'))), s(s(y'''))) -> QUOT(minus(x', plus(y', y''')), s(s(y''')))
QUOT(s(s(x''')), s(s(0))) -> QUOT(x''', s(s(0)))
QUOT(s(minus(x'', s(x'))), s(y0')) -> QUOT(minus(x'', s(plus(x', y0'))), s(y0'))


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

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  1 + x1  
  POL(QUOT(x1, x2))=  x1 + x2  
  POL(0)=  1  
  POL(minus(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
Nar
             ...
               →DP Problem 15
Dependency Graph


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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