R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
F(s(x)) > F(x)
G(s(x), s(y)) > IF(f(x), s(x), s(y))
G(s(x), s(y)) > F(x)
G(x, c(y)) > G(x, g(s(c(y)), y))
G(x, c(y)) > G(s(c(y)), y)
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳Neg POLO
F(s(x)) > F(x)
f(0) > true
f(1) > false
f(s(x)) > f(x)
if(true, x, y) > x
if(false, x, y) > y
g(s(x), s(y)) > if(f(x), s(x), s(y))
g(x, c(y)) > g(x, g(s(c(y)), y))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 3
↳SizeChange Principle
→DP Problem 2
↳Neg POLO
F(s(x)) > F(x)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Negative Polynomial Order
G(x, c(y)) > G(s(c(y)), y)
G(x, c(y)) > G(x, g(s(c(y)), y))
f(0) > true
f(1) > false
f(s(x)) > f(x)
if(true, x, y) > x
if(false, x, y) > y
g(s(x), s(y)) > if(f(x), s(x), s(y))
g(x, c(y)) > g(x, g(s(c(y)), y))
innermost
G(x, c(y)) > G(s(c(y)), y)
G(x, c(y)) > G(x, g(s(c(y)), y))
f(0) > true
f(s(x)) > f(x)
if(true, x, y) > x
if(false, x, y) > y
g(s(x), s(y)) > if(f(x), s(x), s(y))
g(x, c(y)) > g(x, g(s(c(y)), y))
f(1) > false
POL( G(x_{1}, x_{2}) ) = x_{2}
POL( c(x_{1}) ) = x_{1} + 1
POL( g(x_{1}, x_{2}) ) = 0
POL( f(x_{1}) ) = 0
POL( true ) = 0
POL( if(x_{1}, ..., x_{3}) ) = x_{2} + x_{3}
POL( s(x_{1}) ) = 0
POL( false ) = 0
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Neg POLO
...
→DP Problem 4
↳Dependency Graph
f(0) > true
f(1) > false
f(s(x)) > f(x)
if(true, x, y) > x
if(false, x, y) > y
g(s(x), s(y)) > if(f(x), s(x), s(y))
g(x, c(y)) > g(x, g(s(c(y)), y))
innermost