MAYBE Problem: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Proof: DP Processor: DPs: Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,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) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),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#(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_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) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) 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_usual(y,m,s)) -> Sum_sub#(xi,s) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s TDG Processor: DPs: Term_sub#(Case(m,xi,n),s) -> Sum_sub#(xi,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) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),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#(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_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) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) 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_usual(y,m,s)) -> Sum_sub#(xi,s) Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Term_sub#(m,t) Concat#(Cons_sum(xi,k,s),t) -> Concat#(s,t) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s graph: 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#(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#(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#(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#(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#(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#(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) -> Term_sub#(m,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#(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#(t,u) 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#(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#(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) 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_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_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#(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_app(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#(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#(Case(m,xi,n),s) -> Sum_sub#(xi,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_sub(m,s),t) -> 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#(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_app(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#(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) -> 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#(Term_var(x),Cons_sum(xi,k,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_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_inr(m),s) -> Term_sub#(m,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_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_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#(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_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_sub(m,s),t) -> Concat#(s,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#(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_app(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#(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) -> Sum_sub#(xi,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#(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_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_inr(m),s) -> Term_sub#(m,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_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_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#(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) 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_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) -> 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) 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_sum(xi,k,s)) -> Term_sub#(Term_var(x),s) -> Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) 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) Term_sub#(Term_var(x),Cons_sum(xi,k,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_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_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#(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#(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#(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) -> Frozen#(m,Sum_sub(xi,s),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) 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_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) -> Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) 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) 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_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_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_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#(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#(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#(n,s) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),s) -> Term_sub#(Case(m,xi,n),s) -> Frozen#(m,Sum_sub(xi,s),n,s) Term_sub#(Term_var(x),Cons_usual(y,m,s)) -> Term_sub#(Term_var(x),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_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#(Term_var(x),Cons_sum(xi,k,s)) -> Term_sub#(Term_var(x),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_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#(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_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#(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_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#(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#(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_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#(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#(Case(m,xi,n),s) -> Sum_sub#(xi,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#(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_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_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#(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_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#(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#(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#(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#(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_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#(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#(Case(m,xi,n),s) -> Sum_sub#(xi,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#(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_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_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#(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_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#(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#(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#(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#(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_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#(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#(Case(m,xi,n),s) -> Sum_sub#(xi,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) -> 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#(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_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#(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#(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_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#(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#(Case(m,xi,n),s) -> Sum_sub#(xi,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_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_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#(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) SCC Processor: #sccs: 2 #rules: 22 #arcs: 203/529 DPs: Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) 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) Frozen#(m,Sum_constant(Left()),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#(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_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) 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)) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s EDG Processor: DPs: Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) 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) Frozen#(m,Sum_constant(Left()),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#(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_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) 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)) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s graph: Concat#(Concat(s,t),u) -> Concat#(t,u) -> Concat#(Concat(s,t),u) -> Concat#(t,u) 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#(Cons_usual(x,m,s),t) -> Concat#(s,t) 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_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) 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#(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) -> Term_sub#(m,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#(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_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) 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#(Concat(s,t),u) -> 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_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_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#(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_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#(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_inl(m),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_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_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)) 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_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#(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_inl(m),s) -> Term_sub#(m,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_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_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_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)) 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#(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_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_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_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#(Term_sub(m,s),t) -> Term_sub#(m,Concat(s,t)) 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_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#(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_inl(m),s) -> Term_sub#(m,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_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_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_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_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#(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_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_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) 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#(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_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) -> 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) -> 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) 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_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#(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_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_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#(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#(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_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_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_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_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_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_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_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#(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_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_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_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#(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_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_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_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_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_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_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_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#(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_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#(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_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#(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_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_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) 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_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_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_sub(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#(Concat(s,t),u) -> Concat#(s,Concat(t,u)) 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_usual(x,m,s),t) -> Term_sub#(m,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#(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#(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_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_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_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_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_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_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(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_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) SCC Processor: #sccs: 2 #rules: 20 #arcs: 165/400 DPs: Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,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)) Term_sub#(Term_sub(m,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)) Term_sub#(Term_inr(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_pair(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) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Arctic Interpretation Processor: dimension: 1 interpretation: [Concat#](x0, x1) = x0 + 0, [Frozen#](x0, x1, x2, x3) = x0 + x2 + 3, [Term_sub#](x0, x1) = x0 + 0, [Concat](x0, x1) = 2x0 + x1 + 2, [Cons_sum](x0, x1, x2) = 4x0 + 3x1 + x2 + 0, [Cons_usual](x0, x1, x2) = 1x0 + x1 + x2 + 0, [Id] = 0, [Term_var](x0) = x0, [Term_inr](x0) = x0, [Term_inl](x0) = x0 + 5, [Term_pair](x0, x1) = x0 + x1, [Term_app](x0, x1) = x0 + x1 + 2, [Sum_term_var](x0) = 0, [Right] = 2, [Sum_constant](x0) = x0, [Left] = 0, [Frozen](x0, x1, x2, x3) = 2x0 + 2x2 + x3 + 5, [Sum_sub](x0, x1) = x0 + x1 + 0, [Term_sub](x0, x1) = 2x0 + x1 + 0, [Case](x0, x1, x2) = x0 + x2 + 3 orientation: Concat#(Concat(s,t),u) = 2s + t + 2 >= t + 0 = Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) = 3k + s + 4xi + 0 >= s + 0 = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = m + s + 1x + 0 >= m + 0 = Term_sub#(m,t) Term_sub#(Term_sub(m,s),t) = 2m + s + 0 >= m + 0 = Term_sub#(m,Concat(s,t)) Term_sub#(Term_sub(m,s),t) = 2m + s + 0 >= s + 0 = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = m + s + 1x + 0 >= s + 0 = Concat#(s,t) Concat#(Concat(s,t),u) = 2s + t + 2 >= s + 0 = Concat#(s,Concat(t,u)) Term_sub#(Term_inr(m),s) = m + 0 >= m + 0 = Term_sub#(m,s) Term_sub#(Term_inl(m),s) = m + 5 >= m + 0 = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = m + n + 0 >= m + 0 = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = m + n + 0 >= n + 0 = Term_sub#(n,s) Term_sub#(Term_app(m,n),s) = m + n + 2 >= m + 0 = Term_sub#(m,s) Term_sub#(Term_app(m,n),s) = m + n + 2 >= n + 0 = Term_sub#(n,s) Term_sub#(Case(m,xi,n),s) = m + n + 3 >= m + n + 3 = Frozen#(m,Sum_sub(xi,s),n,s) Frozen#(m,Sum_term_var(xi),n,s) = m + n + 3 >= m + 0 = Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) = m + n + 3 >= n + 0 = Term_sub#(n,s) Frozen#(m,Sum_constant(Right()),n,s) = m + n + 3 >= n + 0 = Term_sub#(n,s) Frozen#(m,Sum_constant(Left()),n,s) = m + n + 3 >= m + 0 = Term_sub#(m,s) Term_sub(Case(m,xi,n),s) = 2m + 2n + s + 5 >= 2m + 2n + s + 5 = Frozen(m,Sum_sub(xi,s),n,s) Frozen(m,Sum_constant(Left()),n,s) = 2m + 2n + s + 5 >= 2m + s + 0 = Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) = 2m + 2n + s + 5 >= 2n + s + 0 = Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) = 2m + 2n + s + 5 >= 2m + 2n + s + 3 = Case(Term_sub(m,s),xi,Term_sub(n,s)) Term_sub(Term_app(m,n),s) = 2m + 2n + s + 4 >= 2m + 2n + s + 2 = Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_pair(m,n),s) = 2m + 2n + s + 0 >= 2m + 2n + s + 0 = Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) = 2m + s + 7 >= 2m + s + 5 = Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) = 2m + s + 0 >= 2m + s + 0 = Term_inr(Term_sub(m,s)) Term_sub(Term_var(x),Id()) = 2x + 0 >= x = Term_var(x) Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 2x + 1y + 0 >= m = m Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 2x + 1y + 0 >= s + 2x + 0 = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_sum(xi,k,s)) = 3k + s + 2x + 4xi + 0 >= s + 2x + 0 = Term_sub(Term_var(x),s) Term_sub(Term_sub(m,s),t) = 4m + 2s + t + 2 >= 2m + 2s + t + 2 = Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) = xi + 0 >= 0 = Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) = 3k + 4psi + s + xi + 0 >= k = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = 3k + 4psi + s + xi + 0 >= s + xi + 0 = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = m + s + xi + 1y + 0 >= s + xi + 0 = Sum_sub(xi,s) Concat(Concat(s,t),u) = 4s + 2t + u + 4 >= 2s + 2t + u + 2 = Concat(s,Concat(t,u)) Concat(Cons_usual(x,m,s),t) = 2m + 2s + t + 3x + 2 >= 2m + 2s + t + 1x + 2 = Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Cons_sum(xi,k,s),t) = 5k + 2s + t + 6xi + 2 >= 3k + 2s + t + 4xi + 2 = Cons_sum(xi,k,Concat(s,t)) Concat(Id(),s) = s + 2 >= s = s problem: DPs: Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,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)) Term_sub#(Term_sub(m,s),t) -> Concat#(s,t) Concat#(Cons_usual(x,m,s),t) -> Concat#(s,t) Term_sub#(Term_inr(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_pair(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) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Arctic Interpretation Processor: dimension: 1 interpretation: [Concat#](x0, x1) = x0, [Frozen#](x0, x1, x2, x3) = x0 + x1 + x2 + 0, [Term_sub#](x0, x1) = x0, [Concat](x0, x1) = 1x0 + x1 + 0, [Cons_sum](x0, x1, x2) = x1 + x2 + 0, [Cons_usual](x0, x1, x2) = 5x0 + x1 + x2, [Id] = 2, [Term_var](x0) = 3, [Term_inr](x0) = x0 + 0, [Term_inl](x0) = x0 + 0, [Term_pair](x0, x1) = x0 + x1 + 5, [Term_app](x0, x1) = x0 + x1 + 0, [Sum_term_var](x0) = x0 + 0, [Right] = 6, [Sum_constant](x0) = 0, [Left] = 0, [Frozen](x0, x1, x2, x3) = 1x0 + x1 + 1x2 + x3 + 0, [Sum_sub](x0, x1) = x0 + 0, [Term_sub](x0, x1) = 1x0 + x1 + 0, [Case](x0, x1, x2) = x0 + x1 + x2 + 0 orientation: Concat#(Concat(s,t),u) = 1s + t + 0 >= t = Concat#(t,u) Concat#(Cons_sum(xi,k,s),t) = k + s + 0 >= s = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = m + s + 5x >= m = Term_sub#(m,t) Term_sub#(Term_sub(m,s),t) = 1m + s + 0 >= m = Term_sub#(m,Concat(s,t)) Term_sub#(Term_sub(m,s),t) = 1m + s + 0 >= s = Concat#(s,t) Concat#(Cons_usual(x,m,s),t) = m + s + 5x >= s = Concat#(s,t) Term_sub#(Term_inr(m),s) = m + 0 >= m = Term_sub#(m,s) Term_sub#(Term_inl(m),s) = m + 0 >= m = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = m + n + 5 >= m = Term_sub#(m,s) Term_sub#(Term_pair(m,n),s) = m + n + 5 >= n = Term_sub#(n,s) Term_sub#(Term_app(m,n),s) = m + n + 0 >= m = Term_sub#(m,s) Term_sub#(Term_app(m,n),s) = m + n + 0 >= n = Term_sub#(n,s) Term_sub#(Case(m,xi,n),s) = m + n + xi + 0 >= m + n + xi + 0 = Frozen#(m,Sum_sub(xi,s),n,s) Frozen#(m,Sum_term_var(xi),n,s) = m + n + xi + 0 >= m = Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) = m + n + xi + 0 >= n = Term_sub#(n,s) Frozen#(m,Sum_constant(Right()),n,s) = m + n + 0 >= n = Term_sub#(n,s) Frozen#(m,Sum_constant(Left()),n,s) = m + n + 0 >= m = Term_sub#(m,s) Term_sub(Case(m,xi,n),s) = 1m + 1n + s + 1xi + 1 >= 1m + 1n + s + xi + 0 = Frozen(m,Sum_sub(xi,s),n,s) Frozen(m,Sum_constant(Left()),n,s) = 1m + 1n + s + 0 >= 1m + s + 0 = Term_sub(m,s) Frozen(m,Sum_constant(Right()),n,s) = 1m + 1n + s + 0 >= 1n + s + 0 = Term_sub(n,s) Frozen(m,Sum_term_var(xi),n,s) = 1m + 1n + s + xi + 0 >= 1m + 1n + s + xi + 0 = Case(Term_sub(m,s),xi,Term_sub(n,s)) Term_sub(Term_app(m,n),s) = 1m + 1n + s + 1 >= 1m + 1n + s + 0 = Term_app(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_pair(m,n),s) = 1m + 1n + s + 6 >= 1m + 1n + s + 5 = Term_pair(Term_sub(m,s),Term_sub(n,s)) Term_sub(Term_inl(m),s) = 1m + s + 1 >= 1m + s + 0 = Term_inl(Term_sub(m,s)) Term_sub(Term_inr(m),s) = 1m + s + 1 >= 1m + s + 0 = Term_inr(Term_sub(m,s)) Term_sub(Term_var(x),Id()) = 4 >= 3 = Term_var(x) Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 5y + 4 >= m = m Term_sub(Term_var(x),Cons_usual(y,m,s)) = m + s + 5y + 4 >= s + 4 = Term_sub(Term_var(x),s) Term_sub(Term_var(x),Cons_sum(xi,k,s)) = k + s + 4 >= s + 4 = Term_sub(Term_var(x),s) Term_sub(Term_sub(m,s),t) = 2m + 1s + t + 1 >= 1m + 1s + t + 0 = Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) = xi + 0 >= xi + 0 = Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) = xi + 0 >= 0 = Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) = xi + 0 >= xi + 0 = Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) = xi + 0 >= xi + 0 = Sum_sub(xi,s) Concat(Concat(s,t),u) = 2s + 1t + u + 1 >= 1s + 1t + u + 0 = Concat(s,Concat(t,u)) Concat(Cons_usual(x,m,s),t) = 1m + 1s + t + 6x + 0 >= 1m + 1s + t + 5x + 0 = Cons_usual(x,Term_sub(m,t),Concat(s,t)) Concat(Cons_sum(xi,k,s),t) = 1k + 1s + t + 1 >= k + 1s + t + 0 = Cons_sum(xi,k,Concat(s,t)) Concat(Id(),s) = s + 3 >= s = s problem: DPs: Concat#(Concat(s,t),u) -> Concat#(t,u) Concat#(Cons_sum(xi,k,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_inr(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_pair(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) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(m,s) Frozen#(m,Sum_term_var(xi),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_constant(Right()),n,s) -> Term_sub#(n,s) Frozen#(m,Sum_constant(Left()),n,s) -> Term_sub#(m,s) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Open DPs: 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) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Subterm Criterion Processor: simple projection: pi(Term_sub#) = 1 problem: DPs: TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Qed DPs: Sum_sub#(xi,Cons_sum(psi,k,s)) -> Sum_sub#(xi,s) Sum_sub#(xi,Cons_usual(y,m,s)) -> Sum_sub#(xi,s) TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Subterm Criterion Processor: simple projection: pi(Sum_sub#) = 1 problem: DPs: TRS: 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) Frozen(m,Sum_term_var(xi),n,s) -> Case(Term_sub(m,s),xi,Term_sub(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) Term_sub(Term_sub(m,s),t) -> Term_sub(m,Concat(s,t)) Sum_sub(xi,Id()) -> Sum_term_var(xi) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_constant(k) Sum_sub(xi,Cons_sum(psi,k,s)) -> Sum_sub(xi,s) Sum_sub(xi,Cons_usual(y,m,s)) -> Sum_sub(xi,s) Concat(Concat(s,t),u) -> Concat(s,Concat(t,u)) 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(Id(),s) -> s Qed