R
↳Dependency Pair Analysis
+'(0(x), 0(y)) > 0'(+(x, y))
+'(0(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
+'(1(x), 0(y)) > +'(x, y)
+'(1(x), 1(y)) > 0'(+(+(x, y), 1(#)))
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(1(x), 1(y)) > +'(x, y)
+'(+(x, y), z) > +'(x, +(y, z))
+'(+(x, y), z) > +'(y, z)
*'(0(x), y) > 0'(*(x, y))
*'(0(x), y) > *'(x, y)
*'(1(x), y) > +'(0(*(x, y)), y)
*'(1(x), y) > 0'(*(x, y))
*'(1(x), y) > *'(x, y)
*'(*(x, y), z) > *'(x, *(y, z))
*'(*(x, y), z) > *'(y, z)
SUM(nil) > 0'(#)
SUM(cons(x, l)) > +'(x, sum(l))
SUM(cons(x, l)) > SUM(l)
PROD(cons(x, l)) > *'(x, prod(l))
PROD(cons(x, l)) > PROD(l)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(1(x), 1(y)) > +'(x, y)
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
+'(0(x), 0(y)) > +'(x, y)
0(#) > #
+(x, #) > x
+(#, x) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
*(#, x) > #
*(0(x), y) > 0(*(x, y))
*(1(x), y) > +(0(*(x, y)), y)
*(*(x, y), z) > *(x, *(y, z))
sum(nil) > 0(#)
sum(cons(x, l)) > +(x, sum(l))
prod(nil) > 1(#)
prod(cons(x, l)) > *(x, prod(l))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 5
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(1(x), 1(y)) > +'(x, y)
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
+'(0(x), 0(y)) > +'(x, y)
+(x, #) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(#, x) > x
+(+(x, y), z) > +(x, +(y, z))
+(1(x), 0(y)) > 1(+(x, y))
0(#) > #
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(x, #) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(#, x) > x
+(+(x, y), z) > +(x, +(y, z))
+(1(x), 0(y)) > 1(+(x, y))
0(#) > #
_{ }^{ }POL(#) = 0_{ }^{ } _{ }^{ }POL(0(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL(1(x_{1})) = 1 + x_{1}_{ }^{ } _{ }^{ }POL(+(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ }
+'(1(x), 1(y)) > +'(x, y)
+'(1(x), 1(y)) > +'(+(x, y), 1(#))
+'(1(x), 0(y)) > +'(x, y)
+'(0(x), 1(y)) > +'(x, y)
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 5
↳MRR
...
→DP Problem 6
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+'(0(x), 0(y)) > +'(x, y)
+(x, #) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(#, x) > x
+(+(x, y), z) > +(x, +(y, z))
+(1(x), 0(y)) > 1(+(x, y))
0(#) > #
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(x, #) > x
0(#) > #
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(#, x) > x
+(+(x, y), z) > +(x, +(y, z))
+(1(x), 0(y)) > 1(+(x, y))
_{ }^{ }POL(#) = 0_{ }^{ } _{ }^{ }POL(0(x_{1})) = 1 + x_{1}_{ }^{ } _{ }^{ }POL(1(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL(+(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ }
+'(0(x), 0(y)) > +'(x, y)
0(#) > #
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 5
↳MRR
...
→DP Problem 7
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+(x, #) > x
+(#, x) > x
+(+(x, y), z) > +(x, +(y, z))
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(x, #) > x
+(#, x) > x
+(+(x, y), z) > +(x, +(y, z))
_{ }^{ }POL(#) = 0_{ }^{ } _{ }^{ }POL(+(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ }
+(x, #) > x
+(#, x) > x
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 5
↳MRR
...
→DP Problem 8
↳Modular Removal of Rules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
+'(+(x, y), z) > +'(y, z)
+'(+(x, y), z) > +'(x, +(y, z))
+(+(x, y), z) > +(x, +(y, z))
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
+(+(x, y), z) > +(x, +(y, z))
_{ }^{ }POL(+(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(+'(x_{1}, x_{2})) = 1 + x_{1} + x_{2}_{ }^{ }
+'(+(x, y), z) > +'(y, z)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 5
↳MRR
...
→DP Problem 9
↳Dependency Graph
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
+'(+(x, y), z) > +'(x, +(y, z))
+(+(x, y), z) > +(x, +(y, z))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
*'(*(x, y), z) > *'(y, z)
*'(1(x), y) > *'(x, y)
*'(0(x), y) > *'(x, y)
0(#) > #
+(x, #) > x
+(#, x) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
*(#, x) > #
*(0(x), y) > 0(*(x, y))
*(1(x), y) > +(0(*(x, y)), y)
*(*(x, y), z) > *(x, *(y, z))
sum(nil) > 0(#)
sum(cons(x, l)) > +(x, sum(l))
prod(nil) > 1(#)
prod(cons(x, l)) > *(x, prod(l))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 10
↳SizeChange Principle
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
*'(*(x, y), z) > *'(y, z)
*'(1(x), y) > *'(x, y)
*'(0(x), y) > *'(x, y)
none
innermost


trivial
0(x_{1}) > 0(x_{1})
1(x_{1}) > 1(x_{1})
*(x_{1}, x_{2}) > *(x_{1}, x_{2})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
→DP Problem 4
↳UsableRules
SUM(cons(x, l)) > SUM(l)
0(#) > #
+(x, #) > x
+(#, x) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
*(#, x) > #
*(0(x), y) > 0(*(x, y))
*(1(x), y) > +(0(*(x, y)), y)
*(*(x, y), z) > *(x, *(y, z))
sum(nil) > 0(#)
sum(cons(x, l)) > +(x, sum(l))
prod(nil) > 1(#)
prod(cons(x, l)) > *(x, prod(l))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 11
↳SizeChange Principle
→DP Problem 4
↳UsableRules
SUM(cons(x, l)) > SUM(l)
none
innermost


trivial
cons(x_{1}, x_{2}) > cons(x_{1}, x_{2})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳Usable Rules (Innermost)
PROD(cons(x, l)) > PROD(l)
0(#) > #
+(x, #) > x
+(#, x) > x
+(0(x), 0(y)) > 0(+(x, y))
+(0(x), 1(y)) > 1(+(x, y))
+(1(x), 0(y)) > 1(+(x, y))
+(1(x), 1(y)) > 0(+(+(x, y), 1(#)))
+(+(x, y), z) > +(x, +(y, z))
*(#, x) > #
*(0(x), y) > 0(*(x, y))
*(1(x), y) > +(0(*(x, y)), y)
*(*(x, y), z) > *(x, *(y, z))
sum(nil) > 0(#)
sum(cons(x, l)) > +(x, sum(l))
prod(nil) > 1(#)
prod(cons(x, l)) > *(x, prod(l))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 12
↳SizeChange Principle
PROD(cons(x, l)) > PROD(l)
none
innermost


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