Term Rewriting System R:
[y, z, x]
quot(0, s(y), s(z)) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(quot(x, s(z), s(z)))
Termination of R to be shown.
R
↳Dependency Pair Analysis
R contains the following Dependency Pairs:
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
QUOT(x, 0, s(z)) -> QUOT(x, s(z), s(z))
Furthermore, R contains one SCC.
R
↳DPs
→DP Problem 1
↳Remaining Obligation(s)
The following remains to be proven:
Dependency Pairs:
QUOT(x, 0, s(z)) -> QUOT(x, s(z), s(z))
QUOT(s(x), s(y), z) -> QUOT(x, y, z)
Rules:
quot(0, s(y), s(z)) -> 0
quot(s(x), s(y), z) -> quot(x, y, z)
quot(x, 0, s(z)) -> s(quot(x, s(z), s(z)))
Termination of R could not be shown.
Duration:
0:00 minutes