; @origtpdbfilename ./TRS/TRCSR/OvConsOS_complete_noand_GM.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/OvConsOS_complete_noand_GM.xml"
(format TRS)
(fun a__zeros 0)
(fun cons 2)
(fun |0| 0)
(fun zeros 0)
(fun a__U101 3)
(fun tt 0)
(fun a__U102 3)
(fun a__isNatKind 1)
(fun a__U103 3)
(fun a__isNatIListKind 1)
(fun a__U104 3)
(fun a__U105 2)
(fun a__isNat 1)
(fun a__U106 1)
(fun a__isNatIList 1)
(fun a__U11 2)
(fun a__U12 2)
(fun a__U111 3)
(fun a__U112 3)
(fun a__U113 3)
(fun a__U114 2)
(fun s 1)
(fun a__length 1)
(fun mark 1)
(fun a__U13 1)
(fun a__isNatList 1)
(fun a__U121 2)
(fun a__U122 1)
(fun nil 0)
(fun a__U131 4)
(fun a__U132 4)
(fun a__U133 4)
(fun a__U134 4)
(fun a__U135 4)
(fun a__U136 4)
(fun take 2)
(fun a__U21 2)
(fun a__U22 2)
(fun a__U23 1)
(fun a__U31 2)
(fun a__U32 2)
(fun a__U33 1)
(fun a__U41 3)
(fun a__U42 3)
(fun a__U43 3)
(fun a__U44 3)
(fun a__U45 2)
(fun a__U46 1)
(fun a__U51 2)
(fun a__U52 1)
(fun a__U61 2)
(fun a__U62 1)
(fun a__U71 1)
(fun a__U81 1)
(fun a__U91 3)
(fun a__U92 3)
(fun a__U93 3)
(fun a__U94 3)
(fun a__U95 2)
(fun a__U96 1)
(fun length 1)
(fun a__take 2)
(fun U101 3)
(fun U102 3)
(fun isNatKind 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 U13 1)
(fun isNatList 1)
(fun U121 2)
(fun U122 1)
(fun U131 4)
(fun U132 4)
(fun U133 4)
(fun U134 4)
(fun U135 4)
(fun U136 4)
(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)
(rule a__zeros (cons |0| zeros))
(rule (a__U101 tt V1 V2) (a__U102 (a__isNatKind V1) V1 V2))
(rule (a__U102 tt V1 V2) (a__U103 (a__isNatIListKind V2) V1 V2))
(rule (a__U103 tt V1 V2) (a__U104 (a__isNatIListKind V2) V1 V2))
(rule (a__U104 tt V1 V2) (a__U105 (a__isNat V1) V2))
(rule (a__U105 tt V2) (a__U106 (a__isNatIList V2)))
(rule (a__U106 tt) tt)
(rule (a__U11 tt V1) (a__U12 (a__isNatIListKind V1) V1))
(rule (a__U111 tt L N) (a__U112 (a__isNatIListKind L) L N))
(rule (a__U112 tt L N) (a__U113 (a__isNat N) L N))
(rule (a__U113 tt L N) (a__U114 (a__isNatKind N) L))
(rule (a__U114 tt L) (s (a__length (mark L))))
(rule (a__U12 tt V1) (a__U13 (a__isNatList V1)))
(rule (a__U121 tt IL) (a__U122 (a__isNatIListKind IL)))
(rule (a__U122 tt) nil)
(rule (a__U13 tt) tt)
(rule (a__U131 tt IL M N) (a__U132 (a__isNatIListKind IL) IL M N))
(rule (a__U132 tt IL M N) (a__U133 (a__isNat M) IL M N))
(rule (a__U133 tt IL M N) (a__U134 (a__isNatKind M) IL M N))
(rule (a__U134 tt IL M N) (a__U135 (a__isNat N) IL M N))
(rule (a__U135 tt IL M N) (a__U136 (a__isNatKind N) IL M N))
(rule (a__U136 tt IL M N) (cons (mark N) (take M IL)))
(rule (a__U21 tt V1) (a__U22 (a__isNatKind V1) V1))
(rule (a__U22 tt V1) (a__U23 (a__isNat V1)))
(rule (a__U23 tt) tt)
(rule (a__U31 tt V) (a__U32 (a__isNatIListKind V) V))
(rule (a__U32 tt V) (a__U33 (a__isNatList V)))
(rule (a__U33 tt) tt)
(rule (a__U41 tt V1 V2) (a__U42 (a__isNatKind V1) V1 V2))
(rule (a__U42 tt V1 V2) (a__U43 (a__isNatIListKind V2) V1 V2))
(rule (a__U43 tt V1 V2) (a__U44 (a__isNatIListKind V2) V1 V2))
(rule (a__U44 tt V1 V2) (a__U45 (a__isNat V1) V2))
(rule (a__U45 tt V2) (a__U46 (a__isNatIList V2)))
(rule (a__U46 tt) tt)
(rule (a__U51 tt V2) (a__U52 (a__isNatIListKind V2)))
(rule (a__U52 tt) tt)
(rule (a__U61 tt V2) (a__U62 (a__isNatIListKind V2)))
(rule (a__U62 tt) tt)
(rule (a__U71 tt) tt)
(rule (a__U81 tt) tt)
(rule (a__U91 tt V1 V2) (a__U92 (a__isNatKind V1) V1 V2))
(rule (a__U92 tt V1 V2) (a__U93 (a__isNatIListKind V2) V1 V2))
(rule (a__U93 tt V1 V2) (a__U94 (a__isNatIListKind V2) V1 V2))
(rule (a__U94 tt V1 V2) (a__U95 (a__isNat V1) V2))
(rule (a__U95 tt V2) (a__U96 (a__isNatList V2)))
(rule (a__U96 tt) tt)
(rule (a__isNat |0|) tt)
(rule (a__isNat (length V1)) (a__U11 (a__isNatIListKind V1) V1))
(rule (a__isNat (s V1)) (a__U21 (a__isNatKind V1) V1))
(rule (a__isNatIList V) (a__U31 (a__isNatIListKind V) V))
(rule (a__isNatIList zeros) tt)
(rule (a__isNatIList (cons V1 V2)) (a__U41 (a__isNatKind V1) V1 V2))
(rule (a__isNatIListKind nil) tt)
(rule (a__isNatIListKind zeros) tt)
(rule (a__isNatIListKind (cons V1 V2)) (a__U51 (a__isNatKind V1) V2))
(rule (a__isNatIListKind (take V1 V2)) (a__U61 (a__isNatKind V1) V2))
(rule (a__isNatKind |0|) tt)
(rule (a__isNatKind (length V1)) (a__U71 (a__isNatIListKind V1)))
(rule (a__isNatKind (s V1)) (a__U81 (a__isNatKind V1)))
(rule (a__isNatList nil) tt)
(rule (a__isNatList (cons V1 V2)) (a__U91 (a__isNatKind V1) V1 V2))
(rule (a__isNatList (take V1 V2)) (a__U101 (a__isNatKind V1) V1 V2))
(rule (a__length nil) |0|)
(rule (a__length (cons N L)) (a__U111 (a__isNatList L) L N))
(rule (a__take |0| IL) (a__U121 (a__isNatIList IL) IL))
(rule (a__take (s M) (cons N IL)) (a__U131 (a__isNatIList IL) IL M N))
(rule (mark zeros) a__zeros)
(rule (mark (U101 X1 X2 X3)) (a__U101 (mark X1) X2 X3))
(rule (mark (U102 X1 X2 X3)) (a__U102 (mark X1) X2 X3))
(rule (mark (isNatKind X)) (a__isNatKind X))
(rule (mark (U103 X1 X2 X3)) (a__U103 (mark X1) X2 X3))
(rule (mark (isNatIListKind X)) (a__isNatIListKind X))
(rule (mark (U104 X1 X2 X3)) (a__U104 (mark X1) X2 X3))
(rule (mark (U105 X1 X2)) (a__U105 (mark X1) X2))
(rule (mark (isNat X)) (a__isNat X))
(rule (mark (U106 X)) (a__U106 (mark X)))
(rule (mark (isNatIList X)) (a__isNatIList X))
(rule (mark (U11 X1 X2)) (a__U11 (mark X1) X2))
(rule (mark (U12 X1 X2)) (a__U12 (mark X1) X2))
(rule (mark (U111 X1 X2 X3)) (a__U111 (mark X1) X2 X3))
(rule (mark (U112 X1 X2 X3)) (a__U112 (mark X1) X2 X3))
(rule (mark (U113 X1 X2 X3)) (a__U113 (mark X1) X2 X3))
(rule (mark (U114 X1 X2)) (a__U114 (mark X1) X2))
(rule (mark (length X)) (a__length (mark X)))
(rule (mark (U13 X)) (a__U13 (mark X)))
(rule (mark (isNatList X)) (a__isNatList X))
(rule (mark (U121 X1 X2)) (a__U121 (mark X1) X2))
(rule (mark (U122 X)) (a__U122 (mark X)))
(rule (mark (U131 X1 X2 X3 X4)) (a__U131 (mark X1) X2 X3 X4))
(rule (mark (U132 X1 X2 X3 X4)) (a__U132 (mark X1) X2 X3 X4))
(rule (mark (U133 X1 X2 X3 X4)) (a__U133 (mark X1) X2 X3 X4))
(rule (mark (U134 X1 X2 X3 X4)) (a__U134 (mark X1) X2 X3 X4))
(rule (mark (U135 X1 X2 X3 X4)) (a__U135 (mark X1) X2 X3 X4))
(rule (mark (U136 X1 X2 X3 X4)) (a__U136 (mark X1) X2 X3 X4))
(rule (mark (take X1 X2)) (a__take (mark X1) (mark X2)))
(rule (mark (U21 X1 X2)) (a__U21 (mark X1) X2))
(rule (mark (U22 X1 X2)) (a__U22 (mark X1) X2))
(rule (mark (U23 X)) (a__U23 (mark X)))
(rule (mark (U31 X1 X2)) (a__U31 (mark X1) X2))
(rule (mark (U32 X1 X2)) (a__U32 (mark X1) X2))
(rule (mark (U33 X)) (a__U33 (mark X)))
(rule (mark (U41 X1 X2 X3)) (a__U41 (mark X1) X2 X3))
(rule (mark (U42 X1 X2 X3)) (a__U42 (mark X1) X2 X3))
(rule (mark (U43 X1 X2 X3)) (a__U43 (mark X1) X2 X3))
(rule (mark (U44 X1 X2 X3)) (a__U44 (mark X1) X2 X3))
(rule (mark (U45 X1 X2)) (a__U45 (mark X1) X2))
(rule (mark (U46 X)) (a__U46 (mark X)))
(rule (mark (U51 X1 X2)) (a__U51 (mark X1) X2))
(rule (mark (U52 X)) (a__U52 (mark X)))
(rule (mark (U61 X1 X2)) (a__U61 (mark X1) X2))
(rule (mark (U62 X)) (a__U62 (mark X)))
(rule (mark (U71 X)) (a__U71 (mark X)))
(rule (mark (U81 X)) (a__U81 (mark X)))
(rule (mark (U91 X1 X2 X3)) (a__U91 (mark X1) X2 X3))
(rule (mark (U92 X1 X2 X3)) (a__U92 (mark X1) X2 X3))
(rule (mark (U93 X1 X2 X3)) (a__U93 (mark X1) X2 X3))
(rule (mark (U94 X1 X2 X3)) (a__U94 (mark X1) X2 X3))
(rule (mark (U95 X1 X2)) (a__U95 (mark X1) X2))
(rule (mark (U96 X)) (a__U96 (mark X)))
(rule (mark (cons X1 X2)) (cons (mark X1) X2))
(rule (mark |0|) |0|)
(rule (mark tt) tt)
(rule (mark (s X)) (s (mark X)))
(rule (mark nil) nil)
(rule a__zeros zeros)
(rule (a__U101 X1 X2 X3) (U101 X1 X2 X3))
(rule (a__U102 X1 X2 X3) (U102 X1 X2 X3))
(rule (a__isNatKind X) (isNatKind X))
(rule (a__U103 X1 X2 X3) (U103 X1 X2 X3))
(rule (a__isNatIListKind X) (isNatIListKind X))
(rule (a__U104 X1 X2 X3) (U104 X1 X2 X3))
(rule (a__U105 X1 X2) (U105 X1 X2))
(rule (a__isNat X) (isNat X))
(rule (a__U106 X) (U106 X))
(rule (a__isNatIList X) (isNatIList X))
(rule (a__U11 X1 X2) (U11 X1 X2))
(rule (a__U12 X1 X2) (U12 X1 X2))
(rule (a__U111 X1 X2 X3) (U111 X1 X2 X3))
(rule (a__U112 X1 X2 X3) (U112 X1 X2 X3))
(rule (a__U113 X1 X2 X3) (U113 X1 X2 X3))
(rule (a__U114 X1 X2) (U114 X1 X2))
(rule (a__length X) (length X))
(rule (a__U13 X) (U13 X))
(rule (a__isNatList X) (isNatList X))
(rule (a__U121 X1 X2) (U121 X1 X2))
(rule (a__U122 X) (U122 X))
(rule (a__U131 X1 X2 X3 X4) (U131 X1 X2 X3 X4))
(rule (a__U132 X1 X2 X3 X4) (U132 X1 X2 X3 X4))
(rule (a__U133 X1 X2 X3 X4) (U133 X1 X2 X3 X4))
(rule (a__U134 X1 X2 X3 X4) (U134 X1 X2 X3 X4))
(rule (a__U135 X1 X2 X3 X4) (U135 X1 X2 X3 X4))
(rule (a__U136 X1 X2 X3 X4) (U136 X1 X2 X3 X4))
(rule (a__take X1 X2) (take X1 X2))
(rule (a__U21 X1 X2) (U21 X1 X2))
(rule (a__U22 X1 X2) (U22 X1 X2))
(rule (a__U23 X) (U23 X))
(rule (a__U31 X1 X2) (U31 X1 X2))
(rule (a__U32 X1 X2) (U32 X1 X2))
(rule (a__U33 X) (U33 X))
(rule (a__U41 X1 X2 X3) (U41 X1 X2 X3))
(rule (a__U42 X1 X2 X3) (U42 X1 X2 X3))
(rule (a__U43 X1 X2 X3) (U43 X1 X2 X3))
(rule (a__U44 X1 X2 X3) (U44 X1 X2 X3))
(rule (a__U45 X1 X2) (U45 X1 X2))
(rule (a__U46 X) (U46 X))
(rule (a__U51 X1 X2) (U51 X1 X2))
(rule (a__U52 X) (U52 X))
(rule (a__U61 X1 X2) (U61 X1 X2))
(rule (a__U62 X) (U62 X))
(rule (a__U71 X) (U71 X))
(rule (a__U81 X) (U81 X))
(rule (a__U91 X1 X2 X3) (U91 X1 X2 X3))
(rule (a__U92 X1 X2 X3) (U92 X1 X2 X3))
(rule (a__U93 X1 X2 X3) (U93 X1 X2 X3))
(rule (a__U94 X1 X2 X3) (U94 X1 X2 X3))
(rule (a__U95 X1 X2) (U95 X1 X2))
(rule (a__U96 X) (U96 X))