; @origtpdbfilename ./TRS/TRCSR/OvConsOS_complete_L.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/OvConsOS_complete_L.xml"
(format TRS)
(fun U71 1)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun U91 1)
(fun cons 1)
(fun and 1)
(fun zeros 0)
(fun |0| 0)
(fun U11 1)
(fun U12 1)
(fun isNatList 0)
(fun U21 1)
(fun U22 1)
(fun isNat 0)
(fun U31 1)
(fun U32 1)
(fun U41 1)
(fun U42 1)
(fun U43 1)
(fun isNatIList 0)
(fun U51 1)
(fun U52 1)
(fun U53 1)
(fun U61 1)
(fun U62 1)
(fun U63 1)
(fun U81 1)
(fun nil 0)
(fun isNatIListKind 0)
(fun isNatKind 0)
(fun take 2)
(rule (U71 tt) (s (length L)))
(rule (U91 tt) (cons N))
(rule (and tt) X)
(rule zeros (cons |0|))
(rule (U11 tt) (U12 isNatList))
(rule (U12 tt) tt)
(rule (U21 tt) (U22 isNat))
(rule (U22 tt) tt)
(rule (U31 tt) (U32 isNatList))
(rule (U32 tt) tt)
(rule (U41 tt) (U42 isNat))
(rule (U42 tt) (U43 isNatIList))
(rule (U43 tt) tt)
(rule (U51 tt) (U52 isNat))
(rule (U52 tt) (U53 isNatList))
(rule (U53 tt) tt)
(rule (U61 tt) (U62 isNat))
(rule (U62 tt) (U63 isNatIList))
(rule (U63 tt) tt)
(rule (U81 tt) nil)
(rule isNat tt)
(rule isNat (U11 isNatIListKind))
(rule isNat (U21 isNatKind))
(rule isNatIList (U31 isNatIListKind))
(rule isNatIList tt)
(rule isNatIList (U41 (and isNatKind)))
(rule isNatIListKind tt)
(rule isNatIListKind (and isNatKind))
(rule isNatKind tt)
(rule isNatKind isNatIListKind)
(rule isNatKind isNatKind)
(rule isNatList tt)
(rule isNatList (U51 (and isNatKind)))
(rule isNatList (U61 (and isNatKind)))
(rule (length nil) |0|)
(rule (length (cons N)) (U71 (and (and isNatList))))
(rule (take |0| IL) (U81 (and isNatIList)))
(rule (take (s M) (cons N)) (U91 (and (and isNatIList))))