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

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

P(p(s(x))) -> P(x)
LE(p(s(x)), x) -> LE(x, x)
LE(s(x), s(y)) -> LE(x, y)
MINUS(x, y) -> IF(le(x, y), x, y)
MINUS(x, y) -> LE(x, y)
IF(false, x, y) -> MINUS(p(x), y)
IF(false, x, y) -> P(x)

Furthermore, R contains two SCCs. 


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


Dependency Pair:

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


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem: 



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


Dependency Pair:

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


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 3
             ↳FwdInst
             ...
               →DP Problem 4
                 ↳Argument Filtering and Ordering
       →DP Problem 2
         ↳Nar


Dependency Pair:

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


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
LE(x1, x2) -> LE(x1, x2)
s(x1) -> s(x1)


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 3
             ↳FwdInst
             ...
               →DP Problem 5
                 ↳Dependency Graph
       →DP Problem 2
         ↳Nar


Dependency Pair:


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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


Dependency Pairs:

IF(false, x, y) -> MINUS(p(x), y)
MINUS(x, y) -> IF(le(x, y), x, y)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

MINUS(x, y) -> IF(le(x, y), x, y)
three new Dependency Pairs are created:

MINUS(0, y'') -> IF(true, 0, y'')
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), 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 6
             ↳Narrowing Transformation


Dependency Pairs:

MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
MINUS(s(x''), 0) -> IF(false, s(x''), 0)
IF(false, x, y) -> MINUS(p(x), y)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

IF(false, x, y) -> MINUS(p(x), y)
two new Dependency Pairs are created:

IF(false, 0, y) -> MINUS(s(s(0)), y)
IF(false, s(x''), y) -> MINUS(x'', y)

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

MINUS(s(x''), 0) -> IF(false, s(x''), 0)
IF(false, s(x''), y) -> MINUS(x'', y)
MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

MINUS(s(x''), s(y'')) -> IF(le(x'', y''), s(x''), s(y''))
three new Dependency Pairs are created:

MINUS(s(0), s(y''')) -> IF(true, s(0), s(y'''))
MINUS(s(s(x')), s(0)) -> IF(false, s(s(x')), s(0))
MINUS(s(s(x')), s(s(y'))) -> IF(le(x', y'), 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 6
             ↳Nar
             ...
               →DP Problem 8
                 ↳Instantiation Transformation


Dependency Pairs:

MINUS(s(s(x')), s(s(y'))) -> IF(le(x', y'), s(s(x')), s(s(y')))
MINUS(s(s(x')), s(0)) -> IF(false, s(s(x')), s(0))
IF(false, s(x''), y) -> MINUS(x'', y)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

IF(false, s(x''), y) -> MINUS(x'', y)
three new Dependency Pairs are created:

IF(false, s(x''''), 0) -> MINUS(x'''', 0)
IF(false, s(s(x'''')), s(0)) -> MINUS(s(x''''), s(0))
IF(false, s(s(x'''')), s(s(y'''))) -> MINUS(s(x''''), s(s(y''')))

The transformation is resulting in three new DP problems: 



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


Dependency Pairs:

IF(false, s(s(x'''')), s(s(y'''))) -> MINUS(s(x''''), s(s(y''')))
MINUS(s(s(x')), s(s(y'))) -> IF(le(x', y'), s(s(x')), s(s(y')))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

MINUS(s(s(x')), s(s(y'))) -> IF(le(x', y'), s(s(x')), s(s(y')))
three new Dependency Pairs are created:

MINUS(s(s(0)), s(s(y''))) -> IF(true, s(s(0)), s(s(y'')))
MINUS(s(s(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))
MINUS(s(s(s(x''))), s(s(s(y'')))) -> IF(le(x'', y''), s(s(s(x''))), s(s(s(y''))))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

MINUS(s(s(s(x''))), s(s(s(y'')))) -> IF(le(x'', y''), s(s(s(x''))), s(s(s(y''))))
MINUS(s(s(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))
IF(false, s(s(x'''')), s(s(y'''))) -> MINUS(s(x''''), s(s(y''')))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

MINUS(s(s(s(x''))), s(s(s(y'')))) -> IF(le(x'', y''), s(s(s(x''))), s(s(s(y''))))
three new Dependency Pairs are created:

MINUS(s(s(s(0))), s(s(s(y''')))) -> IF(true, s(s(s(0))), s(s(s(y'''))))
MINUS(s(s(s(s(x')))), s(s(s(0)))) -> IF(false, s(s(s(s(x')))), s(s(s(0))))
MINUS(s(s(s(s(x')))), s(s(s(s(y'))))) -> IF(le(x', y'), s(s(s(s(x')))), s(s(s(s(y')))))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

MINUS(s(s(s(s(x')))), s(s(s(s(y'))))) -> IF(le(x', y'), s(s(s(s(x')))), s(s(s(s(y')))))
MINUS(s(s(s(s(x')))), s(s(s(0)))) -> IF(false, s(s(s(s(x')))), s(s(s(0))))
IF(false, s(s(x'''')), s(s(y'''))) -> MINUS(s(x''''), s(s(y''')))
MINUS(s(s(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

MINUS(s(s(s(s(x')))), s(s(s(s(y'))))) -> IF(le(x', y'), s(s(s(s(x')))), s(s(s(s(y')))))
three new Dependency Pairs are created:

MINUS(s(s(s(s(0)))), s(s(s(s(y''))))) -> IF(true, s(s(s(s(0)))), s(s(s(s(y'')))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(0))))) -> IF(false, s(s(s(s(s(x''))))), s(s(s(s(0)))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(s(y'')))))) -> IF(le(x'', y''), s(s(s(s(s(x''))))), s(s(s(s(s(y''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 16
                 ↳Instantiation Transformation


Dependency Pairs:

MINUS(s(s(s(s(s(x''))))), s(s(s(s(s(y'')))))) -> IF(le(x'', y''), s(s(s(s(s(x''))))), s(s(s(s(s(y''))))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(0))))) -> IF(false, s(s(s(s(s(x''))))), s(s(s(s(0)))))
MINUS(s(s(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))
IF(false, s(s(x'''')), s(s(y'''))) -> MINUS(s(x''''), s(s(y''')))
MINUS(s(s(s(s(x')))), s(s(s(0)))) -> IF(false, s(s(s(s(x')))), s(s(s(0))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

IF(false, s(s(x'''')), s(s(y'''))) -> MINUS(s(x''''), s(s(y''')))
four new Dependency Pairs are created:

IF(false, s(s(s(x'''''))), s(s(0))) -> MINUS(s(s(x''''')), s(s(0)))
IF(false, s(s(s(s(x''')))), s(s(s(0)))) -> MINUS(s(s(s(x'''))), s(s(s(0))))
IF(false, s(s(s(s(s(x'''''))))), s(s(s(s(0))))) -> MINUS(s(s(s(s(x''''')))), s(s(s(s(0)))))
IF(false, s(s(s(s(s(x'''''))))), s(s(s(s(s(y''''')))))) -> MINUS(s(s(s(s(x''''')))), s(s(s(s(s(y'''''))))))

The transformation is resulting in four new DP problems: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 17
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(s(s(x'''''))))), s(s(s(s(s(y''''')))))) -> MINUS(s(s(s(s(x''''')))), s(s(s(s(s(y'''''))))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(s(y'')))))) -> IF(le(x'', y''), s(s(s(s(s(x''))))), s(s(s(s(s(y''))))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

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

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 21
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

IF(false, s(s(s(s(s(s(x'''')))))), s(s(s(s(s(y'''''')))))) -> MINUS(s(s(s(s(s(x''''))))), s(s(s(s(s(y''''''))))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(s(y'')))))) -> IF(le(x'', y''), s(s(s(s(s(x''))))), s(s(s(s(s(y''))))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 18
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(s(s(x'''''))))), s(s(s(s(0))))) -> MINUS(s(s(s(s(x''''')))), s(s(s(s(0)))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(0))))) -> IF(false, s(s(s(s(s(x''))))), s(s(s(s(0)))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

IF(false, s(s(s(s(s(s(x'''')))))), s(s(s(s(0))))) -> MINUS(s(s(s(s(s(x''''))))), s(s(s(s(0)))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 22
                 ↳Argument Filtering and Ordering


Dependency Pairs:

IF(false, s(s(s(s(s(s(x'''')))))), s(s(s(s(0))))) -> MINUS(s(s(s(s(s(x''''))))), s(s(s(s(0)))))
MINUS(s(s(s(s(s(x''))))), s(s(s(s(0))))) -> IF(false, s(s(s(s(s(x''))))), s(s(s(s(0)))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

IF(false, s(s(s(s(s(s(x'''')))))), s(s(s(s(0))))) -> MINUS(s(s(s(s(s(x''''))))), s(s(s(s(0)))))


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> x1
s(x1) -> s(x1)
IF(x1, x2, x3) -> x2


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 30
                 ↳Dependency Graph


Dependency Pair:

MINUS(s(s(s(s(s(x''))))), s(s(s(s(0))))) -> IF(false, s(s(s(s(s(x''))))), s(s(s(s(0)))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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 6
             ↳Nar
             ...
               →DP Problem 19
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(x'''''))), s(s(0))) -> MINUS(s(s(x''''')), s(s(0)))
MINUS(s(s(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

IF(false, s(s(s(s(x'''')))), s(s(0))) -> MINUS(s(s(s(x''''))), s(s(0)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 23
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(s(x'''')))), s(s(0))) -> MINUS(s(s(s(x''''))), s(s(0)))
MINUS(s(s(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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(s(x''))), s(s(0))) -> IF(false, s(s(s(x''))), s(s(0)))
one new Dependency Pair is created:

MINUS(s(s(s(s(x'''''')))), s(s(0))) -> IF(false, s(s(s(s(x'''''')))), s(s(0)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 25
                 ↳Forward Instantiation Transformation


Dependency Pairs:

MINUS(s(s(s(s(x'''''')))), s(s(0))) -> IF(false, s(s(s(s(x'''''')))), s(s(0)))
IF(false, s(s(s(s(x'''')))), s(s(0))) -> MINUS(s(s(s(x''''))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

IF(false, s(s(s(s(s(x''''''''))))), s(s(0))) -> MINUS(s(s(s(s(x'''''''')))), s(s(0)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 27
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(s(s(x''''''''))))), s(s(0))) -> MINUS(s(s(s(s(x'''''''')))), s(s(0)))
MINUS(s(s(s(s(x'''''')))), s(s(0))) -> IF(false, s(s(s(s(x'''''')))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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(s(s(x'''''')))), s(s(0))) -> IF(false, s(s(s(s(x'''''')))), s(s(0)))
one new Dependency Pair is created:

MINUS(s(s(s(s(s(x''''''''''))))), s(s(0))) -> IF(false, s(s(s(s(s(x''''''''''))))), s(s(0)))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 29
                 ↳Argument Filtering and Ordering


Dependency Pairs:

MINUS(s(s(s(s(s(x''''''''''))))), s(s(0))) -> IF(false, s(s(s(s(s(x''''''''''))))), s(s(0)))
IF(false, s(s(s(s(s(x''''''''))))), s(s(0))) -> MINUS(s(s(s(s(x'''''''')))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

IF(false, s(s(s(s(s(x''''''''))))), s(s(0))) -> MINUS(s(s(s(s(x'''''''')))), s(s(0)))


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> x1
s(x1) -> s(x1)
IF(x1, x2, x3) -> x2


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 32
                 ↳Dependency Graph


Dependency Pair:

MINUS(s(s(s(s(s(x''''''''''))))), s(s(0))) -> IF(false, s(s(s(s(s(x''''''''''))))), s(s(0)))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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 6
             ↳Nar
             ...
               →DP Problem 20
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(s(x''')))), s(s(s(0)))) -> MINUS(s(s(s(x'''))), s(s(s(0))))
MINUS(s(s(s(s(x')))), s(s(s(0)))) -> IF(false, s(s(s(s(x')))), s(s(s(0))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

IF(false, s(s(s(s(s(x''''))))), s(s(s(0)))) -> MINUS(s(s(s(s(x'''')))), s(s(s(0))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 24
                 ↳Forward Instantiation Transformation


Dependency Pairs:

IF(false, s(s(s(s(s(x''''))))), s(s(s(0)))) -> MINUS(s(s(s(s(x'''')))), s(s(s(0))))
MINUS(s(s(s(s(x')))), s(s(s(0)))) -> IF(false, s(s(s(s(x')))), s(s(s(0))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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(s(s(x')))), s(s(s(0)))) -> IF(false, s(s(s(s(x')))), s(s(s(0))))
one new Dependency Pair is created:

MINUS(s(s(s(s(s(x''''''))))), s(s(s(0)))) -> IF(false, s(s(s(s(s(x''''''))))), s(s(s(0))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 26
                 ↳Forward Instantiation Transformation


Dependency Pairs:

MINUS(s(s(s(s(s(x''''''))))), s(s(s(0)))) -> IF(false, s(s(s(s(s(x''''''))))), s(s(s(0))))
IF(false, s(s(s(s(s(x''''))))), s(s(s(0)))) -> MINUS(s(s(s(s(x'''')))), s(s(s(0))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




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

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

IF(false, s(s(s(s(s(s(x'''''''')))))), s(s(s(0)))) -> MINUS(s(s(s(s(s(x''''''''))))), s(s(s(0))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 28
                 ↳Argument Filtering and Ordering


Dependency Pairs:

IF(false, s(s(s(s(s(s(x'''''''')))))), s(s(s(0)))) -> MINUS(s(s(s(s(s(x''''''''))))), s(s(s(0))))
MINUS(s(s(s(s(s(x''''''))))), s(s(s(0)))) -> IF(false, s(s(s(s(s(x''''''))))), s(s(s(0))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

IF(false, s(s(s(s(s(s(x'''''''')))))), s(s(s(0)))) -> MINUS(s(s(s(s(s(x''''''''))))), s(s(s(0))))


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> x1
s(x1) -> s(x1)
IF(x1, x2, x3) -> x2


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 31
                 ↳Dependency Graph


Dependency Pair:

MINUS(s(s(s(s(s(x''''''))))), s(s(s(0)))) -> IF(false, s(s(s(s(s(x''''''))))), s(s(s(0))))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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 6
             ↳Nar
             ...
               →DP Problem 10
                 ↳Argument Filtering and Ordering


Dependency Pairs:

IF(false, s(s(x'''')), s(0)) -> MINUS(s(x''''), s(0))
MINUS(s(s(x')), s(0)) -> IF(false, s(s(x')), s(0))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

IF(false, s(s(x'''')), s(0)) -> MINUS(s(x''''), s(0))


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> x1
s(x1) -> s(x1)
IF(x1, x2, x3) -> x2


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 12
                 ↳Dependency Graph


Dependency Pair:

MINUS(s(s(x')), s(0)) -> IF(false, s(s(x')), s(0))


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(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 6
             ↳Nar
             ...
               →DP Problem 11
                 ↳Argument Filtering and Ordering


Dependency Pairs:

IF(false, s(x''''), 0) -> MINUS(x'''', 0)
MINUS(s(x''), 0) -> IF(false, s(x''), 0)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




The following dependency pair can be strictly oriented:

IF(false, s(x''''), 0) -> MINUS(x'''', 0)


There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
IF(x1, x2, x3) -> x2
s(x1) -> s(x1)
MINUS(x1, x2) -> x1


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Nar
           →DP Problem 6
             ↳Nar
             ...
               →DP Problem 13
                 ↳Dependency Graph


Dependency Pair:

MINUS(s(x''), 0) -> IF(false, s(x''), 0)


Rules:


p(0) -> s(s(0))
p(s(x)) -> x
p(p(s(x))) -> p(x)
le(p(s(x)), x) -> le(x, x)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, y) -> if(le(x, y), x, y)
if(true, x, y) -> 0
if(false, x, y) -> s(minus(p(x), y))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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