YES (VAR YS ZS X N XS Y) (STRATEGY CONTEXTSENSITIVE (U11 1) (pair-osb-LNat-csb-osb-LNat-csb 1 2) (cons-osb-Nat-csb-osb-LNat-csb 1) (afterNth-osb-Nat-csb-osb-LNat-csb 1 2) (snd-osb-PLNat-csb 1) (splitAt-osb-Nat-csb-osb-LNat-csb 1 2) (fst-osb-PLNat-csb 1) (head-osb-LNat-csb 1) (natsFrom-osb-Nat-csb 1) (s-osb-Nat-csb 1) (sel-osb-Nat-csb-osb-LNat-csb 1 2) (0) (nil) (tail-osb-LNat-csb 1) (take-osb-Nat-csb-osb-LNat-csb 1 2) ) (RULES U11(pair-osb-LNat-csb-osb-LNat-csb(YS,ZS),X) -> pair-osb-LNat-csb-osb-LNat-csb(cons-osb-Nat-csb-osb-LNat-csb(X,YS),ZS) afterNth-osb-Nat-csb-osb-LNat-csb(N,XS) -> snd-osb-PLNat-csb(splitAt-osb-Nat-csb-osb-LNat-csb(N,XS)) fst-osb-PLNat-csb(pair-osb-LNat-csb-osb-LNat-csb(X,Y)) -> X head-osb-LNat-csb(cons-osb-Nat-csb-osb-LNat-csb(N,XS)) -> N natsFrom-osb-Nat-csb(N) -> cons-osb-Nat-csb-osb-LNat-csb(N,natsFrom-osb-Nat-csb(s-osb-Nat-csb(N))) sel-osb-Nat-csb-osb-LNat-csb(N,XS) -> head-osb-LNat-csb(afterNth-osb-Nat-csb-osb-LNat-csb(N,XS)) snd-osb-PLNat-csb(pair-osb-LNat-csb-osb-LNat-csb(X,Y)) -> Y splitAt-osb-Nat-csb-osb-LNat-csb(0,XS) -> pair-osb-LNat-csb-osb-LNat-csb(nil,XS) splitAt-osb-Nat-csb-osb-LNat-csb(s-osb-Nat-csb(N),cons-osb-Nat-csb-osb-LNat-csb(X,XS)) -> U11(splitAt-osb-Nat-csb-osb-LNat-csb(N,XS),X) tail-osb-LNat-csb(cons-osb-Nat-csb-osb-LNat-csb(N,XS)) -> XS take-osb-Nat-csb-osb-LNat-csb(N,XS) -> fst-osb-PLNat-csb(splitAt-osb-Nat-csb-osb-LNat-csb(N,XS)) ) The TRS is orthogonal, thus termination of innermost context-sensitive rewriting is equivalent to termination of context-sensitive rewriting. Proving termination of context-sensitive rewriting for ToolInputFile: -> Dependency pairs: nFoU11(pair-osb-LNat-csb-osb-LNat-csb(YS,ZS),X) -> X nFoafterNth-osb-Nat-csb-osb-LNat-csb(N,XS) -> nFosnd-osb-PLNat-csb(splitAt-osb-Nat-csb-osb-LNat-csb(N,XS)) nFoafterNth-osb-Nat-csb-osb-LNat-csb(N,XS) -> nFosplitAt-osb-Nat-csb-osb-LNat-csb(N,XS) nFosel-osb-Nat-csb-osb-LNat-csb(N,XS) -> nFohead-osb-LNat-csb(afterNth-osb-Nat-csb-osb-LNat-csb(N,XS)) nFosel-osb-Nat-csb-osb-LNat-csb(N,XS) -> nFoafterNth-osb-Nat-csb-osb-LNat-csb(N,XS) nFosplitAt-osb-Nat-csb-osb-LNat-csb(s-osb-Nat-csb(N),cons-osb-Nat-csb-osb-LNat-csb(X,XS)) -> nFoU11(splitAt-osb-Nat-csb-osb-LNat-csb(N,XS),X) nFosplitAt-osb-Nat-csb-osb-LNat-csb(s-osb-Nat-csb(N),cons-osb-Nat-csb-osb-LNat-csb(X,XS)) -> nFosplitAt-osb-Nat-csb-osb-LNat-csb(N,XS) nFosplitAt-osb-Nat-csb-osb-LNat-csb(s-osb-Nat-csb(N),cons-osb-Nat-csb-osb-LNat-csb(X,XS)) -> XS nFotail-osb-LNat-csb(cons-osb-Nat-csb-osb-LNat-csb(N,XS)) -> XS nFotake-osb-Nat-csb-osb-LNat-csb(N,XS) -> nFofst-osb-PLNat-csb(splitAt-osb-Nat-csb-osb-LNat-csb(N,XS)) nFotake-osb-Nat-csb-osb-LNat-csb(N,XS) -> nFosplitAt-osb-Nat-csb-osb-LNat-csb(N,XS) -> Proof of termination for ToolInputFileo1: -> -> Dependency pairs in cycle: nFosplitAt-osb-Nat-csb-osb-LNat-csb(s-osb-Nat-csb(N),cons-osb-Nat-csb-osb-LNat-csb(X,XS)) -> nFosplitAt-osb-Nat-csb-osb-LNat-csb(N,XS) Termination proved: Cycles verify subterm criterion. SETTINGS: Base ordering: Polynomial ordering Proof mode: SCCs in CSDG + base ordering Upper bound for coeffs: 1 Rationals below 1 for all non-replacing args: No Polynomial interpretation: Linear Coeffs in polynomials: No rationals Delta: automatic Termination was proved succesfully.