(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(*(x)) → *(1(x))
1(*(x)) → 0(#(x))
#(0(x)) → 0(#(x))
#(1(x)) → 1(#(x))
#($(x)) → *($(x))
#(#(x)) → #(x)
#(*(x)) → *(x)
Q is empty.
(1) QTRSRRRProof (EQUIVALENT transformation)
Used ordering:
Polynomial interpretation [POLO]:
POL(#(x1)) = 1 + x1
POL($(x1)) = x1
POL(*(x1)) = 1 + x1
POL(0(x1)) = x1
POL(1(x1)) = x1
With this ordering the following rules can be removed by the rule removal processor [LPAR04] because they are oriented strictly:
#(#(x)) → #(x)
#(*(x)) → *(x)
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(*(x)) → *(1(x))
1(*(x)) → 0(#(x))
#(0(x)) → 0(#(x))
#(1(x)) → 1(#(x))
#($(x)) → *($(x))
Q is empty.
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
01(*(x)) → 11(x)
11(*(x)) → 01(#(x))
11(*(x)) → #1(x)
#1(0(x)) → 01(#(x))
#1(0(x)) → #1(x)
#1(1(x)) → 11(#(x))
#1(1(x)) → #1(x)
The TRS R consists of the following rules:
0(*(x)) → *(1(x))
1(*(x)) → 0(#(x))
#(0(x)) → 0(#(x))
#(1(x)) → 1(#(x))
#($(x)) → *($(x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(5) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
11(*(x)) → 01(#(x))
11(*(x)) → #1(x)
#1(0(x)) → 01(#(x))
#1(0(x)) → #1(x)
#1(1(x)) → #1(x)
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial Order [NEGPOLO,POLO] with Interpretation:
| POL( 01(x1) ) = max{0, x1 - 2} |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
#(0(x)) → 0(#(x))
#(1(x)) → 1(#(x))
#($(x)) → *($(x))
0(*(x)) → *(1(x))
1(*(x)) → 0(#(x))
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
01(*(x)) → 11(x)
#1(1(x)) → 11(#(x))
The TRS R consists of the following rules:
0(*(x)) → *(1(x))
1(*(x)) → 0(#(x))
#(0(x)) → 0(#(x))
#(1(x)) → 1(#(x))
#($(x)) → *($(x))
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 0 SCCs with 2 less nodes.
(8) TRUE