R
↳Dependency Pair Analysis
APP(app(*, x), app(app(+, y), z)) -> APP(app(+, app(app(*, x), y)), app(app(*, x), z))
APP(app(*, x), app(app(+, y), z)) -> APP(+, app(app(*, x), y))
APP(app(*, x), app(app(+, y), z)) -> APP(app(*, x), y)
APP(app(*, x), app(app(+, y), z)) -> APP(app(*, x), z)
APP(app(*, app(app(+, y), z)), x) -> APP(app(+, app(app(*, x), y)), app(app(*, x), z))
APP(app(*, app(app(+, y), z)), x) -> APP(+, app(app(*, x), y))
APP(app(*, app(app(+, y), z)), x) -> APP(app(*, x), y)
APP(app(*, app(app(+, y), z)), x) -> APP(*, x)
APP(app(*, app(app(+, y), z)), x) -> APP(app(*, x), z)
APP(app(*, app(app(*, x), y)), z) -> APP(app(*, x), app(app(*, y), z))
APP(app(*, app(app(*, x), y)), z) -> APP(app(*, y), z)
APP(app(*, app(app(*, x), y)), z) -> APP(*, y)
APP(app(+, app(app(+, x), y)), z) -> APP(app(+, x), app(app(+, y), z))
APP(app(+, app(app(+, x), y)), z) -> APP(app(+, y), z)
APP(app(+, app(app(+, x), y)), z) -> APP(+, y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳ATrans
APP(app(+, app(app(+, x), y)), z) -> APP(app(+, y), z)
app(app(*, x), app(app(+, y), z)) -> app(app(+, app(app(*, x), y)), app(app(*, x), z))
app(app(*, app(app(+, y), z)), x) -> app(app(+, app(app(*, x), y)), app(app(*, x), z))
app(app(*, app(app(*, x), y)), z) -> app(app(*, x), app(app(*, y), z))
app(app(+, app(app(+, x), y)), z) -> app(app(+, x), app(app(+, y), z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳A-Transformation
→DP Problem 2
↳ATrans
APP(app(+, app(app(+, x), y)), z) -> APP(app(+, y), z)
none
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳ATrans
...
→DP Problem 4
↳Size-Change Principle
→DP Problem 2
↳ATrans
+'(+(x, y), z) -> +'(y, z)
none
innermost
|
|
trivial
+(x1, x2) -> +(x1, x2)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳A-Transformation
APP(app(*, app(app(*, x), y)), z) -> APP(app(*, y), z)
APP(app(*, app(app(*, x), y)), z) -> APP(app(*, x), app(app(*, y), z))
APP(app(*, x), app(app(+, y), z)) -> APP(app(*, x), z)
APP(app(*, app(app(+, y), z)), x) -> APP(app(*, x), z)
APP(app(*, app(app(+, y), z)), x) -> APP(app(*, x), y)
APP(app(*, x), app(app(+, y), z)) -> APP(app(*, x), y)
app(app(*, x), app(app(+, y), z)) -> app(app(+, app(app(*, x), y)), app(app(*, x), z))
app(app(*, app(app(+, y), z)), x) -> app(app(+, app(app(*, x), y)), app(app(*, x), z))
app(app(*, app(app(*, x), y)), z) -> app(app(*, x), app(app(*, y), z))
app(app(+, app(app(+, x), y)), z) -> app(app(+, x), app(app(+, y), z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳ATrans
→DP Problem 5
↳Narrowing Transformation
*'(*(x, y), z) -> *'(y, z)
*'(*(x, y), z) -> *'(x, *(y, z))
*'(x, +(y, z)) -> *'(x, z)
*'(+(y, z), x) -> *'(x, z)
*'(+(y, z), x) -> *'(x, y)
*'(x, +(y, z)) -> *'(x, y)
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(y, z), x) -> +(*(x, y), *(x, z))
*(*(x, y), z) -> *(x, *(y, z))
+(+(x, y), z) -> +(x, +(y, z))
innermost
two new Dependency Pairs are created:
*'(*(x, y), z) -> *'(x, *(y, z))
*'(*(x, y0), +(y'', z'')) -> *'(x, +(*(y0, y''), *(y0, z'')))
*'(*(x, *(x'', y'')), z'') -> *'(x, *(x'', *(y'', z'')))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳ATrans
→DP Problem 5
↳Nar
...
→DP Problem 6
↳Polynomial Ordering
*'(*(x, *(x'', y'')), z'') -> *'(x, *(x'', *(y'', z'')))
*'(*(x, y0), +(y'', z'')) -> *'(x, +(*(y0, y''), *(y0, z'')))
*'(x, +(y, z)) -> *'(x, z)
*'(+(y, z), x) -> *'(x, z)
*'(+(y, z), x) -> *'(x, y)
*'(x, +(y, z)) -> *'(x, y)
*'(*(x, y), z) -> *'(y, z)
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(y, z), x) -> +(*(x, y), *(x, z))
*(*(x, y), z) -> *(x, *(y, z))
+(+(x, y), z) -> +(x, +(y, z))
innermost
*'(x, +(y, z)) -> *'(x, z)
*'(+(y, z), x) -> *'(x, z)
*'(+(y, z), x) -> *'(x, y)
*'(x, +(y, z)) -> *'(x, y)
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(*(x, y), z) -> *(x, *(y, z))
*(+(y, z), x) -> +(*(x, y), *(x, z))
+(+(x, y), z) -> +(x, +(y, z))
POL(*'(x1, x2)) = x1 + x1·x2 + x2 POL(*(x1, x2)) = x1 + x1·x2 + x2 POL(+(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳ATrans
→DP Problem 5
↳Nar
...
→DP Problem 7
↳Dependency Graph
*'(*(x, *(x'', y'')), z'') -> *'(x, *(x'', *(y'', z'')))
*'(*(x, y0), +(y'', z'')) -> *'(x, +(*(y0, y''), *(y0, z'')))
*'(*(x, y), z) -> *'(y, z)
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(y, z), x) -> +(*(x, y), *(x, z))
*(*(x, y), z) -> *(x, *(y, z))
+(+(x, y), z) -> +(x, +(y, z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳ATrans
→DP Problem 5
↳Nar
...
→DP Problem 8
↳Usable Rules (Innermost)
*'(*(x, y), z) -> *'(y, z)
*(x, +(y, z)) -> +(*(x, y), *(x, z))
*(+(y, z), x) -> +(*(x, y), *(x, z))
*(*(x, y), z) -> *(x, *(y, z))
+(+(x, y), z) -> +(x, +(y, z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳ATrans
→DP Problem 5
↳Nar
...
→DP Problem 9
↳Size-Change Principle
*'(*(x, y), z) -> *'(y, z)
none
innermost
|
|
trivial
*(x1, x2) -> *(x1, x2)