; @origtpdbfilename ./TRS/TRCSR/OvConsOS_complete-noand_FR.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/OvConsOS_complete-noand_FR.xml"
(format TRS)
(fun zeros 0)
(fun cons 2)
(fun |0| 0)
(fun n__zeros 0)
(fun U101 3)
(fun tt 0)
(fun U102 3)
(fun isNatKind 1)
(fun activate 1)
(fun U103 3)
(fun isNatIListKind 1)
(fun U104 3)
(fun U105 2)
(fun isNat 1)
(fun U106 1)
(fun isNatIList 1)
(fun U11 2)
(fun U12 2)
(fun U111 3)
(fun U112 3)
(fun U113 3)
(fun U114 2)
(fun s 1)
(fun length 1)
(fun U13 1)
(fun isNatList 1)
(fun U121 2)
(fun U122 1)
(fun nil 0)
(fun U131 4)
(fun U132 4)
(fun U133 4)
(fun U134 4)
(fun U135 4)
(fun U136 4)
(fun n__take 2)
(fun U21 2)
(fun U22 2)
(fun U23 1)
(fun U31 2)
(fun U32 2)
(fun U33 1)
(fun U41 3)
(fun U42 3)
(fun U43 3)
(fun U44 3)
(fun U45 2)
(fun U46 1)
(fun U51 2)
(fun U52 1)
(fun U61 2)
(fun U62 1)
(fun U71 1)
(fun U81 1)
(fun U91 3)
(fun U92 3)
(fun U93 3)
(fun U94 3)
(fun U95 2)
(fun U96 1)
(fun n__0 0)
(fun n__length 1)
(fun n__s 1)
(fun n__cons 2)
(fun n__nil 0)
(fun take 2)
(rule zeros (cons |0| n__zeros))
(rule (U101 tt V1 V2) (U102 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U102 tt V1 V2) (U103 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U103 tt V1 V2) (U104 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U104 tt V1 V2) (U105 (isNat (activate V1)) (activate V2)))
(rule (U105 tt V2) (U106 (isNatIList (activate V2))))
(rule (U106 tt) tt)
(rule (U11 tt V1) (U12 (isNatIListKind (activate V1)) (activate V1)))
(rule (U111 tt L N) (U112 (isNatIListKind (activate L)) (activate L) (activate N)))
(rule (U112 tt L N) (U113 (isNat (activate N)) (activate L) (activate N)))
(rule (U113 tt L N) (U114 (isNatKind (activate N)) (activate L)))
(rule (U114 tt L) (s (length (activate L))))
(rule (U12 tt V1) (U13 (isNatList (activate V1))))
(rule (U121 tt IL) (U122 (isNatIListKind (activate IL))))
(rule (U122 tt) nil)
(rule (U13 tt) tt)
(rule (U131 tt IL M N) (U132 (isNatIListKind (activate IL)) (activate IL) (activate M) (activate N)))
(rule (U132 tt IL M N) (U133 (isNat (activate M)) (activate IL) (activate M) (activate N)))
(rule (U133 tt IL M N) (U134 (isNatKind (activate M)) (activate IL) (activate M) (activate N)))
(rule (U134 tt IL M N) (U135 (isNat (activate N)) (activate IL) (activate M) (activate N)))
(rule (U135 tt IL M N) (U136 (isNatKind (activate N)) (activate IL) (activate M) (activate N)))
(rule (U136 tt IL M N) (cons (activate N) (n__take (activate M) (activate IL))))
(rule (U21 tt V1) (U22 (isNatKind (activate V1)) (activate V1)))
(rule (U22 tt V1) (U23 (isNat (activate V1))))
(rule (U23 tt) tt)
(rule (U31 tt V) (U32 (isNatIListKind (activate V)) (activate V)))
(rule (U32 tt V) (U33 (isNatList (activate V))))
(rule (U33 tt) tt)
(rule (U41 tt V1 V2) (U42 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U42 tt V1 V2) (U43 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U43 tt V1 V2) (U44 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U44 tt V1 V2) (U45 (isNat (activate V1)) (activate V2)))
(rule (U45 tt V2) (U46 (isNatIList (activate V2))))
(rule (U46 tt) tt)
(rule (U51 tt V2) (U52 (isNatIListKind (activate V2))))
(rule (U52 tt) tt)
(rule (U61 tt V2) (U62 (isNatIListKind (activate V2))))
(rule (U62 tt) tt)
(rule (U71 tt) tt)
(rule (U81 tt) tt)
(rule (U91 tt V1 V2) (U92 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (U92 tt V1 V2) (U93 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U93 tt V1 V2) (U94 (isNatIListKind (activate V2)) (activate V1) (activate V2)))
(rule (U94 tt V1 V2) (U95 (isNat (activate V1)) (activate V2)))
(rule (U95 tt V2) (U96 (isNatList (activate V2))))
(rule (U96 tt) tt)
(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 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (isNatIListKind n__nil) tt)
(rule (isNatIListKind n__zeros) tt)
(rule (isNatIListKind (n__cons V1 V2)) (U51 (isNatKind (activate V1)) (activate V2)))
(rule (isNatIListKind (n__take V1 V2)) (U61 (isNatKind (activate V1)) (activate V2)))
(rule (isNatKind n__0) tt)
(rule (isNatKind (n__length V1)) (U71 (isNatIListKind (activate V1))))
(rule (isNatKind (n__s V1)) (U81 (isNatKind (activate V1))))
(rule (isNatList n__nil) tt)
(rule (isNatList (n__cons V1 V2)) (U91 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (isNatList (n__take V1 V2)) (U101 (isNatKind (activate V1)) (activate V1) (activate V2)))
(rule (length nil) |0|)
(rule (length (cons N L)) (U111 (isNatList (activate L)) (activate L) N))
(rule (take |0| IL) (U121 (isNatIList IL) IL))
(rule (take (s M) (cons N IL)) (U131 (isNatIList (activate IL)) (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 nil n__nil)
(rule (activate n__zeros) zeros)
(rule (activate (n__take X1 X2)) (take (activate X1) (activate X2)))
(rule (activate n__0) |0|)
(rule (activate (n__length X)) (length (activate X)))
(rule (activate (n__s X)) (s (activate X)))
(rule (activate (n__cons X1 X2)) (cons (activate X1) X2))
(rule (activate n__nil) nil)
(rule (activate X) X)