R
↳Dependency Pair Analysis
LE(s(x), s(y)) -> LE(x, y)
MINUS(s(x), s(y)) -> MINUS(x, y)
MOD(s(x), s(y)) -> IFMOD(le(y, x), s(x), s(y))
MOD(s(x), s(y)) -> LE(y, x)
IFMOD(true, s(x), s(y)) -> MOD(minus(x, y), s(y))
IFMOD(true, s(x), s(y)) -> MINUS(x, y)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
LE(s(x), s(y)) -> LE(x, y)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
one new Dependency Pair is created:
LE(s(x), s(y)) -> LE(x, y)
LE(s(s(x'')), s(s(y''))) -> LE(s(x''), s(y''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳Forward Instantiation Transformation
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
LE(s(s(x'')), s(s(y''))) -> LE(s(x''), s(y''))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
one new Dependency Pair is created:
LE(s(s(x'')), s(s(y''))) -> LE(s(x''), s(y''))
LE(s(s(s(x''''))), s(s(s(y'''')))) -> LE(s(s(x'''')), s(s(y'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 5
↳Polynomial Ordering
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
LE(s(s(s(x''''))), s(s(s(y'''')))) -> LE(s(s(x'''')), s(s(y'''')))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
LE(s(s(s(x''''))), s(s(s(y'''')))) -> LE(s(s(x'''')), s(s(y'''')))
POL(LE(x1, x2)) = 1 + x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 4
↳FwdInst
...
→DP Problem 6
↳Dependency Graph
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
→DP Problem 3
↳Nar
MINUS(s(x), s(y)) -> MINUS(x, y)
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
one new Dependency Pair is created:
MINUS(s(x), s(y)) -> MINUS(x, y)
MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 7
↳Forward Instantiation Transformation
→DP Problem 3
↳Nar
MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
one new Dependency Pair is created:
MINUS(s(s(x'')), s(s(y''))) -> MINUS(s(x''), s(y''))
MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 7
↳FwdInst
...
→DP Problem 8
↳Polynomial Ordering
→DP Problem 3
↳Nar
MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
MINUS(s(s(s(x''''))), s(s(s(y'''')))) -> MINUS(s(s(x'''')), s(s(y'''')))
POL(MINUS(x1, x2)) = 1 + x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 7
↳FwdInst
...
→DP Problem 9
↳Dependency Graph
→DP Problem 3
↳Nar
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Narrowing Transformation
IFMOD(true, s(x), s(y)) -> MOD(minus(x, y), s(y))
MOD(s(x), s(y)) -> IFMOD(le(y, x), s(x), s(y))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
three new Dependency Pairs are created:
MOD(s(x), s(y)) -> IFMOD(le(y, x), s(x), s(y))
MOD(s(x'), s(0)) -> IFMOD(true, s(x'), s(0))
MOD(s(0), s(s(x''))) -> IFMOD(false, s(0), s(s(x'')))
MOD(s(s(y'')), s(s(x''))) -> IFMOD(le(x'', y''), s(s(y'')), s(s(x'')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Narrowing Transformation
MOD(s(s(y'')), s(s(x''))) -> IFMOD(le(x'', y''), s(s(y'')), s(s(x'')))
MOD(s(x'), s(0)) -> IFMOD(true, s(x'), s(0))
IFMOD(true, s(x), s(y)) -> MOD(minus(x, y), s(y))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
two new Dependency Pairs are created:
IFMOD(true, s(x), s(y)) -> MOD(minus(x, y), s(y))
IFMOD(true, s(x''), s(0)) -> MOD(x'', s(0))
IFMOD(true, s(s(x'')), s(s(y''))) -> MOD(minus(x'', y''), s(s(y'')))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
IFMOD(true, s(s(x'')), s(s(y''))) -> MOD(minus(x'', y''), s(s(y'')))
MOD(s(s(y'')), s(s(x''))) -> IFMOD(le(x'', y''), s(s(y'')), s(s(x'')))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
three new Dependency Pairs are created:
MOD(s(s(y'')), s(s(x''))) -> IFMOD(le(x'', y''), s(s(y'')), s(s(x'')))
MOD(s(s(y''')), s(s(0))) -> IFMOD(true, s(s(y''')), s(s(0)))
MOD(s(s(0)), s(s(s(x')))) -> IFMOD(false, s(s(0)), s(s(s(x'))))
MOD(s(s(s(y'))), s(s(s(x')))) -> IFMOD(le(x', y'), s(s(s(y'))), s(s(s(x'))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
MOD(s(s(s(y'))), s(s(s(x')))) -> IFMOD(le(x', y'), s(s(s(y'))), s(s(s(x'))))
MOD(s(s(y''')), s(s(0))) -> IFMOD(true, s(s(y''')), s(s(0)))
IFMOD(true, s(s(x'')), s(s(y''))) -> MOD(minus(x'', y''), s(s(y'')))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
two new Dependency Pairs are created:
IFMOD(true, s(s(x'')), s(s(y''))) -> MOD(minus(x'', y''), s(s(y'')))
IFMOD(true, s(s(x''')), s(s(0))) -> MOD(x''', s(s(0)))
IFMOD(true, s(s(s(x'))), s(s(s(y')))) -> MOD(minus(x', y'), s(s(s(y'))))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 15
↳Polynomial Ordering
IFMOD(true, s(s(s(x'))), s(s(s(y')))) -> MOD(minus(x', y'), s(s(s(y'))))
MOD(s(s(s(y'))), s(s(s(x')))) -> IFMOD(le(x', y'), s(s(s(y'))), s(s(s(x'))))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
IFMOD(true, s(s(s(x'))), s(s(s(y')))) -> MOD(minus(x', y'), s(s(s(y'))))
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
POL(0) = 0 POL(false) = 0 POL(MOD(x1, x2)) = x1 POL(minus(x1, x2)) = x1 POL(true) = 0 POL(s(x1)) = 1 + x1 POL(IF_MOD(x1, x2, x3)) = x2 POL(le(x1, x2)) = 0
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 18
↳Dependency Graph
MOD(s(s(s(y'))), s(s(s(x')))) -> IFMOD(le(x', y'), s(s(s(y'))), s(s(s(x'))))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 16
↳Polynomial Ordering
IFMOD(true, s(s(x''')), s(s(0))) -> MOD(x''', s(s(0)))
MOD(s(s(y''')), s(s(0))) -> IFMOD(true, s(s(y''')), s(s(0)))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
IFMOD(true, s(s(x''')), s(s(0))) -> MOD(x''', s(s(0)))
POL(0) = 0 POL(MOD(x1, x2)) = x1 POL(true) = 0 POL(IF_MOD(x1, x2, x3)) = x2 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 19
↳Dependency Graph
MOD(s(s(y''')), s(s(0))) -> IFMOD(true, s(s(y''')), s(s(0)))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 12
↳Forward Instantiation Transformation
IFMOD(true, s(x''), s(0)) -> MOD(x'', s(0))
MOD(s(x'), s(0)) -> IFMOD(true, s(x'), s(0))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
one new Dependency Pair is created:
IFMOD(true, s(x''), s(0)) -> MOD(x'', s(0))
IFMOD(true, s(s(x'''')), s(0)) -> MOD(s(x''''), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 14
↳Forward Instantiation Transformation
IFMOD(true, s(s(x'''')), s(0)) -> MOD(s(x''''), s(0))
MOD(s(x'), s(0)) -> IFMOD(true, s(x'), s(0))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
one new Dependency Pair is created:
MOD(s(x'), s(0)) -> IFMOD(true, s(x'), s(0))
MOD(s(s(x'''''')), s(0)) -> IFMOD(true, s(s(x'''''')), s(0))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 17
↳Polynomial Ordering
MOD(s(s(x'''''')), s(0)) -> IFMOD(true, s(s(x'''''')), s(0))
IFMOD(true, s(s(x'''')), s(0)) -> MOD(s(x''''), s(0))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost
IFMOD(true, s(s(x'''')), s(0)) -> MOD(s(x''''), s(0))
POL(0) = 0 POL(MOD(x1, x2)) = x1 POL(true) = 0 POL(s(x1)) = 1 + x1 POL(IF_MOD(x1, x2, x3)) = x2
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
→DP Problem 3
↳Nar
→DP Problem 10
↳Nar
...
→DP Problem 20
↳Dependency Graph
MOD(s(s(x'''''')), s(0)) -> IFMOD(true, s(s(x'''''')), s(0))
le(0, y) -> true
le(s(x), 0) -> false
le(s(x), s(y)) -> le(x, y)
minus(x, 0) -> x
minus(s(x), s(y)) -> minus(x, y)
mod(0, y) -> 0
mod(s(x), 0) -> 0
mod(s(x), s(y)) -> ifmod(le(y, x), s(x), s(y))
ifmod(true, s(x), s(y)) -> mod(minus(x, y), s(y))
ifmod(false, s(x), s(y)) -> s(x)
innermost