R
↳Dependency Pair Analysis
PLUS(s(X), Y) -> PLUS(X, Y)
MIN(s(X), s(Y)) -> MIN(X, Y)
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(min(X, Y), Z) -> PLUS(Y, Z)
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) -> MIN(X, Y)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
PLUS(s(X), Y) -> PLUS(X, Y)
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
PLUS(s(X), Y) -> PLUS(X, Y)
PLUS(s(s(X'')), Y'') -> PLUS(s(X''), Y'')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳Forward Instantiation Transformation
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
PLUS(s(s(X'')), Y'') -> PLUS(s(X''), Y'')
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
PLUS(s(s(X'')), Y'') -> PLUS(s(X''), Y'')
PLUS(s(s(s(X''''))), Y'''') -> PLUS(s(s(X'''')), Y'''')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 5
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
PLUS(s(s(s(X''''))), Y'''') -> PLUS(s(s(X'''')), Y'''')
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
PLUS(s(s(s(X''''))), Y'''') -> PLUS(s(s(X'''')), Y'''')
PLUS(x1, x2) -> PLUS(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Narrowing Transformation
→DP Problem 3
↳Nar
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) -> MIN(X, Y)
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(min(X, s(X'')), Z) -> MIN(X, s(plus(X'', Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 7
↳Forward Instantiation Transformation
→DP Problem 3
↳Nar
MIN(s(X), s(Y)) -> MIN(X, Y)
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
MIN(s(X), s(Y)) -> MIN(X, Y)
MIN(s(s(X'')), s(s(Y''))) -> MIN(s(X''), s(Y''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 8
↳Forward Instantiation Transformation
→DP Problem 3
↳Nar
MIN(s(s(X'')), s(s(Y''))) -> MIN(s(X''), s(Y''))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
MIN(s(s(X'')), s(s(Y''))) -> MIN(s(X''), s(Y''))
MIN(s(s(s(X''''))), s(s(s(Y'''')))) -> MIN(s(s(X'''')), s(s(Y'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 9
↳Argument Filtering and Ordering
→DP Problem 3
↳Nar
MIN(s(s(s(X''''))), s(s(s(Y'''')))) -> MIN(s(s(X'''')), s(s(Y'''')))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
MIN(s(s(s(X''''))), s(s(s(Y'''')))) -> MIN(s(s(X'''')), s(s(Y'''')))
MIN(x1, x2) -> MIN(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 7
↳FwdInst
...
→DP Problem 10
↳Dependency Graph
→DP Problem 3
↳Nar
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Narrowing Transformation
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
three new Dependency Pairs are created:
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
QUOT(s(X''), s(0)) -> QUOT(X'', s(0))
QUOT(s(s(X'')), s(s(Y''))) -> QUOT(min(X'', Y''), s(s(Y'')))
QUOT(s(min(X'', Y'')), s(Z)) -> QUOT(min(X'', plus(Y'', Z)), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳Forward Instantiation Transformation
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
QUOT(s(X''), s(0)) -> QUOT(X'', s(0))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(X''), s(0)) -> QUOT(X'', s(0))
QUOT(s(s(X'''')), s(0)) -> QUOT(s(X''''), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
...
→DP Problem 14
↳Argument Filtering and Ordering
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
QUOT(s(s(X'''')), s(0)) -> QUOT(s(X''''), s(0))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(X'''')), s(0)) -> QUOT(s(X''''), s(0))
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
...
→DP Problem 19
↳Dependency Graph
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(X'')), s(s(Y''))) -> QUOT(min(X'', Y''), s(s(Y'')))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
three new Dependency Pairs are created:
QUOT(s(s(X'')), s(s(Y''))) -> QUOT(min(X'', Y''), s(s(Y'')))
QUOT(s(s(X''')), s(s(0))) -> QUOT(X''', s(s(0)))
QUOT(s(s(s(X'))), s(s(s(Y')))) -> QUOT(min(X', Y'), s(s(s(Y'))))
QUOT(s(s(min(X', Y'))), s(s(Z))) -> QUOT(min(X', plus(Y', Z)), s(s(Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 15
↳Argument Filtering and Ordering
→DP Problem 13
↳Nar
QUOT(s(s(X''')), s(s(0))) -> QUOT(X''', s(s(0)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(X''')), s(s(0))) -> QUOT(X''', s(s(0)))
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 16
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(X'))), s(s(s(Y')))) -> QUOT(min(X', Y'), s(s(s(Y'))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
three new Dependency Pairs are created:
QUOT(s(s(s(X'))), s(s(s(Y')))) -> QUOT(min(X', Y'), s(s(s(Y'))))
QUOT(s(s(s(X''))), s(s(s(0)))) -> QUOT(X'', s(s(s(0))))
QUOT(s(s(s(s(X'')))), s(s(s(s(Y''))))) -> QUOT(min(X'', Y''), s(s(s(s(Y'')))))
QUOT(s(s(s(min(X'', Y'')))), s(s(s(Z)))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(Z))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 21
↳Forward Instantiation Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(X''))), s(s(s(0)))) -> QUOT(X'', s(s(s(0))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(s(s(X''))), s(s(s(0)))) -> QUOT(X'', s(s(s(0))))
QUOT(s(s(s(s(s(s(X'''')))))), s(s(s(0)))) -> QUOT(s(s(s(X''''))), s(s(s(0))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 26
↳Forward Instantiation Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(s(s(s(X'''')))))), s(s(s(0)))) -> QUOT(s(s(s(X''''))), s(s(s(0))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(s(s(s(s(s(X'''')))))), s(s(s(0)))) -> QUOT(s(s(s(X''''))), s(s(s(0))))
QUOT(s(s(s(s(s(s(s(s(s(X''''''))))))))), s(s(s(0)))) -> QUOT(s(s(s(s(s(s(X'''''')))))), s(s(s(0))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 33
↳Argument Filtering and Ordering
→DP Problem 13
↳Nar
QUOT(s(s(s(s(s(s(s(s(s(X''''''))))))))), s(s(s(0)))) -> QUOT(s(s(s(s(s(s(X'''''')))))), s(s(s(0))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(s(s(s(s(X''''''))))))))), s(s(s(0)))) -> QUOT(s(s(s(s(s(s(X'''''')))))), s(s(s(0))))
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 48
↳Dependency Graph
→DP Problem 13
↳Nar
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 22
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(s(X'')))), s(s(s(s(Y''))))) -> QUOT(min(X'', Y''), s(s(s(s(Y'')))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
three new Dependency Pairs are created:
QUOT(s(s(s(s(X'')))), s(s(s(s(Y''))))) -> QUOT(min(X'', Y''), s(s(s(s(Y'')))))
QUOT(s(s(s(s(X''')))), s(s(s(s(0))))) -> QUOT(X''', s(s(s(s(0)))))
QUOT(s(s(s(s(s(X'))))), s(s(s(s(s(Y')))))) -> QUOT(min(X', Y'), s(s(s(s(s(Y'))))))
QUOT(s(s(s(s(min(X', Y'))))), s(s(s(s(Z))))) -> QUOT(min(X', plus(Y', Z)), s(s(s(s(Z)))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 27
↳Forward Instantiation Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(s(X''')))), s(s(s(s(0))))) -> QUOT(X''', s(s(s(s(0)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(s(s(s(X''')))), s(s(s(s(0))))) -> QUOT(X''', s(s(s(s(0)))))
QUOT(s(s(s(s(s(s(s(s(X''''')))))))), s(s(s(s(0))))) -> QUOT(s(s(s(s(X''''')))), s(s(s(s(0)))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 34
↳Argument Filtering and Ordering
→DP Problem 13
↳Nar
QUOT(s(s(s(s(s(s(s(s(X''''')))))))), s(s(s(s(0))))) -> QUOT(s(s(s(s(X''''')))), s(s(s(s(0)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(s(s(s(X''''')))))))), s(s(s(s(0))))) -> QUOT(s(s(s(s(X''''')))), s(s(s(s(0)))))
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 28
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(s(s(X'))))), s(s(s(s(s(Y')))))) -> QUOT(min(X', Y'), s(s(s(s(s(Y'))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
three new Dependency Pairs are created:
QUOT(s(s(s(s(s(X'))))), s(s(s(s(s(Y')))))) -> QUOT(min(X', Y'), s(s(s(s(s(Y'))))))
QUOT(s(s(s(s(s(X''))))), s(s(s(s(s(0)))))) -> QUOT(X'', s(s(s(s(s(0))))))
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 35
↳Argument Filtering and Ordering
→DP Problem 13
↳Nar
QUOT(s(s(s(s(s(X''))))), s(s(s(s(s(0)))))) -> QUOT(X'', s(s(s(s(s(0))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(X''))))), s(s(s(s(s(0)))))) -> QUOT(X'', s(s(s(s(s(0))))))
QUOT(x1, x2) -> QUOT(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 47
↳Remaining Obligation(s)
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 47
↳Remaining Obligation(s)
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 29
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(s(min(X', Y'))))), s(s(s(s(Z))))) -> QUOT(min(X', plus(Y', Z)), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(s(s(s(min(X', Y'))))), s(s(s(s(Z))))) -> QUOT(min(X', plus(Y', Z)), s(s(s(s(Z)))))
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 47
↳Remaining Obligation(s)
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 23
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(min(X'', Y'')))), s(s(s(Z)))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(s(s(min(X'', Y'')))), s(s(s(Z)))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(Z))))
QUOT(s(s(s(min(X'', s(X'))))), s(s(s(Z)))) -> QUOT(min(X'', s(plus(X', Z))), s(s(s(Z))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 30
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(min(X'', s(X'))))), s(s(s(Z)))) -> QUOT(min(X'', s(plus(X', Z))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
two new Dependency Pairs are created:
QUOT(s(s(s(min(X'', s(X'))))), s(s(s(Z)))) -> QUOT(min(X'', s(plus(X', Z))), s(s(s(Z))))
QUOT(s(s(s(min(X'', s(0))))), s(s(s(Z)))) -> QUOT(min(X'', s(Z)), s(s(s(Z))))
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 39
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
QUOT(s(s(s(min(X'', s(0))))), s(s(s(Z)))) -> QUOT(min(X'', s(Z)), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
no new Dependency Pairs are created.
QUOT(s(s(s(min(X'', s(0))))), s(s(s(Z)))) -> QUOT(min(X'', s(Z)), s(s(s(Z))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 47
↳Remaining Obligation(s)
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 17
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(min(X', Y'))), s(s(Z))) -> QUOT(min(X', plus(Y', Z)), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(s(min(X', Y'))), s(s(Z))) -> QUOT(min(X', plus(Y', Z)), s(s(Z)))
QUOT(s(s(min(X', s(X'')))), s(s(Z))) -> QUOT(min(X', s(plus(X'', Z))), s(s(Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 24
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(min(X', s(X'')))), s(s(Z))) -> QUOT(min(X', s(plus(X'', Z))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
two new Dependency Pairs are created:
QUOT(s(s(min(X', s(X'')))), s(s(Z))) -> QUOT(min(X', s(plus(X'', Z))), s(s(Z)))
QUOT(s(s(min(X', s(0)))), s(s(Z))) -> QUOT(min(X', s(Z)), s(s(Z)))
QUOT(s(s(min(X', s(s(X0))))), s(s(Z))) -> QUOT(min(X', s(s(plus(X0, Z)))), s(s(Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 31
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(min(X', s(s(X0))))), s(s(Z))) -> QUOT(min(X', s(s(plus(X0, Z)))), s(s(Z)))
QUOT(s(s(min(X', s(0)))), s(s(Z))) -> QUOT(min(X', s(Z)), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
no new Dependency Pairs are created.
QUOT(s(s(min(X', s(0)))), s(s(Z))) -> QUOT(min(X', s(Z)), s(s(Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 40
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(min(X', s(s(X0))))), s(s(Z))) -> QUOT(min(X', s(s(plus(X0, Z)))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
two new Dependency Pairs are created:
QUOT(s(s(min(X', s(s(X0))))), s(s(Z))) -> QUOT(min(X', s(s(plus(X0, Z)))), s(s(Z)))
QUOT(s(s(min(X', s(s(0))))), s(s(Z))) -> QUOT(min(X', s(s(Z))), s(s(Z)))
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
...
→DP Problem 43
↳Narrowing Transformation
→DP Problem 13
↳Nar
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
QUOT(s(s(min(X', s(s(0))))), s(s(Z))) -> QUOT(min(X', s(s(Z))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
no new Dependency Pairs are created.
QUOT(s(s(min(X', s(s(0))))), s(s(Z))) -> QUOT(min(X', s(s(Z))), s(s(Z)))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 47
↳Remaining Obligation(s)
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Narrowing Transformation
QUOT(s(min(X'', Y'')), s(Z)) -> QUOT(min(X'', plus(Y'', Z)), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
one new Dependency Pair is created:
QUOT(s(min(X'', Y'')), s(Z)) -> QUOT(min(X'', plus(Y'', Z)), s(Z))
QUOT(s(min(X'', s(X'))), s(Z)) -> QUOT(min(X'', s(plus(X', Z))), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 18
↳Narrowing Transformation
QUOT(s(min(X'', s(X'))), s(Z)) -> QUOT(min(X'', s(plus(X', Z))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
two new Dependency Pairs are created:
QUOT(s(min(X'', s(X'))), s(Z)) -> QUOT(min(X'', s(plus(X', Z))), s(Z))
QUOT(s(min(X'', s(0))), s(Z)) -> QUOT(min(X'', s(Z)), s(Z))
QUOT(s(min(X'', s(s(X0)))), s(Z)) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 25
↳Narrowing Transformation
QUOT(s(min(X'', s(s(X0)))), s(Z)) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(Z))
QUOT(s(min(X'', s(0))), s(Z)) -> QUOT(min(X'', s(Z)), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
no new Dependency Pairs are created.
QUOT(s(min(X'', s(0))), s(Z)) -> QUOT(min(X'', s(Z)), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 32
↳Narrowing Transformation
QUOT(s(min(X'', s(s(X0)))), s(Z)) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
two new Dependency Pairs are created:
QUOT(s(min(X'', s(s(X0)))), s(Z)) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(Z))
QUOT(s(min(X'', s(s(0)))), s(Z)) -> QUOT(min(X'', s(s(Z))), s(Z))
QUOT(s(min(X'', s(s(s(X'))))), s(Z)) -> QUOT(min(X'', s(s(s(plus(X', Z))))), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 41
↳Narrowing Transformation
QUOT(s(min(X'', s(s(s(X'))))), s(Z)) -> QUOT(min(X'', s(s(s(plus(X', Z))))), s(Z))
QUOT(s(min(X'', s(s(0)))), s(Z)) -> QUOT(min(X'', s(s(Z))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
no new Dependency Pairs are created.
QUOT(s(min(X'', s(s(0)))), s(Z)) -> QUOT(min(X'', s(s(Z))), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 44
↳Narrowing Transformation
QUOT(s(min(X'', s(s(s(X'))))), s(Z)) -> QUOT(min(X'', s(s(s(plus(X', Z))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
two new Dependency Pairs are created:
QUOT(s(min(X'', s(s(s(X'))))), s(Z)) -> QUOT(min(X'', s(s(s(plus(X', Z))))), s(Z))
QUOT(s(min(X'', s(s(s(0))))), s(Z)) -> QUOT(min(X'', s(s(s(Z)))), s(Z))
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 46
↳Narrowing Transformation
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
QUOT(s(min(X'', s(s(s(0))))), s(Z)) -> QUOT(min(X'', s(s(s(Z)))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
no new Dependency Pairs are created.
QUOT(s(min(X'', s(s(s(0))))), s(Z)) -> QUOT(min(X'', s(s(s(Z)))), s(Z))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Nar
→DP Problem 3
↳Nar
→DP Problem 11
↳FwdInst
→DP Problem 12
↳Nar
→DP Problem 13
↳Nar
...
→DP Problem 47
↳Remaining Obligation(s)
QUOT(s(s(s(s(s(s(X'')))))), s(s(s(s(s(s(Y''))))))) -> QUOT(min(X'', Y''), s(s(s(s(s(s(Y'')))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(s(min(X'', Y'')))))), s(s(s(s(s(Z)))))) -> QUOT(min(X'', plus(Y'', Z)), s(s(s(s(s(Z))))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(s(min(X', s(X'')))))), s(s(s(s(Z))))) -> QUOT(min(X', s(plus(X'', Z))), s(s(s(s(Z)))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(s(min(X'', s(s(X0)))))), s(s(s(Z)))) -> QUOT(min(X'', s(s(plus(X0, Z)))), s(s(s(Z))))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(s(min(X', s(s(s(X'')))))), s(s(Z))) -> QUOT(min(X', s(s(s(plus(X'', Z))))), s(s(Z)))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost
QUOT(s(min(X'', s(s(s(s(X0)))))), s(Z)) -> QUOT(min(X'', s(s(s(s(plus(X0, Z)))))), s(Z))
plus(0, Y) -> Y
plus(s(X), Y) -> s(plus(X, Y))
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
min(min(X, Y), Z) -> min(X, plus(Y, Z))
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
innermost