R
↳Dependency Pair Analysis
+'(s(x), y) -> +'(x, y)
++'(:(x, xs), ys) -> ++'(xs, ys)
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
SUM(:(x, :(y, xs))) -> +'(x, y)
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))
SUM(++(xs, :(x, :(y, ys)))) -> ++'(xs, sum(:(x, :(y, ys))))
SUM(++(xs, :(x, :(y, ys)))) -> SUM(:(x, :(y, ys)))
-'(s(x), s(y)) -> -'(x, y)
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
QUOT(s(x), s(y)) -> -'(x, y)
LENGTH(:(x, xs)) -> LENGTH(xs)
AVG(xs) -> QUOT(hd(sum(xs)), length(xs))
AVG(xs) -> HD(sum(xs))
AVG(xs) -> SUM(xs)
AVG(xs) -> LENGTH(xs)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
+'(s(x), y) -> +'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 8
↳Size-Change Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
+'(s(x), y) -> +'(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
++'(:(x, xs), ys) -> ++'(xs, ys)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 9
↳Size-Change Principle
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
++'(:(x, xs), ys) -> ++'(xs, ys)
none
innermost
|
|
trivial
:(x1, x2) -> :(x1, x2)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
-'(s(x), s(y)) -> -'(x, y)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 10
↳Size-Change Principle
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
-'(s(x), s(y)) -> -'(x, y)
none
innermost
|
|
trivial
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳Usable Rules (Innermost)
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
LENGTH(:(x, xs)) -> LENGTH(xs)
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 11
↳Size-Change Principle
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
LENGTH(:(x, xs)) -> LENGTH(xs)
none
innermost
|
|
trivial
:(x1, x2) -> :(x1, x2)
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳Usable Rules (Innermost)
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 12
↳Modular Removal of Rules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
innermost
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
POL(:(x1, x2)) = x1 + x2 POL(SUM(x1)) = 1 + x1 POL(0) = 1 POL(s(x1)) = x1 POL(+(x1, x2)) = x1 + x2
+(0, y) -> y
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 12
↳MRR
...
→DP Problem 13
↳Modular Removal of Rules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
+(s(x), y) -> s(+(x, y))
innermost
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
+(s(x), y) -> s(+(x, y))
POL(:(x1, x2)) = 1 + x1 + x2 POL(SUM(x1)) = 1 + x1 POL(s(x1)) = x1 POL(+(x1, x2)) = x1 + x2
SUM(:(x, :(y, xs))) -> SUM(:(+(x, y), xs))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳Usable Rules (Innermost)
→DP Problem 7
↳UsableRules
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 14
↳Negative Polynomial Order
→DP Problem 7
↳UsableRules
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
-(0, s(y)) -> 0
innermost
QUOT(s(x), s(y)) -> QUOT(-(x, y), s(y))
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
-(0, s(y)) -> 0
POL( QUOT(x1, x2) ) = x1
POL( s(x1) ) = x1 + 1
POL( -(x1, x2) ) = x1
POL( 0 ) = 0
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 14
↳Neg POLO
...
→DP Problem 15
↳Dependency Graph
→DP Problem 7
↳UsableRules
-(s(x), s(y)) -> -(x, y)
-(x, 0) -> x
-(0, s(y)) -> 0
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳Usable Rules (Innermost)
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
++(nil, ys) -> ys
++(:(x, xs), ys) -> :(x, ++(xs, ys))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
sum(++(xs, :(x, :(y, ys)))) -> sum(++(xs, sum(:(x, :(y, ys)))))
-(x, 0) -> x
-(0, s(y)) -> 0
-(s(x), s(y)) -> -(x, y)
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(-(x, y), s(y)))
length(nil) -> 0
length(:(x, xs)) -> s(length(xs))
hd(:(x, xs)) -> x
avg(xs) -> quot(hd(sum(xs)), length(xs))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
→DP Problem 16
↳Rewriting Transformation
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
innermost
one new Dependency Pair is created:
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(x, :(y, ys)))))
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(+(x, y), ys))))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
→DP Problem 16
↳Rw
...
→DP Problem 17
↳Modular Removal of Rules
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(+(x, y), ys))))
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
innermost
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
+(0, y) -> y
+(s(x), y) -> s(+(x, y))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
POL(:(x1, x2)) = x1 + x2 POL(SUM(x1)) = 1 + x1 POL(0) = 1 POL(++(x1, x2)) = 1 + x1 + x2 POL(nil) = 0 POL(sum(x1)) = x1 POL(s(x1)) = x1 POL(+(x1, x2)) = x1 + x2
+(0, y) -> y
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 4
↳UsableRules
→DP Problem 5
↳UsableRules
→DP Problem 6
↳UsableRules
→DP Problem 7
↳UsableRules
→DP Problem 16
↳Rw
...
→DP Problem 18
↳Modular Removal of Rules
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(+(x, y), ys))))
+(s(x), y) -> s(+(x, y))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
innermost
To remove rules and DPs from this DP problem we used the following monotonic and CE-compatible order: Polynomial ordering.
+(s(x), y) -> s(+(x, y))
sum(:(x, nil)) -> :(x, nil)
sum(:(x, :(y, xs))) -> sum(:(+(x, y), xs))
POL(:(x1, x2)) = 1 + x1 + x2 POL(SUM(x1)) = 1 + x1 POL(++(x1, x2)) = 1 + x1 + x2 POL(nil) = 0 POL(sum(x1)) = x1 POL(s(x1)) = x1 POL(+(x1, x2)) = x1 + x2
SUM(++(xs, :(x, :(y, ys)))) -> SUM(++(xs, sum(:(+(x, y), ys))))
Innermost Termination of R successfully shown.
Duration:
0:00 minutes