MAYBE Time: 0.016322 TRS: { Frozen(m, Sum_constant Left(), n, s) -> Term_sub(m, s), Frozen(m, Sum_constant Right(), n, s) -> Term_sub(n, s), Frozen(m, Sum_term_var xi, n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)), Sum_sub(xi, Id()) -> Sum_term_var xi, Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant k, Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)), Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s), Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_inl m, s) -> Term_inl Term_sub(m, s), Term_sub(Term_inr m, s) -> Term_inr Term_sub(m, s), Term_sub(Term_var x, Id()) -> Term_var x, Term_sub(Term_var x, Cons_usual(y, m, s)) -> m, Term_sub(Term_var x, Cons_usual(y, m, s)) -> Term_sub(Term_var x, s), Term_sub(Term_var x, Cons_sum(xi, k, s)) -> Term_sub(Term_var x, s), Concat(Id(), s) -> s, Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)), Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)), Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))} DP: DP: { Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Concat(s, t), u) -> Concat#(t, u)} TRS: { Frozen(m, Sum_constant Left(), n, s) -> Term_sub(m, s), Frozen(m, Sum_constant Right(), n, s) -> Term_sub(n, s), Frozen(m, Sum_term_var xi, n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)), Sum_sub(xi, Id()) -> Sum_term_var xi, Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant k, Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)), Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s), Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_inl m, s) -> Term_inl Term_sub(m, s), Term_sub(Term_inr m, s) -> Term_inr Term_sub(m, s), Term_sub(Term_var x, Id()) -> Term_var x, Term_sub(Term_var x, Cons_usual(y, m, s)) -> m, Term_sub(Term_var x, Cons_usual(y, m, s)) -> Term_sub(Term_var x, s), Term_sub(Term_var x, Cons_sum(xi, k, s)) -> Term_sub(Term_var x, s), Concat(Id(), s) -> s, Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)), Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)), Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))} UR: { Frozen(m, Sum_constant Left(), n, s) -> Term_sub(m, s), Frozen(m, Sum_constant Right(), n, s) -> Term_sub(n, s), Frozen(m, Sum_term_var xi, n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)), Sum_sub(xi, Id()) -> Sum_term_var xi, Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant k, Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)), Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s), Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_inl m, s) -> Term_inl Term_sub(m, s), Term_sub(Term_inr m, s) -> Term_inr Term_sub(m, s), Term_sub(Term_var x, Id()) -> Term_var x, Term_sub(Term_var x, Cons_usual(y, m, s)) -> m, Term_sub(Term_var x, Cons_usual(y, m, s)) -> Term_sub(Term_var x, s), Term_sub(Term_var x, Cons_sum(xi, k, s)) -> Term_sub(Term_var x, s), Concat(Id(), s) -> s, Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)), Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)), Concat(Concat(s, t), u) -> Concat(s, Concat(t, u)), a(z, w) -> z, a(z, w) -> w} EDG: { (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s)) (Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s)) (Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s)) (Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s)) (Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(t, u)) (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u))) (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)) (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t)) (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)) (Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s)) (Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)) (Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s)) (Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t))) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Case(m, xi, n), s) -> Sum_sub#(xi, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t)) (Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t)) (Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)) (Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u))) (Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(t, u)) (Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t)) (Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t)) (Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)) (Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u))) (Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(t, u)) (Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)) (Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)) (Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t)) (Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t)) (Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)) (Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u))) (Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Concat(s, t), u) -> Concat#(t, u)) (Concat#(Concat(s, t), u) -> Concat#(t, u), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t)) (Concat#(Concat(s, t), u) -> Concat#(t, u), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t)) (Concat#(Concat(s, t), u) -> Concat#(t, u), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)) (Concat#(Concat(s, t), u) -> Concat#(t, u), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u))) (Concat#(Concat(s, t), u) -> Concat#(t, u), Concat#(Concat(s, t), u) -> Concat#(t, u)) } STATUS: arrows: 0.654064 SCCS (3): Scc: { Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Concat(s, t), u) -> Concat#(t, u)} Scc: {Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)} Scc: {Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)} SCC (18): Strict: { Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s), Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s), Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s), Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_sub(m, s), t) -> Concat#(s, t), Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_inl m, s) -> Term_sub#(m, s), Term_sub#(Term_inr m, s) -> Term_sub#(m, s), Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t), Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)), Concat#(Concat(s, t), u) -> Concat#(t, u)} Weak: { Frozen(m, Sum_constant Left(), n, s) -> Term_sub(m, s), Frozen(m, Sum_constant Right(), n, s) -> Term_sub(n, s), Frozen(m, Sum_term_var xi, n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)), Sum_sub(xi, Id()) -> Sum_term_var xi, Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant k, Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)), Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s), Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_inl m, s) -> Term_inl Term_sub(m, s), Term_sub(Term_inr m, s) -> Term_inr Term_sub(m, s), Term_sub(Term_var x, Id()) -> Term_var x, Term_sub(Term_var x, Cons_usual(y, m, s)) -> m, Term_sub(Term_var x, Cons_usual(y, m, s)) -> Term_sub(Term_var x, s), Term_sub(Term_var x, Cons_sum(xi, k, s)) -> Term_sub(Term_var x, s), Concat(Id(), s) -> s, Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)), Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)), Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))} Open SCC (2): Strict: {Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s), Term_sub#(Term_var x, Cons_sum(xi, k, s)) -> Term_sub#(Term_var x, s)} Weak: { Frozen(m, Sum_constant Left(), n, s) -> Term_sub(m, s), Frozen(m, Sum_constant Right(), n, s) -> Term_sub(n, s), Frozen(m, Sum_term_var xi, n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)), Sum_sub(xi, Id()) -> Sum_term_var xi, Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant k, Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)), Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s), Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_inl m, s) -> Term_inl Term_sub(m, s), Term_sub(Term_inr m, s) -> Term_inr Term_sub(m, s), Term_sub(Term_var x, Id()) -> Term_var x, Term_sub(Term_var x, Cons_usual(y, m, s)) -> m, Term_sub(Term_var x, Cons_usual(y, m, s)) -> Term_sub(Term_var x, s), Term_sub(Term_var x, Cons_sum(xi, k, s)) -> Term_sub(Term_var x, s), Concat(Id(), s) -> s, Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)), Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)), Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))} Open SCC (2): Strict: {Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_sum(psi, k, s)) -> Sum_sub#(xi, s)} Weak: { Frozen(m, Sum_constant Left(), n, s) -> Term_sub(m, s), Frozen(m, Sum_constant Right(), n, s) -> Term_sub(n, s), Frozen(m, Sum_term_var xi, n, s) -> Case(Term_sub(m, s), xi, Term_sub(n, s)), Sum_sub(xi, Id()) -> Sum_term_var xi, Sum_sub(xi, Cons_usual(y, m, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_sub(xi, s), Sum_sub(xi, Cons_sum(psi, k, s)) -> Sum_constant k, Term_sub(Term_sub(m, s), t) -> Term_sub(m, Concat(s, t)), Term_sub(Case(m, xi, n), s) -> Frozen(m, Sum_sub(xi, s), n, s), Term_sub(Term_app(m, n), s) -> Term_app(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_pair(m, n), s) -> Term_pair(Term_sub(m, s), Term_sub(n, s)), Term_sub(Term_inl m, s) -> Term_inl Term_sub(m, s), Term_sub(Term_inr m, s) -> Term_inr Term_sub(m, s), Term_sub(Term_var x, Id()) -> Term_var x, Term_sub(Term_var x, Cons_usual(y, m, s)) -> m, Term_sub(Term_var x, Cons_usual(y, m, s)) -> Term_sub(Term_var x, s), Term_sub(Term_var x, Cons_sum(xi, k, s)) -> Term_sub(Term_var x, s), Concat(Id(), s) -> s, Concat(Cons_usual(x, m, s), t) -> Cons_usual(x, Term_sub(m, t), Concat(s, t)), Concat(Cons_sum(xi, k, s), t) -> Cons_sum(xi, k, Concat(s, t)), Concat(Concat(s, t), u) -> Concat(s, Concat(t, u))} Open