The rewrite relation of the following TRS is considered.
ap(ap(f,x),x) | → | ap(ap(x,ap(f,x)),ap(ap(cons,x),nil)) | (1) |
ap(ap(ap(foldr,g),h),nil) | → | h | (2) |
ap(ap(ap(foldr,g),h),ap(ap(cons,x),xs)) | → | ap(ap(g,x),ap(ap(ap(foldr,g),h),xs)) | (3) |
t0 | = | ap(ap(ap(f,foldr),foldr),ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),nil)) |
→ | ap(ap(ap(f,foldr),foldr),ap(ap(cons,foldr),nil)) | |
→ | ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),ap(ap(cons,foldr),nil)) | |
→ | ap(ap(ap(f,foldr),foldr),ap(ap(ap(foldr,ap(f,foldr)),ap(ap(cons,foldr),nil)),nil)) | |
= | t3 |