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