R
↳Dependency Pair Analysis
-'(s(x), s(y)) -> -'(x, y)
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x), y) -> P(-(s(x), y))
F(s(x), y) -> -'(s(x), y)
F(s(x), y) -> P(-(y, s(x)))
F(s(x), y) -> -'(y, s(x))
F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(x, s(y)) -> P(-(x, s(y)))
F(x, s(y)) -> -'(x, s(y))
F(x, s(y)) -> P(-(s(y), x))
F(x, s(y)) -> -'(s(y), x)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
-'(s(x), s(y)) -> -'(x, y)
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
p(s(x)) -> x
f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳Size-Change Principle
→DP Problem 2
↳UsableRules
-'(s(x), s(y)) -> -'(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
-(x, 0) -> x
-(s(x), s(y)) -> -(x, y)
p(s(x)) -> x
f(s(x), y) -> f(p(-(s(x), y)), p(-(y, s(x))))
f(x, s(y)) -> f(p(-(x, s(y))), p(-(s(y), x)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Narrowing Transformation
F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
three new Dependency Pairs are created:
F(x, s(y)) -> F(p(-(x, s(y))), p(-(s(y), x)))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
F(0, s(y')) -> F(p(-(0, s(y'))), p(s(y')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 5
↳Rewriting Transformation
F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
one new Dependency Pair is created:
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 6
↳Rewriting Transformation
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
one new Dependency Pair is created:
F(s(y''), s(y0)) -> F(p(-(s(y''), s(y0))), p(-(y0, y'')))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
three new Dependency Pairs are created:
F(s(x), y) -> F(p(-(s(x), y)), p(-(y, s(x))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x''), 0) -> F(p(s(x'')), p(-(0, s(x''))))
F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 8
↳Rewriting Transformation
F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
one new Dependency Pair is created:
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(s(y''), s(x''))))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 9
↳Rewriting Transformation
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
one new Dependency Pair is created:
F(s(x0), s(x'')) -> F(p(-(s(x0), s(x''))), p(-(x'', x0)))
F(s(x0), s(x'')) -> F(p(-(x0, x'')), p(-(x'', x0)))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 10
↳Negative Polynomial Order
F(s(x0), s(x'')) -> F(p(-(x0, x'')), p(-(x'', x0)))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost
F(s(x0), s(x'')) -> F(p(-(x0, x'')), p(-(x'', x0)))
F(s(y''), s(y0)) -> F(p(-(y'', y0)), p(-(y0, y'')))
F(s(x''), s(y'')) -> F(p(-(x'', y'')), p(-(y'', x'')))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
POL( F(x1, x2) ) = x2
POL( s(x1) ) = x1 + 1
POL( p(x1) ) = x1
POL( -(x1, x2) ) = x1
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Nar
...
→DP Problem 11
↳Dependency Graph
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
p(s(x)) -> x
innermost