R
↳Dependency Pair Analysis
+'(s(x), y) -> +'(x, y)
+'(p(x), y) -> +'(x, y)
MINUS(s(x)) -> MINUS(x)
MINUS(p(x)) -> MINUS(x)
*'(s(x), y) -> +'(*(x, y), y)
*'(s(x), y) -> *'(x, y)
*'(p(x), y) -> +'(*(x, y), minus(y))
*'(p(x), y) -> *'(x, y)
*'(p(x), y) -> MINUS(y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
+'(p(x), y) -> +'(x, y)
+'(s(x), y) -> +'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(p(x), y) -> p(+(x, y))
minus(0) -> 0
minus(s(x)) -> p(minus(x))
minus(p(x)) -> s(minus(x))
*(0, y) -> 0
*(s(x), y) -> +(*(x, y), y)
*(p(x), y) -> +(*(x, y), minus(y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳Size-Change Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
+'(p(x), y) -> +'(x, y)
+'(s(x), y) -> +'(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
p(x1) -> p(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
MINUS(p(x)) -> MINUS(x)
MINUS(s(x)) -> MINUS(x)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(p(x), y) -> p(+(x, y))
minus(0) -> 0
minus(s(x)) -> p(minus(x))
minus(p(x)) -> s(minus(x))
*(0, y) -> 0
*(s(x), y) -> +(*(x, y), y)
*(p(x), y) -> +(*(x, y), minus(y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 5
↳Size-Change Principle
→DP Problem 3
↳UsableRules
MINUS(p(x)) -> MINUS(x)
MINUS(s(x)) -> MINUS(x)
none
innermost
|
|
trivial
s(x1) -> s(x1)
p(x1) -> p(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
*'(p(x), y) -> *'(x, y)
*'(s(x), y) -> *'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
+(p(x), y) -> p(+(x, y))
minus(0) -> 0
minus(s(x)) -> p(minus(x))
minus(p(x)) -> s(minus(x))
*(0, y) -> 0
*(s(x), y) -> +(*(x, y), y)
*(p(x), y) -> +(*(x, y), minus(y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Size-Change Principle
*'(p(x), y) -> *'(x, y)
*'(s(x), y) -> *'(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
p(x1) -> p(x1)