MAYBE Time: 0.108082 TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2), mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# from X -> mark# X, mark# from X -> from# mark X, mark# from X -> active# from mark X, mark# s X -> mark# X, mark# s X -> s# mark X, mark# s X -> active# s mark X, mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), mark# sel(X1, X2) -> sel#(mark X1, mark X2), mark# 0() -> active# 0(), mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2), mark# minus(X1, X2) -> minus#(mark X1, mark X2), mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2), mark# quot(X1, X2) -> quot#(mark X1, mark X2), mark# nil() -> active# nil(), mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2), cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2), from# mark X -> from# X, from# active X -> from# X, s# mark X -> s# X, s# active X -> s# X, active# from X -> mark# cons(X, from s X), active# from X -> cons#(X, from s X), active# from X -> from# s X, active# from X -> s# X, active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), active# sel(s N, cons(X, XS)) -> sel#(N, XS), active# sel(0(), cons(X, XS)) -> mark# X, active# minus(X, 0()) -> mark# 0(), active# minus(s X, s Y) -> mark# minus(X, Y), active# minus(s X, s Y) -> minus#(X, Y), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y), active# quot(s X, s Y) -> minus#(X, Y), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y), active# quot(0(), s Y) -> mark# 0(), active# zWquot(XS, nil()) -> mark# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS)), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), active# zWquot(nil(), XS) -> mark# nil(), sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2), minus#(X1, mark X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2), quot#(X1, mark X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2), zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)} TRS: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} UR: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2), a(x, y) -> x, a(x, y) -> y} EDG: { (mark# s X -> mark# X, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# s X -> mark# X, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# s X -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# nil() -> active# nil()) (mark# s X -> mark# X, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# s X -> mark# X, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# s X -> mark# X, mark# quot(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# quot(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# s X -> mark# X, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# s X -> mark# X, mark# minus(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# minus(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# 0() -> active# 0()) (mark# s X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# s X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# s X -> active# s mark X) (mark# s X -> mark# X, mark# s X -> s# mark X) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# from X -> active# from mark X) (mark# s X -> mark# X, mark# from X -> from# mark X) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (from# active X -> from# X, from# active X -> from# X) (from# active X -> from# X, from# mark X -> from# X) (s# active X -> s# X, s# active X -> s# X) (s# active X -> s# X, s# mark X -> s# X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (active# sel(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (active# sel(0(), cons(X, XS)) -> mark# X, mark# nil() -> active# nil()) (active# sel(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> mark# X2) (active# sel(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> mark# X1) (active# sel(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> mark# X2) (active# sel(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> mark# X1) (active# sel(0(), cons(X, XS)) -> mark# X, mark# 0() -> active# 0()) (active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> mark# X2) (active# sel(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> mark# X1) (active# sel(0(), cons(X, XS)) -> mark# X, mark# s X -> active# s mark X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# s X -> s# mark X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# s X -> mark# X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# from X -> active# from mark X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# from X -> from# mark X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# from X -> mark# X) (active# sel(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# sel(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (mark# cons(X1, X2) -> cons#(mark X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# zWquot(nil(), XS) -> mark# nil()) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# zWquot(XS, nil()) -> mark# nil()) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# quot(0(), s Y) -> mark# 0()) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# quot(s X, s Y) -> minus#(X, Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# minus(s X, s Y) -> minus#(X, Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# minus(X, 0()) -> mark# 0()) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# from X -> s# X) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# from X -> from# s X) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# from X -> cons#(X, from s X)) (mark# minus(X1, X2) -> active# minus(mark X1, mark X2), active# from X -> mark# cons(X, from s X)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# zWquot(nil(), XS) -> mark# nil()) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# zWquot(XS, nil()) -> mark# nil()) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# quot(0(), s Y) -> mark# 0()) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# quot(s X, s Y) -> minus#(X, Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# minus(s X, s Y) -> minus#(X, Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# minus(X, 0()) -> mark# 0()) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# from X -> s# X) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# from X -> from# s X) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# from X -> cons#(X, from s X)) (mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# from X -> mark# cons(X, from s X)) (active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y), s# active X -> s# X) (active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y), s# mark X -> s# X) (cons#(X1, active X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, active X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(active X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (sel#(X1, active X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)) (sel#(X1, active X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2)) (sel#(X1, active X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2)) (sel#(X1, active X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2)) (sel#(active X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)) (sel#(active X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2)) (sel#(active X1, X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2)) (sel#(active X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2)) (minus#(X1, active X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2)) (minus#(X1, active X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2)) (minus#(X1, active X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2)) (minus#(X1, active X2) -> minus#(X1, X2), minus#(X1, mark X2) -> minus#(X1, X2)) (minus#(active X1, X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2)) (minus#(active X1, X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2)) (minus#(active X1, X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2)) (minus#(active X1, X2) -> minus#(X1, X2), minus#(X1, mark X2) -> minus#(X1, X2)) (quot#(X1, active X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2)) (quot#(X1, active X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2)) (quot#(X1, active X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2)) (quot#(X1, active X2) -> quot#(X1, X2), quot#(X1, mark X2) -> quot#(X1, X2)) (quot#(active X1, X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2)) (quot#(active X1, X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2)) (quot#(active X1, X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2)) (quot#(active X1, X2) -> quot#(X1, X2), quot#(X1, mark X2) -> quot#(X1, X2)) (zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)) (zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2)) (zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2)) (zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(X1, mark X2) -> zWquot#(X1, X2)) (zWquot#(active X1, X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)) (zWquot#(active X1, X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2)) (zWquot#(active X1, X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2)) (zWquot#(active X1, X2) -> zWquot#(X1, X2), zWquot#(X1, mark X2) -> zWquot#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(mark X1, X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# from X -> active# from mark X, active# zWquot(nil(), XS) -> mark# nil()) (mark# from X -> active# from mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# from X -> active# from mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# from X -> active# from mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# from X -> active# from mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# from X -> active# from mark X, active# zWquot(XS, nil()) -> mark# nil()) (mark# from X -> active# from mark X, active# quot(0(), s Y) -> mark# 0()) (mark# from X -> active# from mark X, active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# from X -> active# from mark X, active# quot(s X, s Y) -> minus#(X, Y)) (mark# from X -> active# from mark X, active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# from X -> active# from mark X, active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# from X -> active# from mark X, active# minus(s X, s Y) -> minus#(X, Y)) (mark# from X -> active# from mark X, active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# from X -> active# from mark X, active# minus(X, 0()) -> mark# 0()) (mark# from X -> active# from mark X, active# sel(0(), cons(X, XS)) -> mark# X) (mark# from X -> active# from mark X, active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# from X -> active# from mark X, active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# from X -> active# from mark X, active# from X -> s# X) (mark# from X -> active# from mark X, active# from X -> from# s X) (mark# from X -> active# from mark X, active# from X -> cons#(X, from s X)) (mark# from X -> active# from mark X, active# from X -> mark# cons(X, from s X)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# zWquot(X1, X2) -> mark# X2) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# zWquot(X1, X2) -> mark# X1) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# nil() -> active# nil()) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# quot(X1, X2) -> mark# X2) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# quot(X1, X2) -> mark# X1) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# minus(X1, X2) -> mark# X2) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# minus(X1, X2) -> mark# X1) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# 0() -> active# 0()) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# sel(X1, X2) -> mark# X2) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# sel(X1, X2) -> mark# X1) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# s X -> active# s mark X) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# s X -> s# mark X) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# s X -> mark# X) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# from X -> active# from mark X) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# from X -> from# mark X) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# from X -> mark# X) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), mark# cons(X1, X2) -> mark# X1) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# zWquot(X1, X2) -> mark# X2) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# zWquot(X1, X2) -> mark# X1) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# nil() -> active# nil()) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# quot(X1, X2) -> mark# X2) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# quot(X1, X2) -> mark# X1) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# minus(X1, X2) -> mark# X2) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# minus(X1, X2) -> mark# X1) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# 0() -> active# 0()) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> mark# X2) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# sel(X1, X2) -> mark# X1) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# s X -> active# s mark X) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# s X -> s# mark X) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# s X -> mark# X) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# from X -> active# from mark X) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# from X -> from# mark X) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# from X -> mark# X) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), mark# cons(X1, X2) -> mark# X1) (mark# from X -> from# mark X, from# active X -> from# X) (mark# from X -> from# mark X, from# mark X -> from# X) (mark# 0() -> active# 0(), active# zWquot(nil(), XS) -> mark# nil()) (mark# 0() -> active# 0(), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# 0() -> active# 0(), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# 0() -> active# 0(), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# 0() -> active# 0(), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# 0() -> active# 0(), active# zWquot(XS, nil()) -> mark# nil()) (mark# 0() -> active# 0(), active# quot(0(), s Y) -> mark# 0()) (mark# 0() -> active# 0(), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# 0() -> active# 0(), active# quot(s X, s Y) -> minus#(X, Y)) (mark# 0() -> active# 0(), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# 0() -> active# 0(), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# 0() -> active# 0(), active# minus(s X, s Y) -> minus#(X, Y)) (mark# 0() -> active# 0(), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# 0() -> active# 0(), active# minus(X, 0()) -> mark# 0()) (mark# 0() -> active# 0(), active# sel(0(), cons(X, XS)) -> mark# X) (mark# 0() -> active# 0(), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# 0() -> active# 0(), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# 0() -> active# 0(), active# from X -> s# X) (mark# 0() -> active# 0(), active# from X -> from# s X) (mark# 0() -> active# 0(), active# from X -> cons#(X, from s X)) (mark# 0() -> active# 0(), active# from X -> mark# cons(X, from s X)) (active# from X -> from# s X, from# active X -> from# X) (active# from X -> from# s X, from# mark X -> from# X) (active# quot(0(), s Y) -> mark# 0(), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# zWquot(X1, X2) -> mark# X2) (active# quot(0(), s Y) -> mark# 0(), mark# zWquot(X1, X2) -> mark# X1) (active# quot(0(), s Y) -> mark# 0(), mark# nil() -> active# nil()) (active# quot(0(), s Y) -> mark# 0(), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# quot(X1, X2) -> mark# X2) (active# quot(0(), s Y) -> mark# 0(), mark# quot(X1, X2) -> mark# X1) (active# quot(0(), s Y) -> mark# 0(), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# minus(X1, X2) -> mark# X2) (active# quot(0(), s Y) -> mark# 0(), mark# minus(X1, X2) -> mark# X1) (active# quot(0(), s Y) -> mark# 0(), mark# 0() -> active# 0()) (active# quot(0(), s Y) -> mark# 0(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# quot(0(), s Y) -> mark# 0(), mark# sel(X1, X2) -> mark# X2) (active# quot(0(), s Y) -> mark# 0(), mark# sel(X1, X2) -> mark# X1) (active# quot(0(), s Y) -> mark# 0(), mark# s X -> active# s mark X) (active# quot(0(), s Y) -> mark# 0(), mark# s X -> s# mark X) (active# quot(0(), s Y) -> mark# 0(), mark# s X -> mark# X) (active# quot(0(), s Y) -> mark# 0(), mark# from X -> active# from mark X) (active# quot(0(), s Y) -> mark# 0(), mark# from X -> from# mark X) (active# quot(0(), s Y) -> mark# 0(), mark# from X -> mark# X) (active# quot(0(), s Y) -> mark# 0(), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# quot(0(), s Y) -> mark# 0(), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# quot(0(), s Y) -> mark# 0(), mark# cons(X1, X2) -> mark# X1) (active# zWquot(nil(), XS) -> mark# nil(), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# zWquot(X1, X2) -> mark# X2) (active# zWquot(nil(), XS) -> mark# nil(), mark# zWquot(X1, X2) -> mark# X1) (active# zWquot(nil(), XS) -> mark# nil(), mark# nil() -> active# nil()) (active# zWquot(nil(), XS) -> mark# nil(), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# quot(X1, X2) -> mark# X2) (active# zWquot(nil(), XS) -> mark# nil(), mark# quot(X1, X2) -> mark# X1) (active# zWquot(nil(), XS) -> mark# nil(), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# minus(X1, X2) -> mark# X2) (active# zWquot(nil(), XS) -> mark# nil(), mark# minus(X1, X2) -> mark# X1) (active# zWquot(nil(), XS) -> mark# nil(), mark# 0() -> active# 0()) (active# zWquot(nil(), XS) -> mark# nil(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# sel(X1, X2) -> mark# X2) (active# zWquot(nil(), XS) -> mark# nil(), mark# sel(X1, X2) -> mark# X1) (active# zWquot(nil(), XS) -> mark# nil(), mark# s X -> active# s mark X) (active# zWquot(nil(), XS) -> mark# nil(), mark# s X -> s# mark X) (active# zWquot(nil(), XS) -> mark# nil(), mark# s X -> mark# X) (active# zWquot(nil(), XS) -> mark# nil(), mark# from X -> active# from mark X) (active# zWquot(nil(), XS) -> mark# nil(), mark# from X -> from# mark X) (active# zWquot(nil(), XS) -> mark# nil(), mark# from X -> mark# X) (active# zWquot(nil(), XS) -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# zWquot(nil(), XS) -> mark# nil(), mark# cons(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# minus(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# minus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# minus(X1, X2) -> mark# X2, mark# from X -> active# from mark X) (mark# minus(X1, X2) -> mark# X2, mark# from X -> from# mark X) (mark# minus(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# minus(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# minus(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# minus(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# zWquot(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# zWquot(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# zWquot(X1, X2) -> mark# X2, mark# from X -> active# from mark X) (mark# zWquot(X1, X2) -> mark# X2, mark# from X -> from# mark X) (mark# zWquot(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# zWquot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> minus#(mark X1, mark X2), minus#(active X1, X2) -> minus#(X1, X2)) (mark# minus(X1, X2) -> minus#(mark X1, mark X2), minus#(mark X1, X2) -> minus#(X1, X2)) (mark# minus(X1, X2) -> minus#(mark X1, mark X2), minus#(X1, active X2) -> minus#(X1, X2)) (mark# minus(X1, X2) -> minus#(mark X1, mark X2), minus#(X1, mark X2) -> minus#(X1, X2)) (mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)) (mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2)) (mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2), zWquot#(X1, active X2) -> zWquot#(X1, X2)) (mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2), zWquot#(X1, mark X2) -> zWquot#(X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# cons(X1, X2) -> mark# X1, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> active# from mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# minus(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# minus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# minus(X1, X2) -> mark# X1, mark# from X -> active# from mark X) (mark# minus(X1, X2) -> mark# X1, mark# from X -> from# mark X) (mark# minus(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# minus(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# minus(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# minus(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# zWquot(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# zWquot(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# zWquot(X1, X2) -> mark# X1, mark# from X -> active# from mark X) (mark# zWquot(X1, X2) -> mark# X1, mark# from X -> from# mark X) (mark# zWquot(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# zWquot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (active# quot(s X, s Y) -> minus#(X, Y), minus#(active X1, X2) -> minus#(X1, X2)) (active# quot(s X, s Y) -> minus#(X, Y), minus#(mark X1, X2) -> minus#(X1, X2)) (active# quot(s X, s Y) -> minus#(X, Y), minus#(X1, active X2) -> minus#(X1, X2)) (active# quot(s X, s Y) -> minus#(X, Y), minus#(X1, mark X2) -> minus#(X1, X2)) (active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(active X1, X2) -> sel#(X1, X2)) (active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(mark X1, X2) -> sel#(X1, X2)) (active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(X1, active X2) -> sel#(X1, X2)) (active# sel(s N, cons(X, XS)) -> sel#(N, XS), sel#(X1, mark X2) -> sel#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(X1, mark X2) -> quot#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(X1, active X2) -> quot#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(mark X1, X2) -> quot#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y), quot#(active X1, X2) -> quot#(X1, X2)) (active# minus(s X, s Y) -> minus#(X, Y), minus#(X1, mark X2) -> minus#(X1, X2)) (active# minus(s X, s Y) -> minus#(X, Y), minus#(X1, active X2) -> minus#(X1, X2)) (active# minus(s X, s Y) -> minus#(X, Y), minus#(mark X1, X2) -> minus#(X1, X2)) (active# minus(s X, s Y) -> minus#(X, Y), minus#(active X1, X2) -> minus#(X1, X2)) (mark# quot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# quot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# quot(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# quot(X1, X2) -> mark# X1, mark# from X -> from# mark X) (mark# quot(X1, X2) -> mark# X1, mark# from X -> active# from mark X) (mark# quot(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# quot(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# quot(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# sel(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# from X -> from# mark X) (mark# sel(X1, X2) -> mark# X1, mark# from X -> active# from mark X) (mark# sel(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# s X -> s# mark X) (mark# sel(X1, X2) -> mark# X1, mark# s X -> active# s mark X) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# quot(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(X1, mark X2) -> quot#(X1, X2)) (active# quot(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(X1, active X2) -> quot#(X1, X2)) (active# quot(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(mark X1, X2) -> quot#(X1, X2)) (active# quot(s X, s Y) -> quot#(minus(X, Y), s Y), quot#(active X1, X2) -> quot#(X1, X2)) (mark# quot(X1, X2) -> quot#(mark X1, mark X2), quot#(X1, mark X2) -> quot#(X1, X2)) (mark# quot(X1, X2) -> quot#(mark X1, mark X2), quot#(X1, active X2) -> quot#(X1, X2)) (mark# quot(X1, X2) -> quot#(mark X1, mark X2), quot#(mark X1, X2) -> quot#(X1, X2)) (mark# quot(X1, X2) -> quot#(mark X1, mark X2), quot#(active X1, X2) -> quot#(X1, X2)) (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, mark X2) -> sel#(X1, X2)) (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(X1, active X2) -> sel#(X1, X2)) (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(mark X1, X2) -> sel#(X1, X2)) (mark# sel(X1, X2) -> sel#(mark X1, mark X2), sel#(active X1, X2) -> sel#(X1, X2)) (mark# quot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# quot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# quot(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# quot(X1, X2) -> mark# X2, mark# from X -> from# mark X) (mark# quot(X1, X2) -> mark# X2, mark# from X -> active# from mark X) (mark# quot(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# quot(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# quot(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# from X -> from# mark X) (mark# sel(X1, X2) -> mark# X2, mark# from X -> active# from mark X) (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# s X -> s# mark X) (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s mark X) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# cons(X1, X2) -> mark# X1) (active# zWquot(XS, nil()) -> mark# nil(), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# from X -> mark# X) (active# zWquot(XS, nil()) -> mark# nil(), mark# from X -> from# mark X) (active# zWquot(XS, nil()) -> mark# nil(), mark# from X -> active# from mark X) (active# zWquot(XS, nil()) -> mark# nil(), mark# s X -> mark# X) (active# zWquot(XS, nil()) -> mark# nil(), mark# s X -> s# mark X) (active# zWquot(XS, nil()) -> mark# nil(), mark# s X -> active# s mark X) (active# zWquot(XS, nil()) -> mark# nil(), mark# sel(X1, X2) -> mark# X1) (active# zWquot(XS, nil()) -> mark# nil(), mark# sel(X1, X2) -> mark# X2) (active# zWquot(XS, nil()) -> mark# nil(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# 0() -> active# 0()) (active# zWquot(XS, nil()) -> mark# nil(), mark# minus(X1, X2) -> mark# X1) (active# zWquot(XS, nil()) -> mark# nil(), mark# minus(X1, X2) -> mark# X2) (active# zWquot(XS, nil()) -> mark# nil(), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# quot(X1, X2) -> mark# X1) (active# zWquot(XS, nil()) -> mark# nil(), mark# quot(X1, X2) -> mark# X2) (active# zWquot(XS, nil()) -> mark# nil(), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# nil() -> active# nil()) (active# zWquot(XS, nil()) -> mark# nil(), mark# zWquot(X1, X2) -> mark# X1) (active# zWquot(XS, nil()) -> mark# nil(), mark# zWquot(X1, X2) -> mark# X2) (active# zWquot(XS, nil()) -> mark# nil(), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# zWquot(XS, nil()) -> mark# nil(), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# cons(X1, X2) -> mark# X1) (active# minus(X, 0()) -> mark# 0(), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# minus(X, 0()) -> mark# 0(), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# minus(X, 0()) -> mark# 0(), mark# from X -> mark# X) (active# minus(X, 0()) -> mark# 0(), mark# from X -> from# mark X) (active# minus(X, 0()) -> mark# 0(), mark# from X -> active# from mark X) (active# minus(X, 0()) -> mark# 0(), mark# s X -> mark# X) (active# minus(X, 0()) -> mark# 0(), mark# s X -> s# mark X) (active# minus(X, 0()) -> mark# 0(), mark# s X -> active# s mark X) (active# minus(X, 0()) -> mark# 0(), mark# sel(X1, X2) -> mark# X1) (active# minus(X, 0()) -> mark# 0(), mark# sel(X1, X2) -> mark# X2) (active# minus(X, 0()) -> mark# 0(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# 0() -> active# 0()) (active# minus(X, 0()) -> mark# 0(), mark# minus(X1, X2) -> mark# X1) (active# minus(X, 0()) -> mark# 0(), mark# minus(X1, X2) -> mark# X2) (active# minus(X, 0()) -> mark# 0(), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# quot(X1, X2) -> mark# X1) (active# minus(X, 0()) -> mark# 0(), mark# quot(X1, X2) -> mark# X2) (active# minus(X, 0()) -> mark# 0(), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# nil() -> active# nil()) (active# minus(X, 0()) -> mark# 0(), mark# zWquot(X1, X2) -> mark# X1) (active# minus(X, 0()) -> mark# 0(), mark# zWquot(X1, X2) -> mark# X2) (active# minus(X, 0()) -> mark# 0(), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# minus(X, 0()) -> mark# 0(), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# nil() -> active# nil(), active# from X -> mark# cons(X, from s X)) (mark# nil() -> active# nil(), active# from X -> cons#(X, from s X)) (mark# nil() -> active# nil(), active# from X -> from# s X) (mark# nil() -> active# nil(), active# from X -> s# X) (mark# nil() -> active# nil(), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# nil() -> active# nil(), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# nil() -> active# nil(), active# sel(0(), cons(X, XS)) -> mark# X) (mark# nil() -> active# nil(), active# minus(X, 0()) -> mark# 0()) (mark# nil() -> active# nil(), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# nil() -> active# nil(), active# minus(s X, s Y) -> minus#(X, Y)) (mark# nil() -> active# nil(), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# nil() -> active# nil(), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# nil() -> active# nil(), active# quot(s X, s Y) -> minus#(X, Y)) (mark# nil() -> active# nil(), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# nil() -> active# nil(), active# quot(0(), s Y) -> mark# 0()) (mark# nil() -> active# nil(), active# zWquot(XS, nil()) -> mark# nil()) (mark# nil() -> active# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# nil() -> active# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# nil() -> active# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# nil() -> active# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# nil() -> active# nil(), active# zWquot(nil(), XS) -> mark# nil()) (mark# s X -> s# mark X, s# mark X -> s# X) (mark# s X -> s# mark X, s# active X -> s# X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# cons(X1, X2) -> mark# X1) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# from X -> mark# X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# from X -> from# mark X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# from X -> active# from mark X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# s X -> mark# X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# s X -> s# mark X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# s X -> active# s mark X) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# sel(X1, X2) -> mark# X1) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# sel(X1, X2) -> mark# X2) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# 0() -> active# 0()) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# minus(X1, X2) -> mark# X1) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# minus(X1, X2) -> mark# X2) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# quot(X1, X2) -> mark# X1) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# quot(X1, X2) -> mark# X2) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# nil() -> active# nil()) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# zWquot(X1, X2) -> mark# X1) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# zWquot(X1, X2) -> mark# X2) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# minus(s X, s Y) -> mark# minus(X, Y), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> mark# cons(X, from s X)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> cons#(X, from s X)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> from# s X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# from X -> s# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# sel(0(), cons(X, XS)) -> mark# X) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# minus(X, 0()) -> mark# 0()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# minus(s X, s Y) -> minus#(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# quot(s X, s Y) -> minus#(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# quot(0(), s Y) -> mark# 0()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zWquot(XS, nil()) -> mark# nil()) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# cons(X1, X2) -> active# cons(mark X1, X2), active# zWquot(nil(), XS) -> mark# nil()) (mark# s X -> active# s mark X, active# from X -> mark# cons(X, from s X)) (mark# s X -> active# s mark X, active# from X -> cons#(X, from s X)) (mark# s X -> active# s mark X, active# from X -> from# s X) (mark# s X -> active# s mark X, active# from X -> s# X) (mark# s X -> active# s mark X, active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# s X -> active# s mark X, active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# s X -> active# s mark X, active# sel(0(), cons(X, XS)) -> mark# X) (mark# s X -> active# s mark X, active# minus(X, 0()) -> mark# 0()) (mark# s X -> active# s mark X, active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# s X -> active# s mark X, active# minus(s X, s Y) -> minus#(X, Y)) (mark# s X -> active# s mark X, active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# s X -> active# s mark X, active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# s X -> active# s mark X, active# quot(s X, s Y) -> minus#(X, Y)) (mark# s X -> active# s mark X, active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# s X -> active# s mark X, active# quot(0(), s Y) -> mark# 0()) (mark# s X -> active# s mark X, active# zWquot(XS, nil()) -> mark# nil()) (mark# s X -> active# s mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# s X -> active# s mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# s X -> active# s mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# s X -> active# s mark X, active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# s X -> active# s mark X, active# zWquot(nil(), XS) -> mark# nil()) (active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS)), cons#(X1, mark X2) -> cons#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS)), cons#(X1, active X2) -> cons#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS)), cons#(mark X1, X2) -> cons#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS)), cons#(active X1, X2) -> cons#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), zWquot#(X1, mark X2) -> zWquot#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), zWquot#(X1, active X2) -> zWquot#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), zWquot#(mark X1, X2) -> zWquot#(X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS), zWquot#(active X1, X2) -> zWquot#(X1, X2)) (zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(X1, mark X2) -> zWquot#(X1, X2)) (zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2)) (zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2)) (zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)) (zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(X1, mark X2) -> zWquot#(X1, X2)) (zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2)) (zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2)) (zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)) (quot#(mark X1, X2) -> quot#(X1, X2), quot#(X1, mark X2) -> quot#(X1, X2)) (quot#(mark X1, X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2)) (quot#(mark X1, X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2)) (quot#(mark X1, X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2)) (quot#(X1, mark X2) -> quot#(X1, X2), quot#(X1, mark X2) -> quot#(X1, X2)) (quot#(X1, mark X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2)) (quot#(X1, mark X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2)) (quot#(X1, mark X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2)) (minus#(mark X1, X2) -> minus#(X1, X2), minus#(X1, mark X2) -> minus#(X1, X2)) (minus#(mark X1, X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2)) (minus#(mark X1, X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2)) (minus#(mark X1, X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2)) (minus#(X1, mark X2) -> minus#(X1, X2), minus#(X1, mark X2) -> minus#(X1, X2)) (minus#(X1, mark X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2)) (minus#(X1, mark X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2)) (minus#(X1, mark X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2)) (sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2)) (sel#(mark X1, X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2)) (sel#(mark X1, X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2)) (sel#(mark X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)) (sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, mark X2) -> sel#(X1, X2)) (sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2)) (sel#(X1, mark X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2)) (sel#(X1, mark X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, mark X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2)) (cons#(X1, mark X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)) (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# from X -> mark# X) (active# from X -> mark# cons(X, from s X), mark# from X -> from# mark X) (active# from X -> mark# cons(X, from s X), mark# from X -> active# from mark X) (active# from X -> mark# cons(X, from s X), mark# s X -> mark# X) (active# from X -> mark# cons(X, from s X), mark# s X -> s# mark X) (active# from X -> mark# cons(X, from s X), mark# s X -> active# s mark X) (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> mark# X2) (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0()) (active# from X -> mark# cons(X, from s X), mark# minus(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# minus(X1, X2) -> mark# X2) (active# from X -> mark# cons(X, from s X), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# quot(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# quot(X1, X2) -> mark# X2) (active# from X -> mark# cons(X, from s X), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# nil() -> active# nil()) (active# from X -> mark# cons(X, from s X), mark# zWquot(X1, X2) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# zWquot(X1, X2) -> mark# X2) (active# from X -> mark# cons(X, from s X), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# from X -> mark# cons(X, from s X), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# from X -> mark# cons(X, from s X)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# from X -> cons#(X, from s X)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# from X -> from# s X) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# from X -> s# X) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# minus(X, 0()) -> mark# 0()) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# minus(s X, s Y) -> minus#(X, Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# quot(s X, s Y) -> minus#(X, Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# quot(0(), s Y) -> mark# 0()) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# zWquot(XS, nil()) -> mark# nil()) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# quot(X1, X2) -> active# quot(mark X1, mark X2), active# zWquot(nil(), XS) -> mark# nil()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> mark# cons(X, from s X)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> cons#(X, from s X)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> from# s X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# from X -> s# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s N, cons(X, XS)) -> sel#(N, XS)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(0(), cons(X, XS)) -> mark# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# minus(X, 0()) -> mark# 0()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# minus(s X, s Y) -> mark# minus(X, Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# minus(s X, s Y) -> minus#(X, Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# quot(s X, s Y) -> s# quot(minus(X, Y), s Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# quot(s X, s Y) -> minus#(X, Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# quot(s X, s Y) -> quot#(minus(X, Y), s Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# quot(0(), s Y) -> mark# 0()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# zWquot(XS, nil()) -> mark# nil()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS))) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> cons#(quot(X, Y), zWquot(XS, YS))) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> quot#(X, Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# zWquot(cons(X, XS), cons(Y, YS)) -> zWquot#(XS, YS)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# zWquot(nil(), XS) -> mark# nil()) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# cons(X1, X2) -> mark# X1) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# cons(X1, X2) -> cons#(mark X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# cons(X1, X2) -> active# cons(mark X1, X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# from X -> mark# X) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# from X -> from# mark X) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# from X -> active# from mark X) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# s X -> mark# X) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# s X -> s# mark X) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# s X -> active# s mark X) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# sel(X1, X2) -> mark# X1) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# sel(X1, X2) -> mark# X2) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# 0() -> active# 0()) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# minus(X1, X2) -> mark# X1) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# minus(X1, X2) -> mark# X2) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# quot(X1, X2) -> mark# X1) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# quot(X1, X2) -> mark# X2) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# nil() -> active# nil()) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# zWquot(X1, X2) -> mark# X1) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# zWquot(X1, X2) -> mark# X2) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) (active# from X -> s# X, s# mark X -> s# X) (active# from X -> s# X, s# active X -> s# X) (s# mark X -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (from# mark X -> from# X, from# mark X -> from# X) (from# mark X -> from# X, from# active X -> from# X) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# cons(X1, X2) -> cons#(mark X1, X2)) (mark# from X -> mark# X, mark# cons(X1, X2) -> active# cons(mark X1, X2)) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# from X -> from# mark X) (mark# from X -> mark# X, mark# from X -> active# from mark X) (mark# from X -> mark# X, mark# s X -> mark# X) (mark# from X -> mark# X, mark# s X -> s# mark X) (mark# from X -> mark# X, mark# s X -> active# s mark X) (mark# from X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# from X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# from X -> mark# X, mark# 0() -> active# 0()) (mark# from X -> mark# X, mark# minus(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# minus(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# minus(X1, X2) -> active# minus(mark X1, mark X2)) (mark# from X -> mark# X, mark# minus(X1, X2) -> minus#(mark X1, mark X2)) (mark# from X -> mark# X, mark# quot(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# quot(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# quot(X1, X2) -> active# quot(mark X1, mark X2)) (mark# from X -> mark# X, mark# quot(X1, X2) -> quot#(mark X1, mark X2)) (mark# from X -> mark# X, mark# nil() -> active# nil()) (mark# from X -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (mark# from X -> mark# X, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2)) (mark# from X -> mark# X, mark# zWquot(X1, X2) -> zWquot#(mark X1, mark X2)) } STATUS: arrows: 0.825231 SCCS (8): Scc: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# from X -> mark# X, mark# from X -> active# from mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), mark# 0() -> active# 0(), mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2), mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2), mark# nil() -> active# nil(), mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# from X -> mark# cons(X, from s X), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), active# sel(0(), cons(X, XS)) -> mark# X, active# minus(X, 0()) -> mark# 0(), active# minus(s X, s Y) -> mark# minus(X, Y), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), active# quot(0(), s Y) -> mark# 0(), active# zWquot(XS, nil()) -> mark# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), active# zWquot(nil(), XS) -> mark# nil()} Scc: { zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)} Scc: { quot#(X1, mark X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2)} Scc: { minus#(X1, mark X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2)} Scc: { sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { from# mark X -> from# X, from# active X -> from# X} Scc: { cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)} SCC (30): Strict: { mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(mark X1, X2), mark# from X -> mark# X, mark# from X -> active# from mark X, mark# s X -> mark# X, mark# s X -> active# s mark X, mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), mark# 0() -> active# 0(), mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> active# minus(mark X1, mark X2), mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> active# quot(mark X1, mark X2), mark# nil() -> active# nil(), mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> active# zWquot(mark X1, mark X2), active# from X -> mark# cons(X, from s X), active# sel(s N, cons(X, XS)) -> mark# sel(N, XS), active# sel(0(), cons(X, XS)) -> mark# X, active# minus(X, 0()) -> mark# 0(), active# minus(s X, s Y) -> mark# minus(X, Y), active# quot(s X, s Y) -> mark# s quot(minus(X, Y), s Y), active# quot(0(), s Y) -> mark# 0(), active# zWquot(XS, nil()) -> mark# nil(), active# zWquot(cons(X, XS), cons(Y, YS)) -> mark# cons(quot(X, Y), zWquot(XS, YS)), active# zWquot(nil(), XS) -> mark# nil()} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (4): Strict: { zWquot#(X1, mark X2) -> zWquot#(X1, X2), zWquot#(X1, active X2) -> zWquot#(X1, X2), zWquot#(mark X1, X2) -> zWquot#(X1, X2), zWquot#(active X1, X2) -> zWquot#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (4): Strict: { quot#(X1, mark X2) -> quot#(X1, X2), quot#(X1, active X2) -> quot#(X1, X2), quot#(mark X1, X2) -> quot#(X1, X2), quot#(active X1, X2) -> quot#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (4): Strict: { minus#(X1, mark X2) -> minus#(X1, X2), minus#(X1, active X2) -> minus#(X1, X2), minus#(mark X1, X2) -> minus#(X1, X2), minus#(active X1, X2) -> minus#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (4): Strict: { sel#(X1, mark X2) -> sel#(X1, X2), sel#(X1, active X2) -> sel#(X1, X2), sel#(mark X1, X2) -> sel#(X1, X2), sel#(active X1, X2) -> sel#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (2): Strict: { from# mark X -> from# X, from# active X -> from# X} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open SCC (4): Strict: { cons#(X1, mark X2) -> cons#(X1, X2), cons#(X1, active X2) -> cons#(X1, X2), cons#(mark X1, X2) -> cons#(X1, X2), cons#(active X1, X2) -> cons#(X1, X2)} Weak: { mark cons(X1, X2) -> active cons(mark X1, X2), mark from X -> active from mark X, mark s X -> active s mark X, mark sel(X1, X2) -> active sel(mark X1, mark X2), mark 0() -> active 0(), mark minus(X1, X2) -> active minus(mark X1, mark X2), mark quot(X1, X2) -> active quot(mark X1, mark X2), mark nil() -> active nil(), mark zWquot(X1, X2) -> active zWquot(mark X1, mark X2), cons(X1, mark X2) -> cons(X1, X2), cons(X1, active X2) -> cons(X1, X2), cons(mark X1, X2) -> cons(X1, X2), cons(active X1, X2) -> cons(X1, X2), from mark X -> from X, from active X -> from X, s mark X -> s X, s active X -> s X, active from X -> mark cons(X, from s X), active sel(s N, cons(X, XS)) -> mark sel(N, XS), active sel(0(), cons(X, XS)) -> mark X, active minus(X, 0()) -> mark 0(), active minus(s X, s Y) -> mark minus(X, Y), active quot(s X, s Y) -> mark s quot(minus(X, Y), s Y), active quot(0(), s Y) -> mark 0(), active zWquot(XS, nil()) -> mark nil(), active zWquot(cons(X, XS), cons(Y, YS)) -> mark cons(quot(X, Y), zWquot(XS, YS)), active zWquot(nil(), XS) -> mark nil(), sel(X1, mark X2) -> sel(X1, X2), sel(X1, active X2) -> sel(X1, X2), sel(mark X1, X2) -> sel(X1, X2), sel(active X1, X2) -> sel(X1, X2), minus(X1, mark X2) -> minus(X1, X2), minus(X1, active X2) -> minus(X1, X2), minus(mark X1, X2) -> minus(X1, X2), minus(active X1, X2) -> minus(X1, X2), quot(X1, mark X2) -> quot(X1, X2), quot(X1, active X2) -> quot(X1, X2), quot(mark X1, X2) -> quot(X1, X2), quot(active X1, X2) -> quot(X1, X2), zWquot(X1, mark X2) -> zWquot(X1, X2), zWquot(X1, active X2) -> zWquot(X1, X2), zWquot(mark X1, X2) -> zWquot(X1, X2), zWquot(active X1, X2) -> zWquot(X1, X2)} Open