(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
AND(x, or(y, z)) → OR(and(x, y), and(x, z))
AND(x, or(y, z)) → AND(x, y)
AND(x, or(y, z)) → AND(x, z)
AND(x, and(y, y)) → AND(x, y)
OR(x, or(y, y)) → OR(x, y)
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 2 SCCs with 1 less node.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
OR(x, or(y, y)) → OR(x, y)
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
OR(x, or(y, y)) → OR(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
OR(
x0,
x1,
x2) =
OR(
x2)
Tags:
OR has argument tags [1,2,0] and root tag 0
Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
OR(
x1,
x2) =
OR(
x1,
x2)
or(
x1,
x2) =
or(
x2)
Homeomorphic Embedding Order
The following usable rules [FROCOS05] were oriented:
none
(7) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(9) TRUE
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
AND(x, or(y, z)) → AND(x, z)
AND(x, or(y, z)) → AND(x, y)
AND(x, and(y, y)) → AND(x, y)
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(11) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
AND(x, or(y, z)) → AND(x, z)
AND(x, or(y, z)) → AND(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
AND(
x0,
x1,
x2) =
AND(
x0)
Tags:
AND has argument tags [1,3,2] and root tag 0
Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
AND(
x1,
x2) =
x2
or(
x1,
x2) =
or(
x1,
x2)
and(
x1,
x2) =
x2
Homeomorphic Embedding Order
The following usable rules [FROCOS05] were oriented:
none
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
AND(x, and(y, y)) → AND(x, y)
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(13) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
AND(x, and(y, y)) → AND(x, y)
The remaining pairs can at least be oriented weakly.
Used ordering: SCNP Order with the following components:
Level mapping:
Top level AFS:
AND(
x0,
x1,
x2) =
AND(
x2)
Tags:
AND has argument tags [1,2,0] and root tag 0
Comparison: MAX
Underlying order for the size change arcs and the rules of R:
Combined order from the following AFS and order.
AND(
x1,
x2) =
AND(
x1,
x2)
and(
x1,
x2) =
and(
x2)
Homeomorphic Embedding Order
The following usable rules [FROCOS05] were oriented:
none
(14) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
and(x, or(y, z)) → or(and(x, y), and(x, z))
and(x, and(y, y)) → and(x, y)
or(or(x, y), and(y, z)) → or(x, y)
or(x, and(x, y)) → x
or(true, y) → true
or(x, false) → x
or(x, x) → x
or(x, or(y, y)) → or(x, y)
and(x, true) → x
and(false, y) → false
and(x, x) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(16) TRUE