MAYBE Time: 2.265493 TRS: { mark cons(X1, X2) -> cons(mark X1, X2), mark from X -> a__from mark X, mark s X -> s mark X, mark 0() -> 0(), mark nil() -> nil(), mark zWquot(X1, X2) -> a__zWquot(mark X1, mark X2), mark sel(X1, X2) -> a__sel(mark X1, mark X2), mark minus(X1, X2) -> a__minus(mark X1, mark X2), mark quot(X1, X2) -> a__quot(mark X1, mark X2), a__from X -> cons(mark X, from s X), a__from X -> from X, a__sel(X1, X2) -> sel(X1, X2), a__sel(s N, cons(X, XS)) -> a__sel(mark N, mark XS), a__sel(0(), cons(X, XS)) -> mark X, a__minus(X, 0()) -> 0(), a__minus(X1, X2) -> minus(X1, X2), a__minus(s X, s Y) -> a__minus(mark X, mark Y), a__quot(X1, X2) -> quot(X1, X2), a__quot(s X, s Y) -> s a__quot(a__minus(mark X, mark Y), s mark Y), a__quot(0(), s Y) -> 0(), a__zWquot(XS, nil()) -> nil(), a__zWquot(X1, X2) -> zWquot(X1, X2), a__zWquot(cons(X, XS), cons(Y, YS)) -> cons(a__quot(mark X, mark Y), zWquot(XS, YS)), a__zWquot(nil(), XS) -> nil()} DP: DP: { mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2), mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2), mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__from# X -> mark# X, a__sel#(s N, cons(X, XS)) -> mark# XS, a__sel#(s N, cons(X, XS)) -> mark# N, a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(0(), cons(X, XS)) -> mark# X, a__minus#(s X, s Y) -> mark# X, a__minus#(s X, s Y) -> mark# Y, a__minus#(s X, s Y) -> a__minus#(mark X, mark Y), a__quot#(s X, s Y) -> mark# X, a__quot#(s X, s Y) -> mark# Y, a__quot#(s X, s Y) -> a__minus#(mark X, mark Y), a__quot#(s X, s Y) -> a__quot#(a__minus(mark X, mark Y), s mark Y), a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y)} TRS: { mark cons(X1, X2) -> cons(mark X1, X2), mark from X -> a__from mark X, mark s X -> s mark X, mark 0() -> 0(), mark nil() -> nil(), mark zWquot(X1, X2) -> a__zWquot(mark X1, mark X2), mark sel(X1, X2) -> a__sel(mark X1, mark X2), mark minus(X1, X2) -> a__minus(mark X1, mark X2), mark quot(X1, X2) -> a__quot(mark X1, mark X2), a__from X -> cons(mark X, from s X), a__from X -> from X, a__sel(X1, X2) -> sel(X1, X2), a__sel(s N, cons(X, XS)) -> a__sel(mark N, mark XS), a__sel(0(), cons(X, XS)) -> mark X, a__minus(X, 0()) -> 0(), a__minus(X1, X2) -> minus(X1, X2), a__minus(s X, s Y) -> a__minus(mark X, mark Y), a__quot(X1, X2) -> quot(X1, X2), a__quot(s X, s Y) -> s a__quot(a__minus(mark X, mark Y), s mark Y), a__quot(0(), s Y) -> 0(), a__zWquot(XS, nil()) -> nil(), a__zWquot(X1, X2) -> zWquot(X1, X2), a__zWquot(cons(X, XS), cons(Y, YS)) -> cons(a__quot(mark X, mark Y), zWquot(XS, YS)), a__zWquot(nil(), XS) -> nil()} EDG: { (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(0(), cons(X, XS)) -> mark# X) (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS)) (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s N, cons(X, XS)) -> mark# N) (mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), a__sel#(s N, cons(X, XS)) -> mark# XS) (mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__quot#(s X, s Y) -> a__quot#(a__minus(mark X, mark Y), s mark Y)) (mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__quot#(s X, s Y) -> a__minus#(mark X, mark Y)) (mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__quot#(s X, s Y) -> mark# Y) (mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__quot#(s X, s Y) -> mark# X) (a__minus#(s X, s Y) -> a__minus#(mark X, mark Y), a__minus#(s X, s Y) -> a__minus#(mark X, mark Y)) (a__minus#(s X, s Y) -> a__minus#(mark X, mark Y), a__minus#(s X, s Y) -> mark# Y) (a__minus#(s X, s Y) -> a__minus#(mark X, mark Y), a__minus#(s X, s Y) -> mark# X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y), a__quot#(s X, s Y) -> a__quot#(a__minus(mark X, mark Y), s mark Y)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y), a__quot#(s X, s Y) -> a__minus#(mark X, mark Y)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y), a__quot#(s X, s Y) -> mark# Y) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y), a__quot#(s X, s Y) -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# sel(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# quot(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# quot(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# quot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# quot(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# quot(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# minus(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# minus(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# sel(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# sel(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# zWquot(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# zWquot(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# s X -> mark# X) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# from X -> a__from# mark X) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# from X -> mark# X) (a__sel#(s N, cons(X, XS)) -> mark# XS, mark# cons(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# Y, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# Y, mark# quot(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# Y, mark# quot(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# Y, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# Y, mark# minus(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# Y, mark# minus(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# Y, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# Y, mark# sel(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# Y, mark# sel(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# Y, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# Y, mark# zWquot(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# Y, mark# zWquot(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# Y, mark# s X -> mark# X) (a__quot#(s X, s Y) -> mark# Y, mark# from X -> a__from# mark X) (a__quot#(s X, s Y) -> mark# Y, mark# from X -> mark# X) (a__quot#(s X, s Y) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# quot(X1, X2) -> a__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) -> a__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# sel(X1, X2) -> a__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# zWquot(X1, X2) -> a__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# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# sel(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# sel(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# quot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# quot(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# quot(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# quot(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# quot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# quot(X1, X2) -> a__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) -> a__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# sel(X1, X2) -> a__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# zWquot(X1, X2) -> a__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# s X -> mark# X) (mark# s X -> mark# X, mark# from X -> a__from# mark X) (mark# s X -> mark# X, mark# from X -> mark# X) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> mark# X2) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# quot(X1, X2) -> mark# X1) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> mark# X2) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# minus(X1, X2) -> mark# X1) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> mark# X2) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# sel(X1, X2) -> mark# X1) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# s X -> mark# X) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# from X -> a__from# mark X) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# from X -> mark# X) (a__sel#(0(), cons(X, XS)) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# X, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# X, mark# quot(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# X, mark# quot(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# X, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# X, mark# minus(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# X, mark# minus(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# X, mark# sel(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# X, mark# sel(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# X, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__quot#(s X, s Y) -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (a__quot#(s X, s Y) -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (a__quot#(s X, s Y) -> mark# X, mark# s X -> mark# X) (a__quot#(s X, s Y) -> mark# X, mark# from X -> a__from# mark X) (a__quot#(s X, s Y) -> mark# X, mark# from X -> mark# X) (a__quot#(s X, s Y) -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> a__from# mark X, a__from# X -> mark# X) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# from X -> mark# X) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# from X -> a__from# mark X) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# s X -> mark# X) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# zWquot(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# zWquot(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# sel(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# sel(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# minus(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# minus(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# quot(X1, X2) -> mark# X1) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# quot(X1, X2) -> mark# X2) (a__sel#(s N, cons(X, XS)) -> mark# N, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> mark# X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# from X -> a__from# mark X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# s X -> mark# X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# sel(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# sel(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# minus(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# minus(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# quot(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# quot(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# X, mark# from X -> mark# X) (a__minus#(s X, s Y) -> mark# X, mark# from X -> a__from# mark X) (a__minus#(s X, s Y) -> mark# X, mark# s X -> mark# X) (a__minus#(s X, s Y) -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# X, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# X, mark# sel(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# X, mark# sel(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# X, mark# minus(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# X, mark# minus(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# X, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# X, mark# quot(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# X, mark# quot(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# X, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__from# X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# from X -> mark# X) (a__from# X -> mark# X, mark# from X -> a__from# mark X) (a__from# X -> mark# X, mark# s X -> mark# X) (a__from# X -> mark# X, mark# zWquot(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# zWquot(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__from# X -> mark# X, mark# sel(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# sel(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__from# X -> mark# X, mark# minus(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# minus(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__from# X -> mark# X, mark# quot(X1, X2) -> mark# X1) (a__from# X -> mark# X, mark# quot(X1, X2) -> mark# X2) (a__from# X -> mark# X, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# from X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# from X -> mark# X, mark# from X -> mark# X) (mark# from X -> mark# X, mark# from X -> a__from# mark X) (mark# from X -> mark# X, mark# s X -> mark# X) (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) -> a__zWquot#(mark X1, mark X2)) (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) -> a__sel#(mark X1, mark X2)) (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) -> a__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) -> a__quot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# minus(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# minus(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X1, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# from X -> mark# X) (mark# zWquot(X1, X2) -> mark# X1, mark# from X -> a__from# mark X) (mark# zWquot(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> mark# X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# from X -> a__from# mark X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# s X -> mark# X) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWquot(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWquot(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# sel(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# sel(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# minus(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# minus(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# quot(X1, X2) -> mark# X1) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# quot(X1, X2) -> mark# X2) (a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# Y, mark# cons(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# Y, mark# from X -> mark# X) (a__minus#(s X, s Y) -> mark# Y, mark# from X -> a__from# mark X) (a__minus#(s X, s Y) -> mark# Y, mark# s X -> mark# X) (a__minus#(s X, s Y) -> mark# Y, mark# zWquot(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# Y, mark# zWquot(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# Y, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# Y, mark# sel(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# Y, mark# sel(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# Y, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# Y, mark# minus(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# Y, mark# minus(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# Y, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (a__minus#(s X, s Y) -> mark# Y, mark# quot(X1, X2) -> mark# X1) (a__minus#(s X, s Y) -> mark# Y, mark# quot(X1, X2) -> mark# X2) (a__minus#(s X, s Y) -> mark# Y, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# minus(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# minus(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# minus(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# from X -> mark# X) (mark# zWquot(X1, X2) -> mark# X2, mark# from X -> a__from# mark X) (mark# zWquot(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2)) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X1) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> mark# X2) (mark# zWquot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2)) (a__quot#(s X, s Y) -> a__minus#(mark X, mark Y), a__minus#(s X, s Y) -> mark# X) (a__quot#(s X, s Y) -> a__minus#(mark X, mark Y), a__minus#(s X, s Y) -> mark# Y) (a__quot#(s X, s Y) -> a__minus#(mark X, mark Y), a__minus#(s X, s Y) -> a__minus#(mark X, mark Y)) (a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(s N, cons(X, XS)) -> mark# XS) (a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(s N, cons(X, XS)) -> mark# N) (a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS)) (a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(0(), cons(X, XS)) -> mark# X) (mark# minus(X1, X2) -> a__minus#(mark X1, mark X2), a__minus#(s X, s Y) -> mark# X) (mark# minus(X1, X2) -> a__minus#(mark X1, mark X2), a__minus#(s X, s Y) -> mark# Y) (mark# minus(X1, X2) -> a__minus#(mark X1, mark X2), a__minus#(s X, s Y) -> a__minus#(mark X, mark Y)) (mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2), a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X) (mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2), a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y) (mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2), a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y)) } STATUS: arrows: 0.620187 SCCS (1): Scc: { mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2), mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2), mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__from# X -> mark# X, a__sel#(s N, cons(X, XS)) -> mark# XS, a__sel#(s N, cons(X, XS)) -> mark# N, a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(0(), cons(X, XS)) -> mark# X, a__minus#(s X, s Y) -> mark# X, a__minus#(s X, s Y) -> mark# Y, a__minus#(s X, s Y) -> a__minus#(mark X, mark Y), a__quot#(s X, s Y) -> mark# X, a__quot#(s X, s Y) -> mark# Y, a__quot#(s X, s Y) -> a__minus#(mark X, mark Y), a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y)} SCC (30): Strict: { mark# cons(X1, X2) -> mark# X1, mark# from X -> mark# X, mark# from X -> a__from# mark X, mark# s X -> mark# X, mark# zWquot(X1, X2) -> mark# X1, mark# zWquot(X1, X2) -> mark# X2, mark# zWquot(X1, X2) -> a__zWquot#(mark X1, mark X2), mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> a__sel#(mark X1, mark X2), mark# minus(X1, X2) -> mark# X1, mark# minus(X1, X2) -> mark# X2, mark# minus(X1, X2) -> a__minus#(mark X1, mark X2), mark# quot(X1, X2) -> mark# X1, mark# quot(X1, X2) -> mark# X2, mark# quot(X1, X2) -> a__quot#(mark X1, mark X2), a__from# X -> mark# X, a__sel#(s N, cons(X, XS)) -> mark# XS, a__sel#(s N, cons(X, XS)) -> mark# N, a__sel#(s N, cons(X, XS)) -> a__sel#(mark N, mark XS), a__sel#(0(), cons(X, XS)) -> mark# X, a__minus#(s X, s Y) -> mark# X, a__minus#(s X, s Y) -> mark# Y, a__minus#(s X, s Y) -> a__minus#(mark X, mark Y), a__quot#(s X, s Y) -> mark# X, a__quot#(s X, s Y) -> mark# Y, a__quot#(s X, s Y) -> a__minus#(mark X, mark Y), a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# X, a__zWquot#(cons(X, XS), cons(Y, YS)) -> mark# Y, a__zWquot#(cons(X, XS), cons(Y, YS)) -> a__quot#(mark X, mark Y)} Weak: { mark cons(X1, X2) -> cons(mark X1, X2), mark from X -> a__from mark X, mark s X -> s mark X, mark 0() -> 0(), mark nil() -> nil(), mark zWquot(X1, X2) -> a__zWquot(mark X1, mark X2), mark sel(X1, X2) -> a__sel(mark X1, mark X2), mark minus(X1, X2) -> a__minus(mark X1, mark X2), mark quot(X1, X2) -> a__quot(mark X1, mark X2), a__from X -> cons(mark X, from s X), a__from X -> from X, a__sel(X1, X2) -> sel(X1, X2), a__sel(s N, cons(X, XS)) -> a__sel(mark N, mark XS), a__sel(0(), cons(X, XS)) -> mark X, a__minus(X, 0()) -> 0(), a__minus(X1, X2) -> minus(X1, X2), a__minus(s X, s Y) -> a__minus(mark X, mark Y), a__quot(X1, X2) -> quot(X1, X2), a__quot(s X, s Y) -> s a__quot(a__minus(mark X, mark Y), s mark Y), a__quot(0(), s Y) -> 0(), a__zWquot(XS, nil()) -> nil(), a__zWquot(X1, X2) -> zWquot(X1, X2), a__zWquot(cons(X, XS), cons(Y, YS)) -> cons(a__quot(mark X, mark Y), zWquot(XS, YS)), a__zWquot(nil(), XS) -> nil()} Open