; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_nokinds_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_nokinds_FR.xml"
(format TRS)
(fun U101 3)
(fun tt 0)
(fun fst 1)
(fun splitAt 2)
(fun activate 1)
(fun U11 3)
(fun snd 1)
(fun U21 2)
(fun U31 2)
(fun U41 2)
(fun cons 2)
(fun n__natsFrom 1)
(fun n__s 1)
(fun U51 3)
(fun head 1)
(fun afterNth 2)
(fun U61 2)
(fun U71 2)
(fun pair 2)
(fun nil 0)
(fun U81 4)
(fun U82 2)
(fun U91 2)
(fun and 2)
(fun isNatural 1)
(fun n__isLNat 1)
(fun isLNat 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__sel 2)
(fun n__pair 2)
(fun n__splitAt 2)
(fun natsFrom 1)
(fun sel 2)
(fun |0| 0)
(fun s 1)
(fun n__and 2)
(fun n__isNatural 1)
(fun tail 1)
(fun take 2)
(rule (U101 tt N XS) (fst (splitAt (activate N) (activate XS))))
(rule (U11 tt N XS) (snd (splitAt (activate N) (activate XS))))
(rule (U21 tt X) (activate X))
(rule (U31 tt N) (activate N))
(rule (U41 tt N) (cons (activate N) (n__natsFrom (n__s (activate N)))))
(rule (U51 tt N XS) (head (afterNth (activate N) (activate XS))))
(rule (U61 tt Y) (activate Y))
(rule (U71 tt XS) (pair nil (activate XS)))
(rule (U81 tt N X XS) (U82 (splitAt (activate N) (activate XS)) (activate X)))
(rule (U82 (pair YS ZS) X) (pair (cons (activate X) YS) ZS))
(rule (U91 tt XS) (activate XS))
(rule (afterNth N XS) (U11 (and (isNatural N) (n__isLNat XS)) N XS))
(rule (and tt X) (activate X))
(rule (fst (pair X Y)) (U21 (and (isLNat X) (n__isLNat Y)) X))
(rule (head (cons N XS)) (U31 (and (isNatural N) (n__isLNat (activate XS))) N))
(rule (isLNat n__nil) tt)
(rule (isLNat (n__afterNth V1 V2)) (and (isNatural (activate V1)) (n__isLNat (activate V2))))
(rule (isLNat (n__cons V1 V2)) (and (isNatural (activate V1)) (n__isLNat (activate V2))))
(rule (isLNat (n__fst V1)) (isPLNat (activate V1)))
(rule (isLNat (n__natsFrom V1)) (isNatural (activate V1)))
(rule (isLNat (n__snd V1)) (isPLNat (activate V1)))
(rule (isLNat (n__tail V1)) (isLNat (activate V1)))
(rule (isLNat (n__take V1 V2)) (and (isNatural (activate V1)) (n__isLNat (activate V2))))
(rule (isNatural n__0) tt)
(rule (isNatural (n__head V1)) (isLNat (activate V1)))
(rule (isNatural (n__s V1)) (isNatural (activate V1)))
(rule (isNatural (n__sel V1 V2)) (and (isNatural (activate V1)) (n__isLNat (activate V2))))
(rule (isPLNat (n__pair V1 V2)) (and (isLNat (activate V1)) (n__isLNat (activate V2))))
(rule (isPLNat (n__splitAt V1 V2)) (and (isNatural (activate V1)) (n__isLNat (activate V2))))
(rule (natsFrom N) (U41 (isNatural N) N))
(rule (sel N XS) (U51 (and (isNatural N) (n__isLNat XS)) N XS))
(rule (snd (pair X Y)) (U61 (and (isLNat X) (n__isLNat Y)) Y))
(rule (splitAt |0| XS) (U71 (isLNat XS) XS))
(rule (splitAt (s N) (cons X XS)) (U81 (and (isNatural N) (n__and (n__isNatural X) (n__isLNat (activate XS)))) N X (activate XS)))
(rule (tail (cons N XS)) (U91 (and (isNatural N) (n__isLNat (activate XS))) (activate XS)))
(rule (take N XS) (U101 (and (isNatural N) (n__isLNat XS)) N XS))
(rule (natsFrom X) (n__natsFrom X))
(rule (s X) (n__s X))
(rule (isLNat X) (n__isLNat 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 (sel X1 X2) (n__sel X1 X2))
(rule (pair X1 X2) (n__pair X1 X2))
(rule (splitAt X1 X2) (n__splitAt X1 X2))
(rule (and X1 X2) (n__and X1 X2))
(rule (isNatural X) (n__isNatural X))
(rule (activate (n__natsFrom X)) (natsFrom (activate X)))
(rule (activate (n__s X)) (s (activate X)))
(rule (activate (n__isLNat X)) (isLNat X))
(rule (activate n__nil) nil)
(rule (activate (n__afterNth X1 X2)) (afterNth (activate X1) (activate X2)))
(rule (activate (n__cons X1 X2)) (cons (activate X1) X2))
(rule (activate (n__fst X)) (fst (activate X)))
(rule (activate (n__snd X)) (snd (activate X)))
(rule (activate (n__tail X)) (tail (activate X)))
(rule (activate (n__take X1 X2)) (take (activate X1) (activate X2)))
(rule (activate n__0) |0|)
(rule (activate (n__head X)) (head (activate X)))
(rule (activate (n__sel X1 X2)) (sel (activate X1) (activate X2)))
(rule (activate (n__pair X1 X2)) (pair (activate X1) (activate X2)))
(rule (activate (n__splitAt X1 X2)) (splitAt (activate X1) (activate X2)))
(rule (activate (n__and X1 X2)) (and (activate X1) X2))
(rule (activate (n__isNatural X)) (isNatural X))
(rule (activate X) X)