MAYBE Time: 5.341267 TRS: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse xs -> rev(xs, nil()), if(true(), xs, ys, zs) -> zs, if(false(), xs, ys, zs) -> rev(xs, ys)} DP: DP: { last# cons(x, cons(y, ys)) -> last# cons(y, ys), dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys), append#(cons(x, xs), ys) -> append#(xs, ys), rev#(xs, ys) -> isEmpty# xs, rev#(xs, ys) -> last# xs, rev#(xs, ys) -> dropLast# xs, rev#(xs, ys) -> append#(ys, last xs), rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse# xs -> rev#(xs, nil()), if#(false(), xs, ys, zs) -> rev#(xs, ys)} TRS: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse xs -> rev(xs, nil()), if(true(), xs, ys, zs) -> zs, if(false(), xs, ys, zs) -> rev(xs, ys)} UR: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), a(z, w) -> z, a(z, w) -> w} EDG: {(rev#(xs, ys) -> last# xs, last# cons(x, cons(y, ys)) -> last# cons(y, ys)) (rev#(xs, ys) -> append#(ys, last xs), append#(cons(x, xs), ys) -> append#(xs, ys)) (rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys), if#(false(), xs, ys, zs) -> rev#(xs, ys)) (last# cons(x, cons(y, ys)) -> last# cons(y, ys), last# cons(x, cons(y, ys)) -> last# cons(y, ys)) (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys)) (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> append#(ys, last xs)) (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> dropLast# xs) (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> last# xs) (reverse# xs -> rev#(xs, nil()), rev#(xs, ys) -> isEmpty# xs) (dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys), dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys)) (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> isEmpty# xs) (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> last# xs) (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> dropLast# xs) (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> append#(ys, last xs)) (if#(false(), xs, ys, zs) -> rev#(xs, ys), rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys)) (append#(cons(x, xs), ys) -> append#(xs, ys), append#(cons(x, xs), ys) -> append#(xs, ys)) (rev#(xs, ys) -> dropLast# xs, dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys))} STATUS: arrows: 0.830000 SCCS (4): Scc: { rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys), if#(false(), xs, ys, zs) -> rev#(xs, ys)} Scc: {append#(cons(x, xs), ys) -> append#(xs, ys)} Scc: {dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys)} Scc: {last# cons(x, cons(y, ys)) -> last# cons(y, ys)} SCC (2): Strict: { rev#(xs, ys) -> if#(isEmpty xs, dropLast xs, append(ys, last xs), ys), if#(false(), xs, ys, zs) -> rev#(xs, ys)} Weak: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse xs -> rev(xs, nil()), if(true(), xs, ys, zs) -> zs, if(false(), xs, ys, zs) -> rev(xs, ys)} Fail SCC (1): Strict: {append#(cons(x, xs), ys) -> append#(xs, ys)} Weak: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse xs -> rev(xs, nil()), if(true(), xs, ys, zs) -> zs, if(false(), xs, ys, zs) -> rev(xs, ys)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3) = x0 + x1, [cons](x0, x1) = x0 + 1, [append](x0, x1) = x0 + 1, [rev](x0, x1) = x0 + 1, [isEmpty](x0) = x0 + 1, [last](x0) = 0, [dropLast](x0) = x0 + 1, [reverse](x0) = 0, [true] = 0, [nil] = 1, [false] = 0, [append#](x0, x1) = x0 Strict: append#(cons(x, xs), ys) -> append#(xs, ys) 1 + 0x + 1xs + 0ys >= 0 + 1xs + 0ys Weak: if(false(), xs, ys, zs) -> rev(xs, ys) 0 + 0xs + 1ys + 1zs >= 1 + 0xs + 1ys if(true(), xs, ys, zs) -> zs 0 + 0xs + 1ys + 1zs >= 1zs reverse xs -> rev(xs, nil()) 0 + 0xs >= 2 + 0xs rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys) 1 + 0xs + 1ys >= 1 + 0xs + 2ys append(cons(x, xs), ys) -> cons(x, append(xs, ys)) 2 + 0x + 1xs + 0ys >= 2 + 0x + 1xs + 0ys append(nil(), ys) -> ys 2 + 0ys >= 1ys dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)) 3 + 0x + 0y + 1ys >= 3 + 0x + 0y + 1ys dropLast cons(x, nil()) -> nil() 3 + 0x >= 1 dropLast nil() -> nil() 2 >= 1 last cons(x, cons(y, ys)) -> last cons(y, ys) 0 + 0x + 0y + 0ys >= 0 + 0y + 0ys last cons(x, nil()) -> x 0 + 0x >= 1x isEmpty cons(x, xs) -> false() 2 + 0x + 1xs >= 0 isEmpty nil() -> true() 2 >= 0 Qed SCC (1): Strict: {dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys)} Weak: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse xs -> rev(xs, nil()), if(true(), xs, ys, zs) -> zs, if(false(), xs, ys, zs) -> rev(xs, ys)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3) = x0, [cons](x0, x1) = x0 + 1, [append](x0, x1) = x0 + 1, [rev](x0, x1) = x0 + 1, [isEmpty](x0) = x0 + 1, [last](x0) = 0, [dropLast](x0) = x0 + 1, [reverse](x0) = 0, [true] = 0, [nil] = 1, [false] = 0, [dropLast#](x0) = x0 + 1 Strict: dropLast# cons(x, cons(y, ys)) -> dropLast# cons(y, ys) 3 + 0x + 0y + 1ys >= 2 + 0y + 1ys Weak: if(false(), xs, ys, zs) -> rev(xs, ys) 0 + 1xs + 0ys + 0zs >= 1 + 0xs + 1ys if(true(), xs, ys, zs) -> zs 0 + 1xs + 0ys + 0zs >= 1zs reverse xs -> rev(xs, nil()) 0 + 0xs >= 2 + 0xs rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys) 1 + 0xs + 1ys >= 1 + 1xs + 0ys append(cons(x, xs), ys) -> cons(x, append(xs, ys)) 2 + 0x + 1xs + 0ys >= 2 + 0x + 1xs + 0ys append(nil(), ys) -> ys 2 + 0ys >= 1ys dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)) 3 + 0x + 0y + 1ys >= 3 + 0x + 0y + 1ys dropLast cons(x, nil()) -> nil() 3 + 0x >= 1 dropLast nil() -> nil() 2 >= 1 last cons(x, cons(y, ys)) -> last cons(y, ys) 0 + 0x + 0y + 0ys >= 0 + 0y + 0ys last cons(x, nil()) -> x 0 + 0x >= 1x isEmpty cons(x, xs) -> false() 2 + 0x + 1xs >= 0 isEmpty nil() -> true() 2 >= 0 Qed SCC (1): Strict: {last# cons(x, cons(y, ys)) -> last# cons(y, ys)} Weak: { isEmpty nil() -> true(), isEmpty cons(x, xs) -> false(), last cons(x, nil()) -> x, last cons(x, cons(y, ys)) -> last cons(y, ys), dropLast nil() -> nil(), dropLast cons(x, nil()) -> nil(), dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)), append(nil(), ys) -> ys, append(cons(x, xs), ys) -> cons(x, append(xs, ys)), rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys), reverse xs -> rev(xs, nil()), if(true(), xs, ys, zs) -> zs, if(false(), xs, ys, zs) -> rev(xs, ys)} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [if](x0, x1, x2, x3) = x0, [cons](x0, x1) = x0 + 1, [append](x0, x1) = x0 + 1, [rev](x0, x1) = x0 + 1, [isEmpty](x0) = x0 + 1, [last](x0) = 0, [dropLast](x0) = x0 + 1, [reverse](x0) = 0, [true] = 0, [nil] = 1, [false] = 0, [last#](x0) = x0 + 1 Strict: last# cons(x, cons(y, ys)) -> last# cons(y, ys) 3 + 0x + 0y + 1ys >= 2 + 0y + 1ys Weak: if(false(), xs, ys, zs) -> rev(xs, ys) 0 + 1xs + 0ys + 0zs >= 1 + 0xs + 1ys if(true(), xs, ys, zs) -> zs 0 + 1xs + 0ys + 0zs >= 1zs reverse xs -> rev(xs, nil()) 0 + 0xs >= 2 + 0xs rev(xs, ys) -> if(isEmpty xs, dropLast xs, append(ys, last xs), ys) 1 + 0xs + 1ys >= 1 + 1xs + 0ys append(cons(x, xs), ys) -> cons(x, append(xs, ys)) 2 + 0x + 1xs + 0ys >= 2 + 0x + 1xs + 0ys append(nil(), ys) -> ys 2 + 0ys >= 1ys dropLast cons(x, cons(y, ys)) -> cons(x, dropLast cons(y, ys)) 3 + 0x + 0y + 1ys >= 3 + 0x + 0y + 1ys dropLast cons(x, nil()) -> nil() 3 + 0x >= 1 dropLast nil() -> nil() 2 >= 1 last cons(x, cons(y, ys)) -> last cons(y, ys) 0 + 0x + 0y + 0ys >= 0 + 0y + 0ys last cons(x, nil()) -> x 0 + 0x >= 1x isEmpty cons(x, xs) -> false() 2 + 0x + 1xs >= 0 isEmpty nil() -> true() 2 >= 0 Qed