YES (VAR ) (RULES 1 -> s-osb-os-osb-Nat-csb-os-csb(0) ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for ToolInputFileo1: -> Dependency pairs: No dependency pairs found. -> Proof of termination for ToolInputFileo1: Termination proved: No cycles in dependency graph. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 2 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic (VAR E L L' N) (RULES conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(E,L),L') -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(E,conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(L,L')) conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(nil,L) -> L cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) initial-osb-os-osb-Nat-csb-os-csb(s-osb-os-osb-Nat-csb-os-csb(N)) -> conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,initial-osb-os-osb-Nat-csb-os-csb(N)),cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,nil)) initial-osb-os-osb-Nat-csb-os-csb(0) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,nil) ) Proving termination of rewriting for ToolInputFileo2: -> Dependency pairs: nFoconc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(E,L),L') -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(E,conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(L,L')) nFoconc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(E,L),L') -> nFoconc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(L,L') nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFoinitial-osb-os-osb-Nat-csb-os-csb(s-osb-os-osb-Nat-csb-os-csb(N)) -> nFoconc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,initial-osb-os-osb-Nat-csb-os-csb(N)),cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,nil)) nFoinitial-osb-os-osb-Nat-csb-os-csb(s-osb-os-osb-Nat-csb-os-csb(N)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,initial-osb-os-osb-Nat-csb-os-csb(N)) nFoinitial-osb-os-osb-Nat-csb-os-csb(s-osb-os-osb-Nat-csb-os-csb(N)) -> nFoinitial-osb-os-osb-Nat-csb-os-csb(N) nFoinitial-osb-os-osb-Nat-csb-os-csb(s-osb-os-osb-Nat-csb-os-csb(N)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,nil) nFoinitial-osb-os-osb-Nat-csb-os-csb(0) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,nil) -> Proof of termination for ToolInputFileo2o1: -> -> Dependency pairs in cycle: nFoinitial-osb-os-osb-Nat-csb-os-csb(s-osb-os-osb-Nat-csb-os-csb(N)) -> nFoinitial-osb-os-osb-Nat-csb-os-csb(N) Termination proved: Cycles verify subterm criterion. -> Proof of termination for ToolInputFileo2o2: -> -> Dependency pairs in cycle: nFoconc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(E,L),L') -> nFoconc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(L,L') Termination proved: Cycles verify subterm criterion. -> Proof of termination for ToolInputFileo2o3: -> -> Dependency pairs in cycle: nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L) UsableRules: cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) Polynomial Interpretation: [conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = 0 [cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X1 + X2 [nil] = 0 [x] = 0 [o] = 0 [free] = 1 [initial-osb-os-osb-Nat-csb-os-csb](X) = 0 [s-osb-os-osb-Nat-csb-os-csb](X) = 0 [0] = 0 [nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X1 + X2 TIME: 1.396e-3 -> -> Dependency pairs in cycle: nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) UsableRules: cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) Polynomial Interpretation: [conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = 0 [cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X1 + X2 [nil] = 0 [x] = 0 [o] = 1 [free] = 0 [initial-osb-os-osb-Nat-csb-os-csb](X) = 0 [s-osb-os-osb-Nat-csb-os-csb](X) = 0 [0] = 0 [nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X2 TIME: 9.61e-4 -> -> Dependency pairs in cycle: nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L) UsableRules: cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) Polynomial Interpretation: [conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = 0 [cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X1 + X2 [nil] = 0 [x] = 0 [o] = 1 [free] = 1 [initial-osb-os-osb-Nat-csb-os-csb](X) = 0 [s-osb-os-osb-Nat-csb-os-csb](X) = 0 [0] = 0 [nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X2 TIME: 8.88e-4 -> -> Dependency pairs in cycle: nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) UsableRules: cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) Polynomial Interpretation: [conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = 0 [cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X1 + X2 + 1 [nil] = 0 [x] = 0 [o] = 0 [free] = 1 [initial-osb-os-osb-Nat-csb-os-csb](X) = 0 [s-osb-os-osb-Nat-csb-os-csb](X) = 0 [0] = 0 [nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X2 TIME: 6.61e-4 -> -> Dependency pairs in cycle: nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) UsableRules: cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,L)) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L))) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(x,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L))) cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L)) Polynomial Interpretation: [conc-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = 0 [cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X2 + 1 [nil] = 0 [x] = 0 [o] = 0 [free] = 0 [initial-osb-os-osb-Nat-csb-os-csb](X) = 0 [s-osb-os-osb-Nat-csb-os-csb](X) = 0 [0] = 0 [nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb](X1,X2) = X2 TIME: 5.69e-4 -> -> Dependency pairs in cycle: nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,cons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(o,L)) -> nFocons-osb-os-osb-Rabbit-csb-os-csb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(free,L) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 2 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic (VAR V) (RULES is'Listocb-Rabbit-ccb-osb-os-osb-Listocb-Rabbit-ccb-csb-os-csb(V) -> tt ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for ToolInputFileo3: -> Dependency pairs: No dependency pairs found. -> Proof of termination for ToolInputFileo3: Termination proved: No cycles in dependency graph. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 2 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic (VAR V) (RULES is'Nat-osb-os-osb-Nat-csb-os-csb(V) -> tt ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for ToolInputFileo4: -> Dependency pairs: No dependency pairs found. -> Proof of termination for ToolInputFileo4: Termination proved: No cycles in dependency graph. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 2 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic (VAR V) (RULES is'NzNat-osb-os-osb-Nat-csb-os-csb(V) -> tt ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for ToolInputFileo5: -> Dependency pairs: No dependency pairs found. -> Proof of termination for ToolInputFileo5: Termination proved: No cycles in dependency graph. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 2 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic (VAR V) (RULES is'Rabbit-osb-os-osb-Rabbit-csb-os-csb(V) -> tt ) The TRS is an overlay system and all critical pairs are trivial, thus termination of innermost rewriting is equivalent to termination of rewriting. Proving termination of innermost rewriting for ToolInputFileo6: -> Dependency pairs: No dependency pairs found. -> Proof of termination for ToolInputFileo6: Termination proved: No cycles in dependency graph. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in DG + base ordering Upper bound for coeffs: 2 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.