MAYBE Time: 0.404240 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 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(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# 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 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 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# cons(sop lift(), 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# 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 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# cons(te a, 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# cons(te a, 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(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# 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# 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# 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# 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# 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# 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# cons(sop lift(), 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# cons(sop lift(), 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# 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# cons(sop lift(), 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(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# 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# cons(sop lift(), 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# 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 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# 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 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# 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# 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# 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 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# 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# cons(sop lift(), 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# cons(sop lift(), 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# 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 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# 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 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 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 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 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) -> 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 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 cons(sop lift(), sortSu circ(sortSu s, 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 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))) (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# cons(te msubst(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(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(te a, sortSu s), sortSu t) -> te# msubst(te a, 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# cons(te a, 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# 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# cons(sop lift(), 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# 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# cons(sop lift(), 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# 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(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# 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 s, sortSu circ(sortSu t, sortSu u))) } STATUS: arrows: 0.244898 SCCS (1): Scc: { 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))} SCC (14): Strict: { 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))} 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = x0, [msubst](x0, x1) = 1, [circ](x0, x1) = 1, [subst](x0, x1) = x0, [sortSu](x0) = 0, [te](x0) = 1, [sop](x0) = 0, [lift] = 0, [id] = 0, [sortSu#](x0) = x0, [te#](x0) = 1 Strict: te# msubst(te msubst(te a, sortSu s), sortSu t) -> te# msubst(te a, sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 1 + 0a + 0t + 0s te# msubst(te msubst(te a, sortSu s), sortSu t) -> sortSu# circ(sortSu s, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu circ(sortSu s, sortSu t), sortSu u) -> sortSu# circ(sortSu s, sortSu circ(sortSu t, sortSu u)) 1 + 0t + 0s + 0u >= 1 + 0t + 0s + 0u sortSu# circ(sortSu circ(sortSu s, sortSu t), sortSu u) -> sortSu# circ(sortSu t, sortSu u) 1 + 0t + 0s + 0u >= 1 + 0t + 0u 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) 1 + 0t + 0s + 0u >= 1 + 0t + 0s + 0u sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu circ(sortSu cons(sop lift(), sortSu t), sortSu u)) -> sortSu# circ(sortSu s, sortSu t) 1 + 0t + 0s + 0u >= 1 + 0t + 0s 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)) 1 + 0t + 0s + 0u >= 0 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(sop lift(), sortSu t)) -> sortSu# circ(sortSu s, sortSu t) 1 + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(sop lift(), sortSu t)) -> sortSu# cons(sop lift(), sortSu circ(sortSu s, sortSu t)) 1 + 0t + 0s >= 0 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(te a, sortSu t)) -> sortSu# circ(sortSu s, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(te a, sortSu t)) -> sortSu# cons(te a, sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 1 + 0a + 0t + 0s sortSu# circ(sortSu cons(te a, sortSu s), sortSu t) -> te# msubst(te a, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0a + 0t sortSu# circ(sortSu cons(te a, sortSu s), sortSu t) -> sortSu# circ(sortSu s, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu cons(te a, sortSu s), sortSu t) -> sortSu# cons(te msubst(te a, sortSu t), sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 1 + 0a + 0t + 0s Weak: te subst(te a, sortSu id()) -> te a 1 + 0a >= 1 + 0a te msubst(te msubst(te a, sortSu s), sortSu t) -> te msubst(te a, sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 1 + 0a + 0t + 0s te msubst(te a, sortSu id()) -> te a 1 + 0a >= 1 + 0a sortSu circ(sortSu id(), sortSu s) -> sortSu s 0 + 0s >= 0 + 0s sortSu circ(sortSu circ(sortSu s, sortSu t), sortSu u) -> sortSu circ(sortSu s, sortSu circ(sortSu t, sortSu u)) 0 + 0t + 0s + 0u >= 0 + 0t + 0s + 0u 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) 0 + 0t + 0s + 0u >= 0 + 0t + 0s + 0u sortSu circ(sortSu cons(sop lift(), sortSu s), sortSu cons(sop lift(), sortSu t)) -> sortSu cons(sop lift(), sortSu circ(sortSu s, sortSu t)) 0 + 0t + 0s >= 0 + 0t + 0s sortSu circ(sortSu cons(sop lift(), sortSu s), sortSu cons(te a, sortSu t)) -> sortSu cons(te a, sortSu circ(sortSu s, sortSu t)) 0 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s sortSu circ(sortSu cons(te a, sortSu s), sortSu t) -> sortSu cons(te msubst(te a, sortSu t), sortSu circ(sortSu s, sortSu t)) 0 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s sortSu circ(sortSu s, sortSu id()) -> sortSu s 0 + 0s >= 0 + 0s SCCS (1): Scc: { 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# 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 (12): Strict: { 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# 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} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [cons](x0, x1) = 0, [msubst](x0, x1) = 1, [circ](x0, x1) = 1, [subst](x0, x1) = 0, [sortSu](x0) = 0, [te](x0) = 0, [sop](x0) = 0, [lift] = 0, [id] = 0, [sortSu#](x0) = x0, [te#](x0) = 1 Strict: te# msubst(te msubst(te a, sortSu s), sortSu t) -> te# msubst(te a, sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 1 + 0a + 0t + 0s te# msubst(te msubst(te a, sortSu s), sortSu t) -> sortSu# circ(sortSu s, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu circ(sortSu s, sortSu t), sortSu u) -> sortSu# circ(sortSu s, sortSu circ(sortSu t, sortSu u)) 1 + 0t + 0s + 0u >= 1 + 0t + 0s + 0u sortSu# circ(sortSu circ(sortSu s, sortSu t), sortSu u) -> sortSu# circ(sortSu t, sortSu u) 1 + 0t + 0s + 0u >= 1 + 0t + 0u 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) 1 + 0t + 0s + 0u >= 1 + 0t + 0s + 0u sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu circ(sortSu cons(sop lift(), sortSu t), sortSu u)) -> sortSu# circ(sortSu s, sortSu t) 1 + 0t + 0s + 0u >= 1 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(sop lift(), sortSu t)) -> sortSu# circ(sortSu s, sortSu t) 1 + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(te a, sortSu t)) -> sortSu# circ(sortSu s, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu cons(sop lift(), sortSu s), sortSu cons(te a, sortSu t)) -> sortSu# cons(te a, sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s sortSu# circ(sortSu cons(te a, sortSu s), sortSu t) -> te# msubst(te a, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0a + 0t sortSu# circ(sortSu cons(te a, sortSu s), sortSu t) -> sortSu# circ(sortSu s, sortSu t) 1 + 0a + 0t + 0s >= 1 + 0t + 0s sortSu# circ(sortSu cons(te a, sortSu s), sortSu t) -> sortSu# cons(te msubst(te a, sortSu t), sortSu circ(sortSu s, sortSu t)) 1 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s Weak: te subst(te a, sortSu id()) -> te a 0 + 0a >= 0 + 0a te msubst(te msubst(te a, sortSu s), sortSu t) -> te msubst(te a, sortSu circ(sortSu s, sortSu t)) 0 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s te msubst(te a, sortSu id()) -> te a 0 + 0a >= 0 + 0a sortSu circ(sortSu id(), sortSu s) -> sortSu s 0 + 0s >= 0 + 0s sortSu circ(sortSu circ(sortSu s, sortSu t), sortSu u) -> sortSu circ(sortSu s, sortSu circ(sortSu t, sortSu u)) 0 + 0t + 0s + 0u >= 0 + 0t + 0s + 0u 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) 0 + 0t + 0s + 0u >= 0 + 0t + 0s + 0u sortSu circ(sortSu cons(sop lift(), sortSu s), sortSu cons(sop lift(), sortSu t)) -> sortSu cons(sop lift(), sortSu circ(sortSu s, sortSu t)) 0 + 0t + 0s >= 0 + 0t + 0s sortSu circ(sortSu cons(sop lift(), sortSu s), sortSu cons(te a, sortSu t)) -> sortSu cons(te a, sortSu circ(sortSu s, sortSu t)) 0 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s sortSu circ(sortSu cons(te a, sortSu s), sortSu t) -> sortSu cons(te msubst(te a, sortSu t), sortSu circ(sortSu s, sortSu t)) 0 + 0a + 0t + 0s >= 0 + 0a + 0t + 0s sortSu circ(sortSu s, sortSu id()) -> sortSu s 0 + 0s >= 0 + 0s 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} Fail