MAYBE Time: 0.326155 TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V1) -> a__U12 a__isNatList V1, a__U22 X -> U22 X, a__U22 tt() -> tt(), a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat length V1 -> a__U11(a__isNatIListKind V1, V1), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V) -> a__U32 a__isNatList V, a__U42(X1, X2) -> U42(X1, X2), a__U42(tt(), V2) -> a__U43 a__isNatIList V2, a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), V1, V2) -> a__U42(a__isNat V1, V2), a__U43 X -> U43 X, a__U43 tt() -> tt(), a__isNatIList V -> a__U31(a__isNatIListKind V, V), a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList zeros() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), V2) -> a__U53 a__isNatList V2, a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), V1, V2) -> a__U52(a__isNat V1, V2), a__U53 X -> U53 X, a__U53 tt() -> tt(), a__U62(X1, X2) -> U62(X1, X2), a__U62(tt(), V2) -> a__U63 a__isNatIList V2, a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), V1, V2) -> a__U62(a__isNat V1, V2), a__U63 X -> U63 X, a__U63 tt() -> tt(), a__length X -> length X, a__length cons(N, L) -> a__U71(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark isNatIListKind X -> a__isNatIListKind X, mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark isNatKind X -> a__isNatKind X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNatList X -> a__isNatList X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), mark U42(X1, X2) -> a__U42(mark X1, X2), mark U43 X -> a__U43 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U53 X -> a__U53 mark X, mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2) -> a__U62(mark X1, X2), mark U63 X -> a__U63 mark X, mark U71(X1, X2) -> a__U71(mark X1, X2), mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), a__U71(X1, X2) -> U71(X1, X2), a__U71(tt(), L) -> s a__length mark L, a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatIListKind X -> isNatIListKind X, a__isNatIListKind cons(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind zeros() -> tt(), a__isNatIListKind nil() -> tt(), a__isNatIListKind take(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatKind X -> isNatKind X, a__isNatKind 0() -> tt(), a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind length V1 -> a__isNatIListKind V1, a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__and(a__isNatIList IL, isNatIListKind IL), a__take(s M, cons(N, IL)) -> a__U91(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N)} DP: DP: { a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatList# cons(V1, V2) -> a__isNatKind# V1, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatList# take(V1, V2) -> a__isNatKind# V1, a__U11#(tt(), V1) -> a__U12# a__isNatList V1, a__U11#(tt(), V1) -> a__isNatList# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# s V1 -> a__isNatKind# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1), a__isNat# length V1 -> a__isNatIListKind# V1, a__U21#(tt(), V1) -> a__U22# a__isNat V1, a__U21#(tt(), V1) -> a__isNat# V1, a__U31#(tt(), V) -> a__isNatList# V, a__U31#(tt(), V) -> a__U32# a__isNatList V, a__U42#(tt(), V2) -> a__U43# a__isNatIList V2, a__U42#(tt(), V2) -> a__isNatIList# V2, a__U41#(tt(), V1, V2) -> a__isNat# V1, a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2), a__isNatIList# V -> a__U31#(a__isNatIListKind V, V), a__isNatIList# V -> a__isNatIListKind# V, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIList# cons(V1, V2) -> a__isNatKind# V1, a__U52#(tt(), V2) -> a__isNatList# V2, a__U52#(tt(), V2) -> a__U53# a__isNatList V2, a__U51#(tt(), V1, V2) -> a__isNat# V1, a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2), a__U62#(tt(), V2) -> a__isNatIList# V2, a__U62#(tt(), V2) -> a__U63# a__isNatIList V2, a__U61#(tt(), V1, V2) -> a__isNat# V1, a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2), a__length# cons(N, L) -> a__isNatList# L, a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length# cons(N, L) -> a__and#(a__isNatList L, isNatIListKind L), a__length# cons(N, L) -> a__and#(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#(), mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2), mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# isNat X -> a__isNat# X, mark# isNatKind X -> a__isNatKind# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# U11(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X, mark# U12 X -> mark# X, mark# isNatList X -> a__isNatList# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X, mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U31(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X, mark# U32 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2), mark# U42(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X, mark# U43 X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2), mark# U52(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X, mark# U53 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2), mark# U62(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X, mark# U63 X -> mark# X, mark# U71(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2), mark# U81 X -> mark# X, mark# U81 X -> a__U81# mark X, mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), a__U71#(tt(), L) -> a__length# mark L, a__U71#(tt(), L) -> mark# L, a__U91#(tt(), IL, M, N) -> mark# N, a__and#(tt(), X) -> mark# X, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1, a__take#(0(), IL) -> a__isNatIList# IL, a__take#(0(), IL) -> a__U81# a__and(a__isNatIList IL, isNatIListKind IL), a__take#(0(), IL) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__take#(s M, cons(N, IL)) -> a__U91#(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N), a__take#(s M, cons(N, IL)) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__take#(s M, cons(N, IL)) -> a__and#(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N)))} TRS: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V1) -> a__U12 a__isNatList V1, a__U22 X -> U22 X, a__U22 tt() -> tt(), a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat length V1 -> a__U11(a__isNatIListKind V1, V1), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V) -> a__U32 a__isNatList V, a__U42(X1, X2) -> U42(X1, X2), a__U42(tt(), V2) -> a__U43 a__isNatIList V2, a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), V1, V2) -> a__U42(a__isNat V1, V2), a__U43 X -> U43 X, a__U43 tt() -> tt(), a__isNatIList V -> a__U31(a__isNatIListKind V, V), a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList zeros() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), V2) -> a__U53 a__isNatList V2, a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), V1, V2) -> a__U52(a__isNat V1, V2), a__U53 X -> U53 X, a__U53 tt() -> tt(), a__U62(X1, X2) -> U62(X1, X2), a__U62(tt(), V2) -> a__U63 a__isNatIList V2, a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), V1, V2) -> a__U62(a__isNat V1, V2), a__U63 X -> U63 X, a__U63 tt() -> tt(), a__length X -> length X, a__length cons(N, L) -> a__U71(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark isNatIListKind X -> a__isNatIListKind X, mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark isNatKind X -> a__isNatKind X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNatList X -> a__isNatList X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), mark U42(X1, X2) -> a__U42(mark X1, X2), mark U43 X -> a__U43 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U53 X -> a__U53 mark X, mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2) -> a__U62(mark X1, X2), mark U63 X -> a__U63 mark X, mark U71(X1, X2) -> a__U71(mark X1, X2), mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), a__U71(X1, X2) -> U71(X1, X2), a__U71(tt(), L) -> s a__length mark L, a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatIListKind X -> isNatIListKind X, a__isNatIListKind cons(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind zeros() -> tt(), a__isNatIListKind nil() -> tt(), a__isNatIListKind take(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatKind X -> isNatKind X, a__isNatKind 0() -> tt(), a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind length V1 -> a__isNatIListKind V1, a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__and(a__isNatIList IL, isNatIListKind IL), a__take(s M, cons(N, IL)) -> a__U91(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N)} UR: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V1) -> a__U12 a__isNatList V1, a__U22 X -> U22 X, a__U22 tt() -> tt(), a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat length V1 -> a__U11(a__isNatIListKind V1, V1), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V) -> a__U32 a__isNatList V, a__U42(X1, X2) -> U42(X1, X2), a__U42(tt(), V2) -> a__U43 a__isNatIList V2, a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), V1, V2) -> a__U42(a__isNat V1, V2), a__U43 X -> U43 X, a__U43 tt() -> tt(), a__isNatIList V -> a__U31(a__isNatIListKind V, V), a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList zeros() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), V2) -> a__U53 a__isNatList V2, a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), V1, V2) -> a__U52(a__isNat V1, V2), a__U53 X -> U53 X, a__U53 tt() -> tt(), a__U62(X1, X2) -> U62(X1, X2), a__U62(tt(), V2) -> a__U63 a__isNatIList V2, a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), V1, V2) -> a__U62(a__isNat V1, V2), a__U63 X -> U63 X, a__U63 tt() -> tt(), a__length X -> length X, a__length cons(N, L) -> a__U71(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark isNatIListKind X -> a__isNatIListKind X, mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark isNatKind X -> a__isNatKind X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNatList X -> a__isNatList X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), mark U42(X1, X2) -> a__U42(mark X1, X2), mark U43 X -> a__U43 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U53 X -> a__U53 mark X, mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2) -> a__U62(mark X1, X2), mark U63 X -> a__U63 mark X, mark U71(X1, X2) -> a__U71(mark X1, X2), mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), a__U71(X1, X2) -> U71(X1, X2), a__U71(tt(), L) -> s a__length mark L, a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatIListKind X -> isNatIListKind X, a__isNatIListKind cons(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind zeros() -> tt(), a__isNatIListKind nil() -> tt(), a__isNatIListKind take(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatKind X -> isNatKind X, a__isNatKind 0() -> tt(), a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind length V1 -> a__isNatIListKind V1, a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__and(a__isNatIList IL, isNatIListKind IL), a__take(s M, cons(N, IL)) -> a__U91(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N), a(x, y) -> x, a(x, y) -> y} EDG: { (a__isNatList# cons(V1, V2) -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__isNatList# cons(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__U11#(tt(), V1) -> a__isNatList# V1, a__isNatList# take(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1) -> a__isNatList# V1, a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U11#(tt(), V1) -> a__isNatList# V1, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U11#(tt(), V1) -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__isNatKind# V1) (a__U11#(tt(), V1) -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U11#(tt(), V1) -> a__isNatList# V1, a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__isNat# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1) (a__isNat# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__isNat# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1) (a__isNat# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U41#(tt(), V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatIListKind# V1) (a__U41#(tt(), V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1)) (a__U41#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U41#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U51#(tt(), V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatIListKind# V1) (a__U51#(tt(), V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1)) (a__U51#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U51#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V1) -> a__isNatList# V1) (mark# U11(X1, X2) -> a__U11#(mark X1, X2), a__U11#(tt(), V1) -> a__U12# a__isNatList V1) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V) -> a__U32# a__isNatList V) (mark# U31(X1, X2) -> a__U31#(mark X1, X2), a__U31#(tt(), V) -> a__isNatList# V) (mark# U52(X1, X2) -> a__U52#(mark X1, X2), a__U52#(tt(), V2) -> a__U53# a__isNatList V2) (mark# U52(X1, X2) -> a__U52#(mark X1, X2), a__U52#(tt(), V2) -> a__isNatList# V2) (mark# U71(X1, X2) -> a__U71#(mark X1, X2), a__U71#(tt(), L) -> mark# L) (mark# U71(X1, X2) -> a__U71#(mark X1, X2), a__U71#(tt(), L) -> a__length# mark L) (a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2)) (a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U51#(tt(), V1, V2) -> a__isNat# V1) (a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2)) (a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U41#(tt(), V1, V2) -> a__isNat# V1) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__isNatKind# V1) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# V -> a__isNatIListKind# V) (a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__isNatIList# V -> a__U31#(a__isNatIListKind V, V)) (a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2), a__U42#(tt(), V2) -> a__isNatIList# V2) (a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2), a__U42#(tt(), V2) -> a__U43# a__isNatIList V2) (a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2), a__U52#(tt(), V2) -> a__U53# a__isNatList V2) (a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2), a__U52#(tt(), V2) -> a__isNatList# V2) (mark# s X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# s X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# s X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# s X -> mark# X, mark# U81 X -> mark# X) (mark# s X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# s X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U63 X -> mark# X) (mark# s X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# s X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# s X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U53 X -> mark# X) (mark# s X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# s X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# s X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# s X -> mark# X, mark# U43 X -> mark# X) (mark# s X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# s X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# s X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# s X -> mark# X, mark# U32 X -> mark# X) (mark# s X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# s X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# s X -> mark# X, mark# U22 X -> mark# X) (mark# s X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# s X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# s X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# s X -> mark# X, mark# U12 X -> mark# X) (mark# s X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# s X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# s X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# s X -> mark# X, mark# isNat X -> a__isNat# X) (mark# s X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# s X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# s X -> mark# X, mark# length X -> mark# X) (mark# s X -> mark# X, mark# length X -> a__length# mark X) (mark# s X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# s X -> mark# X, mark# s X -> mark# X) (mark# s X -> mark# X, mark# zeros() -> a__zeros#()) (mark# s X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# isNatIListKind X -> a__isNatIListKind# X, a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1) (mark# isNatIListKind X -> a__isNatIListKind# X, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (mark# isNatIListKind X -> a__isNatIListKind# X, a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1) (mark# isNatIListKind X -> a__isNatIListKind# X, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# length V1 -> a__isNatIListKind# V1) (mark# isNatKind X -> a__isNatKind# X, a__isNatKind# s V1 -> a__isNatKind# V1) (mark# isNatList X -> a__isNatList# X, a__isNatList# take(V1, V2) -> a__isNatKind# V1) (mark# isNatList X -> a__isNatList# X, a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__isNatKind# V1) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (mark# isNatList X -> a__isNatList# X, a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (mark# U32 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U32 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U32 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U32 X -> mark# X, mark# U81 X -> mark# X) (mark# U32 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U63 X -> mark# X) (mark# U32 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U32 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U53 X -> mark# X) (mark# U32 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U32 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U32 X -> mark# X, mark# U43 X -> mark# X) (mark# U32 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U32 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U32 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U32 X -> mark# X, mark# U32 X -> mark# X) (mark# U32 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U32 X -> mark# X, mark# U22 X -> mark# X) (mark# U32 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U32 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U32 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U32 X -> mark# X, mark# U12 X -> mark# X) (mark# U32 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U32 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U32 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U32 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U32 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U32 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U32 X -> mark# X, mark# length X -> mark# X) (mark# U32 X -> mark# X, mark# length X -> a__length# mark X) (mark# U32 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U32 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U32 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U32 X -> mark# X, mark# s X -> mark# X) (mark# U32 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U32 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__isNatKind# V1) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# V -> a__isNatIListKind# V) (mark# isNatIList X -> a__isNatIList# X, a__isNatIList# V -> a__U31#(a__isNatIListKind V, V)) (mark# U63 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U63 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U63 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U63 X -> mark# X, mark# U81 X -> mark# X) (mark# U63 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U63 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U63 X -> mark# X) (mark# U63 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U63 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U63 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U63 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U63 X -> mark# X, mark# U53 X -> mark# X) (mark# U63 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U63 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U63 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U63 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U63 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U63 X -> mark# X, mark# U43 X -> mark# X) (mark# U63 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U63 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U63 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U63 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U63 X -> mark# X, mark# U32 X -> mark# X) (mark# U63 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U63 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U63 X -> mark# X, mark# U22 X -> mark# X) (mark# U63 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U63 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U63 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U63 X -> mark# X, mark# U12 X -> mark# X) (mark# U63 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U63 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U63 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U63 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U63 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U63 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U63 X -> mark# X, mark# length X -> mark# X) (mark# U63 X -> mark# X, mark# length X -> a__length# mark X) (mark# U63 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U63 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U63 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U63 X -> mark# X, mark# s X -> mark# X) (mark# U63 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U63 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__and#(tt(), X) -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U81 X -> a__U81# mark X) (a__and#(tt(), X) -> mark# X, mark# U81 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U71(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U63 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U63 X -> a__U63# mark X) (a__and#(tt(), X) -> mark# X, mark# U62(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# U53 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U53 X -> a__U53# mark X) (a__and#(tt(), X) -> mark# X, mark# U52(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# isNatIList X -> a__isNatIList# X) (a__and#(tt(), X) -> mark# X, mark# U43 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U43 X -> a__U43# mark X) (a__and#(tt(), X) -> mark# X, mark# U42(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__and#(tt(), X) -> mark# X, mark# U32 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U32 X -> a__U32# mark X) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# U22 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U22 X -> a__U22# mark X) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# isNatList X -> a__isNatList# X) (a__and#(tt(), X) -> mark# X, mark# U12 X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# U12 X -> a__U12# mark X) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# isNatKind X -> a__isNatKind# X) (a__and#(tt(), X) -> mark# X, mark# isNat X -> a__isNat# X) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__and#(tt(), X) -> mark# X, mark# and(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (a__and#(tt(), X) -> mark# X, mark# length X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# length X -> a__length# mark X) (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X2) (a__and#(tt(), X) -> mark# X, mark# take(X1, X2) -> mark# X1) (a__and#(tt(), X) -> mark# X, mark# s X -> mark# X) (a__and#(tt(), X) -> mark# X, mark# zeros() -> a__zeros#()) (a__and#(tt(), X) -> mark# X, mark# cons(X1, X2) -> mark# X1) (a__U42#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__isNatKind# V1) (a__U42#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U42#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U42#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__isNatIListKind# V) (a__U42#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__U31#(a__isNatIListKind V, V)) (a__U62#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__isNatKind# V1) (a__U62#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U62#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U62#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__isNatIListKind# V) (a__U62#(tt(), V2) -> a__isNatIList# V2, a__isNatIList# V -> a__U31#(a__isNatIListKind V, V)) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2)) (mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), a__U41#(tt(), V1, V2) -> a__isNat# V1) (mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2)) (mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), a__U61#(tt(), V1, V2) -> a__isNat# V1) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__and#(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N))) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__and#(a__isNatList L, isNatIListKind L)) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L)) (mark# length X -> a__length# mark X, a__length# cons(N, L) -> a__isNatList# L) (a__U71#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__and#(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N))) (a__U71#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__and#(a__isNatList L, isNatIListKind L)) (a__U71#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L)) (a__U71#(tt(), L) -> a__length# mark L, a__length# cons(N, L) -> a__isNatList# L) (mark# take(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# take(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# take(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# take(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# take(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# take(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# take(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# take(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# take(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# take(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# take(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# take(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# take(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# take(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# take(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# take(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U11(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U11(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U11(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U11(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U11(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U11(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U11(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U11(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U11(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U11(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U11(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U11(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U31(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U31(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U31(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U31(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U31(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U31(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U31(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U31(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U31(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U31(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U31(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U42(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U42(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U42(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U42(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U42(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U42(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U42(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U42(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U42(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U42(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U42(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U42(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U42(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U42(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U42(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U42(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U42(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U52(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U52(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U52(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U52(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U52(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U52(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U52(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U52(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U52(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U52(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U52(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U52(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U52(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U52(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U52(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U62(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U62(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U62(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U62(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U62(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U62(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U62(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U62(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U62(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U62(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U62(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U62(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U62(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U62(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U62(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U62(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U62(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U81 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U63 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U53 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U43 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U32 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U22 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U12 X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# length X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# length X -> a__length# mark X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# s X -> mark# X) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U91(X1, X2, X3, X4) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__U71#(tt(), L) -> mark# L, mark# U91(X1, X2, X3, X4) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U81 X -> a__U81# mark X) (a__U71#(tt(), L) -> mark# L, mark# U81 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# U71(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U63 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U63 X -> a__U63# mark X) (a__U71#(tt(), L) -> mark# L, mark# U62(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# U61(X1, X2, X3) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (a__U71#(tt(), L) -> mark# L, mark# U53 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U53 X -> a__U53# mark X) (a__U71#(tt(), L) -> mark# L, mark# U52(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# U51(X1, X2, X3) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U71#(tt(), L) -> mark# L, mark# isNatIList X -> a__isNatIList# X) (a__U71#(tt(), L) -> mark# L, mark# U43 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U43 X -> a__U43# mark X) (a__U71#(tt(), L) -> mark# L, mark# U42(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# U41(X1, X2, X3) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U71#(tt(), L) -> mark# L, mark# U32 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U32 X -> a__U32# mark X) (a__U71#(tt(), L) -> mark# L, mark# U31(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# U22 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U22 X -> a__U22# mark X) (a__U71#(tt(), L) -> mark# L, mark# U21(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# isNatList X -> a__isNatList# X) (a__U71#(tt(), L) -> mark# L, mark# U12 X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# U12 X -> a__U12# mark X) (a__U71#(tt(), L) -> mark# L, mark# U11(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# isNatKind X -> a__isNatKind# X) (a__U71#(tt(), L) -> mark# L, mark# isNat X -> a__isNat# X) (a__U71#(tt(), L) -> mark# L, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U71#(tt(), L) -> mark# L, mark# and(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# isNatIListKind X -> a__isNatIListKind# X) (a__U71#(tt(), L) -> mark# L, mark# length X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# length X -> a__length# mark X) (a__U71#(tt(), L) -> mark# L, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (a__U71#(tt(), L) -> mark# L, mark# take(X1, X2) -> mark# X2) (a__U71#(tt(), L) -> mark# L, mark# take(X1, X2) -> mark# X1) (a__U71#(tt(), L) -> mark# L, mark# s X -> mark# X) (a__U71#(tt(), L) -> mark# L, mark# zeros() -> a__zeros#()) (a__U71#(tt(), L) -> mark# L, mark# cons(X1, X2) -> mark# X1) (a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1), a__U11#(tt(), V1) -> a__isNatList# V1) (a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1), a__U11#(tt(), V1) -> a__U12# a__isNatList V1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U91(X1, X2, X3, X4) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U81 X -> a__U81# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U81 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U71(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U63 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U63 X -> a__U63# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U62(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U61(X1, X2, X3) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U53 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U53 X -> a__U53# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U52(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U51(X1, X2, X3) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# isNatIList X -> a__isNatIList# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U43 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U43 X -> a__U43# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U42(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U41(X1, X2, X3) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U32 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U32 X -> a__U32# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U31(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U22 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U22 X -> a__U22# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U21(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# isNatList X -> a__isNatList# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U12 X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U12 X -> a__U12# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U11(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# isNatKind X -> a__isNatKind# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# isNat X -> a__isNat# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# and(X1, X2) -> a__and#(mark X1, X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# and(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# isNatIListKind X -> a__isNatIListKind# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# length X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# length X -> a__length# mark X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (a__U91#(tt(), IL, M, N) -> mark# N, mark# take(X1, X2) -> mark# X2) (a__U91#(tt(), IL, M, N) -> mark# N, mark# take(X1, X2) -> mark# X1) (a__U91#(tt(), IL, M, N) -> mark# N, mark# s X -> mark# X) (a__U91#(tt(), IL, M, N) -> mark# N, mark# zeros() -> a__zeros#()) (a__U91#(tt(), IL, M, N) -> mark# N, mark# cons(X1, X2) -> mark# X1) (a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__and#(tt(), X) -> mark# X) (a__length# cons(N, L) -> a__and#(a__isNatList L, isNatIListKind L), a__and#(tt(), X) -> mark# X) (a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__and#(tt(), X) -> mark# X) (a__take#(0(), IL) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__and#(tt(), X) -> mark# X) (a__length# cons(N, L) -> a__and#(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), a__and#(tt(), X) -> mark# X) (a__take#(s M, cons(N, IL)) -> a__and#(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), a__and#(tt(), X) -> mark# X) (a__take#(s M, cons(N, IL)) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__and#(tt(), X) -> mark# X) (a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__and#(tt(), X) -> mark# X) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(0(), IL) -> a__isNatIList# IL) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(0(), IL) -> a__U81# a__and(a__isNatIList IL, isNatIListKind IL)) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(0(), IL) -> a__and#(a__isNatIList IL, isNatIListKind IL)) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> a__isNatIList# IL) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> a__U91#(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N)) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> a__and#(a__isNatIList IL, isNatIListKind IL)) (mark# take(X1, X2) -> a__take#(mark X1, mark X2), a__take#(s M, cons(N, IL)) -> a__and#(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N)))) (a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__and#(tt(), X) -> mark# X) (a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__and#(tt(), X) -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# cons(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# zeros() -> a__zeros#()) (mark# take(X1, X2) -> mark# X2, mark# s X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> mark# X2) (mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# take(X1, X2) -> mark# X2, mark# length X -> a__length# mark X) (mark# take(X1, X2) -> mark# X2, mark# length X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# isNat X -> a__isNat# X) (mark# take(X1, X2) -> mark# X2, mark# isNatKind X -> a__isNatKind# X) (mark# take(X1, X2) -> mark# X2, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U11(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U12 X -> a__U12# mark X) (mark# take(X1, X2) -> mark# X2, mark# U12 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# isNatList X -> a__isNatList# X) (mark# take(X1, X2) -> mark# X2, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U21(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U22 X -> a__U22# mark X) (mark# take(X1, X2) -> mark# X2, mark# U22 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U31(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U32 X -> a__U32# mark X) (mark# take(X1, X2) -> mark# X2, mark# U32 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X2, mark# U41(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U42(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U43 X -> a__U43# mark X) (mark# take(X1, X2) -> mark# X2, mark# U43 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# isNatIList X -> a__isNatIList# X) (mark# take(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X2, mark# U51(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U52(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U53 X -> a__U53# mark X) (mark# take(X1, X2) -> mark# X2, mark# U53 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# take(X1, X2) -> mark# X2, mark# U61(X1, X2, X3) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U62(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U63 X -> a__U63# mark X) (mark# take(X1, X2) -> mark# X2, mark# U63 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U71(X1, X2) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# take(X1, X2) -> mark# X2, mark# U81 X -> mark# X) (mark# take(X1, X2) -> mark# X2, mark# U81 X -> a__U81# mark X) (mark# take(X1, X2) -> mark# X2, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# take(X1, X2) -> mark# X2, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__U21#(tt(), V1) -> a__isNat# V1) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# cons(V1, V2) -> a__isNatKind# V1) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__length# cons(N, L) -> a__isNatList# L, a__isNatList# take(V1, V2) -> a__isNatKind# V1) (mark# U71(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U71(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U71(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U71(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U71(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U71(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U71(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U71(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U71(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U71(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U71(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U71(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U71(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U71(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U71(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U71(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U71(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U61(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U61(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U61(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# length X -> a__length# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# length X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U43 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U53 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U63 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U61(X1, X2, X3) -> mark# X1, mark# U81 X -> mark# X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U61(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U61(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U51(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U51(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U51(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# length X -> a__length# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# length X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U43 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U53 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U63 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U51(X1, X2, X3) -> mark# X1, mark# U81 X -> mark# X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U51(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U51(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U41(X1, X2, X3) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U41(X1, X2, X3) -> mark# X1, mark# s X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U41(X1, X2, X3) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# length X -> a__length# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# length X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U12 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U22 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U32 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U43 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U53 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U63 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U41(X1, X2, X3) -> mark# X1, mark# U81 X -> mark# X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U41(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U41(X1, X2, X3) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U21(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# U21(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# U21(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U21(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# U21(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# U21(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U21(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U21(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# U21(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# U21(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U21(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# and(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# and(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# and(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# and(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# and(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# and(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# and(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# and(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# and(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# and(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# and(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# and(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# and(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# and(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# and(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# and(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# and(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# and(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# cons(X1, X2) -> mark# X1, mark# cons(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# zeros() -> a__zeros#()) (mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2) (mark# cons(X1, X2) -> mark# X1, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# cons(X1, X2) -> mark# X1, mark# length X -> a__length# mark X) (mark# cons(X1, X2) -> mark# X1, mark# length X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# isNat X -> a__isNat# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatKind X -> a__isNatKind# X) (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U11(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U12 X -> a__U12# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U12 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatList X -> a__isNatList# X) (mark# cons(X1, X2) -> mark# X1, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U21(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U22 X -> a__U22# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U22 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U31(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U32 X -> a__U32# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U32 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# cons(X1, X2) -> mark# X1, mark# U41(X1, X2, X3) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U42(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U43 X -> a__U43# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U43 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# isNatIList X -> a__isNatIList# X) (mark# cons(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# cons(X1, X2) -> mark# X1, mark# U51(X1, X2, X3) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U52(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U53 X -> a__U53# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U53 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# cons(X1, X2) -> mark# X1, mark# U61(X1, X2, X3) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U62(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U63 X -> a__U63# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U63 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U71(X1, X2) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# cons(X1, X2) -> mark# X1, mark# U81 X -> mark# X) (mark# cons(X1, X2) -> mark# X1, mark# U81 X -> a__U81# mark X) (mark# cons(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# cons(X1, X2) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__U71#(tt(), L) -> a__length# mark L) (a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__U71#(tt(), L) -> mark# L) (mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), a__U51#(tt(), V1, V2) -> a__isNat# V1) (mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2)) (a__take#(s M, cons(N, IL)) -> a__U91#(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N), a__U91#(tt(), IL, M, N) -> mark# N) (a__U52#(tt(), V2) -> a__isNatList# V2, a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U52#(tt(), V2) -> a__isNatList# V2, a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U52#(tt(), V2) -> a__isNatList# V2, a__isNatList# cons(V1, V2) -> a__isNatKind# V1) (a__U52#(tt(), V2) -> a__isNatList# V2, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U52#(tt(), V2) -> a__isNatList# V2, a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U52#(tt(), V2) -> a__isNatList# V2, a__isNatList# take(V1, V2) -> a__isNatKind# V1) (mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), a__U91#(tt(), IL, M, N) -> mark# N) (mark# U81 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U81 X -> mark# X, mark# s X -> mark# X) (mark# U81 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U81 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U81 X -> mark# X, mark# length X -> a__length# mark X) (mark# U81 X -> mark# X, mark# length X -> mark# X) (mark# U81 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U81 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U81 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U81 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U81 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U81 X -> mark# X, mark# U12 X -> mark# X) (mark# U81 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U81 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U81 X -> mark# X, mark# U22 X -> mark# X) (mark# U81 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U81 X -> mark# X, mark# U32 X -> mark# X) (mark# U81 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U81 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U81 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U81 X -> mark# X, mark# U43 X -> mark# X) (mark# U81 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U81 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U81 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U81 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U81 X -> mark# X, mark# U53 X -> mark# X) (mark# U81 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U81 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U81 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U81 X -> mark# X, mark# U63 X -> mark# X) (mark# U81 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U81 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U81 X -> mark# X, mark# U81 X -> mark# X) (mark# U81 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U53 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U53 X -> mark# X, mark# s X -> mark# X) (mark# U53 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U53 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U53 X -> mark# X, mark# length X -> a__length# mark X) (mark# U53 X -> mark# X, mark# length X -> mark# X) (mark# U53 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U53 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U53 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U53 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U53 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U53 X -> mark# X, mark# U12 X -> mark# X) (mark# U53 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U53 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U53 X -> mark# X, mark# U22 X -> mark# X) (mark# U53 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U53 X -> mark# X, mark# U32 X -> mark# X) (mark# U53 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U53 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U53 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U53 X -> mark# X, mark# U43 X -> mark# X) (mark# U53 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U53 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U53 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U53 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U53 X -> mark# X, mark# U53 X -> mark# X) (mark# U53 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U53 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U53 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U53 X -> mark# X, mark# U63 X -> mark# X) (mark# U53 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U53 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U53 X -> mark# X, mark# U81 X -> mark# X) (mark# U53 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U53 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U53 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U43 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U43 X -> mark# X, mark# s X -> mark# X) (mark# U43 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U43 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U43 X -> mark# X, mark# length X -> a__length# mark X) (mark# U43 X -> mark# X, mark# length X -> mark# X) (mark# U43 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U43 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U43 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U43 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U43 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U43 X -> mark# X, mark# U12 X -> mark# X) (mark# U43 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U43 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U43 X -> mark# X, mark# U22 X -> mark# X) (mark# U43 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U43 X -> mark# X, mark# U32 X -> mark# X) (mark# U43 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U43 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U43 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U43 X -> mark# X, mark# U43 X -> mark# X) (mark# U43 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U43 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U43 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U43 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U43 X -> mark# X, mark# U53 X -> mark# X) (mark# U43 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U43 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U43 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U43 X -> mark# X, mark# U63 X -> mark# X) (mark# U43 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U43 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U43 X -> mark# X, mark# U81 X -> mark# X) (mark# U43 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U43 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U43 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U22 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U22 X -> mark# X, mark# s X -> mark# X) (mark# U22 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U22 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U22 X -> mark# X, mark# length X -> a__length# mark X) (mark# U22 X -> mark# X, mark# length X -> mark# X) (mark# U22 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U22 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U22 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U22 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U22 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U22 X -> mark# X, mark# U12 X -> mark# X) (mark# U22 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U22 X -> mark# X, mark# U22 X -> mark# X) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U22 X -> mark# X, mark# U32 X -> mark# X) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U22 X -> mark# X, mark# U43 X -> mark# X) (mark# U22 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U22 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U22 X -> mark# X, mark# U53 X -> mark# X) (mark# U22 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U22 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U22 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U22 X -> mark# X, mark# U63 X -> mark# X) (mark# U22 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U22 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U22 X -> mark# X, mark# U81 X -> mark# X) (mark# U22 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U22 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U22 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# U12 X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# zeros() -> a__zeros#()) (mark# U12 X -> mark# X, mark# s X -> mark# X) (mark# U12 X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# U12 X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# U12 X -> mark# X, mark# length X -> a__length# mark X) (mark# U12 X -> mark# X, mark# length X -> mark# X) (mark# U12 X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# U12 X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# U12 X -> mark# X, mark# isNat X -> a__isNat# X) (mark# U12 X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# U12 X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# U12 X -> mark# X, mark# U12 X -> mark# X) (mark# U12 X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# U12 X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# U12 X -> mark# X, mark# U22 X -> mark# X) (mark# U12 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# U12 X -> mark# X, mark# U32 X -> mark# X) (mark# U12 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# U12 X -> mark# X, mark# U43 X -> mark# X) (mark# U12 X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# U12 X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# U12 X -> mark# X, mark# U53 X -> mark# X) (mark# U12 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# U12 X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# U12 X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# U12 X -> mark# X, mark# U63 X -> mark# X) (mark# U12 X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# U12 X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# U12 X -> mark# X, mark# U81 X -> mark# X) (mark# U12 X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# U12 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# U12 X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (mark# isNat X -> a__isNat# X, a__isNat# s V1 -> a__isNatKind# V1) (mark# isNat X -> a__isNat# X, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1)) (mark# isNat X -> a__isNat# X, a__isNat# length V1 -> a__isNatIListKind# V1) (mark# length X -> mark# X, mark# cons(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# zeros() -> a__zeros#()) (mark# length X -> mark# X, mark# s X -> mark# X) (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# take(X1, X2) -> mark# X2) (mark# length X -> mark# X, mark# take(X1, X2) -> a__take#(mark X1, mark X2)) (mark# length X -> mark# X, mark# length X -> a__length# mark X) (mark# length X -> mark# X, mark# length X -> mark# X) (mark# length X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X) (mark# length X -> mark# X, mark# and(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# and(X1, X2) -> a__and#(mark X1, X2)) (mark# length X -> mark# X, mark# isNat X -> a__isNat# X) (mark# length X -> mark# X, mark# isNatKind X -> a__isNatKind# X) (mark# length X -> mark# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2)) (mark# length X -> mark# X, mark# U11(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U12 X -> a__U12# mark X) (mark# length X -> mark# X, mark# U12 X -> mark# X) (mark# length X -> mark# X, mark# isNatList X -> a__isNatList# X) (mark# length X -> mark# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2)) (mark# length X -> mark# X, mark# U21(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U22 X -> a__U22# mark X) (mark# length X -> mark# X, mark# U22 X -> mark# X) (mark# length X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2)) (mark# length X -> mark# X, mark# U31(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U32 X -> a__U32# mark X) (mark# length X -> mark# X, mark# U32 X -> mark# X) (mark# length X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3)) (mark# length X -> mark# X, mark# U41(X1, X2, X3) -> mark# X1) (mark# length X -> mark# X, mark# U42(X1, X2) -> a__U42#(mark X1, X2)) (mark# length X -> mark# X, mark# U42(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U43 X -> a__U43# mark X) (mark# length X -> mark# X, mark# U43 X -> mark# X) (mark# length X -> mark# X, mark# isNatIList X -> a__isNatIList# X) (mark# length X -> mark# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3)) (mark# length X -> mark# X, mark# U51(X1, X2, X3) -> mark# X1) (mark# length X -> mark# X, mark# U52(X1, X2) -> a__U52#(mark X1, X2)) (mark# length X -> mark# X, mark# U52(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U53 X -> a__U53# mark X) (mark# length X -> mark# X, mark# U53 X -> mark# X) (mark# length X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3)) (mark# length X -> mark# X, mark# U61(X1, X2, X3) -> mark# X1) (mark# length X -> mark# X, mark# U62(X1, X2) -> a__U62#(mark X1, X2)) (mark# length X -> mark# X, mark# U62(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U63 X -> a__U63# mark X) (mark# length X -> mark# X, mark# U63 X -> mark# X) (mark# length X -> mark# X, mark# U71(X1, X2) -> mark# X1) (mark# length X -> mark# X, mark# U71(X1, X2) -> a__U71#(mark X1, X2)) (mark# length X -> mark# X, mark# U81 X -> mark# X) (mark# length X -> mark# X, mark# U81 X -> a__U81# mark X) (mark# length X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1) (mark# length X -> mark# X, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4)) (a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2), a__U62#(tt(), V2) -> a__isNatIList# V2) (a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2), a__U62#(tt(), V2) -> a__U63# a__isNatIList V2) (a__isNatIList# V -> a__isNatIListKind# V, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__isNatIList# V -> a__isNatIListKind# V, a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1) (a__isNatIList# V -> a__isNatIListKind# V, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__isNatIList# V -> a__isNatIListKind# V, a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1) (a__U31#(tt(), V) -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U31#(tt(), V) -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U31#(tt(), V) -> a__isNatList# V, a__isNatList# cons(V1, V2) -> a__isNatKind# V1) (a__U31#(tt(), V) -> a__isNatList# V, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__U31#(tt(), V) -> a__isNatList# V, a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__U31#(tt(), V) -> a__isNatList# V, a__isNatList# take(V1, V2) -> a__isNatKind# V1) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# V -> a__U31#(a__isNatIListKind V, V)) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# V -> a__isNatIListKind# V) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2)) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__take#(0(), IL) -> a__isNatIList# IL, a__isNatIList# cons(V1, V2) -> a__isNatKind# V1) (a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U61#(tt(), V1, V2) -> a__isNat# V1) (a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2)) (mark# U62(X1, X2) -> a__U62#(mark X1, X2), a__U62#(tt(), V2) -> a__isNatIList# V2) (mark# U62(X1, X2) -> a__U62#(mark X1, X2), a__U62#(tt(), V2) -> a__U63# a__isNatIList V2) (mark# U42(X1, X2) -> a__U42#(mark X1, X2), a__U42#(tt(), V2) -> a__U43# a__isNatIList V2) (mark# U42(X1, X2) -> a__U42#(mark X1, X2), a__U42#(tt(), V2) -> a__isNatIList# V2) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__U22# a__isNat V1) (mark# U21(X1, X2) -> a__U21#(mark X1, X2), a__U21#(tt(), V1) -> a__isNat# V1) (mark# and(X1, X2) -> a__and#(mark X1, X2), a__and#(tt(), X) -> mark# X) (a__isNatKind# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__isNatKind# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1) (a__isNatKind# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2)) (a__isNatKind# length V1 -> a__isNatIListKind# V1, a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1) (a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__U61#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U61#(tt(), V1, V2) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U61#(tt(), V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1)) (a__U61#(tt(), V1, V2) -> a__isNat# V1, a__isNat# length V1 -> a__isNatIListKind# V1) (a__isNatIList# cons(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatIList# cons(V1, V2) -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# s V1 -> a__isNatKind# V1) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1)) (a__U21#(tt(), V1) -> a__isNat# V1, a__isNat# length V1 -> a__isNatIListKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNat# s V1 -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__isNatList# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1) (a__isNatList# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1) (a__isNatIList# V -> a__U31#(a__isNatIListKind V, V), a__U31#(tt(), V) -> a__isNatList# V) (a__isNatIList# V -> a__U31#(a__isNatIListKind V, V), a__U31#(tt(), V) -> a__U32# a__isNatList V) } STATUS: arrows: 0.859229 SCCS (1): Scc: { a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatList# cons(V1, V2) -> a__isNatKind# V1, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatList# take(V1, V2) -> a__isNatKind# V1, a__U11#(tt(), V1) -> a__isNatList# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# s V1 -> a__isNatKind# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1), a__isNat# length V1 -> a__isNatIListKind# V1, a__U21#(tt(), V1) -> a__isNat# V1, a__U31#(tt(), V) -> a__isNatList# V, a__U42#(tt(), V2) -> a__isNatIList# V2, a__U41#(tt(), V1, V2) -> a__isNat# V1, a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2), a__isNatIList# V -> a__U31#(a__isNatIListKind V, V), a__isNatIList# V -> a__isNatIListKind# V, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIList# cons(V1, V2) -> a__isNatKind# V1, a__U52#(tt(), V2) -> a__isNatList# V2, a__U51#(tt(), V1, V2) -> a__isNat# V1, a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2), a__U62#(tt(), V2) -> a__isNatIList# V2, a__U61#(tt(), V1, V2) -> a__isNat# V1, a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2), a__length# cons(N, L) -> a__isNatList# L, a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length# cons(N, L) -> a__and#(a__isNatList L, isNatIListKind L), a__length# cons(N, L) -> a__and#(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2), mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# isNat X -> a__isNat# X, mark# isNatKind X -> a__isNatKind# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X, mark# isNatList X -> a__isNatList# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2), mark# U42(X1, X2) -> mark# X1, mark# U43 X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2), mark# U52(X1, X2) -> mark# X1, mark# U53 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2), mark# U62(X1, X2) -> mark# X1, mark# U63 X -> mark# X, mark# U71(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2), mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), a__U71#(tt(), L) -> a__length# mark L, a__U71#(tt(), L) -> mark# L, a__U91#(tt(), IL, M, N) -> mark# N, a__and#(tt(), X) -> mark# X, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1, a__take#(0(), IL) -> a__isNatIList# IL, a__take#(0(), IL) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__take#(s M, cons(N, IL)) -> a__U91#(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N), a__take#(s M, cons(N, IL)) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__take#(s M, cons(N, IL)) -> a__and#(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N)))} SCC (90): Strict: { a__isNatList# cons(V1, V2) -> a__U51#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatList# cons(V1, V2) -> a__isNatKind# V1, a__isNatList# take(V1, V2) -> a__U61#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatList# take(V1, V2) -> a__isNatKind# V1, a__U11#(tt(), V1) -> a__isNatList# V1, a__isNat# s V1 -> a__U21#(a__isNatKind V1, V1), a__isNat# s V1 -> a__isNatKind# V1, a__isNat# length V1 -> a__U11#(a__isNatIListKind V1, V1), a__isNat# length V1 -> a__isNatIListKind# V1, a__U21#(tt(), V1) -> a__isNat# V1, a__U31#(tt(), V) -> a__isNatList# V, a__U42#(tt(), V2) -> a__isNatIList# V2, a__U41#(tt(), V1, V2) -> a__isNat# V1, a__U41#(tt(), V1, V2) -> a__U42#(a__isNat V1, V2), a__isNatIList# V -> a__U31#(a__isNatIListKind V, V), a__isNatIList# V -> a__isNatIListKind# V, a__isNatIList# cons(V1, V2) -> a__U41#(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIList# cons(V1, V2) -> a__isNatKind# V1, a__U52#(tt(), V2) -> a__isNatList# V2, a__U51#(tt(), V1, V2) -> a__isNat# V1, a__U51#(tt(), V1, V2) -> a__U52#(a__isNat V1, V2), a__U62#(tt(), V2) -> a__isNatIList# V2, a__U61#(tt(), V1, V2) -> a__isNat# V1, a__U61#(tt(), V1, V2) -> a__U62#(a__isNat V1, V2), a__length# cons(N, L) -> a__isNatList# L, a__length# cons(N, L) -> a__U71#(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length# cons(N, L) -> a__and#(a__isNatList L, isNatIListKind L), a__length# cons(N, L) -> a__and#(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), mark# cons(X1, X2) -> mark# X1, mark# s X -> mark# X, mark# take(X1, X2) -> mark# X1, mark# take(X1, X2) -> mark# X2, mark# take(X1, X2) -> a__take#(mark X1, mark X2), mark# length X -> a__length# mark X, mark# length X -> mark# X, mark# isNatIListKind X -> a__isNatIListKind# X, mark# and(X1, X2) -> mark# X1, mark# and(X1, X2) -> a__and#(mark X1, X2), mark# isNat X -> a__isNat# X, mark# isNatKind X -> a__isNatKind# X, mark# U11(X1, X2) -> a__U11#(mark X1, X2), mark# U11(X1, X2) -> mark# X1, mark# U12 X -> mark# X, mark# isNatList X -> a__isNatList# X, mark# U21(X1, X2) -> a__U21#(mark X1, X2), mark# U21(X1, X2) -> mark# X1, mark# U22 X -> mark# X, mark# U31(X1, X2) -> a__U31#(mark X1, X2), mark# U31(X1, X2) -> mark# X1, mark# U32 X -> mark# X, mark# U41(X1, X2, X3) -> a__U41#(mark X1, X2, X3), mark# U41(X1, X2, X3) -> mark# X1, mark# U42(X1, X2) -> a__U42#(mark X1, X2), mark# U42(X1, X2) -> mark# X1, mark# U43 X -> mark# X, mark# isNatIList X -> a__isNatIList# X, mark# U51(X1, X2, X3) -> a__U51#(mark X1, X2, X3), mark# U51(X1, X2, X3) -> mark# X1, mark# U52(X1, X2) -> a__U52#(mark X1, X2), mark# U52(X1, X2) -> mark# X1, mark# U53 X -> mark# X, mark# U61(X1, X2, X3) -> a__U61#(mark X1, X2, X3), mark# U61(X1, X2, X3) -> mark# X1, mark# U62(X1, X2) -> a__U62#(mark X1, X2), mark# U62(X1, X2) -> mark# X1, mark# U63 X -> mark# X, mark# U71(X1, X2) -> mark# X1, mark# U71(X1, X2) -> a__U71#(mark X1, X2), mark# U81 X -> mark# X, mark# U91(X1, X2, X3, X4) -> mark# X1, mark# U91(X1, X2, X3, X4) -> a__U91#(mark X1, X2, X3, X4), a__U71#(tt(), L) -> a__length# mark L, a__U71#(tt(), L) -> mark# L, a__U91#(tt(), IL, M, N) -> mark# N, a__and#(tt(), X) -> mark# X, a__isNatIListKind# cons(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind# cons(V1, V2) -> a__isNatKind# V1, a__isNatIListKind# take(V1, V2) -> a__and#(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind# take(V1, V2) -> a__isNatKind# V1, a__isNatKind# s V1 -> a__isNatKind# V1, a__isNatKind# length V1 -> a__isNatIListKind# V1, a__take#(0(), IL) -> a__isNatIList# IL, a__take#(0(), IL) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__take#(s M, cons(N, IL)) -> a__isNatIList# IL, a__take#(s M, cons(N, IL)) -> a__U91#(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N), a__take#(s M, cons(N, IL)) -> a__and#(a__isNatIList IL, isNatIListKind IL), a__take#(s M, cons(N, IL)) -> a__and#(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N)))} Weak: { a__zeros() -> cons(0(), zeros()), a__zeros() -> zeros(), a__U12 X -> U12 X, a__U12 tt() -> tt(), a__isNatList X -> isNatList X, a__isNatList cons(V1, V2) -> a__U51(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatList nil() -> tt(), a__isNatList take(V1, V2) -> a__U61(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__U11(X1, X2) -> U11(X1, X2), a__U11(tt(), V1) -> a__U12 a__isNatList V1, a__U22 X -> U22 X, a__U22 tt() -> tt(), a__isNat X -> isNat X, a__isNat 0() -> tt(), a__isNat s V1 -> a__U21(a__isNatKind V1, V1), a__isNat length V1 -> a__U11(a__isNatIListKind V1, V1), a__U21(X1, X2) -> U21(X1, X2), a__U21(tt(), V1) -> a__U22 a__isNat V1, a__U32 X -> U32 X, a__U32 tt() -> tt(), a__U31(X1, X2) -> U31(X1, X2), a__U31(tt(), V) -> a__U32 a__isNatList V, a__U42(X1, X2) -> U42(X1, X2), a__U42(tt(), V2) -> a__U43 a__isNatIList V2, a__U41(X1, X2, X3) -> U41(X1, X2, X3), a__U41(tt(), V1, V2) -> a__U42(a__isNat V1, V2), a__U43 X -> U43 X, a__U43 tt() -> tt(), a__isNatIList V -> a__U31(a__isNatIListKind V, V), a__isNatIList X -> isNatIList X, a__isNatIList cons(V1, V2) -> a__U41(a__and(a__isNatKind V1, isNatIListKind V2), V1, V2), a__isNatIList zeros() -> tt(), a__U52(X1, X2) -> U52(X1, X2), a__U52(tt(), V2) -> a__U53 a__isNatList V2, a__U51(X1, X2, X3) -> U51(X1, X2, X3), a__U51(tt(), V1, V2) -> a__U52(a__isNat V1, V2), a__U53 X -> U53 X, a__U53 tt() -> tt(), a__U62(X1, X2) -> U62(X1, X2), a__U62(tt(), V2) -> a__U63 a__isNatIList V2, a__U61(X1, X2, X3) -> U61(X1, X2, X3), a__U61(tt(), V1, V2) -> a__U62(a__isNat V1, V2), a__U63 X -> U63 X, a__U63 tt() -> tt(), a__length X -> length X, a__length cons(N, L) -> a__U71(a__and(a__and(a__isNatList L, isNatIListKind L), and(isNat N, isNatKind N)), L), a__length nil() -> 0(), mark cons(X1, X2) -> cons(mark X1, X2), mark 0() -> 0(), mark zeros() -> a__zeros(), mark tt() -> tt(), mark s X -> s mark X, mark nil() -> nil(), mark take(X1, X2) -> a__take(mark X1, mark X2), mark length X -> a__length mark X, mark isNatIListKind X -> a__isNatIListKind X, mark and(X1, X2) -> a__and(mark X1, X2), mark isNat X -> a__isNat X, mark isNatKind X -> a__isNatKind X, mark U11(X1, X2) -> a__U11(mark X1, X2), mark U12 X -> a__U12 mark X, mark isNatList X -> a__isNatList X, mark U21(X1, X2) -> a__U21(mark X1, X2), mark U22 X -> a__U22 mark X, mark U31(X1, X2) -> a__U31(mark X1, X2), mark U32 X -> a__U32 mark X, mark U41(X1, X2, X3) -> a__U41(mark X1, X2, X3), mark U42(X1, X2) -> a__U42(mark X1, X2), mark U43 X -> a__U43 mark X, mark isNatIList X -> a__isNatIList X, mark U51(X1, X2, X3) -> a__U51(mark X1, X2, X3), mark U52(X1, X2) -> a__U52(mark X1, X2), mark U53 X -> a__U53 mark X, mark U61(X1, X2, X3) -> a__U61(mark X1, X2, X3), mark U62(X1, X2) -> a__U62(mark X1, X2), mark U63 X -> a__U63 mark X, mark U71(X1, X2) -> a__U71(mark X1, X2), mark U81 X -> a__U81 mark X, mark U91(X1, X2, X3, X4) -> a__U91(mark X1, X2, X3, X4), a__U71(X1, X2) -> U71(X1, X2), a__U71(tt(), L) -> s a__length mark L, a__U81 X -> U81 X, a__U81 tt() -> nil(), a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4), a__U91(tt(), IL, M, N) -> cons(mark N, take(M, IL)), a__and(X1, X2) -> and(X1, X2), a__and(tt(), X) -> mark X, a__isNatIListKind X -> isNatIListKind X, a__isNatIListKind cons(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatIListKind zeros() -> tt(), a__isNatIListKind nil() -> tt(), a__isNatIListKind take(V1, V2) -> a__and(a__isNatKind V1, isNatIListKind V2), a__isNatKind X -> isNatKind X, a__isNatKind 0() -> tt(), a__isNatKind s V1 -> a__isNatKind V1, a__isNatKind length V1 -> a__isNatIListKind V1, a__take(X1, X2) -> take(X1, X2), a__take(0(), IL) -> a__U81 a__and(a__isNatIList IL, isNatIListKind IL), a__take(s M, cons(N, IL)) -> a__U91(a__and(a__and(a__isNatIList IL, isNatIListKind IL), and(and(isNat M, isNatKind M), and(isNat N, isNatKind N))), IL, M, N)} Open