MAYBE Time: 0.812338 TRS: { msubst(a, id()) -> a, msubst(msubst(a, s), t) -> msubst(a, circ(s, t)), circ(s, id()) -> s, circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t)), circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t)), circ(cons(lift(), s), cons(lift(), t)) -> cons(lift(), circ(s, t)), circ(cons(lift(), s), circ(cons(lift(), t), u)) -> circ(cons(lift(), circ(s, t)), u), circ(circ(s, t), u) -> circ(s, circ(t, u)), circ(id(), s) -> s, subst(a, id()) -> a} DP: DP: { msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t)), msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t), circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(circ(s, t), u) -> circ#(t, u), circ#(circ(s, t), u) -> circ#(s, circ(t, u))} TRS: { msubst(a, id()) -> a, msubst(msubst(a, s), t) -> msubst(a, circ(s, t)), circ(s, id()) -> s, circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t)), circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t)), circ(cons(lift(), s), cons(lift(), t)) -> cons(lift(), circ(s, t)), circ(cons(lift(), s), circ(cons(lift(), t), u)) -> circ(cons(lift(), circ(s, t)), u), circ(circ(s, t), u) -> circ(s, circ(t, u)), circ(id(), s) -> s, subst(a, id()) -> a} UR: { msubst(a, id()) -> a, msubst(msubst(a, s), t) -> msubst(a, circ(s, t)), circ(s, id()) -> s, circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t)), circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t)), circ(cons(lift(), s), cons(lift(), t)) -> cons(lift(), circ(s, t)), circ(cons(lift(), s), circ(cons(lift(), t), u)) -> circ(cons(lift(), circ(s, t)), u), circ(circ(s, t), u) -> circ(s, circ(t, u)), circ(id(), s) -> s, a(x, y) -> x, a(x, y) -> y} EDG: {(circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(circ(s, t), u) -> circ#(t, u)) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(s, circ(t, u)), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(cons(a, s), t) -> msubst#(a, t), msubst#(msubst(a, s), t) -> circ#(s, t)) (circ#(cons(a, s), t) -> msubst#(a, t), msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t))) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(t, u)) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(t, u)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(t, u)) (circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(t, u)) (circ#(cons(a, s), t) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> circ#(s, t)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(t, u)) (msubst#(msubst(a, s), t) -> circ#(s, t), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (circ#(circ(s, t), u) -> circ#(t, u), circ#(cons(a, s), t) -> msubst#(a, t)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(cons(a, s), t) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(circ(s, t), u) -> circ#(t, u)) (circ#(circ(s, t), u) -> circ#(t, u), circ#(circ(s, t), u) -> circ#(s, circ(t, u))) (msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t)), msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t))) (msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t)), msubst#(msubst(a, s), t) -> circ#(s, t))} STATUS: arrows: 0.340000 SCCS (1): Scc: { msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t)), msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t), circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(circ(s, t), u) -> circ#(t, u), circ#(circ(s, t), u) -> circ#(s, circ(t, u))} SCC (10): Strict: { msubst#(msubst(a, s), t) -> msubst#(a, circ(s, t)), msubst#(msubst(a, s), t) -> circ#(s, t), circ#(cons(a, s), t) -> msubst#(a, t), circ#(cons(a, s), t) -> circ#(s, t), circ#(cons(lift(), s), cons(a, t)) -> circ#(s, t), circ#(cons(lift(), s), cons(lift(), t)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(s, t), circ#(cons(lift(), s), circ(cons(lift(), t), u)) -> circ#(cons(lift(), circ(s, t)), u), circ#(circ(s, t), u) -> circ#(t, u), circ#(circ(s, t), u) -> circ#(s, circ(t, u))} Weak: { msubst(a, id()) -> a, msubst(msubst(a, s), t) -> msubst(a, circ(s, t)), circ(s, id()) -> s, circ(cons(a, s), t) -> cons(msubst(a, t), circ(s, t)), circ(cons(lift(), s), cons(a, t)) -> cons(a, circ(s, t)), circ(cons(lift(), s), cons(lift(), t)) -> cons(lift(), circ(s, t)), circ(cons(lift(), s), circ(cons(lift(), t), u)) -> circ(cons(lift(), circ(s, t)), u), circ(circ(s, t), u) -> circ(s, circ(t, u)), circ(id(), s) -> s, subst(a, id()) -> a} Open