YES (VAR m xi n s x y k t psi u) (RULES 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 ) Proving termination of rewriting for lse: -> Dependency pairs: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Term_sub(Case(m,xi,n),s) -> nF_Sum_sub(xi,s) nF_Frozen(m,Sum_constant(Left),n,s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_constant(Right),n,s) -> nF_Term_sub(n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_var(x),Cons_usual(y,m,s)) -> nF_Term_sub(Term_var(x),s) nF_Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> nF_Term_sub(Term_var(x),s) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Sum_sub(xi,Cons_sum(psi,k,s)) -> nF_Sum_sub(xi,s) nF_Sum_sub(xi,Cons_usual(y,m,s)) -> nF_Sum_sub(xi,s) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Concat(Cons_usual(x,m,s),t) -> nF_Concat(s,t) nF_Concat(Cons_sum(xi,k,s),t) -> nF_Concat(s,t) -> Proof of termination for lse_1_1: -> -> Dependency pairs in cycle: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Concat(Cons_sum(xi,k,s),t) -> nF_Concat(s,t) nF_Concat(Cons_usual(x,m,s),t) -> nF_Concat(s,t) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_constant(Right),n,s) -> nF_Term_sub(n,s) nF_Frozen(m,Sum_constant(Left),n,s) -> nF_Term_sub(m,s) UsableRules: 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 Polynomial Interpretation: [Term_sub](X1,X2) = X1.X2 + X1 + X2 [Case](X1,X2,X3) = X1 + X3 + 1 [Frozen](X1,X2,X3,X4) = X1.X4 + X2.X4 + X3.X4 + X1 + X3 + X4 + 1 [Sum_sub](X1,X2) = 1 [Sum_constant](X) = 0 [Left] = 0 [Right] = 0 [Sum_term_var](X) = 1 [Term_app](X1,X2) = X1 + X2 + 1 [Term_pair](X1,X2) = X1 + X2 + 1 [Term_inl](X) = X [Term_inr](X) = X [Term_var](X) = 0 [Id] = 1 [Cons_usual](X1,X2,X3) = X2 + X3 + 1 [Cons_sum](X1,X2,X3) = X3 [Concat](X1,X2) = X1.X2 + X1 + X2 [nF_Term_sub](X1,X2) = X1 [nF_Concat](X1,X2) = X1 [nF_Frozen](X1,X2,X3,X4) = X1 + X3 + 1 TIME: 0.157153 -> -> Dependency pairs in cycle: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Frozen(m,Sum_constant(Right),n,s) -> nF_Term_sub(n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) nF_Concat(Cons_usual(x,m,s),t) -> nF_Concat(s,t) nF_Concat(Cons_sum(xi,k,s),t) -> nF_Concat(s,t) UsableRules: 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 Polynomial Interpretation: [Term_sub](X1,X2) = X1.X2 + X1 + X2 [Case](X1,X2,X3) = X1 + X3 + 1 [Frozen](X1,X2,X3,X4) = X1.X4 + X2.X4 + X3.X4 + X1 + X3 + X4 + 1 [Sum_sub](X1,X2) = 1 [Sum_constant](X) = 0 [Left] = 0 [Right] = 0 [Sum_term_var](X) = 1 [Term_app](X1,X2) = X1 + X2 + 1 [Term_pair](X1,X2) = X1 + X2 + 1 [Term_inl](X) = X [Term_inr](X) = X [Term_var](X) = X.X + X [Id] = 1 [Cons_usual](X1,X2,X3) = X2 + X3 + 1 [Cons_sum](X1,X2,X3) = X3 + 1 [Concat](X1,X2) = X1.X2 + X1 + X2 [nF_Term_sub](X1,X2) = X1 [nF_Frozen](X1,X2,X3,X4) = X1 + X3 [nF_Concat](X1,X2) = X1 TIME: 0.154349 -> -> Dependency pairs in cycle: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Concat(Cons_usual(x,m,s),t) -> nF_Concat(s,t) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_constant(Right),n,s) -> nF_Term_sub(n,s) UsableRules: 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 Polynomial Interpretation: [Term_sub](X1,X2) = X1.X2 + X1 + X2 [Case](X1,X2,X3) = X1 + X3 + 1 [Frozen](X1,X2,X3,X4) = X1.X4 + X2.X4 + X3.X4 + X1 + X3 + X4 + 1 [Sum_sub](X1,X2) = 1 [Sum_constant](X) = 0 [Left] = 0 [Right] = 0 [Sum_term_var](X) = 1 [Term_app](X1,X2) = X1 + X2 + 1 [Term_pair](X1,X2) = X1 + X2 + 1 [Term_inl](X) = X [Term_inr](X) = X [Term_var](X) = 0 [Id] = 1 [Cons_usual](X1,X2,X3) = X2 + X3 + 1 [Cons_sum](X1,X2,X3) = X3 [Concat](X1,X2) = X1.X2 + X1 + X2 [nF_Term_sub](X1,X2) = X1 [nF_Concat](X1,X2) = X1 [nF_Frozen](X1,X2,X3,X4) = X1 + X3 + 1 TIME: 0.143961 -> -> Dependency pairs in cycle: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) nF_Concat(Cons_usual(x,m,s),t) -> nF_Concat(s,t) UsableRules: 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 Polynomial Interpretation: [Term_sub](X1,X2) = X1.X2 + X1 + X2 [Case](X1,X2,X3) = X1 + X3 + 1 [Frozen](X1,X2,X3,X4) = X1.X4 + X2.X4 + X3.X4 + X1 + X3 + X4 + 1 [Sum_sub](X1,X2) = 1 [Sum_constant](X) = 0 [Left] = 0 [Right] = 0 [Sum_term_var](X) = 1 [Term_app](X1,X2) = X1 + X2 + 1 [Term_pair](X1,X2) = X1 + X2 + 1 [Term_inl](X) = X [Term_inr](X) = X [Term_var](X) = X.X + X [Id] = 1 [Cons_usual](X1,X2,X3) = X2 + X3 + 1 [Cons_sum](X1,X2,X3) = X3 [Concat](X1,X2) = X1.X2 + X1 + X2 [nF_Term_sub](X1,X2) = X1 [nF_Frozen](X1,X2,X3,X4) = X1 + X3 [nF_Concat](X1,X2) = X1 TIME: 0.147531 -> -> Dependency pairs in cycle: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(m,s) UsableRules: 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 Polynomial Interpretation: [Term_sub](X1,X2) = X1.X2 + X1 + X2 [Case](X1,X2,X3) = X1 + X3 + 1 [Frozen](X1,X2,X3,X4) = X1.X4 + X2.X4 + X3.X4 + X1 + X3 + X4 + 1 [Sum_sub](X1,X2) = 1 [Sum_constant](X) = 0 [Left] = 0 [Right] = 0 [Sum_term_var](X) = 1 [Term_app](X1,X2) = X1 + X2 + 1 [Term_pair](X1,X2) = X1 + X2 + 1 [Term_inl](X) = X [Term_inr](X) = X [Term_var](X) = 1 [Id] = 0 [Cons_usual](X1,X2,X3) = X2 + X3 + 1 [Cons_sum](X1,X2,X3) = X3 [Concat](X1,X2) = X1.X2 + X1 + X2 [nF_Term_sub](X1,X2) = X1 [nF_Concat](X1,X2) = X1 [nF_Frozen](X1,X2,X3,X4) = X1 + X3 + 1 TIME: 0.149311 -> -> Dependency pairs in cycle: nF_Term_sub(Case(m,xi,n),s) -> nF_Frozen(m,Sum_sub(xi,s),n,s) nF_Frozen(m,Sum_term_var(xi),n,s) -> nF_Term_sub(n,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_app(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_pair(m,n),s) -> nF_Term_sub(n,s) nF_Term_sub(Term_inl(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_inr(m),s) -> nF_Term_sub(m,s) nF_Term_sub(Term_sub(m,s),t) -> nF_Term_sub(m,Concat(s,t)) nF_Concat(Cons_usual(x,m,s),t) -> nF_Term_sub(m,t) nF_Term_sub(Term_sub(m,s),t) -> nF_Concat(s,t) nF_Concat(Concat(s,t),u) -> nF_Concat(s,Concat(t,u)) nF_Concat(Concat(s,t),u) -> nF_Concat(t,u) Termination proved: Cycles verify subterm criterion. -> Proof of termination for lse_1_2: -> -> Dependency pairs in cycle: nF_Sum_sub(xi,Cons_usual(y,m,s)) -> nF_Sum_sub(xi,s) nF_Sum_sub(xi,Cons_sum(psi,k,s)) -> nF_Sum_sub(xi,s) Termination proved: Cycles verify subterm criterion. -> Proof of termination for lse_1_3: -> -> Dependency pairs in cycle: nF_Term_sub(Term_var(x),Cons_sum(xi,k,s)) -> nF_Term_sub(Term_var(x),s) nF_Term_sub(Term_var(x),Cons_usual(y,m,s)) -> nF_Term_sub(Term_var(x),s) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Simple mixed Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.