R
↳Dependency Pair Analysis
+'(a, b) > +'(b, a)
+'(a, +(b, z)) > +'(b, +(a, z))
+'(a, +(b, z)) > +'(a, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(+(x, y), z) > +'(y, z)
F(+(x, y), z) > +'(f(x, z), f(y, z))
F(+(x, y), z) > F(x, z)
F(+(x, y), z) > F(y, z)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
+'(a, +(b, z)) > +'(a, z)
+(a, b) > +(b, a)
+(a, +(b, z)) > +(b, +(a, z))
+(+(x, y), z) > +(x, +(y, z))
f(a, y) > a
f(b, y) > b
f(+(x, y), z) > +(f(x, z), f(y, z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳ATransformation
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
+'(a, +(b, z)) > +'(a, z)
none
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳ATrans
...
→DP Problem 5
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
A(b(z)) > A(z)
none
innermost


trivial
b(x_{1}) > b(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
+'(+(x, y), z) > +'(y, z)
+(a, b) > +(b, a)
+(a, +(b, z)) > +(b, +(a, z))
+(+(x, y), z) > +(x, +(y, z))
f(a, y) > a
f(b, y) > b
f(+(x, y), z) > +(f(x, z), f(y, z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 6
↳SizeChange Principle
→DP Problem 3
↳UsableRules
+'(+(x, y), z) > +'(y, z)
none
innermost


trivial
+(x_{1}, x_{2}) > +(x_{1}, x_{2})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
F(+(x, y), z) > F(y, z)
+(a, b) > +(b, a)
+(a, +(b, z)) > +(b, +(a, z))
+(+(x, y), z) > +(x, +(y, z))
f(a, y) > a
f(b, y) > b
f(+(x, y), z) > +(f(x, z), f(y, z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 7
↳SizeChange Principle
F(+(x, y), z) > F(y, z)
none
innermost


trivial
+(x_{1}, x_{2}) > +(x_{1}, x_{2})