Term Rewriting System R:
[x, y, z, k, l]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(minus(x, y), z) -> PLUS(y, z)
QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))
QUOT(s(x), s(y)) -> MINUS(x, y)
PLUS(s(x), y) -> PLUS(x, y)
APP(cons(x, l), k) -> APP(l, k)
SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))
SUM(cons(x, cons(y, l))) -> PLUS(x, y)
SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))
SUM(app(l, cons(x, cons(y, k)))) -> APP(l, sum(cons(x, cons(y, k))))
SUM(app(l, cons(x, cons(y, k)))) -> SUM(cons(x, cons(y, k)))

Furthermore, R contains six SCCs.


   R
DPs
       →DP Problem 1
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:

PLUS(s(x), y) -> PLUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following dependency pair can be strictly oriented:

PLUS(s(x), y) -> PLUS(x, y)


The following rules can be oriented:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
quot > s
plus > s

resulting in one new DP problem.
Used Argument Filtering System:
PLUS(x1, x2) -> PLUS(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
plus(x1, x2) -> plus(x1, x2)
app(x1, x2) -> app(x1, x2)
cons(x1, x2) -> x2
sum(x1) -> x1


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 7
Dependency Graph
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:

APP(cons(x, l), k) -> APP(l, k)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following dependency pair can be strictly oriented:

APP(cons(x, l), k) -> APP(l, k)


The following rules can be oriented:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
nil > 0
sum > 0
quot > 0
app > cons > 0
plus > 0
minus > 0
APP > 0
s > 0

resulting in one new DP problem.
Used Argument Filtering System:
APP(x1, x2) -> APP(x1, x2)
cons(x1, x2) -> cons(x1, x2)
minus(x1, x2) -> minus(x1, x2)
s(x1) -> x1
plus(x1, x2) -> x2
quot(x1, x2) -> x2
app(x1, x2) -> app(x1, x2)
sum(x1) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 8
Dependency Graph
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Argument Filtering and Ordering
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pairs:

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))
MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following dependency pair can be strictly oriented:

MINUS(minus(x, y), z) -> MINUS(x, plus(y, z))


The following rules can be oriented:

plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
nil > 0
sum > 0
{MINUS, plus, minus} > 0
cons > 0
quot > 0
app > 0
s > 0

resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> x1
minus(x1, x2) -> minus(x1, x2)
plus(x1, x2) -> plus(x1, x2)
quot(x1, x2) -> x2
app(x1, x2) -> app(x1, x2)
cons(x1, x2) -> x2
sum(x1) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 9
Argument Filtering and Ordering
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:

MINUS(s(x), s(y)) -> MINUS(x, y)


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following dependency pair can be strictly oriented:

MINUS(s(x), s(y)) -> MINUS(x, y)


The following rules can be oriented:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
quot > s
plus > s

resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
quot(x1, x2) -> quot(x1, x2)
plus(x1, x2) -> plus(x1, x2)
app(x1, x2) -> app(x1, x2)
cons(x1, x2) -> x2
sum(x1) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 9
AFS
             ...
               →DP Problem 10
Dependency Graph
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
Argument Filtering and Ordering
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following dependency pair can be strictly oriented:

SUM(cons(x, cons(y, l))) -> SUM(cons(plus(x, y), l))


The following rules can be oriented:

plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
nil > 0
sum > 0
{cons, app} > 0
quot > 0
plus > 0
SUM > 0
minus > 0
s > 0

resulting in one new DP problem.
Used Argument Filtering System:
SUM(x1) -> SUM(x1)
cons(x1, x2) -> cons(x1, x2)
plus(x1, x2) -> x2
s(x1) -> x1
minus(x1, x2) -> minus(x1, x2)
quot(x1, x2) -> x2
app(x1, x2) -> app(x1, x2)
sum(x1) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
AFS
           →DP Problem 11
Dependency Graph
       →DP Problem 5
AFS
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
Argument Filtering and Ordering
       →DP Problem 6
Remaining


Dependency Pair:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





The following dependency pair can be strictly oriented:

QUOT(s(x), s(y)) -> QUOT(minus(x, y), s(y))


The following rules can be oriented:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
quot > s
plus > s

resulting in one new DP problem.
Used Argument Filtering System:
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1
plus(x1, x2) -> plus(x1, x2)
quot(x1, x2) -> quot(x1, x2)
app(x1, x2) -> app(x1, x2)
cons(x1, x2) -> x2
sum(x1) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
AFS
           →DP Problem 12
Dependency Graph
       →DP Problem 6
Remaining


Dependency Pair:


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
       →DP Problem 4
AFS
       →DP Problem 5
AFS
       →DP Problem 6
Remaining Obligation(s)




The following remains to be proven:
Dependency Pair:

SUM(app(l, cons(x, cons(y, k)))) -> SUM(app(l, sum(cons(x, cons(y, k)))))


Rules:


minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
minus(minus(x, y), z) -> minus(x, plus(y, z))
quot(0, s(y)) -> 0
quot(s(x), s(y)) -> s(quot(minus(x, y), s(y)))
plus(0, y) -> y
plus(s(x), y) -> s(plus(x, y))
app(nil, k) -> k
app(l, nil) -> l
app(cons(x, l), k) -> cons(x, app(l, k))
sum(cons(x, nil)) -> cons(x, nil)
sum(cons(x, cons(y, l))) -> sum(cons(plus(x, y), l))
sum(app(l, cons(x, cons(y, k)))) -> sum(app(l, sum(cons(x, cons(y, k)))))




Termination of R could not be shown.
Duration:
0:00 minutes