R
↳Dependency Pair Analysis
NOT(x) -> XOR(x, true)
OR(x, y) -> XOR(and(x, y), xor(x, y))
OR(x, y) -> AND(x, y)
OR(x, y) -> XOR(x, y)
IMPLIES(x, y) -> XOR(and(x, y), xor(x, true))
IMPLIES(x, y) -> AND(x, y)
IMPLIES(x, y) -> XOR(x, true)
AND(xor(x, y), z) -> XOR(and(x, z), and(y, z))
AND(xor(x, y), z) -> AND(x, z)
AND(xor(x, y), z) -> AND(y, z)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
AND(xor(x, y), z) -> AND(y, z)
AND(xor(x, y), z) -> AND(x, z)
not(x) -> xor(x, true)
or(x, y) -> xor(and(x, y), xor(x, y))
implies(x, y) -> xor(and(x, y), xor(x, true))
and(x, true) -> x
and(x, false) -> false
and(x, x) -> x
and(xor(x, y), z) -> xor(and(x, z), and(y, z))
xor(x, false) -> x
xor(x, x) -> false
innermost
one new Dependency Pair is created:
AND(xor(x, y), z) -> AND(x, z)
AND(xor(xor(x'', y''), y), z'') -> AND(xor(x'', y''), z'')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Forward Instantiation Transformation
AND(xor(xor(x'', y''), y), z'') -> AND(xor(x'', y''), z'')
AND(xor(x, y), z) -> AND(y, z)
not(x) -> xor(x, true)
or(x, y) -> xor(and(x, y), xor(x, y))
implies(x, y) -> xor(and(x, y), xor(x, true))
and(x, true) -> x
and(x, false) -> false
and(x, x) -> x
and(xor(x, y), z) -> xor(and(x, z), and(y, z))
xor(x, false) -> x
xor(x, x) -> false
innermost
two new Dependency Pairs are created:
AND(xor(x, y), z) -> AND(y, z)
AND(xor(x, xor(x'', y'')), z'') -> AND(xor(x'', y''), z'')
AND(xor(x, xor(xor(x'''', y''''), y'')), z') -> AND(xor(xor(x'''', y''''), y''), z')
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 3
↳Polynomial Ordering
AND(xor(x, xor(xor(x'''', y''''), y'')), z') -> AND(xor(xor(x'''', y''''), y''), z')
AND(xor(x, xor(x'', y'')), z'') -> AND(xor(x'', y''), z'')
AND(xor(xor(x'', y''), y), z'') -> AND(xor(x'', y''), z'')
not(x) -> xor(x, true)
or(x, y) -> xor(and(x, y), xor(x, y))
implies(x, y) -> xor(and(x, y), xor(x, true))
and(x, true) -> x
and(x, false) -> false
and(x, x) -> x
and(xor(x, y), z) -> xor(and(x, z), and(y, z))
xor(x, false) -> x
xor(x, x) -> false
innermost
AND(xor(x, xor(xor(x'''', y''''), y'')), z') -> AND(xor(xor(x'''', y''''), y''), z')
AND(xor(x, xor(x'', y'')), z'') -> AND(xor(x'', y''), z'')
AND(xor(xor(x'', y''), y), z'') -> AND(xor(x'', y''), z'')
xor(x, false) -> x
xor(x, x) -> false
POL(xor(x1, x2)) = 1 + x1 + x2 POL(false) = 0 POL(AND(x1, x2)) = 1 + x1 + x2
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳FwdInst
...
→DP Problem 4
↳Dependency Graph
not(x) -> xor(x, true)
or(x, y) -> xor(and(x, y), xor(x, y))
implies(x, y) -> xor(and(x, y), xor(x, true))
and(x, true) -> x
and(x, false) -> false
and(x, x) -> x
and(xor(x, y), z) -> xor(and(x, z), and(y, z))
xor(x, false) -> x
xor(x, x) -> false
innermost