; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_nokinds-noand_Z.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nokinds-noand_Z.xml"
(format TRS)
(fun U101 2)
(fun tt 0)
(fun U102 1)
(fun isLNat 1)
(fun activate 1)
(fun U11 3)
(fun U12 3)
(fun U111 1)
(fun snd 1)
(fun splitAt 2)
(fun U121 1)
(fun U131 2)
(fun U132 1)
(fun U141 2)
(fun U142 1)
(fun U151 2)
(fun U152 1)
(fun U161 2)
(fun cons 2)
(fun n__natsFrom 1)
(fun s 1)
(fun U171 3)
(fun U172 3)
(fun head 1)
(fun afterNth 2)
(fun U181 2)
(fun U182 2)
(fun U191 2)
(fun pair 2)
(fun nil 0)
(fun U201 4)
(fun U202 4)
(fun isNatural 1)
(fun U203 4)
(fun U204 2)
(fun U21 3)
(fun U22 2)
(fun U211 2)
(fun U212 2)
(fun U221 3)
(fun U222 3)
(fun fst 1)
(fun U31 3)
(fun U32 2)
(fun U41 2)
(fun U42 1)
(fun U51 2)
(fun U52 1)
(fun U61 1)
(fun U71 1)
(fun U81 1)
(fun U91 1)
(fun n__nil 0)
(fun n__afterNth 2)
(fun n__cons 2)
(fun n__fst 1)
(fun isPLNat 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 V2) (U102 (isLNat (activate V2))))
(rule (U102 tt) tt)
(rule (U11 tt N XS) (U12 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U111 tt) tt)
(rule (U12 tt N XS) (snd (splitAt (activate N) (activate XS))))
(rule (U121 tt) tt)
(rule (U131 tt V2) (U132 (isLNat (activate V2))))
(rule (U132 tt) tt)
(rule (U141 tt V2) (U142 (isLNat (activate V2))))
(rule (U142 tt) tt)
(rule (U151 tt V2) (U152 (isLNat (activate V2))))
(rule (U152 tt) tt)
(rule (U161 tt N) (cons (activate N) (n__natsFrom (s (activate N)))))
(rule (U171 tt N XS) (U172 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U172 tt N XS) (head (afterNth (activate N) (activate XS))))
(rule (U181 tt Y) (U182 (isLNat (activate Y)) (activate Y)))
(rule (U182 tt Y) (activate Y))
(rule (U191 tt XS) (pair nil (activate XS)))
(rule (U201 tt N X XS) (U202 (isNatural (activate X)) (activate N) (activate X) (activate XS)))
(rule (U202 tt N X XS) (U203 (isLNat (activate XS)) (activate N) (activate X) (activate XS)))
(rule (U203 tt N X XS) (U204 (splitAt (activate N) (activate XS)) (activate X)))
(rule (U204 (pair YS ZS) X) (pair (cons (activate X) YS) ZS))
(rule (U21 tt X Y) (U22 (isLNat (activate Y)) (activate X)))
(rule (U211 tt XS) (U212 (isLNat (activate XS)) (activate XS)))
(rule (U212 tt XS) (activate XS))
(rule (U22 tt X) (activate X))
(rule (U221 tt N XS) (U222 (isLNat (activate XS)) (activate N) (activate XS)))
(rule (U222 tt N XS) (fst (splitAt (activate N) (activate XS))))
(rule (U31 tt N XS) (U32 (isLNat (activate XS)) (activate N)))
(rule (U32 tt N) (activate N))
(rule (U41 tt V2) (U42 (isLNat (activate V2))))
(rule (U42 tt) tt)
(rule (U51 tt V2) (U52 (isLNat (activate V2))))
(rule (U52 tt) tt)
(rule (U61 tt) tt)
(rule (U71 tt) tt)
(rule (U81 tt) tt)
(rule (U91 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 (isNatural (activate V1)) (activate V2)))
(rule (isLNat (n__cons V1 V2)) (U51 (isNatural (activate V1)) (activate V2)))
(rule (isLNat (n__fst V1)) (U61 (isPLNat (activate V1))))
(rule (isLNat (n__natsFrom V1)) (U71 (isNatural (activate V1))))
(rule (isLNat (n__snd V1)) (U81 (isPLNat (activate V1))))
(rule (isLNat (n__tail V1)) (U91 (isLNat (activate V1))))
(rule (isLNat (n__take V1 V2)) (U101 (isNatural (activate V1)) (activate V2)))
(rule (isNatural n__0) tt)
(rule (isNatural (n__head V1)) (U111 (isLNat (activate V1))))
(rule (isNatural (n__s V1)) (U121 (isNatural (activate V1))))
(rule (isNatural (n__sel V1 V2)) (U131 (isNatural (activate V1)) (activate V2)))
(rule (isPLNat (n__pair V1 V2)) (U141 (isLNat (activate V1)) (activate V2)))
(rule (isPLNat (n__splitAt V1 V2)) (U151 (isNatural (activate V1)) (activate V2)))
(rule (natsFrom N) (U161 (isNatural N) N))
(rule (sel N XS) (U171 (isNatural N) N XS))
(rule (snd (pair X Y)) (U181 (isLNat X) Y))
(rule (splitAt |0| XS) (U191 (isLNat XS) XS))
(rule (splitAt (s N) (cons X XS)) (U201 (isNatural N) N X (activate XS)))
(rule (tail (cons N XS)) (U211 (isNatural N) (activate XS)))
(rule (take N XS) (U221 (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)