The
1st
component contains the
pair
a__f#(y0,y0) |
→ |
a__h#(a) |
(27) |
a__h#(a) |
→ |
a__g#(mark(a),a) |
(29) |
a__g#(a,X) |
→ |
a__f#(b,X) |
(16) |
1.1.1.1.1.1.1 Usable Rules Processor
We restrict the rewrite rules to the following usable rules of the DP problem.
mark(a) |
→ |
a__a |
(7) |
a__a |
→ |
b |
(4) |
a__a |
→ |
a |
(12) |
1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor
We restrict the innermost strategy to the following left hand sides.
a__a |
mark(h(x0)) |
mark(g(x0,x1)) |
mark(a) |
mark(f(x0,x1)) |
mark(b) |
1.1.1.1.1.1.1.1.1 Narrowing Processor
We consider all narrowings of the pair
below position
1
to get the following set of pairs
a__h#(a) |
→ |
a__g#(a__a,a) |
(30) |
1.1.1.1.1.1.1.1.1.1 Usable Rules Processor
We restrict the rewrite rules to the following usable rules of the DP problem.
a__a |
→ |
b |
(4) |
a__a |
→ |
a |
(12) |
1.1.1.1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor
We restrict the innermost strategy to the following left hand sides.
1.1.1.1.1.1.1.1.1.1.1.1 Narrowing Processor
We consider all narrowings of the pair
below position
1
to get the following set of pairs
a__h#(a) |
→ |
a__g#(b,a) |
(31) |
a__h#(a) |
→ |
a__g#(a,a) |
(32) |
1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 1
component.
-
The
1st
component contains the
pair
a__h#(a) |
→ |
a__g#(a,a) |
(32) |
a__g#(a,X) |
→ |
a__f#(b,X) |
(16) |
a__f#(y0,y0) |
→ |
a__h#(a) |
(27) |
1.1.1.1.1.1.1.1.1.1.1.1.1.1 Usable Rules Processor
We restrict the rewrite rules to the following usable rules of the DP problem.
There are no rules.
1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Innermost Lhss Removal Processor
We restrict the innermost strategy to the following left hand sides.
There are no lhss.
1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Instantiation Processor
We instantiate the pair
to the following set of pairs
a__g#(a,a) |
→ |
a__f#(b,a) |
(33) |
1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1.1 Dependency Graph Processor
The dependency pairs are split into 0
components.