MAYBE Time: 0.396159 TRS: {f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))), f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))), L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w)))} DP: DP: {f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil())), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, nil())) -> f#(s 0(), nil()), L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), L# f(s s y, f(z, w)) -> f#(s z, w), L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w)))} TRS: {f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))), f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))), L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w)))} UR: {f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))), f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil())))} EDG: {(L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), f#(x, f(s s y, nil())) -> f#(s 0(), nil())) (L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (L# f(s s y, f(z, w)) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, nil())) -> f#(s 0(), nil())) (f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (L# f(s s y, f(z, w)) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(s 0(), nil())) (L# f(s s y, f(z, w)) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (L# f(s s y, f(z, w)) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (L# f(s s y, f(z, w)) -> f#(s z, w), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (L# f(s s y, f(z, w)) -> f#(s z, w), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (L# f(s s y, f(z, w)) -> f#(s z, w), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w))), L# f(s s y, f(z, w)) -> f#(y, f(s z, w))) (L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w))), L# f(s s y, f(z, w)) -> f#(s z, w)) (L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w))), L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w)))) (L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w))), L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w)))) (f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(s 0(), nil())) (L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (L# f(s s y, f(z, w)) -> f#(s 0(), f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(s 0(), nil())) (f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(s 0(), nil())) (f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w))) (f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w)))) (f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s z, w)) (f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, nil())) -> f#(y, f(s 0(), nil()))) (f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))) (f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, nil())) -> f#(s 0(), nil()))} STATUS: arrows: 0.540000 SCCS (2): Scc: {L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w)))} Scc: {f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))} SCC (1): Strict: {L# f(s s y, f(z, w)) -> L# f(s 0(), f(y, f(s z, w)))} Weak: {f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))), f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))), L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w)))} Fail SCC (4): Strict: {f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)), f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, f(z, w))) -> f#(s z, w), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))} Weak: {f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))), f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))), L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [L](x0) = 0, [0] = 0, [nil] = 1, [f#](x0, x1) = x0 + x1 + 1 Strict: f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))) 4 + 1x + 1y >= 4 + 1x + 1y f#(x, f(s s y, f(z, w))) -> f#(s z, w) 3 + 1x + 1y + 1z + 1w >= 2 + 1z + 1w f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))) 3 + 1x + 1y + 1z + 1w >= 3 + 1x + 1y + 1z + 1w f#(x, f(s s y, f(z, w))) -> f#(y, f(s z, w)) 3 + 1x + 1y + 1z + 1w >= 2 + 1y + 1z + 1w Weak: L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w))) 0 + 0y + 0z + 0w >= 0 + 0y + 0z + 0w f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))) 3 + 1x + 1y >= 3 + 1x + 1y f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))) 2 + 1x + 1y + 1z + 1w >= 2 + 1x + 1y + 1z + 1w SCCS (1): Scc: {f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))} SCC (2): Strict: {f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))), f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil())))} Weak: {f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))), f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))), L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w)))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [f](x0, x1) = x0 + x1, [s](x0) = x0 + 1, [L](x0) = x0, [0] = 0, [nil] = 0, [f#](x0, x1) = x0 Strict: f#(x, f(s s y, nil())) -> f#(s x, f(y, f(s 0(), nil()))) 2 + 0x + 1y >= 1 + 0x + 1y f#(x, f(s s y, f(z, w))) -> f#(s x, f(y, f(s z, w))) 2 + 0x + 1y + 1z + 1w >= 1 + 0x + 1y + 1z + 1w Weak: L f(s s y, f(z, w)) -> L f(s 0(), f(y, f(s z, w))) 2 + 1y + 1z + 1w >= 2 + 1y + 1z + 1w f(x, f(s s y, nil())) -> f(s x, f(y, f(s 0(), nil()))) 2 + 1x + 1y >= 2 + 1x + 1y f(x, f(s s y, f(z, w))) -> f(s x, f(y, f(s z, w))) 2 + 1x + 1y + 1z + 1w >= 2 + 1x + 1y + 1z + 1w Qed