YES Time: 0.166921 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))} 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)) } SCCS (3): 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: { 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 (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))} SPSC: Simple Projection: pi(Term_sub#) = 1 Strict: {Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)} EDG: {(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))} SCCS (1): Scc: {Term_sub#(Term_var x, Cons_usual(y, m, s)) -> Term_sub#(Term_var x, s)} SCC (1): Strict: {Term_sub#(Term_var x, Cons_usual(y, m, 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))} SPSC: Simple Projection: pi(Term_sub#) = 1 Strict: {} Qed 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))} SPSC: Simple Projection: pi(Sum_sub#) = 1 Strict: {Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s)} EDG: {(Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s), Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s))} SCCS (1): Scc: {Sum_sub#(xi, Cons_usual(y, m, s)) -> Sum_sub#(xi, s)} SCC (1): Strict: {Sum_sub#(xi, Cons_usual(y, m, 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))} SPSC: Simple Projection: pi(Sum_sub#) = 1 Strict: {} Qed 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [Frozen](x0, x1, x2, x3) = 0, [Case](x0, x1, x2) = x0 + x1, [Cons_usual](x0, x1, x2) = x0 + x1, [Cons_sum](x0, x1, x2) = x0, [Sum_sub](x0, x1) = 0, [Term_sub](x0, x1) = x0 + x1, [Term_app](x0, x1) = x0 + x1, [Term_pair](x0, x1) = x0 + x1, [Concat](x0, x1) = x0 + x1 + 1, [Sum_constant](x0) = 0, [Sum_term_var](x0) = 0, [Term_inl](x0) = x0, [Term_inr](x0) = x0, [Term_var](x0) = 0, [Left] = 0, [Right] = 0, [Id] = 0, [Frozen#](x0, x1, x2, x3) = x0 + x1, [Term_sub#](x0, x1) = x0, [Concat#](x0, x1) = x0 Strict: Concat#(Concat(s, t), u) -> Concat#(t, u) 1 + 1s + 1t + 0u >= 0 + 1t + 0u Concat#(Concat(s, t), u) -> Concat#(s, Concat(t, u)) 1 + 1s + 1t + 0u >= 0 + 1s + 0t + 0u Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t) 0 + 0xi + 1s + 0k + 0t >= 0 + 1s + 0t Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t) 0 + 1m + 1s + 0x + 0t >= 0 + 1s + 0t Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t) 0 + 1m + 1s + 0x + 0t >= 0 + 1m + 0t Term_sub#(Term_inr m, s) -> Term_sub#(m, s) 0 + 1m + 0s >= 0 + 1m + 0s Term_sub#(Term_inl m, s) -> Term_sub#(m, s) 0 + 1m + 0s >= 0 + 1m + 0s Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0xi + 0s + 1n Term_sub#(Term_sub(m, s), t) -> Concat#(s, t) 0 + 1m + 1s + 0t >= 0 + 1s + 0t Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)) 0 + 1m + 1s + 0t >= 0 + 1m + 0s + 0t Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0s Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Weak: EDG: { (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)) (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) -> 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#(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_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) -> 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_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) -> 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))) (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_inl m, 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_pair(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_app(m, n), s) -> Term_sub#(m, s)) (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#(Term_sub(m, s), t) -> 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_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_inl m, 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_pair(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_app(m, n), s) -> Term_sub#(m, s)) (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#(Term_sub(m, s), t) -> 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_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_inl m, 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_pair(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_app(m, n), s) -> Term_sub#(m, s)) (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#(Term_sub(m, s), t) -> 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_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#(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_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#(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_pair(m, n), s) -> Term_sub#(n, 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_inr m, s) -> Term_sub#(m, s)) (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_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#(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_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#(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_pair(m, n), s) -> Term_sub#(n, 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_inr m, s) -> Term_sub#(m, s)) (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_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#(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#(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_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#(n, 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_inr m, s) -> Term_sub#(m, 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#(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_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#(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)) (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)) (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) -> Term_sub#(m, 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#(Term_sub(m, s), t) -> 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)) (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#(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_pair(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#(n, 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_inr m, s) -> Term_sub#(m, s)) } SCCS (1): 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)} SCC (16): 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)} 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [Frozen](x0, x1, x2, x3) = 0, [Case](x0, x1, x2) = x0 + x1, [Cons_usual](x0, x1, x2) = x0 + x1 + 1, [Cons_sum](x0, x1, x2) = x0, [Sum_sub](x0, x1) = 0, [Term_sub](x0, x1) = x0 + x1, [Term_app](x0, x1) = x0 + x1, [Term_pair](x0, x1) = x0 + x1, [Concat](x0, x1) = 0, [Sum_constant](x0) = 0, [Sum_term_var](x0) = 0, [Term_inl](x0) = x0, [Term_inr](x0) = x0 + 1, [Term_var](x0) = 0, [Left] = 0, [Right] = 0, [Id] = 0, [Frozen#](x0, x1, x2, x3) = x0 + x1, [Term_sub#](x0, x1) = x0, [Concat#](x0, x1) = x0 Strict: Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t) 0 + 0xi + 1s + 0k + 0t >= 0 + 1s + 0t Concat#(Cons_usual(x, m, s), t) -> Concat#(s, t) 1 + 1m + 1s + 0x + 0t >= 0 + 1s + 0t Concat#(Cons_usual(x, m, s), t) -> Term_sub#(m, t) 1 + 1m + 1s + 0x + 0t >= 0 + 1m + 0t Term_sub#(Term_inr m, s) -> Term_sub#(m, s) 1 + 1m + 0s >= 0 + 1m + 0s Term_sub#(Term_inl m, s) -> Term_sub#(m, s) 0 + 1m + 0s >= 0 + 1m + 0s Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0xi + 0s + 1n Term_sub#(Term_sub(m, s), t) -> Concat#(s, t) 0 + 1m + 1s + 0t >= 0 + 1s + 0t Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)) 0 + 1m + 1s + 0t >= 0 + 1m + 0s + 0t Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0s Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Weak: EDG: {(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)) (Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t), Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)) (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) -> 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_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) -> 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))) (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_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#(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_app(m, n), s) -> Term_sub#(m, s)) (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#(Term_sub(m, s), t) -> 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_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_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#(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_app(m, n), s) -> Term_sub#(m, s)) (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#(Term_sub(m, s), t) -> 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_inl 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) -> Concat#(s, t)) (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_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#(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_pair(m, n), s) -> Term_sub#(n, 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#(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_sub(m, s), t) -> Concat#(s, t)) (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_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#(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_pair(m, n), s) -> Term_sub#(n, 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#(m, 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) -> Concat#(s, t)) (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_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#(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_pair(m, n), s) -> Term_sub#(n, s)) (Term_sub#(Term_app(m, 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_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#(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_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#(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)) (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) -> Term_sub#(m, 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#(Term_sub(m, s), t) -> 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)) (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#(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_pair(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#(n, s)) (Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_inl m, s) -> Term_sub#(m, s))} SCCS (2): Scc: {Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)} 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#(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)} SCC (1): Strict: {Concat#(Cons_sum(xi, k, s), t) -> Concat#(s, t)} 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))} SPSC: Simple Projection: pi(Concat#) = 0 Strict: {} Qed SCC (11): 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#(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)} 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [Frozen](x0, x1, x2, x3) = 0, [Case](x0, x1, x2) = x0 + x1 + 1, [Cons_usual](x0, x1, x2) = 1, [Cons_sum](x0, x1, x2) = 1, [Sum_sub](x0, x1) = 1, [Term_sub](x0, x1) = x0 + x1, [Term_app](x0, x1) = x0 + x1, [Term_pair](x0, x1) = x0 + x1, [Concat](x0, x1) = 0, [Sum_constant](x0) = 0, [Sum_term_var](x0) = 0, [Term_inl](x0) = x0 + 1, [Term_inr](x0) = 0, [Term_var](x0) = 1, [Left] = 0, [Right] = 0, [Id] = 0, [Frozen#](x0, x1, x2, x3) = x0 + x1 + x2, [Term_sub#](x0, x1) = x0 Strict: Term_sub#(Term_inl m, s) -> Term_sub#(m, s) 1 + 1m + 0s >= 0 + 1m + 0s Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s) 1 + 1m + 0xi + 0s + 1n >= 1 + 1m + 0xi + 0s + 1n Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)) 0 + 1m + 1s + 0t >= 0 + 1m + 0s + 0t Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0s Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Weak: EDG: {(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)) (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) -> 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) -> Term_sub#(m, Concat(s, t))) (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) -> 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) -> Term_sub#(m, Concat(s, t))) (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_pair(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_app(m, n), s) -> Term_sub#(m, s)) (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#(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_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#(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_app(m, n), s) -> Term_sub#(m, s)) (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#(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_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_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#(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_pair(m, n), s) -> Term_sub#(n, s)) (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_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_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#(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_pair(m, n), s) -> Term_sub#(n, 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#(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#(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_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#(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_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)) (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#(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_app(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_pair(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#(n, s))} SCCS (1): 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#(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)} SCC (10): 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#(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)} 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [Frozen](x0, x1, x2, x3) = 0, [Case](x0, x1, x2) = x0 + x1, [Cons_usual](x0, x1, x2) = x0, [Cons_sum](x0, x1, x2) = 0, [Sum_sub](x0, x1) = 0, [Term_sub](x0, x1) = x0, [Term_app](x0, x1) = x0 + x1 + 1, [Term_pair](x0, x1) = x0 + x1, [Concat](x0, x1) = 1, [Sum_constant](x0) = 0, [Sum_term_var](x0) = 0, [Term_inl](x0) = 0, [Term_inr](x0) = 0, [Term_var](x0) = 0, [Left] = 0, [Right] = 0, [Id] = 0, [Frozen#](x0, x1, x2, x3) = x0 + x1, [Term_sub#](x0, x1) = x0 Strict: Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Term_app(m, n), s) -> Term_sub#(n, s) 1 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_app(m, n), s) -> Term_sub#(m, s) 1 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0xi + 0s + 1n Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)) 0 + 1m + 0s + 0t >= 0 + 1m + 0s + 0t Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0s Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Weak: EDG: {(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)) (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#(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) -> Term_sub#(m, Concat(s, t))) (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#(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) -> Term_sub#(m, Concat(s, t))) (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_pair(m, n), s) -> Term_sub#(m, s)) (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#(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_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_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#(n, 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#(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#(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_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#(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_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)) (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#(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_pair(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#(n, s))} SCCS (1): 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#(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_pair(m, n), s) -> Term_sub#(n, s)} SCC (8): 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#(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_pair(m, n), s) -> Term_sub#(n, 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))} POLY: Mode: weak, max_in=1, output_bits=-1, dnum=1, ur=true Interpretation: [Frozen](x0, x1, x2, x3) = 0, [Case](x0, x1, x2) = x0 + x1 + 1, [Cons_usual](x0, x1, x2) = 0, [Cons_sum](x0, x1, x2) = 0, [Sum_sub](x0, x1) = 0, [Term_sub](x0, x1) = x0 + x1, [Term_app](x0, x1) = x0 + x1, [Term_pair](x0, x1) = x0 + x1, [Concat](x0, x1) = 0, [Sum_constant](x0) = 0, [Sum_term_var](x0) = 0, [Term_inl](x0) = 0, [Term_inr](x0) = 0, [Term_var](x0) = 0, [Left] = 0, [Right] = 0, [Id] = 0, [Frozen#](x0, x1, x2, x3) = x0 + x1, [Term_sub#](x0, x1) = x0 Strict: Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Term_sub#(Term_pair(m, n), s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Term_sub#(Case(m, xi, n), s) -> Frozen#(m, Sum_sub(xi, s), n, s) 1 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0xi + 0s + 1n Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)) 0 + 1m + 1s + 0t >= 0 + 1m + 0s + 0t Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(n, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_term_var xi, n, s) -> Term_sub#(m, s) 0 + 1m + 0xi + 0s + 1n >= 0 + 1m + 0s Frozen#(m, Sum_constant Right(), n, s) -> Term_sub#(n, s) 0 + 1m + 0s + 1n >= 0 + 0s + 1n Frozen#(m, Sum_constant Left(), n, s) -> Term_sub#(m, s) 0 + 1m + 0s + 1n >= 0 + 1m + 0s Weak: EDG: {(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_pair(m, n), s) -> Term_sub#(m, 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_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_pair(m, n), s) -> Term_sub#(m, 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))) (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_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#(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)) (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))) (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_pair(m, n), s) -> Term_sub#(n, s)) (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_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_pair(m, 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) -> Term_sub#(m, Concat(s, t))) (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_pair(m, n), s) -> Term_sub#(n, s))} SCCS (1): Scc: { 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_pair(m, n), s) -> Term_sub#(n, s)} SCC (3): Strict: { 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_pair(m, n), s) -> Term_sub#(n, 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))} SPSC: Simple Projection: pi(Term_sub#) = 0 Strict: { Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)} EDG: {(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_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#(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#(Term_pair(m, n), s) -> Term_sub#(n, s))} SCCS (1): Scc: { Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)} SCC (2): Strict: { Term_sub#(Term_sub(m, s), t) -> Term_sub#(m, Concat(s, t)), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, 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))} SPSC: Simple Projection: pi(Term_sub#) = 0 Strict: {Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)} EDG: {(Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s), Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s))} SCCS (1): Scc: {Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, s)} SCC (1): Strict: {Term_sub#(Term_pair(m, n), s) -> Term_sub#(n, 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))} SPSC: Simple Projection: pi(Term_sub#) = 0 Strict: {} Qed