; @origtpdbfilename ./TRS/TRCSR/LISTUTILITIES_complete_noand_C.trs
; @xtcfilename "./TRS_Standard/Transformed_CSR_04/LISTUTILITIES_complete_noand_C.xml"
(format TRS)
(fun active 1)
(fun U101 3)
(fun tt 0)
(fun mark 1)
(fun U102 3)
(fun isNaturalKind 1)
(fun U103 3)
(fun isLNatKind 1)
(fun U104 3)
(fun U105 2)
(fun isNatural 1)
(fun U106 1)
(fun isLNat 1)
(fun U11 3)
(fun U12 3)
(fun U111 2)
(fun U112 1)
(fun U13 3)
(fun U121 2)
(fun U122 1)
(fun U14 3)
(fun U131 1)
(fun snd 1)
(fun splitAt 2)
(fun U141 1)
(fun U151 1)
(fun U161 1)
(fun U171 2)
(fun U172 1)
(fun U181 2)
(fun U182 2)
(fun U183 1)
(fun U191 2)
(fun U192 2)
(fun U193 1)
(fun U201 3)
(fun U202 3)
(fun U203 3)
(fun U204 3)
(fun U205 2)
(fun U206 1)
(fun U21 3)
(fun U22 3)
(fun U211 1)
(fun U23 3)
(fun U221 1)
(fun U24 2)
(fun U231 2)
(fun U232 1)
(fun U241 3)
(fun U242 3)
(fun U243 3)
(fun U244 3)
(fun U245 2)
(fun U246 1)
(fun U251 3)
(fun U252 3)
(fun U253 3)
(fun U254 3)
(fun U255 2)
(fun U256 1)
(fun U261 2)
(fun U262 1)
(fun U271 2)
(fun U272 1)
(fun U281 2)
(fun U282 2)
(fun cons 2)
(fun natsFrom 1)
(fun s 1)
(fun U291 3)
(fun U292 3)
(fun U293 3)
(fun U294 3)
(fun head 1)
(fun afterNth 2)
(fun U301 3)
(fun U302 2)
(fun U303 2)
(fun U304 2)
(fun U31 3)
(fun U32 3)
(fun U311 2)
(fun U312 2)
(fun pair 2)
(fun nil 0)
(fun U33 3)
(fun U321 4)
(fun U322 4)
(fun U323 4)
(fun U324 4)
(fun U325 4)
(fun U326 4)
(fun U327 2)
(fun U34 2)
(fun U331 3)
(fun U332 2)
(fun U333 2)
(fun U334 2)
(fun U341 3)
(fun U342 3)
(fun U343 3)
(fun U344 3)
(fun fst 1)
(fun U41 3)
(fun U42 3)
(fun U43 3)
(fun U44 3)
(fun U45 2)
(fun U46 1)
(fun U51 3)
(fun U52 3)
(fun U53 3)
(fun U54 3)
(fun U55 2)
(fun U56 1)
(fun U61 2)
(fun U62 2)
(fun isPLNatKind 1)
(fun U63 1)
(fun isPLNat 1)
(fun U71 2)
(fun U72 2)
(fun U73 1)
(fun U81 2)
(fun U82 2)
(fun U83 1)
(fun U91 2)
(fun U92 2)
(fun U93 1)
(fun tail 1)
(fun take 2)
(fun |0| 0)
(fun sel 2)
(fun proper 1)
(fun ok 1)
(fun top 1)
(rule (active (U101 tt V1 V2)) (mark (U102 (isNaturalKind V1) V1 V2)))
(rule (active (U102 tt V1 V2)) (mark (U103 (isLNatKind V2) V1 V2)))
(rule (active (U103 tt V1 V2)) (mark (U104 (isLNatKind V2) V1 V2)))
(rule (active (U104 tt V1 V2)) (mark (U105 (isNatural V1) V2)))
(rule (active (U105 tt V2)) (mark (U106 (isLNat V2))))
(rule (active (U106 tt)) (mark tt))
(rule (active (U11 tt N XS)) (mark (U12 (isNaturalKind N) N XS)))
(rule (active (U111 tt V2)) (mark (U112 (isLNatKind V2))))
(rule (active (U112 tt)) (mark tt))
(rule (active (U12 tt N XS)) (mark (U13 (isLNat XS) N XS)))
(rule (active (U121 tt V2)) (mark (U122 (isLNatKind V2))))
(rule (active (U122 tt)) (mark tt))
(rule (active (U13 tt N XS)) (mark (U14 (isLNatKind XS) N XS)))
(rule (active (U131 tt)) (mark tt))
(rule (active (U14 tt N XS)) (mark (snd (splitAt N XS))))
(rule (active (U141 tt)) (mark tt))
(rule (active (U151 tt)) (mark tt))
(rule (active (U161 tt)) (mark tt))
(rule (active (U171 tt V2)) (mark (U172 (isLNatKind V2))))
(rule (active (U172 tt)) (mark tt))
(rule (active (U181 tt V1)) (mark (U182 (isLNatKind V1) V1)))
(rule (active (U182 tt V1)) (mark (U183 (isLNat V1))))
(rule (active (U183 tt)) (mark tt))
(rule (active (U191 tt V1)) (mark (U192 (isNaturalKind V1) V1)))
(rule (active (U192 tt V1)) (mark (U193 (isNatural V1))))
(rule (active (U193 tt)) (mark tt))
(rule (active (U201 tt V1 V2)) (mark (U202 (isNaturalKind V1) V1 V2)))
(rule (active (U202 tt V1 V2)) (mark (U203 (isLNatKind V2) V1 V2)))
(rule (active (U203 tt V1 V2)) (mark (U204 (isLNatKind V2) V1 V2)))
(rule (active (U204 tt V1 V2)) (mark (U205 (isNatural V1) V2)))
(rule (active (U205 tt V2)) (mark (U206 (isLNat V2))))
(rule (active (U206 tt)) (mark tt))
(rule (active (U21 tt X Y)) (mark (U22 (isLNatKind X) X Y)))
(rule (active (U211 tt)) (mark tt))
(rule (active (U22 tt X Y)) (mark (U23 (isLNat Y) X Y)))
(rule (active (U221 tt)) (mark tt))
(rule (active (U23 tt X Y)) (mark (U24 (isLNatKind Y) X)))
(rule (active (U231 tt V2)) (mark (U232 (isLNatKind V2))))
(rule (active (U232 tt)) (mark tt))
(rule (active (U24 tt X)) (mark X))
(rule (active (U241 tt V1 V2)) (mark (U242 (isLNatKind V1) V1 V2)))
(rule (active (U242 tt V1 V2)) (mark (U243 (isLNatKind V2) V1 V2)))
(rule (active (U243 tt V1 V2)) (mark (U244 (isLNatKind V2) V1 V2)))
(rule (active (U244 tt V1 V2)) (mark (U245 (isLNat V1) V2)))
(rule (active (U245 tt V2)) (mark (U246 (isLNat V2))))
(rule (active (U246 tt)) (mark tt))
(rule (active (U251 tt V1 V2)) (mark (U252 (isNaturalKind V1) V1 V2)))
(rule (active (U252 tt V1 V2)) (mark (U253 (isLNatKind V2) V1 V2)))
(rule (active (U253 tt V1 V2)) (mark (U254 (isLNatKind V2) V1 V2)))
(rule (active (U254 tt V1 V2)) (mark (U255 (isNatural V1) V2)))
(rule (active (U255 tt V2)) (mark (U256 (isLNat V2))))
(rule (active (U256 tt)) (mark tt))
(rule (active (U261 tt V2)) (mark (U262 (isLNatKind V2))))
(rule (active (U262 tt)) (mark tt))
(rule (active (U271 tt V2)) (mark (U272 (isLNatKind V2))))
(rule (active (U272 tt)) (mark tt))
(rule (active (U281 tt N)) (mark (U282 (isNaturalKind N) N)))
(rule (active (U282 tt N)) (mark (cons N (natsFrom (s N)))))
(rule (active (U291 tt N XS)) (mark (U292 (isNaturalKind N) N XS)))
(rule (active (U292 tt N XS)) (mark (U293 (isLNat XS) N XS)))
(rule (active (U293 tt N XS)) (mark (U294 (isLNatKind XS) N XS)))
(rule (active (U294 tt N XS)) (mark (head (afterNth N XS))))
(rule (active (U301 tt X Y)) (mark (U302 (isLNatKind X) Y)))
(rule (active (U302 tt Y)) (mark (U303 (isLNat Y) Y)))
(rule (active (U303 tt Y)) (mark (U304 (isLNatKind Y) Y)))
(rule (active (U304 tt Y)) (mark Y))
(rule (active (U31 tt N XS)) (mark (U32 (isNaturalKind N) N XS)))
(rule (active (U311 tt XS)) (mark (U312 (isLNatKind XS) XS)))
(rule (active (U312 tt XS)) (mark (pair nil XS)))
(rule (active (U32 tt N XS)) (mark (U33 (isLNat XS) N XS)))
(rule (active (U321 tt N X XS)) (mark (U322 (isNaturalKind N) N X XS)))
(rule (active (U322 tt N X XS)) (mark (U323 (isNatural X) N X XS)))
(rule (active (U323 tt N X XS)) (mark (U324 (isNaturalKind X) N X XS)))
(rule (active (U324 tt N X XS)) (mark (U325 (isLNat XS) N X XS)))
(rule (active (U325 tt N X XS)) (mark (U326 (isLNatKind XS) N X XS)))
(rule (active (U326 tt N X XS)) (mark (U327 (splitAt N XS) X)))
(rule (active (U327 (pair YS ZS) X)) (mark (pair (cons X YS) ZS)))
(rule (active (U33 tt N XS)) (mark (U34 (isLNatKind XS) N)))
(rule (active (U331 tt N XS)) (mark (U332 (isNaturalKind N) XS)))
(rule (active (U332 tt XS)) (mark (U333 (isLNat XS) XS)))
(rule (active (U333 tt XS)) (mark (U334 (isLNatKind XS) XS)))
(rule (active (U334 tt XS)) (mark XS))
(rule (active (U34 tt N)) (mark N))
(rule (active (U341 tt N XS)) (mark (U342 (isNaturalKind N) N XS)))
(rule (active (U342 tt N XS)) (mark (U343 (isLNat XS) N XS)))
(rule (active (U343 tt N XS)) (mark (U344 (isLNatKind XS) N XS)))
(rule (active (U344 tt N XS)) (mark (fst (splitAt N XS))))
(rule (active (U41 tt V1 V2)) (mark (U42 (isNaturalKind V1) V1 V2)))
(rule (active (U42 tt V1 V2)) (mark (U43 (isLNatKind V2) V1 V2)))
(rule (active (U43 tt V1 V2)) (mark (U44 (isLNatKind V2) V1 V2)))
(rule (active (U44 tt V1 V2)) (mark (U45 (isNatural V1) V2)))
(rule (active (U45 tt V2)) (mark (U46 (isLNat V2))))
(rule (active (U46 tt)) (mark tt))
(rule (active (U51 tt V1 V2)) (mark (U52 (isNaturalKind V1) V1 V2)))
(rule (active (U52 tt V1 V2)) (mark (U53 (isLNatKind V2) V1 V2)))
(rule (active (U53 tt V1 V2)) (mark (U54 (isLNatKind V2) V1 V2)))
(rule (active (U54 tt V1 V2)) (mark (U55 (isNatural V1) V2)))
(rule (active (U55 tt V2)) (mark (U56 (isLNat V2))))
(rule (active (U56 tt)) (mark tt))
(rule (active (U61 tt V1)) (mark (U62 (isPLNatKind V1) V1)))
(rule (active (U62 tt V1)) (mark (U63 (isPLNat V1))))
(rule (active (U63 tt)) (mark tt))
(rule (active (U71 tt V1)) (mark (U72 (isNaturalKind V1) V1)))
(rule (active (U72 tt V1)) (mark (U73 (isNatural V1))))
(rule (active (U73 tt)) (mark tt))
(rule (active (U81 tt V1)) (mark (U82 (isPLNatKind V1) V1)))
(rule (active (U82 tt V1)) (mark (U83 (isPLNat V1))))
(rule (active (U83 tt)) (mark tt))
(rule (active (U91 tt V1)) (mark (U92 (isLNatKind V1) V1)))
(rule (active (U92 tt V1)) (mark (U93 (isLNat V1))))
(rule (active (U93 tt)) (mark tt))
(rule (active (afterNth N XS)) (mark (U11 (isNatural N) N XS)))
(rule (active (fst (pair X Y))) (mark (U21 (isLNat X) X Y)))
(rule (active (head (cons N XS))) (mark (U31 (isNatural N) N XS)))
(rule (active (isLNat nil)) (mark tt))
(rule (active (isLNat (afterNth V1 V2))) (mark (U41 (isNaturalKind V1) V1 V2)))
(rule (active (isLNat (cons V1 V2))) (mark (U51 (isNaturalKind V1) V1 V2)))
(rule (active (isLNat (fst V1))) (mark (U61 (isPLNatKind V1) V1)))
(rule (active (isLNat (natsFrom V1))) (mark (U71 (isNaturalKind V1) V1)))
(rule (active (isLNat (snd V1))) (mark (U81 (isPLNatKind V1) V1)))
(rule (active (isLNat (tail V1))) (mark (U91 (isLNatKind V1) V1)))
(rule (active (isLNat (take V1 V2))) (mark (U101 (isNaturalKind V1) V1 V2)))
(rule (active (isLNatKind nil)) (mark tt))
(rule (active (isLNatKind (afterNth V1 V2))) (mark (U111 (isNaturalKind V1) V2)))
(rule (active (isLNatKind (cons V1 V2))) (mark (U121 (isNaturalKind V1) V2)))
(rule (active (isLNatKind (fst V1))) (mark (U131 (isPLNatKind V1))))
(rule (active (isLNatKind (natsFrom V1))) (mark (U141 (isNaturalKind V1))))
(rule (active (isLNatKind (snd V1))) (mark (U151 (isPLNatKind V1))))
(rule (active (isLNatKind (tail V1))) (mark (U161 (isLNatKind V1))))
(rule (active (isLNatKind (take V1 V2))) (mark (U171 (isNaturalKind V1) V2)))
(rule (active (isNatural |0|)) (mark tt))
(rule (active (isNatural (head V1))) (mark (U181 (isLNatKind V1) V1)))
(rule (active (isNatural (s V1))) (mark (U191 (isNaturalKind V1) V1)))
(rule (active (isNatural (sel V1 V2))) (mark (U201 (isNaturalKind V1) V1 V2)))
(rule (active (isNaturalKind |0|)) (mark tt))
(rule (active (isNaturalKind (head V1))) (mark (U211 (isLNatKind V1))))
(rule (active (isNaturalKind (s V1))) (mark (U221 (isNaturalKind V1))))
(rule (active (isNaturalKind (sel V1 V2))) (mark (U231 (isNaturalKind V1) V2)))
(rule (active (isPLNat (pair V1 V2))) (mark (U241 (isLNatKind V1) V1 V2)))
(rule (active (isPLNat (splitAt V1 V2))) (mark (U251 (isNaturalKind V1) V1 V2)))
(rule (active (isPLNatKind (pair V1 V2))) (mark (U261 (isLNatKind V1) V2)))
(rule (active (isPLNatKind (splitAt V1 V2))) (mark (U271 (isNaturalKind V1) V2)))
(rule (active (natsFrom N)) (mark (U281 (isNatural N) N)))
(rule (active (sel N XS)) (mark (U291 (isNatural N) N XS)))
(rule (active (snd (pair X Y))) (mark (U301 (isLNat X) X Y)))
(rule (active (splitAt |0| XS)) (mark (U311 (isLNat XS) XS)))
(rule (active (splitAt (s N) (cons X XS))) (mark (U321 (isNatural N) N X XS)))
(rule (active (tail (cons N XS))) (mark (U331 (isNatural N) N XS)))
(rule (active (take N XS)) (mark (U341 (isNatural N) N XS)))
(rule (active (U101 X1 X2 X3)) (U101 (active X1) X2 X3))
(rule (active (U102 X1 X2 X3)) (U102 (active X1) X2 X3))
(rule (active (U103 X1 X2 X3)) (U103 (active X1) X2 X3))
(rule (active (U104 X1 X2 X3)) (U104 (active X1) X2 X3))
(rule (active (U105 X1 X2)) (U105 (active X1) X2))
(rule (active (U106 X)) (U106 (active X)))
(rule (active (U11 X1 X2 X3)) (U11 (active X1) X2 X3))
(rule (active (U12 X1 X2 X3)) (U12 (active X1) X2 X3))
(rule (active (U111 X1 X2)) (U111 (active X1) X2))
(rule (active (U112 X)) (U112 (active X)))
(rule (active (U13 X1 X2 X3)) (U13 (active X1) X2 X3))
(rule (active (U121 X1 X2)) (U121 (active X1) X2))
(rule (active (U122 X)) (U122 (active X)))
(rule (active (U14 X1 X2 X3)) (U14 (active X1) X2 X3))
(rule (active (U131 X)) (U131 (active X)))
(rule (active (snd X)) (snd (active X)))
(rule (active (splitAt X1 X2)) (splitAt (active X1) X2))
(rule (active (splitAt X1 X2)) (splitAt X1 (active X2)))
(rule (active (U141 X)) (U141 (active X)))
(rule (active (U151 X)) (U151 (active X)))
(rule (active (U161 X)) (U161 (active X)))
(rule (active (U171 X1 X2)) (U171 (active X1) X2))
(rule (active (U172 X)) (U172 (active X)))
(rule (active (U181 X1 X2)) (U181 (active X1) X2))
(rule (active (U182 X1 X2)) (U182 (active X1) X2))
(rule (active (U183 X)) (U183 (active X)))
(rule (active (U191 X1 X2)) (U191 (active X1) X2))
(rule (active (U192 X1 X2)) (U192 (active X1) X2))
(rule (active (U193 X)) (U193 (active X)))
(rule (active (U201 X1 X2 X3)) (U201 (active X1) X2 X3))
(rule (active (U202 X1 X2 X3)) (U202 (active X1) X2 X3))
(rule (active (U203 X1 X2 X3)) (U203 (active X1) X2 X3))
(rule (active (U204 X1 X2 X3)) (U204 (active X1) X2 X3))
(rule (active (U205 X1 X2)) (U205 (active X1) X2))
(rule (active (U206 X)) (U206 (active X)))
(rule (active (U21 X1 X2 X3)) (U21 (active X1) X2 X3))
(rule (active (U22 X1 X2 X3)) (U22 (active X1) X2 X3))
(rule (active (U211 X)) (U211 (active X)))
(rule (active (U23 X1 X2 X3)) (U23 (active X1) X2 X3))
(rule (active (U221 X)) (U221 (active X)))
(rule (active (U24 X1 X2)) (U24 (active X1) X2))
(rule (active (U231 X1 X2)) (U231 (active X1) X2))
(rule (active (U232 X)) (U232 (active X)))
(rule (active (U241 X1 X2 X3)) (U241 (active X1) X2 X3))
(rule (active (U242 X1 X2 X3)) (U242 (active X1) X2 X3))
(rule (active (U243 X1 X2 X3)) (U243 (active X1) X2 X3))
(rule (active (U244 X1 X2 X3)) (U244 (active X1) X2 X3))
(rule (active (U245 X1 X2)) (U245 (active X1) X2))
(rule (active (U246 X)) (U246 (active X)))
(rule (active (U251 X1 X2 X3)) (U251 (active X1) X2 X3))
(rule (active (U252 X1 X2 X3)) (U252 (active X1) X2 X3))
(rule (active (U253 X1 X2 X3)) (U253 (active X1) X2 X3))
(rule (active (U254 X1 X2 X3)) (U254 (active X1) X2 X3))
(rule (active (U255 X1 X2)) (U255 (active X1) X2))
(rule (active (U256 X)) (U256 (active X)))
(rule (active (U261 X1 X2)) (U261 (active X1) X2))
(rule (active (U262 X)) (U262 (active X)))
(rule (active (U271 X1 X2)) (U271 (active X1) X2))
(rule (active (U272 X)) (U272 (active X)))
(rule (active (U281 X1 X2)) (U281 (active X1) X2))
(rule (active (U282 X1 X2)) (U282 (active X1) X2))
(rule (active (cons X1 X2)) (cons (active X1) X2))
(rule (active (natsFrom X)) (natsFrom (active X)))
(rule (active (s X)) (s (active X)))
(rule (active (U291 X1 X2 X3)) (U291 (active X1) X2 X3))
(rule (active (U292 X1 X2 X3)) (U292 (active X1) X2 X3))
(rule (active (U293 X1 X2 X3)) (U293 (active X1) X2 X3))
(rule (active (U294 X1 X2 X3)) (U294 (active X1) X2 X3))
(rule (active (head X)) (head (active X)))
(rule (active (afterNth X1 X2)) (afterNth (active X1) X2))
(rule (active (afterNth X1 X2)) (afterNth X1 (active X2)))
(rule (active (U301 X1 X2 X3)) (U301 (active X1) X2 X3))
(rule (active (U302 X1 X2)) (U302 (active X1) X2))
(rule (active (U303 X1 X2)) (U303 (active X1) X2))
(rule (active (U304 X1 X2)) (U304 (active X1) X2))
(rule (active (U31 X1 X2 X3)) (U31 (active X1) X2 X3))
(rule (active (U32 X1 X2 X3)) (U32 (active X1) X2 X3))
(rule (active (U311 X1 X2)) (U311 (active X1) X2))
(rule (active (U312 X1 X2)) (U312 (active X1) X2))
(rule (active (pair X1 X2)) (pair (active X1) X2))
(rule (active (pair X1 X2)) (pair X1 (active X2)))
(rule (active (U33 X1 X2 X3)) (U33 (active X1) X2 X3))
(rule (active (U321 X1 X2 X3 X4)) (U321 (active X1) X2 X3 X4))
(rule (active (U322 X1 X2 X3 X4)) (U322 (active X1) X2 X3 X4))
(rule (active (U323 X1 X2 X3 X4)) (U323 (active X1) X2 X3 X4))
(rule (active (U324 X1 X2 X3 X4)) (U324 (active X1) X2 X3 X4))
(rule (active (U325 X1 X2 X3 X4)) (U325 (active X1) X2 X3 X4))
(rule (active (U326 X1 X2 X3 X4)) (U326 (active X1) X2 X3 X4))
(rule (active (U327 X1 X2)) (U327 (active X1) X2))
(rule (active (U34 X1 X2)) (U34 (active X1) X2))
(rule (active (U331 X1 X2 X3)) (U331 (active X1) X2 X3))
(rule (active (U332 X1 X2)) (U332 (active X1) X2))
(rule (active (U333 X1 X2)) (U333 (active X1) X2))
(rule (active (U334 X1 X2)) (U334 (active X1) X2))
(rule (active (U341 X1 X2 X3)) (U341 (active X1) X2 X3))
(rule (active (U342 X1 X2 X3)) (U342 (active X1) X2 X3))
(rule (active (U343 X1 X2 X3)) (U343 (active X1) X2 X3))
(rule (active (U344 X1 X2 X3)) (U344 (active X1) X2 X3))
(rule (active (fst X)) (fst (active X)))
(rule (active (U41 X1 X2 X3)) (U41 (active X1) X2 X3))
(rule (active (U42 X1 X2 X3)) (U42 (active X1) X2 X3))
(rule (active (U43 X1 X2 X3)) (U43 (active X1) X2 X3))
(rule (active (U44 X1 X2 X3)) (U44 (active X1) X2 X3))
(rule (active (U45 X1 X2)) (U45 (active X1) X2))
(rule (active (U46 X)) (U46 (active X)))
(rule (active (U51 X1 X2 X3)) (U51 (active X1) X2 X3))
(rule (active (U52 X1 X2 X3)) (U52 (active X1) X2 X3))
(rule (active (U53 X1 X2 X3)) (U53 (active X1) X2 X3))
(rule (active (U54 X1 X2 X3)) (U54 (active X1) X2 X3))
(rule (active (U55 X1 X2)) (U55 (active X1) X2))
(rule (active (U56 X)) (U56 (active X)))
(rule (active (U61 X1 X2)) (U61 (active X1) X2))
(rule (active (U62 X1 X2)) (U62 (active X1) X2))
(rule (active (U63 X)) (U63 (active X)))
(rule (active (U71 X1 X2)) (U71 (active X1) X2))
(rule (active (U72 X1 X2)) (U72 (active X1) X2))
(rule (active (U73 X)) (U73 (active X)))
(rule (active (U81 X1 X2)) (U81 (active X1) X2))
(rule (active (U82 X1 X2)) (U82 (active X1) X2))
(rule (active (U83 X)) (U83 (active X)))
(rule (active (U91 X1 X2)) (U91 (active X1) X2))
(rule (active (U92 X1 X2)) (U92 (active X1) X2))
(rule (active (U93 X)) (U93 (active X)))
(rule (active (tail X)) (tail (active X)))
(rule (active (take X1 X2)) (take (active X1) X2))
(rule (active (take X1 X2)) (take X1 (active X2)))
(rule (active (sel X1 X2)) (sel (active X1) X2))
(rule (active (sel X1 X2)) (sel X1 (active X2)))
(rule (U101 (mark X1) X2 X3) (mark (U101 X1 X2 X3)))
(rule (U102 (mark X1) X2 X3) (mark (U102 X1 X2 X3)))
(rule (U103 (mark X1) X2 X3) (mark (U103 X1 X2 X3)))
(rule (U104 (mark X1) X2 X3) (mark (U104 X1 X2 X3)))
(rule (U105 (mark X1) X2) (mark (U105 X1 X2)))
(rule (U106 (mark X)) (mark (U106 X)))
(rule (U11 (mark X1) X2 X3) (mark (U11 X1 X2 X3)))
(rule (U12 (mark X1) X2 X3) (mark (U12 X1 X2 X3)))
(rule (U111 (mark X1) X2) (mark (U111 X1 X2)))
(rule (U112 (mark X)) (mark (U112 X)))
(rule (U13 (mark X1) X2 X3) (mark (U13 X1 X2 X3)))
(rule (U121 (mark X1) X2) (mark (U121 X1 X2)))
(rule (U122 (mark X)) (mark (U122 X)))
(rule (U14 (mark X1) X2 X3) (mark (U14 X1 X2 X3)))
(rule (U131 (mark X)) (mark (U131 X)))
(rule (snd (mark X)) (mark (snd X)))
(rule (splitAt (mark X1) X2) (mark (splitAt X1 X2)))
(rule (splitAt X1 (mark X2)) (mark (splitAt X1 X2)))
(rule (U141 (mark X)) (mark (U141 X)))
(rule (U151 (mark X)) (mark (U151 X)))
(rule (U161 (mark X)) (mark (U161 X)))
(rule (U171 (mark X1) X2) (mark (U171 X1 X2)))
(rule (U172 (mark X)) (mark (U172 X)))
(rule (U181 (mark X1) X2) (mark (U181 X1 X2)))
(rule (U182 (mark X1) X2) (mark (U182 X1 X2)))
(rule (U183 (mark X)) (mark (U183 X)))
(rule (U191 (mark X1) X2) (mark (U191 X1 X2)))
(rule (U192 (mark X1) X2) (mark (U192 X1 X2)))
(rule (U193 (mark X)) (mark (U193 X)))
(rule (U201 (mark X1) X2 X3) (mark (U201 X1 X2 X3)))
(rule (U202 (mark X1) X2 X3) (mark (U202 X1 X2 X3)))
(rule (U203 (mark X1) X2 X3) (mark (U203 X1 X2 X3)))
(rule (U204 (mark X1) X2 X3) (mark (U204 X1 X2 X3)))
(rule (U205 (mark X1) X2) (mark (U205 X1 X2)))
(rule (U206 (mark X)) (mark (U206 X)))
(rule (U21 (mark X1) X2 X3) (mark (U21 X1 X2 X3)))
(rule (U22 (mark X1) X2 X3) (mark (U22 X1 X2 X3)))
(rule (U211 (mark X)) (mark (U211 X)))
(rule (U23 (mark X1) X2 X3) (mark (U23 X1 X2 X3)))
(rule (U221 (mark X)) (mark (U221 X)))
(rule (U24 (mark X1) X2) (mark (U24 X1 X2)))
(rule (U231 (mark X1) X2) (mark (U231 X1 X2)))
(rule (U232 (mark X)) (mark (U232 X)))
(rule (U241 (mark X1) X2 X3) (mark (U241 X1 X2 X3)))
(rule (U242 (mark X1) X2 X3) (mark (U242 X1 X2 X3)))
(rule (U243 (mark X1) X2 X3) (mark (U243 X1 X2 X3)))
(rule (U244 (mark X1) X2 X3) (mark (U244 X1 X2 X3)))
(rule (U245 (mark X1) X2) (mark (U245 X1 X2)))
(rule (U246 (mark X)) (mark (U246 X)))
(rule (U251 (mark X1) X2 X3) (mark (U251 X1 X2 X3)))
(rule (U252 (mark X1) X2 X3) (mark (U252 X1 X2 X3)))
(rule (U253 (mark X1) X2 X3) (mark (U253 X1 X2 X3)))
(rule (U254 (mark X1) X2 X3) (mark (U254 X1 X2 X3)))
(rule (U255 (mark X1) X2) (mark (U255 X1 X2)))
(rule (U256 (mark X)) (mark (U256 X)))
(rule (U261 (mark X1) X2) (mark (U261 X1 X2)))
(rule (U262 (mark X)) (mark (U262 X)))
(rule (U271 (mark X1) X2) (mark (U271 X1 X2)))
(rule (U272 (mark X)) (mark (U272 X)))
(rule (U281 (mark X1) X2) (mark (U281 X1 X2)))
(rule (U282 (mark X1) X2) (mark (U282 X1 X2)))
(rule (cons (mark X1) X2) (mark (cons X1 X2)))
(rule (natsFrom (mark X)) (mark (natsFrom X)))
(rule (s (mark X)) (mark (s X)))
(rule (U291 (mark X1) X2 X3) (mark (U291 X1 X2 X3)))
(rule (U292 (mark X1) X2 X3) (mark (U292 X1 X2 X3)))
(rule (U293 (mark X1) X2 X3) (mark (U293 X1 X2 X3)))
(rule (U294 (mark X1) X2 X3) (mark (U294 X1 X2 X3)))
(rule (head (mark X)) (mark (head X)))
(rule (afterNth (mark X1) X2) (mark (afterNth X1 X2)))
(rule (afterNth X1 (mark X2)) (mark (afterNth X1 X2)))
(rule (U301 (mark X1) X2 X3) (mark (U301 X1 X2 X3)))
(rule (U302 (mark X1) X2) (mark (U302 X1 X2)))
(rule (U303 (mark X1) X2) (mark (U303 X1 X2)))
(rule (U304 (mark X1) X2) (mark (U304 X1 X2)))
(rule (U31 (mark X1) X2 X3) (mark (U31 X1 X2 X3)))
(rule (U32 (mark X1) X2 X3) (mark (U32 X1 X2 X3)))
(rule (U311 (mark X1) X2) (mark (U311 X1 X2)))
(rule (U312 (mark X1) X2) (mark (U312 X1 X2)))
(rule (pair (mark X1) X2) (mark (pair X1 X2)))
(rule (pair X1 (mark X2)) (mark (pair X1 X2)))
(rule (U33 (mark X1) X2 X3) (mark (U33 X1 X2 X3)))
(rule (U321 (mark X1) X2 X3 X4) (mark (U321 X1 X2 X3 X4)))
(rule (U322 (mark X1) X2 X3 X4) (mark (U322 X1 X2 X3 X4)))
(rule (U323 (mark X1) X2 X3 X4) (mark (U323 X1 X2 X3 X4)))
(rule (U324 (mark X1) X2 X3 X4) (mark (U324 X1 X2 X3 X4)))
(rule (U325 (mark X1) X2 X3 X4) (mark (U325 X1 X2 X3 X4)))
(rule (U326 (mark X1) X2 X3 X4) (mark (U326 X1 X2 X3 X4)))
(rule (U327 (mark X1) X2) (mark (U327 X1 X2)))
(rule (U34 (mark X1) X2) (mark (U34 X1 X2)))
(rule (U331 (mark X1) X2 X3) (mark (U331 X1 X2 X3)))
(rule (U332 (mark X1) X2) (mark (U332 X1 X2)))
(rule (U333 (mark X1) X2) (mark (U333 X1 X2)))
(rule (U334 (mark X1) X2) (mark (U334 X1 X2)))
(rule (U341 (mark X1) X2 X3) (mark (U341 X1 X2 X3)))
(rule (U342 (mark X1) X2 X3) (mark (U342 X1 X2 X3)))
(rule (U343 (mark X1) X2 X3) (mark (U343 X1 X2 X3)))
(rule (U344 (mark X1) X2 X3) (mark (U344 X1 X2 X3)))
(rule (fst (mark X)) (mark (fst X)))
(rule (U41 (mark X1) X2 X3) (mark (U41 X1 X2 X3)))
(rule (U42 (mark X1) X2 X3) (mark (U42 X1 X2 X3)))
(rule (U43 (mark X1) X2 X3) (mark (U43 X1 X2 X3)))
(rule (U44 (mark X1) X2 X3) (mark (U44 X1 X2 X3)))
(rule (U45 (mark X1) X2) (mark (U45 X1 X2)))
(rule (U46 (mark X)) (mark (U46 X)))
(rule (U51 (mark X1) X2 X3) (mark (U51 X1 X2 X3)))
(rule (U52 (mark X1) X2 X3) (mark (U52 X1 X2 X3)))
(rule (U53 (mark X1) X2 X3) (mark (U53 X1 X2 X3)))
(rule (U54 (mark X1) X2 X3) (mark (U54 X1 X2 X3)))
(rule (U55 (mark X1) X2) (mark (U55 X1 X2)))
(rule (U56 (mark X)) (mark (U56 X)))
(rule (U61 (mark X1) X2) (mark (U61 X1 X2)))
(rule (U62 (mark X1) X2) (mark (U62 X1 X2)))
(rule (U63 (mark X)) (mark (U63 X)))
(rule (U71 (mark X1) X2) (mark (U71 X1 X2)))
(rule (U72 (mark X1) X2) (mark (U72 X1 X2)))
(rule (U73 (mark X)) (mark (U73 X)))
(rule (U81 (mark X1) X2) (mark (U81 X1 X2)))
(rule (U82 (mark X1) X2) (mark (U82 X1 X2)))
(rule (U83 (mark X)) (mark (U83 X)))
(rule (U91 (mark X1) X2) (mark (U91 X1 X2)))
(rule (U92 (mark X1) X2) (mark (U92 X1 X2)))
(rule (U93 (mark X)) (mark (U93 X)))
(rule (tail (mark X)) (mark (tail X)))
(rule (take (mark X1) X2) (mark (take X1 X2)))
(rule (take X1 (mark X2)) (mark (take X1 X2)))
(rule (sel (mark X1) X2) (mark (sel X1 X2)))
(rule (sel X1 (mark X2)) (mark (sel X1 X2)))
(rule (proper (U101 X1 X2 X3)) (U101 (proper X1) (proper X2) (proper X3)))
(rule (proper tt) (ok tt))
(rule (proper (U102 X1 X2 X3)) (U102 (proper X1) (proper X2) (proper X3)))
(rule (proper (isNaturalKind X)) (isNaturalKind (proper X)))
(rule (proper (U103 X1 X2 X3)) (U103 (proper X1) (proper X2) (proper X3)))
(rule (proper (isLNatKind X)) (isLNatKind (proper X)))
(rule (proper (U104 X1 X2 X3)) (U104 (proper X1) (proper X2) (proper X3)))
(rule (proper (U105 X1 X2)) (U105 (proper X1) (proper X2)))
(rule (proper (isNatural X)) (isNatural (proper X)))
(rule (proper (U106 X)) (U106 (proper X)))
(rule (proper (isLNat X)) (isLNat (proper X)))
(rule (proper (U11 X1 X2 X3)) (U11 (proper X1) (proper X2) (proper X3)))
(rule (proper (U12 X1 X2 X3)) (U12 (proper X1) (proper X2) (proper X3)))
(rule (proper (U111 X1 X2)) (U111 (proper X1) (proper X2)))
(rule (proper (U112 X)) (U112 (proper X)))
(rule (proper (U13 X1 X2 X3)) (U13 (proper X1) (proper X2) (proper X3)))
(rule (proper (U121 X1 X2)) (U121 (proper X1) (proper X2)))
(rule (proper (U122 X)) (U122 (proper X)))
(rule (proper (U14 X1 X2 X3)) (U14 (proper X1) (proper X2) (proper X3)))
(rule (proper (U131 X)) (U131 (proper X)))
(rule (proper (snd X)) (snd (proper X)))
(rule (proper (splitAt X1 X2)) (splitAt (proper X1) (proper X2)))
(rule (proper (U141 X)) (U141 (proper X)))
(rule (proper (U151 X)) (U151 (proper X)))
(rule (proper (U161 X)) (U161 (proper X)))
(rule (proper (U171 X1 X2)) (U171 (proper X1) (proper X2)))
(rule (proper (U172 X)) (U172 (proper X)))
(rule (proper (U181 X1 X2)) (U181 (proper X1) (proper X2)))
(rule (proper (U182 X1 X2)) (U182 (proper X1) (proper X2)))
(rule (proper (U183 X)) (U183 (proper X)))
(rule (proper (U191 X1 X2)) (U191 (proper X1) (proper X2)))
(rule (proper (U192 X1 X2)) (U192 (proper X1) (proper X2)))
(rule (proper (U193 X)) (U193 (proper X)))
(rule (proper (U201 X1 X2 X3)) (U201 (proper X1) (proper X2) (proper X3)))
(rule (proper (U202 X1 X2 X3)) (U202 (proper X1) (proper X2) (proper X3)))
(rule (proper (U203 X1 X2 X3)) (U203 (proper X1) (proper X2) (proper X3)))
(rule (proper (U204 X1 X2 X3)) (U204 (proper X1) (proper X2) (proper X3)))
(rule (proper (U205 X1 X2)) (U205 (proper X1) (proper X2)))
(rule (proper (U206 X)) (U206 (proper X)))
(rule (proper (U21 X1 X2 X3)) (U21 (proper X1) (proper X2) (proper X3)))
(rule (proper (U22 X1 X2 X3)) (U22 (proper X1) (proper X2) (proper X3)))
(rule (proper (U211 X)) (U211 (proper X)))
(rule (proper (U23 X1 X2 X3)) (U23 (proper X1) (proper X2) (proper X3)))
(rule (proper (U221 X)) (U221 (proper X)))
(rule (proper (U24 X1 X2)) (U24 (proper X1) (proper X2)))
(rule (proper (U231 X1 X2)) (U231 (proper X1) (proper X2)))
(rule (proper (U232 X)) (U232 (proper X)))
(rule (proper (U241 X1 X2 X3)) (U241 (proper X1) (proper X2) (proper X3)))
(rule (proper (U242 X1 X2 X3)) (U242 (proper X1) (proper X2) (proper X3)))
(rule (proper (U243 X1 X2 X3)) (U243 (proper X1) (proper X2) (proper X3)))
(rule (proper (U244 X1 X2 X3)) (U244 (proper X1) (proper X2) (proper X3)))
(rule (proper (U245 X1 X2)) (U245 (proper X1) (proper X2)))
(rule (proper (U246 X)) (U246 (proper X)))
(rule (proper (U251 X1 X2 X3)) (U251 (proper X1) (proper X2) (proper X3)))
(rule (proper (U252 X1 X2 X3)) (U252 (proper X1) (proper X2) (proper X3)))
(rule (proper (U253 X1 X2 X3)) (U253 (proper X1) (proper X2) (proper X3)))
(rule (proper (U254 X1 X2 X3)) (U254 (proper X1) (proper X2) (proper X3)))
(rule (proper (U255 X1 X2)) (U255 (proper X1) (proper X2)))
(rule (proper (U256 X)) (U256 (proper X)))
(rule (proper (U261 X1 X2)) (U261 (proper X1) (proper X2)))
(rule (proper (U262 X)) (U262 (proper X)))
(rule (proper (U271 X1 X2)) (U271 (proper X1) (proper X2)))
(rule (proper (U272 X)) (U272 (proper X)))
(rule (proper (U281 X1 X2)) (U281 (proper X1) (proper X2)))
(rule (proper (U282 X1 X2)) (U282 (proper X1) (proper X2)))
(rule (proper (cons X1 X2)) (cons (proper X1) (proper X2)))
(rule (proper (natsFrom X)) (natsFrom (proper X)))
(rule (proper (s X)) (s (proper X)))
(rule (proper (U291 X1 X2 X3)) (U291 (proper X1) (proper X2) (proper X3)))
(rule (proper (U292 X1 X2 X3)) (U292 (proper X1) (proper X2) (proper X3)))
(rule (proper (U293 X1 X2 X3)) (U293 (proper X1) (proper X2) (proper X3)))
(rule (proper (U294 X1 X2 X3)) (U294 (proper X1) (proper X2) (proper X3)))
(rule (proper (head X)) (head (proper X)))
(rule (proper (afterNth X1 X2)) (afterNth (proper X1) (proper X2)))
(rule (proper (U301 X1 X2 X3)) (U301 (proper X1) (proper X2) (proper X3)))
(rule (proper (U302 X1 X2)) (U302 (proper X1) (proper X2)))
(rule (proper (U303 X1 X2)) (U303 (proper X1) (proper X2)))
(rule (proper (U304 X1 X2)) (U304 (proper X1) (proper X2)))
(rule (proper (U31 X1 X2 X3)) (U31 (proper X1) (proper X2) (proper X3)))
(rule (proper (U32 X1 X2 X3)) (U32 (proper X1) (proper X2) (proper X3)))
(rule (proper (U311 X1 X2)) (U311 (proper X1) (proper X2)))
(rule (proper (U312 X1 X2)) (U312 (proper X1) (proper X2)))
(rule (proper (pair X1 X2)) (pair (proper X1) (proper X2)))
(rule (proper nil) (ok nil))
(rule (proper (U33 X1 X2 X3)) (U33 (proper X1) (proper X2) (proper X3)))
(rule (proper (U321 X1 X2 X3 X4)) (U321 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U322 X1 X2 X3 X4)) (U322 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U323 X1 X2 X3 X4)) (U323 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U324 X1 X2 X3 X4)) (U324 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U325 X1 X2 X3 X4)) (U325 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U326 X1 X2 X3 X4)) (U326 (proper X1) (proper X2) (proper X3) (proper X4)))
(rule (proper (U327 X1 X2)) (U327 (proper X1) (proper X2)))
(rule (proper (U34 X1 X2)) (U34 (proper X1) (proper X2)))
(rule (proper (U331 X1 X2 X3)) (U331 (proper X1) (proper X2) (proper X3)))
(rule (proper (U332 X1 X2)) (U332 (proper X1) (proper X2)))
(rule (proper (U333 X1 X2)) (U333 (proper X1) (proper X2)))
(rule (proper (U334 X1 X2)) (U334 (proper X1) (proper X2)))
(rule (proper (U341 X1 X2 X3)) (U341 (proper X1) (proper X2) (proper X3)))
(rule (proper (U342 X1 X2 X3)) (U342 (proper X1) (proper X2) (proper X3)))
(rule (proper (U343 X1 X2 X3)) (U343 (proper X1) (proper X2) (proper X3)))
(rule (proper (U344 X1 X2 X3)) (U344 (proper X1) (proper X2) (proper X3)))
(rule (proper (fst X)) (fst (proper X)))
(rule (proper (U41 X1 X2 X3)) (U41 (proper X1) (proper X2) (proper X3)))
(rule (proper (U42 X1 X2 X3)) (U42 (proper X1) (proper X2) (proper X3)))
(rule (proper (U43 X1 X2 X3)) (U43 (proper X1) (proper X2) (proper X3)))
(rule (proper (U44 X1 X2 X3)) (U44 (proper X1) (proper X2) (proper X3)))
(rule (proper (U45 X1 X2)) (U45 (proper X1) (proper X2)))
(rule (proper (U46 X)) (U46 (proper X)))
(rule (proper (U51 X1 X2 X3)) (U51 (proper X1) (proper X2) (proper X3)))
(rule (proper (U52 X1 X2 X3)) (U52 (proper X1) (proper X2) (proper X3)))
(rule (proper (U53 X1 X2 X3)) (U53 (proper X1) (proper X2) (proper X3)))
(rule (proper (U54 X1 X2 X3)) (U54 (proper X1) (proper X2) (proper X3)))
(rule (proper (U55 X1 X2)) (U55 (proper X1) (proper X2)))
(rule (proper (U56 X)) (U56 (proper X)))
(rule (proper (U61 X1 X2)) (U61 (proper X1) (proper X2)))
(rule (proper (U62 X1 X2)) (U62 (proper X1) (proper X2)))
(rule (proper (isPLNatKind X)) (isPLNatKind (proper X)))
(rule (proper (U63 X)) (U63 (proper X)))
(rule (proper (isPLNat X)) (isPLNat (proper X)))
(rule (proper (U71 X1 X2)) (U71 (proper X1) (proper X2)))
(rule (proper (U72 X1 X2)) (U72 (proper X1) (proper X2)))
(rule (proper (U73 X)) (U73 (proper X)))
(rule (proper (U81 X1 X2)) (U81 (proper X1) (proper X2)))
(rule (proper (U82 X1 X2)) (U82 (proper X1) (proper X2)))
(rule (proper (U83 X)) (U83 (proper X)))
(rule (proper (U91 X1 X2)) (U91 (proper X1) (proper X2)))
(rule (proper (U92 X1 X2)) (U92 (proper X1) (proper X2)))
(rule (proper (U93 X)) (U93 (proper X)))
(rule (proper (tail X)) (tail (proper X)))
(rule (proper (take X1 X2)) (take (proper X1) (proper X2)))
(rule (proper |0|) (ok |0|))
(rule (proper (sel X1 X2)) (sel (proper X1) (proper X2)))
(rule (U101 (ok X1) (ok X2) (ok X3)) (ok (U101 X1 X2 X3)))
(rule (U102 (ok X1) (ok X2) (ok X3)) (ok (U102 X1 X2 X3)))
(rule (isNaturalKind (ok X)) (ok (isNaturalKind X)))
(rule (U103 (ok X1) (ok X2) (ok X3)) (ok (U103 X1 X2 X3)))
(rule (isLNatKind (ok X)) (ok (isLNatKind X)))
(rule (U104 (ok X1) (ok X2) (ok X3)) (ok (U104 X1 X2 X3)))
(rule (U105 (ok X1) (ok X2)) (ok (U105 X1 X2)))
(rule (isNatural (ok X)) (ok (isNatural X)))
(rule (U106 (ok X)) (ok (U106 X)))
(rule (isLNat (ok X)) (ok (isLNat X)))
(rule (U11 (ok X1) (ok X2) (ok X3)) (ok (U11 X1 X2 X3)))
(rule (U12 (ok X1) (ok X2) (ok X3)) (ok (U12 X1 X2 X3)))
(rule (U111 (ok X1) (ok X2)) (ok (U111 X1 X2)))
(rule (U112 (ok X)) (ok (U112 X)))
(rule (U13 (ok X1) (ok X2) (ok X3)) (ok (U13 X1 X2 X3)))
(rule (U121 (ok X1) (ok X2)) (ok (U121 X1 X2)))
(rule (U122 (ok X)) (ok (U122 X)))
(rule (U14 (ok X1) (ok X2) (ok X3)) (ok (U14 X1 X2 X3)))
(rule (U131 (ok X)) (ok (U131 X)))
(rule (snd (ok X)) (ok (snd X)))
(rule (splitAt (ok X1) (ok X2)) (ok (splitAt X1 X2)))
(rule (U141 (ok X)) (ok (U141 X)))
(rule (U151 (ok X)) (ok (U151 X)))
(rule (U161 (ok X)) (ok (U161 X)))
(rule (U171 (ok X1) (ok X2)) (ok (U171 X1 X2)))
(rule (U172 (ok X)) (ok (U172 X)))
(rule (U181 (ok X1) (ok X2)) (ok (U181 X1 X2)))
(rule (U182 (ok X1) (ok X2)) (ok (U182 X1 X2)))
(rule (U183 (ok X)) (ok (U183 X)))
(rule (U191 (ok X1) (ok X2)) (ok (U191 X1 X2)))
(rule (U192 (ok X1) (ok X2)) (ok (U192 X1 X2)))
(rule (U193 (ok X)) (ok (U193 X)))
(rule (U201 (ok X1) (ok X2) (ok X3)) (ok (U201 X1 X2 X3)))
(rule (U202 (ok X1) (ok X2) (ok X3)) (ok (U202 X1 X2 X3)))
(rule (U203 (ok X1) (ok X2) (ok X3)) (ok (U203 X1 X2 X3)))
(rule (U204 (ok X1) (ok X2) (ok X3)) (ok (U204 X1 X2 X3)))
(rule (U205 (ok X1) (ok X2)) (ok (U205 X1 X2)))
(rule (U206 (ok X)) (ok (U206 X)))
(rule (U21 (ok X1) (ok X2) (ok X3)) (ok (U21 X1 X2 X3)))
(rule (U22 (ok X1) (ok X2) (ok X3)) (ok (U22 X1 X2 X3)))
(rule (U211 (ok X)) (ok (U211 X)))
(rule (U23 (ok X1) (ok X2) (ok X3)) (ok (U23 X1 X2 X3)))
(rule (U221 (ok X)) (ok (U221 X)))
(rule (U24 (ok X1) (ok X2)) (ok (U24 X1 X2)))
(rule (U231 (ok X1) (ok X2)) (ok (U231 X1 X2)))
(rule (U232 (ok X)) (ok (U232 X)))
(rule (U241 (ok X1) (ok X2) (ok X3)) (ok (U241 X1 X2 X3)))
(rule (U242 (ok X1) (ok X2) (ok X3)) (ok (U242 X1 X2 X3)))
(rule (U243 (ok X1) (ok X2) (ok X3)) (ok (U243 X1 X2 X3)))
(rule (U244 (ok X1) (ok X2) (ok X3)) (ok (U244 X1 X2 X3)))
(rule (U245 (ok X1) (ok X2)) (ok (U245 X1 X2)))
(rule (U246 (ok X)) (ok (U246 X)))
(rule (U251 (ok X1) (ok X2) (ok X3)) (ok (U251 X1 X2 X3)))
(rule (U252 (ok X1) (ok X2) (ok X3)) (ok (U252 X1 X2 X3)))
(rule (U253 (ok X1) (ok X2) (ok X3)) (ok (U253 X1 X2 X3)))
(rule (U254 (ok X1) (ok X2) (ok X3)) (ok (U254 X1 X2 X3)))
(rule (U255 (ok X1) (ok X2)) (ok (U255 X1 X2)))
(rule (U256 (ok X)) (ok (U256 X)))
(rule (U261 (ok X1) (ok X2)) (ok (U261 X1 X2)))
(rule (U262 (ok X)) (ok (U262 X)))
(rule (U271 (ok X1) (ok X2)) (ok (U271 X1 X2)))
(rule (U272 (ok X)) (ok (U272 X)))
(rule (U281 (ok X1) (ok X2)) (ok (U281 X1 X2)))
(rule (U282 (ok X1) (ok X2)) (ok (U282 X1 X2)))
(rule (cons (ok X1) (ok X2)) (ok (cons X1 X2)))
(rule (natsFrom (ok X)) (ok (natsFrom X)))
(rule (s (ok X)) (ok (s X)))
(rule (U291 (ok X1) (ok X2) (ok X3)) (ok (U291 X1 X2 X3)))
(rule (U292 (ok X1) (ok X2) (ok X3)) (ok (U292 X1 X2 X3)))
(rule (U293 (ok X1) (ok X2) (ok X3)) (ok (U293 X1 X2 X3)))
(rule (U294 (ok X1) (ok X2) (ok X3)) (ok (U294 X1 X2 X3)))
(rule (head (ok X)) (ok (head X)))
(rule (afterNth (ok X1) (ok X2)) (ok (afterNth X1 X2)))
(rule (U301 (ok X1) (ok X2) (ok X3)) (ok (U301 X1 X2 X3)))
(rule (U302 (ok X1) (ok X2)) (ok (U302 X1 X2)))
(rule (U303 (ok X1) (ok X2)) (ok (U303 X1 X2)))
(rule (U304 (ok X1) (ok X2)) (ok (U304 X1 X2)))
(rule (U31 (ok X1) (ok X2) (ok X3)) (ok (U31 X1 X2 X3)))
(rule (U32 (ok X1) (ok X2) (ok X3)) (ok (U32 X1 X2 X3)))
(rule (U311 (ok X1) (ok X2)) (ok (U311 X1 X2)))
(rule (U312 (ok X1) (ok X2)) (ok (U312 X1 X2)))
(rule (pair (ok X1) (ok X2)) (ok (pair X1 X2)))
(rule (U33 (ok X1) (ok X2) (ok X3)) (ok (U33 X1 X2 X3)))
(rule (U321 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U321 X1 X2 X3 X4)))
(rule (U322 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U322 X1 X2 X3 X4)))
(rule (U323 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U323 X1 X2 X3 X4)))
(rule (U324 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U324 X1 X2 X3 X4)))
(rule (U325 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U325 X1 X2 X3 X4)))
(rule (U326 (ok X1) (ok X2) (ok X3) (ok X4)) (ok (U326 X1 X2 X3 X4)))
(rule (U327 (ok X1) (ok X2)) (ok (U327 X1 X2)))
(rule (U34 (ok X1) (ok X2)) (ok (U34 X1 X2)))
(rule (U331 (ok X1) (ok X2) (ok X3)) (ok (U331 X1 X2 X3)))
(rule (U332 (ok X1) (ok X2)) (ok (U332 X1 X2)))
(rule (U333 (ok X1) (ok X2)) (ok (U333 X1 X2)))
(rule (U334 (ok X1) (ok X2)) (ok (U334 X1 X2)))
(rule (U341 (ok X1) (ok X2) (ok X3)) (ok (U341 X1 X2 X3)))
(rule (U342 (ok X1) (ok X2) (ok X3)) (ok (U342 X1 X2 X3)))
(rule (U343 (ok X1) (ok X2) (ok X3)) (ok (U343 X1 X2 X3)))
(rule (U344 (ok X1) (ok X2) (ok X3)) (ok (U344 X1 X2 X3)))
(rule (fst (ok X)) (ok (fst X)))
(rule (U41 (ok X1) (ok X2) (ok X3)) (ok (U41 X1 X2 X3)))
(rule (U42 (ok X1) (ok X2) (ok X3)) (ok (U42 X1 X2 X3)))
(rule (U43 (ok X1) (ok X2) (ok X3)) (ok (U43 X1 X2 X3)))
(rule (U44 (ok X1) (ok X2) (ok X3)) (ok (U44 X1 X2 X3)))
(rule (U45 (ok X1) (ok X2)) (ok (U45 X1 X2)))
(rule (U46 (ok X)) (ok (U46 X)))
(rule (U51 (ok X1) (ok X2) (ok X3)) (ok (U51 X1 X2 X3)))
(rule (U52 (ok X1) (ok X2) (ok X3)) (ok (U52 X1 X2 X3)))
(rule (U53 (ok X1) (ok X2) (ok X3)) (ok (U53 X1 X2 X3)))
(rule (U54 (ok X1) (ok X2) (ok X3)) (ok (U54 X1 X2 X3)))
(rule (U55 (ok X1) (ok X2)) (ok (U55 X1 X2)))
(rule (U56 (ok X)) (ok (U56 X)))
(rule (U61 (ok X1) (ok X2)) (ok (U61 X1 X2)))
(rule (U62 (ok X1) (ok X2)) (ok (U62 X1 X2)))
(rule (isPLNatKind (ok X)) (ok (isPLNatKind X)))
(rule (U63 (ok X)) (ok (U63 X)))
(rule (isPLNat (ok X)) (ok (isPLNat X)))
(rule (U71 (ok X1) (ok X2)) (ok (U71 X1 X2)))
(rule (U72 (ok X1) (ok X2)) (ok (U72 X1 X2)))
(rule (U73 (ok X)) (ok (U73 X)))
(rule (U81 (ok X1) (ok X2)) (ok (U81 X1 X2)))
(rule (U82 (ok X1) (ok X2)) (ok (U82 X1 X2)))
(rule (U83 (ok X)) (ok (U83 X)))
(rule (U91 (ok X1) (ok X2)) (ok (U91 X1 X2)))
(rule (U92 (ok X1) (ok X2)) (ok (U92 X1 X2)))
(rule (U93 (ok X)) (ok (U93 X)))
(rule (tail (ok X)) (ok (tail X)))
(rule (take (ok X1) (ok X2)) (ok (take X1 X2)))
(rule (sel (ok X1) (ok X2)) (ok (sel X1 X2)))
(rule (top (mark X)) (top (proper X)))
(rule (top (ok X)) (top (active X)))