Term Rewriting System R:
[x, y]
minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(+(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(y)
F(minus(x)) -> MINUS(minus(minus(f(x))))
F(minus(x)) -> MINUS(minus(f(x)))
F(minus(x)) -> MINUS(f(x))
F(minus(x)) -> F(x)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Narrowing Transformation


Dependency Pairs:

MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(minus(minus(x)))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(+(x, y)) -> MINUS(minus(minus(x)))
four new Dependency Pairs are created:

MINUS(+(x'', y)) -> MINUS(x'')
MINUS(+(minus(x''), y)) -> MINUS(minus(x''))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Narrowing Transformation


Dependency Pairs:

MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(y)


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(+(x, y)) -> MINUS(minus(x))
three new Dependency Pairs are created:

MINUS(+(minus(x''), y)) -> MINUS(x'')
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 3
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(minus(minus(y)))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(+(x, y)) -> MINUS(minus(minus(y)))
four new Dependency Pairs are created:

MINUS(+(x, y')) -> MINUS(y')
MINUS(+(x, minus(x''))) -> MINUS(minus(x''))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 4
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, y')) -> MINUS(y')
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(minus(y))
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(+(x, y)) -> MINUS(minus(y))
three new Dependency Pairs are created:

MINUS(+(x, minus(x''))) -> MINUS(x'')
MINUS(+(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 5
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(+(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, y')) -> MINUS(y')
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(*(x, y)) -> MINUS(minus(minus(x)))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(*(x, y)) -> MINUS(minus(minus(x)))
four new Dependency Pairs are created:

MINUS(*(x'', y)) -> MINUS(x'')
MINUS(*(minus(x''), y)) -> MINUS(minus(x''))
MINUS(*(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(*(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 6
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(*(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(*(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, y')) -> MINUS(y')
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x'', y)) -> MINUS(x'')
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(*(x, y)) -> MINUS(minus(x))
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(x)
MINUS(+(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(*(x, y)) -> MINUS(minus(x))
three new Dependency Pairs are created:

MINUS(*(minus(x''), y)) -> MINUS(x'')
MINUS(*(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 7
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(*(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, y')) -> MINUS(y')
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x'', y)) -> MINUS(x'')
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(minus(minus(y)))
MINUS(*(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(x)
MINUS(*(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(*(x, y)) -> MINUS(minus(minus(y)))
four new Dependency Pairs are created:

MINUS(*(x, y')) -> MINUS(y')
MINUS(*(x, minus(x''))) -> MINUS(minus(x''))
MINUS(*(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(*(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 8
                 ↳Narrowing Transformation


Dependency Pairs:

MINUS(*(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(*(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(*(x, y')) -> MINUS(y')
MINUS(*(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, y')) -> MINUS(y')
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x'', y)) -> MINUS(x'')
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(minus(y))
MINUS(*(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(x)
MINUS(*(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost




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

MINUS(*(x, y)) -> MINUS(minus(y))
three new Dependency Pairs are created:

MINUS(*(x, minus(x''))) -> MINUS(x'')
MINUS(*(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳Nar
           →DP Problem 2
             ↳Nar
             ...
               →DP Problem 9
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MINUS(*(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(*(x, y')) -> MINUS(y')
MINUS(*(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, *(x'', y''))) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, +(x'', y''))) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x, y')) -> MINUS(y')
MINUS(+(*(x'', y''), y)) -> MINUS(+(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(*(x'', y)) -> MINUS(x'')
MINUS(+(+(x'', y''), y)) -> MINUS(*(minus(minus(minus(x''))), minus(minus(minus(y'')))))
MINUS(+(*(x'', y''), y)) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(+(x'', y''), y)) -> MINUS(minus(*(minus(minus(minus(x''))), minus(minus(minus(y''))))))
MINUS(+(x'', y)) -> MINUS(x'')
MINUS(*(x, y)) -> MINUS(y)
MINUS(*(x, y)) -> MINUS(x)
MINUS(+(x, y)) -> MINUS(y)
MINUS(+(x, y)) -> MINUS(x)
MINUS(*(x, *(x'', y''))) -> MINUS(minus(+(minus(minus(minus(x''))), minus(minus(minus(y''))))))


Rules:


minus(minus(x)) -> x
minus(+(x, y)) -> *(minus(minus(minus(x))), minus(minus(minus(y))))
minus(*(x, y)) -> +(minus(minus(minus(x))), minus(minus(minus(y))))
f(minus(x)) -> minus(minus(minus(f(x))))


Strategy:

innermost



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