MAYBE Problem: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Proof: DP Processor: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Restore Modifier: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) SCC Processor: #sccs: 1 #rules: 9 #arcs: 81/81 DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x0, [f](x0, x1) = 0, [b] = 0, [a] = 1 orientation: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 0 = f#(b(),x) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 0 = f#(b(),f(a(),f(a(),f(a(),f(b(),x))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 0 = f#(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 0 >= 0 = f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) problem: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Matrix Interpretation Processor: dimension: 1 interpretation: [f#](x0, x1) = x1, [f](x0, x1) = x0, [b] = 0, [a] = 1 orientation: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 0 = f#(a(),f(b(),x)) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 0 = f#(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x)))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 0 = f#(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) = 1 >= 1 = f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) problem: DPs: f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),x))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(a(),f(b(),x)))) f#(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f#(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))) TRS: f(a(),f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),x))))))) -> f(a(),f(b(),f(a(),f(a(),f(b(),f(a(),f(a(),f(a(),f(b(),x))))))))) Open