MAYBE Time: 1.123459 TRS: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} DP: DP: { mark# 0() -> active# 0(), mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X, mark# dbl X -> dbl# mark X, mark# s X -> active# s X, mark# nil() -> active# nil(), mark# dbls X -> mark# X, mark# dbls X -> active# dbls mark X, mark# dbls X -> dbls# mark X, mark# cons(X1, X2) -> active# cons(X1, X2), 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# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2), mark# indx(X1, X2) -> indx#(mark X1, X2), mark# from X -> active# from X, active# dbl 0() -> mark# 0(), active# dbl s X -> mark# s s dbl X, active# dbl s X -> dbl# X, active# dbl s X -> s# dbl X, active# dbl s X -> s# s dbl X, active# dbls nil() -> mark# nil(), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), active# dbls cons(X, Y) -> dbl# X, active# dbls cons(X, Y) -> dbls# Y, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), active# sel(0(), cons(X, Y)) -> mark# X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), active# sel(s X, cons(Y, Z)) -> sel#(X, Z), active# indx(nil(), X) -> mark# nil(), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), active# indx(cons(X, Y), Z) -> sel#(X, Z), active# indx(cons(X, Y), Z) -> indx#(Y, Z), active# from X -> mark# cons(X, from s X), active# from X -> s# X, active# from X -> cons#(X, from s X), active# from X -> from# s X, dbl# mark X -> dbl# X, dbl# active X -> dbl# X, s# mark X -> s# X, s# active X -> s# X, dbls# mark X -> dbls# X, dbls# active X -> dbls# X, 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), 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), indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2), from# mark X -> from# X, from# active X -> from# X} TRS: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} UR: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} EDG: { (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(active X1, X2) -> cons#(X1, X2)) (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(mark X1, X2) -> cons#(X1, X2)) (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(X1, active X2) -> cons#(X1, X2)) (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# dbls X -> mark# X, mark# from X -> active# from X) (mark# dbls X -> mark# X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# dbls X -> mark# X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# dbls X -> mark# X, mark# indx(X1, X2) -> mark# X1) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# dbls X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# dbls X -> mark# X, mark# dbls X -> dbls# mark X) (mark# dbls X -> mark# X, mark# dbls X -> active# dbls mark X) (mark# dbls X -> mark# X, mark# dbls X -> mark# X) (mark# dbls X -> mark# X, mark# nil() -> active# nil()) (mark# dbls X -> mark# X, mark# s X -> active# s X) (mark# dbls X -> mark# X, mark# dbl X -> dbl# mark X) (mark# dbls X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# dbls X -> mark# X, mark# dbl X -> mark# X) (mark# dbls X -> mark# X, mark# 0() -> active# 0()) (active# dbls cons(X, Y) -> dbl# X, dbl# active X -> dbl# X) (active# dbls cons(X, Y) -> dbl# X, dbl# mark X -> dbl# X) (active# from X -> s# X, s# active X -> s# X) (active# from X -> s# X, s# mark X -> s# X) (dbl# active X -> dbl# X, dbl# active X -> dbl# X) (dbl# active X -> dbl# X, dbl# mark X -> dbl# X) (s# active X -> s# X, s# active X -> s# X) (s# active X -> s# X, s# mark X -> s# X) (dbls# active X -> dbls# X, dbls# active X -> dbls# X) (dbls# active X -> dbls# X, dbls# mark X -> dbls# X) (from# active X -> from# X, from# active X -> from# X) (from# active X -> from# X, from# mark X -> from# X) (mark# nil() -> active# nil(), active# from X -> from# s X) (mark# nil() -> active# nil(), active# from X -> cons#(X, from s X)) (mark# nil() -> active# nil(), active# from X -> s# X) (mark# nil() -> active# nil(), active# from X -> mark# cons(X, from s X)) (mark# nil() -> active# nil(), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# nil() -> active# nil(), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# nil() -> active# nil(), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# nil() -> active# nil(), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# nil() -> active# nil(), active# indx(nil(), X) -> mark# nil()) (mark# nil() -> active# nil(), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# nil() -> active# nil(), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# nil() -> active# nil(), active# sel(0(), cons(X, Y)) -> mark# X) (mark# nil() -> active# nil(), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# nil() -> active# nil(), active# dbls cons(X, Y) -> dbls# Y) (mark# nil() -> active# nil(), active# dbls cons(X, Y) -> dbl# X) (mark# nil() -> active# nil(), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# nil() -> active# nil(), active# dbls nil() -> mark# nil()) (mark# nil() -> active# nil(), active# dbl s X -> s# s dbl X) (mark# nil() -> active# nil(), active# dbl s X -> s# dbl X) (mark# nil() -> active# nil(), active# dbl s X -> dbl# X) (mark# nil() -> active# nil(), active# dbl s X -> mark# s s dbl X) (mark# nil() -> active# nil(), active# dbl 0() -> mark# 0()) (mark# indx(X1, X2) -> mark# X1, mark# from X -> active# from X) (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# indx(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> dbls# mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> active# dbls mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> mark# X) (mark# indx(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# indx(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# indx(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (active# dbls nil() -> mark# nil(), mark# from X -> active# from X) (active# dbls nil() -> mark# nil(), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# dbls nil() -> mark# nil(), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# dbls nil() -> mark# nil(), mark# indx(X1, X2) -> mark# X1) (active# dbls nil() -> mark# nil(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# dbls nil() -> mark# nil(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# dbls nil() -> mark# nil(), mark# sel(X1, X2) -> mark# X2) (active# dbls nil() -> mark# nil(), mark# sel(X1, X2) -> mark# X1) (active# dbls nil() -> mark# nil(), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# dbls nil() -> mark# nil(), mark# dbls X -> dbls# mark X) (active# dbls nil() -> mark# nil(), mark# dbls X -> active# dbls mark X) (active# dbls nil() -> mark# nil(), mark# dbls X -> mark# X) (active# dbls nil() -> mark# nil(), mark# nil() -> active# nil()) (active# dbls nil() -> mark# nil(), mark# s X -> active# s X) (active# dbls nil() -> mark# nil(), mark# dbl X -> dbl# mark X) (active# dbls nil() -> mark# nil(), mark# dbl X -> active# dbl mark X) (active# dbls nil() -> mark# nil(), mark# dbl X -> mark# X) (active# dbls nil() -> mark# nil(), mark# 0() -> active# 0()) (mark# dbl X -> dbl# mark X, dbl# active X -> dbl# X) (mark# dbl X -> dbl# mark X, dbl# mark X -> dbl# X) (mark# dbls X -> dbls# mark X, dbls# active X -> dbls# X) (mark# dbls X -> dbls# mark X, dbls# mark X -> dbls# X) (active# dbl s X -> s# dbl X, s# active X -> s# X) (active# dbl s X -> s# dbl X, s# mark X -> s# X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# from X -> active# from X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# indx(X1, X2) -> mark# X1) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> mark# X2) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> mark# X1) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbls X -> dbls# mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbls X -> active# dbls mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbls X -> mark# X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# nil() -> active# nil()) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# s X -> active# s X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbl X -> dbl# mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbl X -> active# dbl mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbl X -> mark# X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# 0() -> active# 0()) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> from# s X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> cons#(X, from s X)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> s# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> mark# cons(X, from s X)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(nil(), X) -> mark# nil()) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> dbls# Y) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> dbl# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls nil() -> mark# nil()) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> s# s dbl X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> s# dbl X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> dbl# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> mark# s s dbl X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl 0() -> mark# 0()) (active# dbls cons(X, Y) -> dbls# Y, dbls# active X -> dbls# X) (active# dbls cons(X, Y) -> dbls# Y, dbls# mark X -> dbls# X) (mark# sel(X1, X2) -> mark# X2, mark# from X -> active# from X) (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, 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) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> dbls# mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> active# dbls mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s X) (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> dbl# mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> active# dbl mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# indx(X1, X2) -> indx#(mark X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (mark# indx(X1, X2) -> indx#(mark X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (mark# indx(X1, X2) -> indx#(mark X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (mark# indx(X1, X2) -> indx#(mark X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (mark# dbl X -> active# dbl mark X, active# from X -> from# s X) (mark# dbl X -> active# dbl mark X, active# from X -> cons#(X, from s X)) (mark# dbl X -> active# dbl mark X, active# from X -> s# X) (mark# dbl X -> active# dbl mark X, active# from X -> mark# cons(X, from s X)) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# dbl X -> active# dbl mark X, active# indx(nil(), X) -> mark# nil()) (mark# dbl X -> active# dbl mark X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# dbl X -> active# dbl mark X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# dbl X -> active# dbl mark X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> dbls# Y) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> dbl# X) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# dbl X -> active# dbl mark X, active# dbls nil() -> mark# nil()) (mark# dbl X -> active# dbl mark X, active# dbl s X -> s# s dbl X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> s# dbl X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> dbl# X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> mark# s s dbl X) (mark# dbl X -> active# dbl mark X, active# dbl 0() -> mark# 0()) (active# dbl s X -> s# s dbl X, s# active X -> s# X) (active# dbl s X -> s# s dbl X, 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)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(active X1, X2) -> sel#(X1, X2)) (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(mark X1, X2) -> sel#(X1, X2)) (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(X1, active X2) -> sel#(X1, X2)) (active# indx(cons(X, Y), Z) -> sel#(X, Z), sel#(X1, mark X2) -> sel#(X1, X2)) (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 -> cons#(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# from X -> mark# cons(X, from s X)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(nil(), X) -> mark# nil()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> dbls# Y) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> dbl# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls nil() -> mark# nil()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> s# s dbl X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> s# dbl X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> dbl# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> mark# s s dbl X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl 0() -> mark# 0()) (active# from X -> mark# cons(X, from s X), mark# from X -> active# from X) (active# from X -> mark# cons(X, from s X), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# indx(X1, X2) -> mark# X1) (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# sel(X1, X2) -> active# sel(mark X1, mark X2)) (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) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# from X -> mark# cons(X, from s X), mark# dbls X -> dbls# mark X) (active# from X -> mark# cons(X, from s X), mark# dbls X -> active# dbls mark X) (active# from X -> mark# cons(X, from s X), mark# dbls X -> mark# X) (active# from X -> mark# cons(X, from s X), mark# nil() -> active# nil()) (active# from X -> mark# cons(X, from s X), mark# s X -> active# s X) (active# from X -> mark# cons(X, from s X), mark# dbl X -> dbl# mark X) (active# from X -> mark# cons(X, from s X), mark# dbl X -> active# dbl mark X) (active# from X -> mark# cons(X, from s X), mark# dbl X -> mark# X) (active# from X -> mark# cons(X, from s X), mark# 0() -> active# 0()) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# 0() -> active# 0()) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbl X -> mark# X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbl X -> active# dbl mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbl X -> dbl# mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# s X -> active# s X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# nil() -> active# nil()) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbls X -> mark# X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbls X -> active# dbls mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbls X -> dbls# mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> mark# X1) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> mark# X2) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# indx(X1, X2) -> mark# X1) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# from X -> active# from X) (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(X1, mark X2) -> indx#(X1, X2)) (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(X1, active X2) -> indx#(X1, X2)) (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(mark X1, X2) -> indx#(X1, X2)) (active# indx(cons(X, Y), Z) -> indx#(Y, Z), indx#(active X1, X2) -> indx#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(X1, mark X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(X1, active X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(mark X1, X2) -> sel#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> sel#(X, Z), sel#(active X1, X2) -> sel#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(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)) (mark# dbls X -> active# dbls mark X, active# dbl 0() -> mark# 0()) (mark# dbls X -> active# dbls mark X, active# dbl s X -> mark# s s dbl X) (mark# dbls X -> active# dbls mark X, active# dbl s X -> dbl# X) (mark# dbls X -> active# dbls mark X, active# dbl s X -> s# dbl X) (mark# dbls X -> active# dbls mark X, active# dbl s X -> s# s dbl X) (mark# dbls X -> active# dbls mark X, active# dbls nil() -> mark# nil()) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> dbl# X) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> dbls# Y) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# dbls X -> active# dbls mark X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# dbls X -> active# dbls mark X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# dbls X -> active# dbls mark X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# dbls X -> active# dbls mark X, active# indx(nil(), X) -> mark# nil()) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# dbls X -> active# dbls mark X, active# from X -> mark# cons(X, from s X)) (mark# dbls X -> active# dbls mark X, active# from X -> s# X) (mark# dbls X -> active# dbls mark X, active# from X -> cons#(X, from s X)) (mark# dbls X -> active# dbls mark X, active# from X -> from# s X) (active# dbl s X -> mark# s s dbl X, mark# 0() -> active# 0()) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> active# dbl mark X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> dbl# mark X) (active# dbl s X -> mark# s s dbl X, mark# s X -> active# s X) (active# dbl s X -> mark# s s dbl X, mark# nil() -> active# nil()) (active# dbl s X -> mark# s s dbl X, mark# dbls X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# dbls X -> active# dbls mark X) (active# dbl s X -> mark# s s dbl X, mark# dbls X -> dbls# mark X) (active# dbl s X -> mark# s s dbl X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> mark# X1) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> mark# X2) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# indx(X1, X2) -> mark# X1) (active# dbl s X -> mark# s s dbl X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# from X -> active# from X) (active# from X -> cons#(X, from s X), cons#(X1, mark 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#(mark X1, X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(active X1, X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(X1, mark X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(X1, active X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(mark X1, X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(active X1, X2) -> cons#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# 0() -> active# 0()) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbl X -> mark# X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbl X -> active# dbl mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbl X -> dbl# mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# s X -> active# s X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# nil() -> active# nil()) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbls X -> mark# X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbls X -> active# dbls mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbls X -> dbls# mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X1) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X2) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# indx(X1, X2) -> mark# X1) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# from X -> active# from X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl 0() -> mark# 0()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> mark# s s dbl X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> dbl# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> s# dbl X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> s# s dbl X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls nil() -> mark# nil()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> dbl# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> dbls# Y) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(nil(), X) -> mark# nil()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> mark# cons(X, from s X)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> s# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> cons#(X, from s X)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> from# s X) (active# from X -> from# s X, from# mark X -> from# X) (active# from X -> from# s X, from# active X -> from# X) (mark# from X -> active# from X, active# dbl 0() -> mark# 0()) (mark# from X -> active# from X, active# dbl s X -> mark# s s dbl X) (mark# from X -> active# from X, active# dbl s X -> dbl# X) (mark# from X -> active# from X, active# dbl s X -> s# dbl X) (mark# from X -> active# from X, active# dbl s X -> s# s dbl X) (mark# from X -> active# from X, active# dbls nil() -> mark# nil()) (mark# from X -> active# from X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# from X -> active# from X, active# dbls cons(X, Y) -> dbl# X) (mark# from X -> active# from X, active# dbls cons(X, Y) -> dbls# Y) (mark# from X -> active# from X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# from X -> active# from X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# from X -> active# from X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# from X -> active# from X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# from X -> active# from X, active# indx(nil(), X) -> mark# nil()) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# from X -> active# from X, active# from X -> mark# cons(X, from s X)) (mark# from X -> active# from X, active# from X -> s# X) (mark# from X -> active# from X, active# from X -> cons#(X, from s X)) (mark# from X -> active# from X, active# from X -> from# s X) (mark# s X -> active# s X, active# dbl 0() -> mark# 0()) (mark# s X -> active# s X, active# dbl s X -> mark# s s dbl X) (mark# s X -> active# s X, active# dbl s X -> dbl# X) (mark# s X -> active# s X, active# dbl s X -> s# dbl X) (mark# s X -> active# s X, active# dbl s X -> s# s dbl X) (mark# s X -> active# s X, active# dbls nil() -> mark# nil()) (mark# s X -> active# s X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# s X -> active# s X, active# dbls cons(X, Y) -> dbl# X) (mark# s X -> active# s X, active# dbls cons(X, Y) -> dbls# Y) (mark# s X -> active# s X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# s X -> active# s X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# s X -> active# s X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# s X -> active# s X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# s X -> active# s X, active# indx(nil(), X) -> mark# nil()) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# s X -> active# s X, active# from X -> mark# cons(X, from s X)) (mark# s X -> active# s X, active# from X -> s# X) (mark# s X -> active# s X, active# from X -> cons#(X, from s X)) (mark# s X -> active# s X, active# from X -> from# s X) (active# indx(nil(), X) -> mark# nil(), mark# 0() -> active# 0()) (active# indx(nil(), X) -> mark# nil(), mark# dbl X -> mark# X) (active# indx(nil(), X) -> mark# nil(), mark# dbl X -> active# dbl mark X) (active# indx(nil(), X) -> mark# nil(), mark# dbl X -> dbl# mark X) (active# indx(nil(), X) -> mark# nil(), mark# s X -> active# s X) (active# indx(nil(), X) -> mark# nil(), mark# nil() -> active# nil()) (active# indx(nil(), X) -> mark# nil(), mark# dbls X -> mark# X) (active# indx(nil(), X) -> mark# nil(), mark# dbls X -> active# dbls mark X) (active# indx(nil(), X) -> mark# nil(), mark# dbls X -> dbls# mark X) (active# indx(nil(), X) -> mark# nil(), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# indx(nil(), X) -> mark# nil(), mark# sel(X1, X2) -> mark# X1) (active# indx(nil(), X) -> mark# nil(), mark# sel(X1, X2) -> mark# X2) (active# indx(nil(), X) -> mark# nil(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# indx(nil(), X) -> mark# nil(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# indx(nil(), X) -> mark# nil(), mark# indx(X1, X2) -> mark# X1) (active# indx(nil(), X) -> mark# nil(), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# indx(nil(), X) -> mark# nil(), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# indx(nil(), X) -> mark# nil(), mark# from X -> active# from X) (active# dbl 0() -> mark# 0(), mark# 0() -> active# 0()) (active# dbl 0() -> mark# 0(), mark# dbl X -> mark# X) (active# dbl 0() -> mark# 0(), mark# dbl X -> active# dbl mark X) (active# dbl 0() -> mark# 0(), mark# dbl X -> dbl# mark X) (active# dbl 0() -> mark# 0(), mark# s X -> active# s X) (active# dbl 0() -> mark# 0(), mark# nil() -> active# nil()) (active# dbl 0() -> mark# 0(), mark# dbls X -> mark# X) (active# dbl 0() -> mark# 0(), mark# dbls X -> active# dbls mark X) (active# dbl 0() -> mark# 0(), mark# dbls X -> dbls# mark X) (active# dbl 0() -> mark# 0(), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# dbl 0() -> mark# 0(), mark# sel(X1, X2) -> mark# X1) (active# dbl 0() -> mark# 0(), mark# sel(X1, X2) -> mark# X2) (active# dbl 0() -> mark# 0(), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# dbl 0() -> mark# 0(), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# dbl 0() -> mark# 0(), mark# indx(X1, X2) -> mark# X1) (active# dbl 0() -> mark# 0(), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# dbl 0() -> mark# 0(), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# dbl 0() -> mark# 0(), mark# from X -> active# from X) (mark# sel(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# sel(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# sel(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> active# dbls mark X) (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> dbls# mark X) (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (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# indx(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X1, mark# from X -> active# from X) (mark# 0() -> active# 0(), active# dbl 0() -> mark# 0()) (mark# 0() -> active# 0(), active# dbl s X -> mark# s s dbl X) (mark# 0() -> active# 0(), active# dbl s X -> dbl# X) (mark# 0() -> active# 0(), active# dbl s X -> s# dbl X) (mark# 0() -> active# 0(), active# dbl s X -> s# s dbl X) (mark# 0() -> active# 0(), active# dbls nil() -> mark# nil()) (mark# 0() -> active# 0(), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# 0() -> active# 0(), active# dbls cons(X, Y) -> dbl# X) (mark# 0() -> active# 0(), active# dbls cons(X, Y) -> dbls# Y) (mark# 0() -> active# 0(), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# 0() -> active# 0(), active# sel(0(), cons(X, Y)) -> mark# X) (mark# 0() -> active# 0(), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# 0() -> active# 0(), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# 0() -> active# 0(), active# indx(nil(), X) -> mark# nil()) (mark# 0() -> active# 0(), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# 0() -> active# 0(), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# 0() -> active# 0(), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# 0() -> active# 0(), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# 0() -> active# 0(), active# from X -> mark# cons(X, from s X)) (mark# 0() -> active# 0(), active# from X -> s# X) (mark# 0() -> active# 0(), active# from X -> cons#(X, from s X)) (mark# 0() -> active# 0(), active# from X -> from# s X) (from# mark X -> from# X, from# mark X -> from# X) (from# mark X -> from# X, from# active X -> from# X) (dbls# mark X -> dbls# X, dbls# mark X -> dbls# X) (dbls# mark X -> dbls# X, dbls# active X -> dbls# X) (s# mark X -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X) (dbl# mark X -> dbl# X, dbl# active X -> dbl# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# 0() -> active# 0()) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbl X -> active# dbl mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbl X -> dbl# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# s X -> active# s X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# nil() -> active# nil()) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbls X -> active# dbls mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbls X -> dbls# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1) (active# sel(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# from X -> active# from X) (active# dbl s X -> dbl# X, dbl# mark X -> dbl# X) (active# dbl s X -> dbl# X, dbl# active X -> dbl# X) (mark# dbl X -> mark# X, mark# 0() -> active# 0()) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# dbl X -> mark# X, mark# dbl X -> dbl# mark X) (mark# dbl X -> mark# X, mark# s X -> active# s X) (mark# dbl X -> mark# X, mark# nil() -> active# nil()) (mark# dbl X -> mark# X, mark# dbls X -> mark# X) (mark# dbl X -> mark# X, mark# dbls X -> active# dbls mark X) (mark# dbl X -> mark# X, mark# dbls X -> dbls# mark X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# dbl X -> mark# X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# dbl X -> mark# X, mark# from X -> active# from X) (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)) } EDG: { (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(active X1, X2) -> cons#(X1, X2)) (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(mark X1, X2) -> cons#(X1, X2)) (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(X1, active X2) -> cons#(X1, X2)) (active# dbls cons(X, Y) -> cons#(dbl X, dbls Y), cons#(X1, mark X2) -> cons#(X1, X2)) (mark# dbls X -> mark# X, mark# from X -> active# from X) (mark# dbls X -> mark# X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# dbls X -> mark# X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# dbls X -> mark# X, mark# indx(X1, X2) -> mark# X1) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# dbls X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# dbls X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# dbls X -> mark# X, mark# dbls X -> dbls# mark X) (mark# dbls X -> mark# X, mark# dbls X -> active# dbls mark X) (mark# dbls X -> mark# X, mark# dbls X -> mark# X) (mark# dbls X -> mark# X, mark# nil() -> active# nil()) (mark# dbls X -> mark# X, mark# s X -> active# s X) (mark# dbls X -> mark# X, mark# dbl X -> dbl# mark X) (mark# dbls X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# dbls X -> mark# X, mark# dbl X -> mark# X) (mark# dbls X -> mark# X, mark# 0() -> active# 0()) (dbl# active X -> dbl# X, dbl# active X -> dbl# X) (dbl# active X -> dbl# X, dbl# mark X -> dbl# X) (s# active X -> s# X, s# active X -> s# X) (s# active X -> s# X, s# mark X -> s# X) (dbls# active X -> dbls# X, dbls# active X -> dbls# X) (dbls# active X -> dbls# X, dbls# mark X -> dbls# X) (from# active X -> from# X, from# active X -> from# X) (from# active X -> from# X, from# mark X -> from# X) (mark# indx(X1, X2) -> mark# X1, mark# from X -> active# from X) (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> mark# X1) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2) (mark# indx(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X1) (mark# indx(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> dbls# mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> active# dbls mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbls X -> mark# X) (mark# indx(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# indx(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# indx(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# indx(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (active# dbls nil() -> mark# nil(), mark# nil() -> active# nil()) (mark# dbl X -> dbl# mark X, dbl# active X -> dbl# X) (mark# dbl X -> dbl# mark X, dbl# mark X -> dbl# X) (mark# dbls X -> dbls# mark X, dbls# active X -> dbls# X) (mark# dbls X -> dbls# mark X, dbls# mark X -> dbls# X) (active# dbl s X -> s# dbl X, s# active X -> s# X) (active# dbl s X -> s# dbl X, s# mark X -> s# X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# from X -> active# from X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# indx(X1, X2) -> mark# X1) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> mark# X2) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# sel(X1, X2) -> mark# X1) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbls X -> dbls# mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbls X -> active# dbls mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbls X -> mark# X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# s X -> active# s X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbl X -> dbl# mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbl X -> active# dbl mark X) (active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), mark# dbl X -> mark# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> from# s X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> cons#(X, from s X)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> s# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# from X -> mark# cons(X, from s X)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# indx(nil(), X) -> mark# nil()) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> dbls# Y) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> dbl# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbls nil() -> mark# nil()) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> s# s dbl X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> s# dbl X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> dbl# X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl s X -> mark# s s dbl X) (mark# indx(X1, X2) -> active# indx(mark X1, X2), active# dbl 0() -> mark# 0()) (mark# sel(X1, X2) -> mark# X2, mark# from X -> active# from X) (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# indx(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> sel#(mark X1, 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) -> mark# X2) (mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X2, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> dbls# mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> active# dbls mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbls X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# nil() -> active# nil()) (mark# sel(X1, X2) -> mark# X2, mark# s X -> active# s X) (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> dbl# mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> active# dbl mark X) (mark# sel(X1, X2) -> mark# X2, mark# dbl X -> mark# X) (mark# sel(X1, X2) -> mark# X2, mark# 0() -> active# 0()) (mark# indx(X1, X2) -> indx#(mark X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (mark# indx(X1, X2) -> indx#(mark X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (mark# dbl X -> active# dbl mark X, active# from X -> from# s X) (mark# dbl X -> active# dbl mark X, active# from X -> cons#(X, from s X)) (mark# dbl X -> active# dbl mark X, active# from X -> s# X) (mark# dbl X -> active# dbl mark X, active# from X -> mark# cons(X, from s X)) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# dbl X -> active# dbl mark X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# dbl X -> active# dbl mark X, active# indx(nil(), X) -> mark# nil()) (mark# dbl X -> active# dbl mark X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# dbl X -> active# dbl mark X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# dbl X -> active# dbl mark X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> dbls# Y) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> dbl# X) (mark# dbl X -> active# dbl mark X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# dbl X -> active# dbl mark X, active# dbls nil() -> mark# nil()) (mark# dbl X -> active# dbl mark X, active# dbl s X -> s# s dbl X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> s# dbl X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> dbl# X) (mark# dbl X -> active# dbl mark X, active# dbl s X -> mark# s s dbl X) (mark# dbl X -> active# dbl mark X, active# dbl 0() -> mark# 0()) (active# dbl s X -> s# s dbl X, s# active X -> s# X) (active# dbl s X -> s# s dbl X, 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)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(X1, active X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(active X1, X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (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 -> cons#(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# from X -> mark# cons(X, from s X)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# indx(nil(), X) -> mark# nil()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> dbls# Y) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> dbl# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbls nil() -> mark# nil()) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> s# s dbl X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> s# dbl X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> dbl# X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl s X -> mark# s s dbl X) (mark# sel(X1, X2) -> active# sel(mark X1, mark X2), active# dbl 0() -> mark# 0()) (active# from X -> mark# cons(X, from s X), mark# from X -> active# from X) (active# from X -> mark# cons(X, from s X), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# from X -> mark# cons(X, from s X), mark# indx(X1, X2) -> mark# X1) (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# sel(X1, X2) -> active# sel(mark X1, mark X2)) (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) -> mark# X1) (active# from X -> mark# cons(X, from s X), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# from X -> mark# cons(X, from s X), mark# dbls X -> dbls# mark X) (active# from X -> mark# cons(X, from s X), mark# dbls X -> active# dbls mark X) (active# from X -> mark# cons(X, from s X), mark# dbls X -> mark# X) (active# from X -> mark# cons(X, from s X), mark# s X -> active# s X) (active# from X -> mark# cons(X, from s X), mark# dbl X -> dbl# mark X) (active# from X -> mark# cons(X, from s X), mark# dbl X -> active# dbl mark X) (active# from X -> mark# cons(X, from s X), mark# dbl X -> mark# X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbl X -> mark# X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbl X -> active# dbl mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbl X -> dbl# mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# s X -> active# s X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbls X -> mark# X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbls X -> active# dbls mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# dbls X -> dbls# mark X) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> mark# X1) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> mark# X2) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# indx(X1, X2) -> mark# X1) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), mark# from X -> active# from X) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(mark X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, mark X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2)) (indx#(X1, mark X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(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)) (mark# dbls X -> active# dbls mark X, active# dbl 0() -> mark# 0()) (mark# dbls X -> active# dbls mark X, active# dbl s X -> mark# s s dbl X) (mark# dbls X -> active# dbls mark X, active# dbl s X -> dbl# X) (mark# dbls X -> active# dbls mark X, active# dbl s X -> s# dbl X) (mark# dbls X -> active# dbls mark X, active# dbl s X -> s# s dbl X) (mark# dbls X -> active# dbls mark X, active# dbls nil() -> mark# nil()) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> dbl# X) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> dbls# Y) (mark# dbls X -> active# dbls mark X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# dbls X -> active# dbls mark X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# dbls X -> active# dbls mark X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# dbls X -> active# dbls mark X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# dbls X -> active# dbls mark X, active# indx(nil(), X) -> mark# nil()) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# dbls X -> active# dbls mark X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# dbls X -> active# dbls mark X, active# from X -> mark# cons(X, from s X)) (mark# dbls X -> active# dbls mark X, active# from X -> s# X) (mark# dbls X -> active# dbls mark X, active# from X -> cons#(X, from s X)) (mark# dbls X -> active# dbls mark X, active# from X -> from# s X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> active# dbl mark X) (active# dbl s X -> mark# s s dbl X, mark# dbl X -> dbl# mark X) (active# dbl s X -> mark# s s dbl X, mark# s X -> active# s X) (active# dbl s X -> mark# s s dbl X, mark# dbls X -> mark# X) (active# dbl s X -> mark# s s dbl X, mark# dbls X -> active# dbls mark X) (active# dbl s X -> mark# s s dbl X, mark# dbls X -> dbls# mark X) (active# dbl s X -> mark# s s dbl X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> mark# X1) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> mark# X2) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# dbl s X -> mark# s s dbl X, mark# indx(X1, X2) -> mark# X1) (active# dbl s X -> mark# s s dbl X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# dbl s X -> mark# s s dbl X, mark# from X -> active# from X) (active# from X -> cons#(X, from s X), cons#(X1, mark X2) -> cons#(X1, X2)) (active# from X -> cons#(X, from s X), cons#(X1, active X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(X1, mark X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(X1, active X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(mark X1, X2) -> cons#(X1, X2)) (active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z)), cons#(active X1, X2) -> cons#(X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbl X -> mark# X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbl X -> active# dbl mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbl X -> dbl# mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# s X -> active# s X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbls X -> mark# X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbls X -> active# dbls mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# dbls X -> dbls# mark X) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# cons(X1, X2) -> active# cons(X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X1) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> mark# X2) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# indx(X1, X2) -> mark# X1) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), mark# from X -> active# from X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl 0() -> mark# 0()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> mark# s s dbl X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> dbl# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> s# dbl X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbl s X -> s# s dbl X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls nil() -> mark# nil()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> dbl# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> dbls# Y) (mark# cons(X1, X2) -> active# cons(X1, X2), active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# sel(0(), cons(X, Y)) -> mark# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(nil(), X) -> mark# nil()) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> mark# cons(X, from s X)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> s# X) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> cons#(X, from s X)) (mark# cons(X1, X2) -> active# cons(X1, X2), active# from X -> from# s X) (active# from X -> from# s X, from# mark X -> from# X) (active# from X -> from# s X, from# active X -> from# X) (mark# from X -> active# from X, active# dbl 0() -> mark# 0()) (mark# from X -> active# from X, active# dbl s X -> mark# s s dbl X) (mark# from X -> active# from X, active# dbl s X -> dbl# X) (mark# from X -> active# from X, active# dbl s X -> s# dbl X) (mark# from X -> active# from X, active# dbl s X -> s# s dbl X) (mark# from X -> active# from X, active# dbls nil() -> mark# nil()) (mark# from X -> active# from X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# from X -> active# from X, active# dbls cons(X, Y) -> dbl# X) (mark# from X -> active# from X, active# dbls cons(X, Y) -> dbls# Y) (mark# from X -> active# from X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# from X -> active# from X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# from X -> active# from X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# from X -> active# from X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# from X -> active# from X, active# indx(nil(), X) -> mark# nil()) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# from X -> active# from X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# from X -> active# from X, active# from X -> mark# cons(X, from s X)) (mark# from X -> active# from X, active# from X -> s# X) (mark# from X -> active# from X, active# from X -> cons#(X, from s X)) (mark# from X -> active# from X, active# from X -> from# s X) (mark# s X -> active# s X, active# dbl 0() -> mark# 0()) (mark# s X -> active# s X, active# dbl s X -> mark# s s dbl X) (mark# s X -> active# s X, active# dbl s X -> dbl# X) (mark# s X -> active# s X, active# dbl s X -> s# dbl X) (mark# s X -> active# s X, active# dbl s X -> s# s dbl X) (mark# s X -> active# s X, active# dbls nil() -> mark# nil()) (mark# s X -> active# s X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y)) (mark# s X -> active# s X, active# dbls cons(X, Y) -> dbl# X) (mark# s X -> active# s X, active# dbls cons(X, Y) -> dbls# Y) (mark# s X -> active# s X, active# dbls cons(X, Y) -> cons#(dbl X, dbls Y)) (mark# s X -> active# s X, active# sel(0(), cons(X, Y)) -> mark# X) (mark# s X -> active# s X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z)) (mark# s X -> active# s X, active# sel(s X, cons(Y, Z)) -> sel#(X, Z)) (mark# s X -> active# s X, active# indx(nil(), X) -> mark# nil()) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z))) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> cons#(sel(X, Z), indx(Y, Z))) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> sel#(X, Z)) (mark# s X -> active# s X, active# indx(cons(X, Y), Z) -> indx#(Y, Z)) (mark# s X -> active# s X, active# from X -> mark# cons(X, from s X)) (mark# s X -> active# s X, active# from X -> s# X) (mark# s X -> active# s X, active# from X -> cons#(X, from s X)) (mark# s X -> active# s X, active# from X -> from# s X) (active# indx(nil(), X) -> mark# nil(), mark# nil() -> active# nil()) (active# dbl 0() -> mark# 0(), mark# 0() -> active# 0()) (mark# sel(X1, X2) -> mark# X1, mark# 0() -> active# 0()) (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> active# dbl mark X) (mark# sel(X1, X2) -> mark# X1, mark# dbl X -> dbl# mark X) (mark# sel(X1, X2) -> mark# X1, mark# s X -> active# s X) (mark# sel(X1, X2) -> mark# X1, mark# nil() -> active# nil()) (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> mark# X) (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> active# dbls mark X) (mark# sel(X1, X2) -> mark# X1, mark# dbls X -> dbls# mark X) (mark# sel(X1, X2) -> mark# X1, mark# cons(X1, X2) -> active# cons(X1, X2)) (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# indx(X1, X2) -> mark# X1) (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# sel(X1, X2) -> mark# X1, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# sel(X1, X2) -> mark# X1, mark# from X -> active# from X) (from# mark X -> from# X, from# mark X -> from# X) (from# mark X -> from# X, from# active X -> from# X) (dbls# mark X -> dbls# X, dbls# mark X -> dbls# X) (dbls# mark X -> dbls# X, dbls# active X -> dbls# X) (s# mark X -> s# X, s# mark X -> s# X) (s# mark X -> s# X, s# active X -> s# X) (dbl# mark X -> dbl# X, dbl# mark X -> dbl# X) (dbl# mark X -> dbl# X, dbl# active X -> dbl# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# 0() -> active# 0()) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbl X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbl X -> active# dbl mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbl X -> dbl# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# s X -> active# s X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# nil() -> active# nil()) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbls X -> mark# X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbls X -> active# dbls mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# dbls X -> dbls# mark X) (active# sel(0(), cons(X, Y)) -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X1) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> mark# X2) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> mark# X1) (active# sel(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (active# sel(0(), cons(X, Y)) -> mark# X, mark# from X -> active# from X) (mark# dbl X -> mark# X, mark# 0() -> active# 0()) (mark# dbl X -> mark# X, mark# dbl X -> mark# X) (mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X) (mark# dbl X -> mark# X, mark# dbl X -> dbl# mark X) (mark# dbl X -> mark# X, mark# s X -> active# s X) (mark# dbl X -> mark# X, mark# nil() -> active# nil()) (mark# dbl X -> mark# X, mark# dbls X -> mark# X) (mark# dbl X -> mark# X, mark# dbls X -> active# dbls mark X) (mark# dbl X -> mark# X, mark# dbls X -> dbls# mark X) (mark# dbl X -> mark# X, mark# cons(X1, X2) -> active# cons(X1, X2)) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> mark# X2) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> active# sel(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# sel(X1, X2) -> sel#(mark X1, mark X2)) (mark# dbl X -> mark# X, mark# indx(X1, X2) -> mark# X1) (mark# dbl X -> mark# X, mark# indx(X1, X2) -> active# indx(mark X1, X2)) (mark# dbl X -> mark# X, mark# indx(X1, X2) -> indx#(mark X1, X2)) (mark# dbl X -> mark# X, mark# from X -> active# from X) (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)) } STATUS: arrows: 0.883333 SCCS (8): Scc: { mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X, mark# s X -> active# s X, mark# dbls X -> mark# X, mark# dbls X -> active# dbls mark X, mark# cons(X1, X2) -> active# cons(X1, X2), mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2), mark# from X -> active# from X, active# dbl s X -> mark# s s dbl X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), active# sel(0(), cons(X, Y)) -> mark# X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), active# from X -> mark# cons(X, from s X)} Scc: { indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)} Scc: { from# mark X -> from# X, from# active X -> from# X} Scc: { dbls# mark X -> dbls# X, dbls# active X -> dbls# X} Scc: { s# mark X -> s# X, s# active X -> s# X} Scc: { dbl# mark X -> dbl# X, dbl# active X -> dbl# 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: { 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 (18): Strict: { mark# dbl X -> mark# X, mark# dbl X -> active# dbl mark X, mark# s X -> active# s X, mark# dbls X -> mark# X, mark# dbls X -> active# dbls mark X, mark# cons(X1, X2) -> active# cons(X1, X2), mark# sel(X1, X2) -> mark# X1, mark# sel(X1, X2) -> mark# X2, mark# sel(X1, X2) -> active# sel(mark X1, mark X2), mark# indx(X1, X2) -> mark# X1, mark# indx(X1, X2) -> active# indx(mark X1, X2), mark# from X -> active# from X, active# dbl s X -> mark# s s dbl X, active# dbls cons(X, Y) -> mark# cons(dbl X, dbls Y), active# sel(0(), cons(X, Y)) -> mark# X, active# sel(s X, cons(Y, Z)) -> mark# sel(X, Z), active# indx(cons(X, Y), Z) -> mark# cons(sel(X, Z), indx(Y, Z)), active# from X -> mark# cons(X, from s X)} Weak: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} Open SCC (4): Strict: { indx#(X1, mark X2) -> indx#(X1, X2), indx#(X1, active X2) -> indx#(X1, X2), indx#(mark X1, X2) -> indx#(X1, X2), indx#(active X1, X2) -> indx#(X1, X2)} Weak: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} Open SCC (2): Strict: { from# mark X -> from# X, from# active X -> from# X} Weak: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} Open SCC (2): Strict: { dbls# mark X -> dbls# X, dbls# active X -> dbls# X} Weak: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} Open SCC (2): Strict: { s# mark X -> s# X, s# active X -> s# X} Weak: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} Open SCC (2): Strict: { dbl# mark X -> dbl# X, dbl# active X -> dbl# X} Weak: { mark 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} 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 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} 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 0() -> active 0(), mark dbl X -> active dbl mark X, mark s X -> active s X, mark nil() -> active nil(), mark dbls X -> active dbls mark X, mark cons(X1, X2) -> active cons(X1, X2), mark sel(X1, X2) -> active sel(mark X1, mark X2), mark indx(X1, X2) -> active indx(mark X1, X2), mark from X -> active from X, active dbl 0() -> mark 0(), active dbl s X -> mark s s dbl X, active dbls nil() -> mark nil(), active dbls cons(X, Y) -> mark cons(dbl X, dbls Y), active sel(0(), cons(X, Y)) -> mark X, active sel(s X, cons(Y, Z)) -> mark sel(X, Z), active indx(nil(), X) -> mark nil(), active indx(cons(X, Y), Z) -> mark cons(sel(X, Z), indx(Y, Z)), active from X -> mark cons(X, from s X), dbl mark X -> dbl X, dbl active X -> dbl X, s mark X -> s X, s active X -> s X, dbls mark X -> dbls X, dbls active X -> dbls X, 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), 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), indx(X1, mark X2) -> indx(X1, X2), indx(X1, active X2) -> indx(X1, X2), indx(mark X1, X2) -> indx(X1, X2), indx(active X1, X2) -> indx(X1, X2), from mark X -> from X, from active X -> from X} Open