(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
active(if(false, X, Y)) → mark(Y)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
mark(false) → active(false)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(active(x1)) = x1
POL(c) = 0
POL(f(x1)) = 2·x1
POL(false) = 2
POL(if(x1, x2, x3)) = 2·x1 + 2·x2 + 2·x3
POL(mark(x1)) = x1
POL(true) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
active(if(false, X, Y)) → mark(Y)
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
mark(false) → active(false)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
(3) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(active(x1)) = x1
POL(c) = 0
POL(f(x1)) = 2·x1
POL(false) = 2
POL(if(x1, x2, x3)) = x1 + 2·x2 + x3
POL(mark(x1)) = 2·x1
POL(true) = 0
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
mark(false) → active(false)
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
(5) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVE(f(X)) → MARK(if(X, c, f(true)))
ACTIVE(f(X)) → IF(X, c, f(true))
ACTIVE(f(X)) → F(true)
ACTIVE(if(true, X, Y)) → MARK(X)
MARK(f(X)) → ACTIVE(f(mark(X)))
MARK(f(X)) → F(mark(X))
MARK(f(X)) → MARK(X)
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), mark(X2), X3))
MARK(if(X1, X2, X3)) → IF(mark(X1), mark(X2), X3)
MARK(if(X1, X2, X3)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X2)
MARK(c) → ACTIVE(c)
MARK(true) → ACTIVE(true)
F(mark(X)) → F(X)
F(active(X)) → F(X)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
IF(active(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, active(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, active(X3)) → IF(X1, X2, X3)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(7) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 6 less nodes.
(8) Complex Obligation (AND)
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
IF(active(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, active(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, active(X3)) → IF(X1, X2, X3)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(10) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
IF(X1, mark(X2), X3) → IF(X1, X2, X3)
IF(mark(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
IF(active(X1), X2, X3) → IF(X1, X2, X3)
IF(X1, active(X2), X3) → IF(X1, X2, X3)
IF(X1, X2, active(X3)) → IF(X1, X2, X3)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- IF(X1, mark(X2), X3) → IF(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
- IF(mark(X1), X2, X3) → IF(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- IF(X1, X2, mark(X3)) → IF(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
- IF(active(X1), X2, X3) → IF(X1, X2, X3)
The graph contains the following edges 1 > 1, 2 >= 2, 3 >= 3
- IF(X1, active(X2), X3) → IF(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 > 2, 3 >= 3
- IF(X1, X2, active(X3)) → IF(X1, X2, X3)
The graph contains the following edges 1 >= 1, 2 >= 2, 3 > 3
(13) TRUE
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(active(X)) → F(X)
F(mark(X)) → F(X)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(16) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(active(X)) → F(X)
F(mark(X)) → F(X)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(17) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- F(active(X)) → F(X)
The graph contains the following edges 1 > 1
- F(mark(X)) → F(X)
The graph contains the following edges 1 > 1
(18) TRUE
(19) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(if(X, c, f(true)))
MARK(f(X)) → MARK(X)
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), mark(X2), X3))
ACTIVE(if(true, X, Y)) → MARK(X)
MARK(if(X1, X2, X3)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X2)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(20) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
MARK(f(X)) → MARK(X)
Used ordering: Polynomial interpretation [POLO]:
POL(ACTIVE(x1)) = x1
POL(MARK(x1)) = x1
POL(active(x1)) = x1
POL(c) = 0
POL(f(x1)) = 1 + x1
POL(if(x1, x2, x3)) = x1 + x2 + x3
POL(mark(x1)) = x1
POL(true) = 0
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(if(X, c, f(true)))
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), mark(X2), X3))
ACTIVE(if(true, X, Y)) → MARK(X)
MARK(if(X1, X2, X3)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X2)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(22) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
ACTIVE(if(true, X, Y)) → MARK(X)
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(if(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
active(f(X)) → mark(if(X, c, f(true)))
mark(f(X)) → active(f(mark(X)))
active(if(true, X, Y)) → mark(X)
mark(true) → active(true)
mark(c) → active(c)
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(if(X, c, f(true)))
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), mark(X2), X3))
MARK(if(X1, X2, X3)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X2)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(24) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(if(X1, X2, X3)) → ACTIVE(if(mark(X1), mark(X2), X3))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(if(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(f(X)) → ACTIVE(f(mark(X)))
ACTIVE(f(X)) → MARK(if(X, c, f(true)))
MARK(if(X1, X2, X3)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X2)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(26) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
MARK(f(X)) → ACTIVE(f(mark(X)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(if(x1, x2, x3)) = | | + | | · | x1 | + | | · | x2 | + | | · | x3 |
The following usable rules [FROCOS05] were oriented:
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
active(f(X)) → mark(if(X, c, f(true)))
mark(f(X)) → active(f(mark(X)))
active(if(true, X, Y)) → mark(X)
mark(true) → active(true)
mark(c) → active(c)
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
ACTIVE(f(X)) → MARK(if(X, c, f(true)))
MARK(if(X1, X2, X3)) → MARK(X1)
MARK(if(X1, X2, X3)) → MARK(X2)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(28) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(29) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(if(X1, X2, X3)) → MARK(X2)
MARK(if(X1, X2, X3)) → MARK(X1)
The TRS R consists of the following rules:
active(f(X)) → mark(if(X, c, f(true)))
active(if(true, X, Y)) → mark(X)
mark(f(X)) → active(f(mark(X)))
mark(if(X1, X2, X3)) → active(if(mark(X1), mark(X2), X3))
mark(c) → active(c)
mark(true) → active(true)
f(mark(X)) → f(X)
f(active(X)) → f(X)
if(mark(X1), X2, X3) → if(X1, X2, X3)
if(X1, mark(X2), X3) → if(X1, X2, X3)
if(X1, X2, mark(X3)) → if(X1, X2, X3)
if(active(X1), X2, X3) → if(X1, X2, X3)
if(X1, active(X2), X3) → if(X1, X2, X3)
if(X1, X2, active(X3)) → if(X1, X2, X3)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(30) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(31) Obligation:
Q DP problem:
The TRS P consists of the following rules:
MARK(if(X1, X2, X3)) → MARK(X2)
MARK(if(X1, X2, X3)) → MARK(X1)
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(32) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- MARK(if(X1, X2, X3)) → MARK(X2)
The graph contains the following edges 1 > 1
- MARK(if(X1, X2, X3)) → MARK(X1)
The graph contains the following edges 1 > 1
(33) TRUE