; @origtpdbfilename ./TRS/TRCSR/OvConsOS_nokinds_Z.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/OvConsOS_nokinds_Z.xml"
(format TRS)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun n__zeros 0)
(fun U11 2)
(fun tt 0)
(fun s 1)
(fun length 1)
(fun activate 1)
(fun U21 1)
(fun nil 0)
(fun U31 4)
(fun n__take 2)
(fun and 2)
(fun isNat 1)
(fun n__0 0)
(fun n__length 1)
(fun isNatList 1)
(fun n__s 1)
(fun isNatIList 1)
(fun n__cons 2)
(fun n__isNatIList 1)
(fun n__nil 0)
(fun n__isNatList 1)
(fun n__isNat 1)
(fun take 2)
(fun n__and 2)
(rule zeros (cons |0| n__zeros))
(rule (U11 tt L) (s (length (activate L))))
(rule (U21 tt) nil)
(rule (U31 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)) (isNatList (activate V1)))
(rule (isNat (n__s V1)) (isNat (activate V1)))
(rule (isNatIList V) (isNatList (activate V)))
(rule (isNatIList n__zeros) tt)
(rule (isNatIList (n__cons V1 V2)) (and (isNat (activate V1)) (n__isNatIList (activate V2))))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons V1 V2)) (and (isNat (activate V1)) (n__isNatList (activate V2))))
(rule (isNatList (n__take V1 V2)) (and (isNat (activate V1)) (n__isNatIList (activate V2))))
(rule (length nil) |0|)
(rule (length (cons N L)) (U11 (and (isNatList (activate L)) (n__isNat N)) (activate L)))
(rule (take |0| IL) (U21 (isNatIList IL)))
(rule (take (s M) (cons N IL)) (U31 (and (isNatIList (activate IL)) (n__and (isNat M) (n__isNat 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 (isNatIList X) (n__isNatIList X))
(rule nil n__nil)
(rule (isNatList X) (n__isNatList X))
(rule (isNat X) (n__isNat X))
(rule (and X1 X2) (n__and X1 X2))
(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__isNatIList X)) (isNatIList X))
(rule (activate n__nil) nil)
(rule (activate (n__isNatList X)) (isNatList X))
(rule (activate (n__isNat X)) (isNat X))
(rule (activate (n__and X1 X2)) (and X1 X2))
(rule (activate X) X)