Term Rewriting System R:
[x, y, z]
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Innermost Termination of R to be shown.

R
Dependency Pair Analysis

R contains the following Dependency Pairs:

MINUS(s(x), s(y)) -> MINUS(x, y)
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)
PLUS(minus(x, s(0)), minus(y, s(s(z)))) -> PLUS(minus(y, s(s(z))), minus(x, s(0)))
PLUS(plus(x, s(0)), plus(y, s(s(z)))) -> PLUS(plus(y, s(s(z))), plus(x, s(0)))

Furthermore, R contains three SCCs.

R
DPs
→DP Problem 1
Argument Filtering and Ordering
→DP Problem 2
AFS
→DP Problem 3
AFS

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> s(x1)

R
DPs
→DP Problem 1
AFS
→DP Problem 4
Dependency Graph
→DP Problem 2
AFS
→DP Problem 3
AFS

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Strategy:

innermost

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

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)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

The following usable rules for innermost can be oriented:

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

Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
minus(x1, x2) -> x1

R
DPs
→DP Problem 1
AFS
→DP Problem 2
AFS
→DP Problem 5
Dependency Graph
→DP Problem 3
AFS

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Strategy:

innermost

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

Dependency Pair:

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

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:
PLUS(x1, x2) -> PLUS(x1, x2)
s(x1) -> s(x1)

R
DPs
→DP Problem 1
AFS
→DP Problem 2
AFS
→DP Problem 3
AFS
→DP Problem 6
Dependency Graph

Dependency Pair:

Rules:

minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
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))
plus(minus(x, s(0)), minus(y, s(s(z)))) -> plus(minus(y, s(s(z))), minus(x, s(0)))
plus(plus(x, s(0)), plus(y, s(s(z)))) -> plus(plus(y, s(s(z))), plus(x, s(0)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:00 minutes