; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_complete-noand_Z.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_complete-noand_Z.xml"
(format TRS)
(fun U101 3)
(fun tt 0)
(fun U102 3)
(fun isNaturalKind 1)
(fun activate 1)
(fun U103 3)
(fun isLNatKind 1)
(fun U104 3)
(fun U105 2)
(fun isNatural 1)
(fun U106 1)
(fun isLNat 1)
(fun U11 3)
(fun U12 3)
(fun U111 2)
(fun U112 1)
(fun U13 3)
(fun U121 2)
(fun U122 1)
(fun U14 3)
(fun U131 1)
(fun snd 1)
(fun splitAt 2)
(fun U141 1)
(fun U151 1)
(fun U161 1)
(fun U171 2)
(fun U172 1)
(fun U181 2)
(fun U182 2)
(fun U183 1)
(fun U191 2)
(fun U192 2)
(fun U193 1)
(fun U201 3)
(fun U202 3)
(fun U203 3)
(fun U204 3)
(fun U205 2)
(fun U206 1)
(fun U21 3)
(fun U22 3)
(fun U211 1)
(fun U23 3)
(fun U221 1)
(fun U24 2)
(fun U231 2)
(fun U232 1)
(fun U241 3)
(fun U242 3)
(fun U243 3)
(fun U244 3)
(fun U245 2)
(fun U246 1)
(fun U251 3)
(fun U252 3)
(fun U253 3)
(fun U254 3)
(fun U255 2)
(fun U256 1)
(fun U261 2)
(fun U262 1)
(fun U271 2)
(fun U272 1)
(fun U281 2)
(fun U282 2)
(fun cons 2)
(fun n__natsFrom 1)
(fun s 1)
(fun U291 3)
(fun U292 3)
(fun U293 3)
(fun U294 3)
(fun head 1)
(fun afterNth 2)
(fun U301 3)
(fun U302 2)
(fun U303 2)
(fun U304 2)
(fun U31 3)
(fun U32 3)
(fun U311 2)
(fun U312 2)
(fun pair 2)
(fun nil 0)
(fun U33 3)
(fun U321 4)
(fun U322 4)
(fun U323 4)
(fun U324 4)
(fun U325 4)
(fun U326 4)
(fun U327 2)
(fun U34 2)
(fun U331 3)
(fun U332 2)
(fun U333 2)
(fun U334 2)
(fun U341 3)
(fun U342 3)
(fun U343 3)
(fun U344 3)
(fun fst 1)
(fun U41 3)
(fun U42 3)
(fun U43 3)
(fun U44 3)
(fun U45 2)
(fun U46 1)
(fun U51 3)
(fun U52 3)
(fun U53 3)
(fun U54 3)
(fun U55 2)
(fun U56 1)
(fun U61 2)
(fun U62 2)
(fun isPLNatKind 1)
(fun U63 1)
(fun isPLNat 1)
(fun U71 2)
(fun U72 2)
(fun U73 1)
(fun U81 2)
(fun U82 2)
(fun U83 1)
(fun U91 2)
(fun U92 2)
(fun U93 1)
(fun n__nil 0)
(fun n__afterNth 2)
(fun n__cons 2)
(fun n__fst 1)
(fun n__snd 1)
(fun n__tail 1)
(fun n__take 2)
(fun n__0 0)
(fun n__head 1)
(fun n__s 1)
(fun n__sel 2)
(fun n__pair 2)
(fun n__splitAt 2)
(fun natsFrom 1)
(fun sel 2)
(fun |0| 0)
(fun tail 1)
(fun take 2)
(rule (U101 tt V1 V2) (U102 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (U102 tt V1 V2) (U103 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U103 tt V1 V2) (U104 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U104 tt V1 V2) (U105 (isNatural (activate V1)) (activate V2)))
(rule (U105 tt V2) (U106 (isLNat (activate V2))))
(rule (U106 tt) tt)
(rule (U11 tt N XS) (U12 (isNaturalKind (activate N)) (activate N) (activate XS)))
(rule (U111 tt V2) (U112 (isLNatKind (activate V2))))
(rule (U112 tt) tt)
(rule (U12 tt N XS) (U13 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U121 tt V2) (U122 (isLNatKind (activate V2))))
(rule (U122 tt) tt)
(rule (U13 tt N XS) (U14 (isLNatKind (activate XS)) (activate N) (activate XS)))
(rule (U131 tt) tt)
(rule (U14 tt N XS) (snd (splitAt (activate N) (activate XS))))
(rule (U141 tt) tt)
(rule (U151 tt) tt)
(rule (U161 tt) tt)
(rule (U171 tt V2) (U172 (isLNatKind (activate V2))))
(rule (U172 tt) tt)
(rule (U181 tt V1) (U182 (isLNatKind (activate V1)) (activate V1)))
(rule (U182 tt V1) (U183 (isLNat (activate V1))))
(rule (U183 tt) tt)
(rule (U191 tt V1) (U192 (isNaturalKind (activate V1)) (activate V1)))
(rule (U192 tt V1) (U193 (isNatural (activate V1))))
(rule (U193 tt) tt)
(rule (U201 tt V1 V2) (U202 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (U202 tt V1 V2) (U203 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U203 tt V1 V2) (U204 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U204 tt V1 V2) (U205 (isNatural (activate V1)) (activate V2)))
(rule (U205 tt V2) (U206 (isLNat (activate V2))))
(rule (U206 tt) tt)
(rule (U21 tt X Y) (U22 (isLNatKind (activate X)) (activate X) (activate Y)))
(rule (U211 tt) tt)
(rule (U22 tt X Y) (U23 (isLNat (activate Y)) (activate X) (activate Y)))
(rule (U221 tt) tt)
(rule (U23 tt X Y) (U24 (isLNatKind (activate Y)) (activate X)))
(rule (U231 tt V2) (U232 (isLNatKind (activate V2))))
(rule (U232 tt) tt)
(rule (U24 tt X) (activate X))
(rule (U241 tt V1 V2) (U242 (isLNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U242 tt V1 V2) (U243 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U243 tt V1 V2) (U244 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U244 tt V1 V2) (U245 (isLNat (activate V1)) (activate V2)))
(rule (U245 tt V2) (U246 (isLNat (activate V2))))
(rule (U246 tt) tt)
(rule (U251 tt V1 V2) (U252 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (U252 tt V1 V2) (U253 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U253 tt V1 V2) (U254 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U254 tt V1 V2) (U255 (isNatural (activate V1)) (activate V2)))
(rule (U255 tt V2) (U256 (isLNat (activate V2))))
(rule (U256 tt) tt)
(rule (U261 tt V2) (U262 (isLNatKind (activate V2))))
(rule (U262 tt) tt)
(rule (U271 tt V2) (U272 (isLNatKind (activate V2))))
(rule (U272 tt) tt)
(rule (U281 tt N) (U282 (isNaturalKind (activate N)) (activate N)))
(rule (U282 tt N) (cons (activate N) (n__natsFrom (s (activate N)))))
(rule (U291 tt N XS) (U292 (isNaturalKind (activate N)) (activate N) (activate XS)))
(rule (U292 tt N XS) (U293 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U293 tt N XS) (U294 (isLNatKind (activate XS)) (activate N) (activate XS)))
(rule (U294 tt N XS) (head (afterNth (activate N) (activate XS))))
(rule (U301 tt X Y) (U302 (isLNatKind (activate X)) (activate Y)))
(rule (U302 tt Y) (U303 (isLNat (activate Y)) (activate Y)))
(rule (U303 tt Y) (U304 (isLNatKind (activate Y)) (activate Y)))
(rule (U304 tt Y) (activate Y))
(rule (U31 tt N XS) (U32 (isNaturalKind (activate N)) (activate N) (activate XS)))
(rule (U311 tt XS) (U312 (isLNatKind (activate XS)) (activate XS)))
(rule (U312 tt XS) (pair nil (activate XS)))
(rule (U32 tt N XS) (U33 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U321 tt N X XS) (U322 (isNaturalKind (activate N)) (activate N) (activate X) (activate XS)))
(rule (U322 tt N X XS) (U323 (isNatural (activate X)) (activate N) (activate X) (activate XS)))
(rule (U323 tt N X XS) (U324 (isNaturalKind (activate X)) (activate N) (activate X) (activate XS)))
(rule (U324 tt N X XS) (U325 (isLNat (activate XS)) (activate N) (activate X) (activate XS)))
(rule (U325 tt N X XS) (U326 (isLNatKind (activate XS)) (activate N) (activate X) (activate XS)))
(rule (U326 tt N X XS) (U327 (splitAt (activate N) (activate XS)) (activate X)))
(rule (U327 (pair YS ZS) X) (pair (cons (activate X) YS) ZS))
(rule (U33 tt N XS) (U34 (isLNatKind (activate XS)) (activate N)))
(rule (U331 tt N XS) (U332 (isNaturalKind (activate N)) (activate XS)))
(rule (U332 tt XS) (U333 (isLNat (activate XS)) (activate XS)))
(rule (U333 tt XS) (U334 (isLNatKind (activate XS)) (activate XS)))
(rule (U334 tt XS) (activate XS))
(rule (U34 tt N) (activate N))
(rule (U341 tt N XS) (U342 (isNaturalKind (activate N)) (activate N) (activate XS)))
(rule (U342 tt N XS) (U343 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U343 tt N XS) (U344 (isLNatKind (activate XS)) (activate N) (activate XS)))
(rule (U344 tt N XS) (fst (splitAt (activate N) (activate XS))))
(rule (U41 tt V1 V2) (U42 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (U42 tt V1 V2) (U43 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U43 tt V1 V2) (U44 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U44 tt V1 V2) (U45 (isNatural (activate V1)) (activate V2)))
(rule (U45 tt V2) (U46 (isLNat (activate V2))))
(rule (U46 tt) tt)
(rule (U51 tt V1 V2) (U52 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (U52 tt V1 V2) (U53 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U53 tt V1 V2) (U54 (isLNatKind (activate V2)) (activate V1) (activate V2)))
(rule (U54 tt V1 V2) (U55 (isNatural (activate V1)) (activate V2)))
(rule (U55 tt V2) (U56 (isLNat (activate V2))))
(rule (U56 tt) tt)
(rule (U61 tt V1) (U62 (isPLNatKind (activate V1)) (activate V1)))
(rule (U62 tt V1) (U63 (isPLNat (activate V1))))
(rule (U63 tt) tt)
(rule (U71 tt V1) (U72 (isNaturalKind (activate V1)) (activate V1)))
(rule (U72 tt V1) (U73 (isNatural (activate V1))))
(rule (U73 tt) tt)
(rule (U81 tt V1) (U82 (isPLNatKind (activate V1)) (activate V1)))
(rule (U82 tt V1) (U83 (isPLNat (activate V1))))
(rule (U83 tt) tt)
(rule (U91 tt V1) (U92 (isLNatKind (activate V1)) (activate V1)))
(rule (U92 tt V1) (U93 (isLNat (activate V1))))
(rule (U93 tt) tt)
(rule (afterNth N XS) (U11 (isNatural N) N XS))
(rule (fst (pair X Y)) (U21 (isLNat X) X Y))
(rule (head (cons N XS)) (U31 (isNatural N) N (activate XS)))
(rule (isLNat n__nil) tt)
(rule (isLNat (n__afterNth V1 V2)) (U41 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (isLNat (n__cons V1 V2)) (U51 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (isLNat (n__fst V1)) (U61 (isPLNatKind (activate V1)) (activate V1)))
(rule (isLNat (n__natsFrom V1)) (U71 (isNaturalKind (activate V1)) (activate V1)))
(rule (isLNat (n__snd V1)) (U81 (isPLNatKind (activate V1)) (activate V1)))
(rule (isLNat (n__tail V1)) (U91 (isLNatKind (activate V1)) (activate V1)))
(rule (isLNat (n__take V1 V2)) (U101 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (isLNatKind n__nil) tt)
(rule (isLNatKind (n__afterNth V1 V2)) (U111 (isNaturalKind (activate V1)) (activate V2)))
(rule (isLNatKind (n__cons V1 V2)) (U121 (isNaturalKind (activate V1)) (activate V2)))
(rule (isLNatKind (n__fst V1)) (U131 (isPLNatKind (activate V1))))
(rule (isLNatKind (n__natsFrom V1)) (U141 (isNaturalKind (activate V1))))
(rule (isLNatKind (n__snd V1)) (U151 (isPLNatKind (activate V1))))
(rule (isLNatKind (n__tail V1)) (U161 (isLNatKind (activate V1))))
(rule (isLNatKind (n__take V1 V2)) (U171 (isNaturalKind (activate V1)) (activate V2)))
(rule (isNatural n__0) tt)
(rule (isNatural (n__head V1)) (U181 (isLNatKind (activate V1)) (activate V1)))
(rule (isNatural (n__s V1)) (U191 (isNaturalKind (activate V1)) (activate V1)))
(rule (isNatural (n__sel V1 V2)) (U201 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (isNaturalKind n__0) tt)
(rule (isNaturalKind (n__head V1)) (U211 (isLNatKind (activate V1))))
(rule (isNaturalKind (n__s V1)) (U221 (isNaturalKind (activate V1))))
(rule (isNaturalKind (n__sel V1 V2)) (U231 (isNaturalKind (activate V1)) (activate V2)))
(rule (isPLNat (n__pair V1 V2)) (U241 (isLNatKind (activate V1)) (activate V1) (activate V2)))
(rule (isPLNat (n__splitAt V1 V2)) (U251 (isNaturalKind (activate V1)) (activate V1) (activate V2)))
(rule (isPLNatKind (n__pair V1 V2)) (U261 (isLNatKind (activate V1)) (activate V2)))
(rule (isPLNatKind (n__splitAt V1 V2)) (U271 (isNaturalKind (activate V1)) (activate V2)))
(rule (natsFrom N) (U281 (isNatural N) N))
(rule (sel N XS) (U291 (isNatural N) N XS))
(rule (snd (pair X Y)) (U301 (isLNat X) X Y))
(rule (splitAt |0| XS) (U311 (isLNat XS) XS))
(rule (splitAt (s N) (cons X XS)) (U321 (isNatural N) N X (activate XS)))
(rule (tail (cons N XS)) (U331 (isNatural N) N (activate XS)))
(rule (take N XS) (U341 (isNatural N) N XS))
(rule (natsFrom X) (n__natsFrom X))
(rule nil n__nil)
(rule (afterNth X1 X2) (n__afterNth X1 X2))
(rule (cons X1 X2) (n__cons X1 X2))
(rule (fst X) (n__fst X))
(rule (snd X) (n__snd X))
(rule (tail X) (n__tail X))
(rule (take X1 X2) (n__take X1 X2))
(rule |0| n__0)
(rule (head X) (n__head X))
(rule (s X) (n__s X))
(rule (sel X1 X2) (n__sel X1 X2))
(rule (pair X1 X2) (n__pair X1 X2))
(rule (splitAt X1 X2) (n__splitAt X1 X2))
(rule (activate (n__natsFrom X)) (natsFrom X))
(rule (activate n__nil) nil)
(rule (activate (n__afterNth X1 X2)) (afterNth X1 X2))
(rule (activate (n__cons X1 X2)) (cons X1 X2))
(rule (activate (n__fst X)) (fst X))
(rule (activate (n__snd X)) (snd X))
(rule (activate (n__tail X)) (tail X))
(rule (activate (n__take X1 X2)) (take X1 X2))
(rule (activate n__0) |0|)
(rule (activate (n__head X)) (head X))
(rule (activate (n__s X)) (s X))
(rule (activate (n__sel X1 X2)) (sel X1 X2))
(rule (activate (n__pair X1 X2)) (pair X1 X2))
(rule (activate (n__splitAt X1 X2)) (splitAt X1 X2))
(rule (activate X) X)