; @origtpdbfilename ./TRS/TRCSR/OvConsOS_complete_Z.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/OvConsOS_complete_Z.xml"
(format TRS)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun n__zeros 0)
(fun U11 2)
(fun tt 0)
(fun U12 1)
(fun isNatList 1)
(fun activate 1)
(fun U21 2)
(fun U22 1)
(fun isNat 1)
(fun U31 2)
(fun U32 1)
(fun U41 3)
(fun U42 2)
(fun U43 1)
(fun isNatIList 1)
(fun U51 3)
(fun U52 2)
(fun U53 1)
(fun U61 3)
(fun U62 2)
(fun U63 1)
(fun U71 2)
(fun s 1)
(fun length 1)
(fun U81 1)
(fun nil 0)
(fun U91 4)
(fun n__take 2)
(fun and 2)
(fun n__0 0)
(fun n__length 1)
(fun isNatIListKind 1)
(fun n__s 1)
(fun isNatKind 1)
(fun n__cons 2)
(fun n__isNatIListKind 1)
(fun n__nil 0)
(fun n__and 2)
(fun n__isNatKind 1)
(fun take 2)
(rule zeros (cons |0| n__zeros))
(rule (U11 tt V1) (U12 (isNatList (activate V1))))
(rule (U12 tt) tt)
(rule (U21 tt V1) (U22 (isNat (activate V1))))
(rule (U22 tt) tt)
(rule (U31 tt V) (U32 (isNatList (activate V))))
(rule (U32 tt) tt)
(rule (U41 tt V1 V2) (U42 (isNat (activate V1)) (activate V2)))
(rule (U42 tt V2) (U43 (isNatIList (activate V2))))
(rule (U43 tt) tt)
(rule (U51 tt V1 V2) (U52 (isNat (activate V1)) (activate V2)))
(rule (U52 tt V2) (U53 (isNatList (activate V2))))
(rule (U53 tt) tt)
(rule (U61 tt V1 V2) (U62 (isNat (activate V1)) (activate V2)))
(rule (U62 tt V2) (U63 (isNatIList (activate V2))))
(rule (U63 tt) tt)
(rule (U71 tt L) (s (length (activate L))))
(rule (U81 tt) nil)
(rule (U91 tt IL M N) (cons (activate N) (n__take (activate M) (activate IL))))
(rule (and tt X) (activate X))
(rule (isNat n__0) tt)
(rule (isNat (n__length V1)) (U11 (isNatIListKind (activate V1)) (activate V1)))
(rule (isNat (n__s V1)) (U21 (isNatKind (activate V1)) (activate V1)))
(rule (isNatIList V) (U31 (isNatIListKind (activate V)) (activate V)))
(rule (isNatIList n__zeros) tt)
(rule (isNatIList (n__cons V1 V2)) (U41 (and (isNatKind (activate V1)) (n__isNatIListKind (activate V2))) (activate V1) (activate V2)))
(rule (isNatIListKind n__nil) tt)
(rule (isNatIListKind n__zeros) tt)
(rule (isNatIListKind (n__cons V1 V2)) (and (isNatKind (activate V1)) (n__isNatIListKind (activate V2))))
(rule (isNatIListKind (n__take V1 V2)) (and (isNatKind (activate V1)) (n__isNatIListKind (activate V2))))
(rule (isNatKind n__0) tt)
(rule (isNatKind (n__length V1)) (isNatIListKind (activate V1)))
(rule (isNatKind (n__s V1)) (isNatKind (activate V1)))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons V1 V2)) (U51 (and (isNatKind (activate V1)) (n__isNatIListKind (activate V2))) (activate V1) (activate V2)))
(rule (isNatList (n__take V1 V2)) (U61 (and (isNatKind (activate V1)) (n__isNatIListKind (activate V2))) (activate V1) (activate V2)))
(rule (length nil) |0|)
(rule (length (cons N L)) (U71 (and (and (isNatList (activate L)) (n__isNatIListKind (activate L))) (n__and (isNat N) (n__isNatKind N))) (activate L)))
(rule (take |0| IL) (U81 (and (isNatIList IL) (n__isNatIListKind IL))))
(rule (take (s M) (cons N IL)) (U91 (and (and (isNatIList (activate IL)) (n__isNatIListKind (activate IL))) (n__and (and (isNat M) (n__isNatKind M)) (n__and (isNat N) (n__isNatKind N)))) (activate IL) M N))
(rule zeros n__zeros)
(rule (take X1 X2) (n__take X1 X2))
(rule |0| n__0)
(rule (length X) (n__length X))
(rule (s X) (n__s X))
(rule (cons X1 X2) (n__cons X1 X2))
(rule (isNatIListKind X) (n__isNatIListKind X))
(rule nil n__nil)
(rule (and X1 X2) (n__and X1 X2))
(rule (isNatKind X) (n__isNatKind X))
(rule (activate n__zeros) zeros)
(rule (activate (n__take X1 X2)) (take X1 X2))
(rule (activate n__0) |0|)
(rule (activate (n__length X)) (length X))
(rule (activate (n__s X)) (s X))
(rule (activate (n__cons X1 X2)) (cons X1 X2))
(rule (activate (n__isNatIListKind X)) (isNatIListKind X))
(rule (activate n__nil) nil)
(rule (activate (n__and X1 X2)) (and X1 X2))
(rule (activate (n__isNatKind X)) (isNatKind X))
(rule (activate X) X)