The rewrite relation of the following TRS is considered.
ap(ap(ff,x),x) | → | ap(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (1) |
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (2) |
ap#(ap(ff,x),x) | → | ap#(ap(cons,x),nil) | (3) |
ap#(ap(ff,x),x) | → | ap#(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (4) |
ap#(ap(ff,x),x) | → | ap#(cons,x) | (5) |
The dependency pairs are split into 1 component.
ap#(ap(ff,x),x) | → | ap#(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (4) |
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (2) |
[ap(x1, x2)] | = |
|
|||||||||||||||||||
[ff] | = |
|
|||||||||||||||||||
[nil] | = |
|
|||||||||||||||||||
[ap#(x1, x2)] | = |
|
|||||||||||||||||||
[cons] | = |
|
ap(ap(ff,x),x) | → | ap(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (1) |
ap#(ap(ff,x),x) | → | ap#(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (4) |
The dependency pairs are split into 1 component.
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (2) |
[ap(x1, x2)] | = |
|
|||||||||||||||||||
[ff] | = |
|
|||||||||||||||||||
[nil] | = |
|
|||||||||||||||||||
[ap#(x1, x2)] | = |
|
|||||||||||||||||||
[cons] | = |
|
ap(ap(ff,x),x) | → | ap(ap(x,ap(ff,x)),ap(ap(cons,x),nil)) | (1) |
ap#(ap(ff,x),x) | → | ap#(x,ap(ff,x)) | (2) |
The dependency pairs are split into 0 components.