MAYBE 1007.28/297.16 MAYBE 1007.28/297.16 1007.28/297.16 We are left with following problem, upon which TcT provides the 1007.28/297.16 certificate MAYBE. 1007.28/297.16 1007.28/297.16 Strict Trs: 1007.28/297.16 { a__zeros() -> cons(0(), zeros()) 1007.28/297.16 , a__zeros() -> zeros() 1007.28/297.16 , a__U11(X1, X2) -> U11(X1, X2) 1007.28/297.16 , a__U11(tt(), V1) -> a__U12(a__isNatList(V1)) 1007.28/297.16 , a__U12(X) -> U12(X) 1007.28/297.16 , a__U12(tt()) -> tt() 1007.28/297.16 , a__isNatList(X) -> isNatList(X) 1007.28/297.16 , a__isNatList(cons(V1, V2)) -> 1007.28/297.16 a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.16 , a__isNatList(nil()) -> tt() 1007.28/297.16 , a__isNatList(take(V1, V2)) -> 1007.28/297.16 a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.16 , a__U21(X1, X2) -> U21(X1, X2) 1007.28/297.16 , a__U21(tt(), V1) -> a__U22(a__isNat(V1)) 1007.28/297.16 , a__U22(X) -> U22(X) 1007.28/297.16 , a__U22(tt()) -> tt() 1007.28/297.16 , a__isNat(X) -> isNat(X) 1007.28/297.16 , a__isNat(0()) -> tt() 1007.28/297.16 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1007.28/297.16 , a__isNat(length(V1)) -> a__U11(a__isNatIListKind(V1), V1) 1007.28/297.16 , a__U31(X1, X2) -> U31(X1, X2) 1007.28/297.16 , a__U31(tt(), V) -> a__U32(a__isNatList(V)) 1007.28/297.16 , a__U32(X) -> U32(X) 1007.28/297.16 , a__U32(tt()) -> tt() 1007.28/297.16 , a__U41(X1, X2, X3) -> U41(X1, X2, X3) 1007.28/297.16 , a__U41(tt(), V1, V2) -> a__U42(a__isNat(V1), V2) 1007.28/297.16 , a__U42(X1, X2) -> U42(X1, X2) 1007.28/297.16 , a__U42(tt(), V2) -> a__U43(a__isNatIList(V2)) 1007.28/297.16 , a__U43(X) -> U43(X) 1007.28/297.16 , a__U43(tt()) -> tt() 1007.28/297.16 , a__isNatIList(V) -> a__U31(a__isNatIListKind(V), V) 1007.28/297.16 , a__isNatIList(X) -> isNatIList(X) 1007.28/297.16 , a__isNatIList(cons(V1, V2)) -> 1007.28/297.16 a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.16 , a__isNatIList(zeros()) -> tt() 1007.28/297.16 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1007.28/297.16 , a__U51(tt(), V1, V2) -> a__U52(a__isNat(V1), V2) 1007.28/297.16 , a__U52(X1, X2) -> U52(X1, X2) 1007.28/297.16 , a__U52(tt(), V2) -> a__U53(a__isNatList(V2)) 1007.28/297.16 , a__U53(X) -> U53(X) 1007.28/297.16 , a__U53(tt()) -> tt() 1007.28/297.16 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 1007.28/297.16 , a__U61(tt(), V1, V2) -> a__U62(a__isNat(V1), V2) 1007.28/297.16 , a__U62(X1, X2) -> U62(X1, X2) 1007.28/297.16 , a__U62(tt(), V2) -> a__U63(a__isNatIList(V2)) 1007.28/297.16 , a__U63(X) -> U63(X) 1007.28/297.16 , a__U63(tt()) -> tt() 1007.28/297.16 , a__U71(X1, X2) -> U71(X1, X2) 1007.28/297.16 , a__U71(tt(), L) -> s(a__length(mark(L))) 1007.28/297.16 , a__length(X) -> length(X) 1007.28/297.16 , a__length(cons(N, L)) -> 1007.28/297.16 a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.16 and(isNat(N), isNatKind(N))), 1007.28/297.16 L) 1007.28/297.16 , a__length(nil()) -> 0() 1007.28/297.16 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1007.28/297.16 , mark(0()) -> 0() 1007.28/297.16 , mark(zeros()) -> a__zeros() 1007.28/297.16 , mark(tt()) -> tt() 1007.28/297.16 , mark(s(X)) -> s(mark(X)) 1007.28/297.16 , mark(nil()) -> nil() 1007.28/297.16 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1007.28/297.16 , mark(length(X)) -> a__length(mark(X)) 1007.28/297.16 , mark(isNatIListKind(X)) -> a__isNatIListKind(X) 1007.28/297.16 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1007.28/297.16 , mark(isNat(X)) -> a__isNat(X) 1007.28/297.16 , mark(isNatKind(X)) -> a__isNatKind(X) 1007.28/297.16 , mark(U11(X1, X2)) -> a__U11(mark(X1), X2) 1007.28/297.16 , mark(U12(X)) -> a__U12(mark(X)) 1007.28/297.16 , mark(isNatList(X)) -> a__isNatList(X) 1007.28/297.16 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1007.28/297.16 , mark(U22(X)) -> a__U22(mark(X)) 1007.28/297.16 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1007.28/297.16 , mark(U32(X)) -> a__U32(mark(X)) 1007.28/297.16 , mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3) 1007.28/297.16 , mark(U42(X1, X2)) -> a__U42(mark(X1), X2) 1007.28/297.16 , mark(U43(X)) -> a__U43(mark(X)) 1007.28/297.16 , mark(isNatIList(X)) -> a__isNatIList(X) 1007.28/297.16 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1007.28/297.16 , mark(U52(X1, X2)) -> a__U52(mark(X1), X2) 1007.28/297.16 , mark(U53(X)) -> a__U53(mark(X)) 1007.28/297.16 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 1007.28/297.16 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 1007.28/297.16 , mark(U63(X)) -> a__U63(mark(X)) 1007.28/297.16 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1007.28/297.16 , mark(U81(X)) -> a__U81(mark(X)) 1007.28/297.16 , mark(U91(X1, X2, X3, X4)) -> a__U91(mark(X1), X2, X3, X4) 1007.28/297.16 , a__U81(X) -> U81(X) 1007.28/297.16 , a__U81(tt()) -> nil() 1007.28/297.16 , a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4) 1007.28/297.16 , a__U91(tt(), IL, M, N) -> cons(mark(N), take(M, IL)) 1007.28/297.16 , a__and(X1, X2) -> and(X1, X2) 1007.28/297.16 , a__and(tt(), X) -> mark(X) 1007.28/297.16 , a__isNatIListKind(X) -> isNatIListKind(X) 1007.28/297.16 , a__isNatIListKind(cons(V1, V2)) -> 1007.28/297.16 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.16 , a__isNatIListKind(zeros()) -> tt() 1007.28/297.16 , a__isNatIListKind(nil()) -> tt() 1007.28/297.16 , a__isNatIListKind(take(V1, V2)) -> 1007.28/297.16 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.16 , a__isNatKind(X) -> isNatKind(X) 1007.28/297.16 , a__isNatKind(0()) -> tt() 1007.28/297.16 , a__isNatKind(s(V1)) -> a__isNatKind(V1) 1007.28/297.16 , a__isNatKind(length(V1)) -> a__isNatIListKind(V1) 1007.28/297.16 , a__take(X1, X2) -> take(X1, X2) 1007.28/297.16 , a__take(0(), IL) -> 1007.28/297.16 a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL))) 1007.28/297.16 , a__take(s(M), cons(N, IL)) -> 1007.28/297.16 a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.16 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.16 IL, 1007.28/297.16 M, 1007.28/297.16 N) } 1007.28/297.16 Obligation: 1007.28/297.16 runtime complexity 1007.28/297.16 Answer: 1007.28/297.16 MAYBE 1007.28/297.16 1007.28/297.16 None of the processors succeeded. 1007.28/297.16 1007.28/297.16 Details of failed attempt(s): 1007.28/297.16 ----------------------------- 1007.28/297.16 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1007.28/297.16 following reason: 1007.28/297.16 1007.28/297.16 Computation stopped due to timeout after 297.0 seconds. 1007.28/297.16 1007.28/297.16 2) 'Best' failed due to the following reason: 1007.28/297.16 1007.28/297.16 None of the processors succeeded. 1007.28/297.16 1007.28/297.16 Details of failed attempt(s): 1007.28/297.16 ----------------------------- 1007.28/297.16 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1007.28/297.16 seconds)' failed due to the following reason: 1007.28/297.16 1007.28/297.16 Computation stopped due to timeout after 148.0 seconds. 1007.28/297.16 1007.28/297.16 2) 'Best' failed due to the following reason: 1007.28/297.16 1007.28/297.16 None of the processors succeeded. 1007.28/297.16 1007.28/297.16 Details of failed attempt(s): 1007.28/297.16 ----------------------------- 1007.28/297.16 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1007.28/297.16 to the following reason: 1007.28/297.16 1007.28/297.16 The processor is inapplicable, reason: 1007.28/297.16 Processor only applicable for innermost runtime complexity analysis 1007.28/297.16 1007.28/297.16 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1007.28/297.16 following reason: 1007.28/297.16 1007.28/297.16 The processor is inapplicable, reason: 1007.28/297.16 Processor only applicable for innermost runtime complexity analysis 1007.28/297.16 1007.28/297.16 1007.28/297.16 3) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1007.28/297.16 failed due to the following reason: 1007.28/297.16 1007.28/297.16 None of the processors succeeded. 1007.28/297.16 1007.28/297.16 Details of failed attempt(s): 1007.28/297.16 ----------------------------- 1007.28/297.16 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1007.28/297.16 failed due to the following reason: 1007.28/297.16 1007.28/297.16 match-boundness of the problem could not be verified. 1007.28/297.16 1007.28/297.16 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1007.28/297.16 failed due to the following reason: 1007.28/297.16 1007.28/297.16 match-boundness of the problem could not be verified. 1007.28/297.16 1007.28/297.16 1007.28/297.16 1007.28/297.16 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1007.28/297.16 the following reason: 1007.28/297.16 1007.28/297.16 We add the following weak dependency pairs: 1007.28/297.16 1007.28/297.16 Strict DPs: 1007.28/297.16 { a__zeros^#() -> c_1() 1007.28/297.16 , a__zeros^#() -> c_2() 1007.28/297.16 , a__U11^#(X1, X2) -> c_3(X1, X2) 1007.28/297.16 , a__U11^#(tt(), V1) -> c_4(a__U12^#(a__isNatList(V1))) 1007.28/297.16 , a__U12^#(X) -> c_5(X) 1007.28/297.16 , a__U12^#(tt()) -> c_6() 1007.28/297.16 , a__isNatList^#(X) -> c_7(X) 1007.28/297.16 , a__isNatList^#(cons(V1, V2)) -> 1007.28/297.16 c_8(a__U51^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1007.28/297.16 , a__isNatList^#(nil()) -> c_9() 1007.28/297.16 , a__isNatList^#(take(V1, V2)) -> 1007.28/297.16 c_10(a__U61^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.16 V1, 1007.28/297.16 V2)) 1007.28/297.16 , a__U51^#(X1, X2, X3) -> c_33(X1, X2, X3) 1007.28/297.16 , a__U51^#(tt(), V1, V2) -> c_34(a__U52^#(a__isNat(V1), V2)) 1007.28/297.16 , a__U61^#(X1, X2, X3) -> c_39(X1, X2, X3) 1007.28/297.16 , a__U61^#(tt(), V1, V2) -> c_40(a__U62^#(a__isNat(V1), V2)) 1007.28/297.16 , a__U21^#(X1, X2) -> c_11(X1, X2) 1007.28/297.16 , a__U21^#(tt(), V1) -> c_12(a__U22^#(a__isNat(V1))) 1007.28/297.16 , a__U22^#(X) -> c_13(X) 1007.28/297.16 , a__U22^#(tt()) -> c_14() 1007.28/297.16 , a__isNat^#(X) -> c_15(X) 1007.28/297.16 , a__isNat^#(0()) -> c_16() 1007.28/297.16 , a__isNat^#(s(V1)) -> c_17(a__U21^#(a__isNatKind(V1), V1)) 1007.28/297.16 , a__isNat^#(length(V1)) -> 1007.28/297.16 c_18(a__U11^#(a__isNatIListKind(V1), V1)) 1007.28/297.16 , a__U31^#(X1, X2) -> c_19(X1, X2) 1007.28/297.16 , a__U31^#(tt(), V) -> c_20(a__U32^#(a__isNatList(V))) 1007.28/297.16 , a__U32^#(X) -> c_21(X) 1007.28/297.16 , a__U32^#(tt()) -> c_22() 1007.28/297.16 , a__U41^#(X1, X2, X3) -> c_23(X1, X2, X3) 1007.28/297.16 , a__U41^#(tt(), V1, V2) -> c_24(a__U42^#(a__isNat(V1), V2)) 1007.28/297.16 , a__U42^#(X1, X2) -> c_25(X1, X2) 1007.28/297.16 , a__U42^#(tt(), V2) -> c_26(a__U43^#(a__isNatIList(V2))) 1007.28/297.16 , a__U43^#(X) -> c_27(X) 1007.28/297.16 , a__U43^#(tt()) -> c_28() 1007.28/297.16 , a__isNatIList^#(V) -> c_29(a__U31^#(a__isNatIListKind(V), V)) 1007.28/297.16 , a__isNatIList^#(X) -> c_30(X) 1007.28/297.16 , a__isNatIList^#(cons(V1, V2)) -> 1007.28/297.16 c_31(a__U41^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.16 V1, 1007.28/297.16 V2)) 1007.28/297.16 , a__isNatIList^#(zeros()) -> c_32() 1007.28/297.16 , a__U52^#(X1, X2) -> c_35(X1, X2) 1007.28/297.16 , a__U52^#(tt(), V2) -> c_36(a__U53^#(a__isNatList(V2))) 1007.28/297.16 , a__U53^#(X) -> c_37(X) 1007.28/297.16 , a__U53^#(tt()) -> c_38() 1007.28/297.16 , a__U62^#(X1, X2) -> c_41(X1, X2) 1007.28/297.16 , a__U62^#(tt(), V2) -> c_42(a__U63^#(a__isNatIList(V2))) 1007.28/297.16 , a__U63^#(X) -> c_43(X) 1007.28/297.16 , a__U63^#(tt()) -> c_44() 1007.28/297.16 , a__U71^#(X1, X2) -> c_45(X1, X2) 1007.28/297.16 , a__U71^#(tt(), L) -> c_46(a__length^#(mark(L))) 1007.28/297.16 , a__length^#(X) -> c_47(X) 1007.28/297.16 , a__length^#(cons(N, L)) -> 1007.28/297.16 c_48(a__U71^#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.16 and(isNat(N), isNatKind(N))), 1007.28/297.16 L)) 1007.28/297.16 , a__length^#(nil()) -> c_49() 1007.28/297.16 , mark^#(cons(X1, X2)) -> c_50(mark^#(X1), X2) 1007.28/297.16 , mark^#(0()) -> c_51() 1007.28/297.16 , mark^#(zeros()) -> c_52(a__zeros^#()) 1007.28/297.16 , mark^#(tt()) -> c_53() 1007.28/297.16 , mark^#(s(X)) -> c_54(mark^#(X)) 1007.28/297.16 , mark^#(nil()) -> c_55() 1007.28/297.16 , mark^#(take(X1, X2)) -> c_56(a__take^#(mark(X1), mark(X2))) 1007.28/297.16 , mark^#(length(X)) -> c_57(a__length^#(mark(X))) 1007.28/297.16 , mark^#(isNatIListKind(X)) -> c_58(a__isNatIListKind^#(X)) 1007.28/297.16 , mark^#(and(X1, X2)) -> c_59(a__and^#(mark(X1), X2)) 1007.28/297.16 , mark^#(isNat(X)) -> c_60(a__isNat^#(X)) 1007.28/297.16 , mark^#(isNatKind(X)) -> c_61(a__isNatKind^#(X)) 1007.28/297.16 , mark^#(U11(X1, X2)) -> c_62(a__U11^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U12(X)) -> c_63(a__U12^#(mark(X))) 1007.28/297.16 , mark^#(isNatList(X)) -> c_64(a__isNatList^#(X)) 1007.28/297.16 , mark^#(U21(X1, X2)) -> c_65(a__U21^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U22(X)) -> c_66(a__U22^#(mark(X))) 1007.28/297.16 , mark^#(U31(X1, X2)) -> c_67(a__U31^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U32(X)) -> c_68(a__U32^#(mark(X))) 1007.28/297.16 , mark^#(U41(X1, X2, X3)) -> c_69(a__U41^#(mark(X1), X2, X3)) 1007.28/297.16 , mark^#(U42(X1, X2)) -> c_70(a__U42^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U43(X)) -> c_71(a__U43^#(mark(X))) 1007.28/297.16 , mark^#(isNatIList(X)) -> c_72(a__isNatIList^#(X)) 1007.28/297.16 , mark^#(U51(X1, X2, X3)) -> c_73(a__U51^#(mark(X1), X2, X3)) 1007.28/297.16 , mark^#(U52(X1, X2)) -> c_74(a__U52^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U53(X)) -> c_75(a__U53^#(mark(X))) 1007.28/297.16 , mark^#(U61(X1, X2, X3)) -> c_76(a__U61^#(mark(X1), X2, X3)) 1007.28/297.16 , mark^#(U62(X1, X2)) -> c_77(a__U62^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U63(X)) -> c_78(a__U63^#(mark(X))) 1007.28/297.16 , mark^#(U71(X1, X2)) -> c_79(a__U71^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U81(X)) -> c_80(a__U81^#(mark(X))) 1007.28/297.16 , mark^#(U91(X1, X2, X3, X4)) -> 1007.28/297.16 c_81(a__U91^#(mark(X1), X2, X3, X4)) 1007.28/297.16 , a__take^#(X1, X2) -> c_97(X1, X2) 1007.28/297.16 , a__take^#(0(), IL) -> 1007.28/297.16 c_98(a__U81^#(a__and(a__isNatIList(IL), isNatIListKind(IL)))) 1007.28/297.16 , a__take^#(s(M), cons(N, IL)) -> 1007.28/297.16 c_99(a__U91^#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.16 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.16 IL, 1007.28/297.16 M, 1007.28/297.16 N)) 1007.28/297.16 , a__isNatIListKind^#(X) -> c_88(X) 1007.28/297.16 , a__isNatIListKind^#(cons(V1, V2)) -> 1007.28/297.16 c_89(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.16 , a__isNatIListKind^#(zeros()) -> c_90() 1007.28/297.16 , a__isNatIListKind^#(nil()) -> c_91() 1007.28/297.16 , a__isNatIListKind^#(take(V1, V2)) -> 1007.28/297.16 c_92(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.16 , a__and^#(X1, X2) -> c_86(X1, X2) 1007.28/297.16 , a__and^#(tt(), X) -> c_87(mark^#(X)) 1007.28/297.16 , a__isNatKind^#(X) -> c_93(X) 1007.28/297.16 , a__isNatKind^#(0()) -> c_94() 1007.28/297.16 , a__isNatKind^#(s(V1)) -> c_95(a__isNatKind^#(V1)) 1007.28/297.16 , a__isNatKind^#(length(V1)) -> c_96(a__isNatIListKind^#(V1)) 1007.28/297.16 , a__U81^#(X) -> c_82(X) 1007.28/297.16 , a__U81^#(tt()) -> c_83() 1007.28/297.16 , a__U91^#(X1, X2, X3, X4) -> c_84(X1, X2, X3, X4) 1007.28/297.16 , a__U91^#(tt(), IL, M, N) -> c_85(mark^#(N), M, IL) } 1007.28/297.16 1007.28/297.16 and mark the set of starting terms. 1007.28/297.16 1007.28/297.16 We are left with following problem, upon which TcT provides the 1007.28/297.16 certificate MAYBE. 1007.28/297.16 1007.28/297.16 Strict DPs: 1007.28/297.16 { a__zeros^#() -> c_1() 1007.28/297.16 , a__zeros^#() -> c_2() 1007.28/297.16 , a__U11^#(X1, X2) -> c_3(X1, X2) 1007.28/297.16 , a__U11^#(tt(), V1) -> c_4(a__U12^#(a__isNatList(V1))) 1007.28/297.16 , a__U12^#(X) -> c_5(X) 1007.28/297.16 , a__U12^#(tt()) -> c_6() 1007.28/297.16 , a__isNatList^#(X) -> c_7(X) 1007.28/297.16 , a__isNatList^#(cons(V1, V2)) -> 1007.28/297.16 c_8(a__U51^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1007.28/297.16 , a__isNatList^#(nil()) -> c_9() 1007.28/297.16 , a__isNatList^#(take(V1, V2)) -> 1007.28/297.16 c_10(a__U61^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.16 V1, 1007.28/297.16 V2)) 1007.28/297.16 , a__U51^#(X1, X2, X3) -> c_33(X1, X2, X3) 1007.28/297.16 , a__U51^#(tt(), V1, V2) -> c_34(a__U52^#(a__isNat(V1), V2)) 1007.28/297.16 , a__U61^#(X1, X2, X3) -> c_39(X1, X2, X3) 1007.28/297.16 , a__U61^#(tt(), V1, V2) -> c_40(a__U62^#(a__isNat(V1), V2)) 1007.28/297.16 , a__U21^#(X1, X2) -> c_11(X1, X2) 1007.28/297.16 , a__U21^#(tt(), V1) -> c_12(a__U22^#(a__isNat(V1))) 1007.28/297.16 , a__U22^#(X) -> c_13(X) 1007.28/297.16 , a__U22^#(tt()) -> c_14() 1007.28/297.16 , a__isNat^#(X) -> c_15(X) 1007.28/297.16 , a__isNat^#(0()) -> c_16() 1007.28/297.16 , a__isNat^#(s(V1)) -> c_17(a__U21^#(a__isNatKind(V1), V1)) 1007.28/297.16 , a__isNat^#(length(V1)) -> 1007.28/297.16 c_18(a__U11^#(a__isNatIListKind(V1), V1)) 1007.28/297.16 , a__U31^#(X1, X2) -> c_19(X1, X2) 1007.28/297.16 , a__U31^#(tt(), V) -> c_20(a__U32^#(a__isNatList(V))) 1007.28/297.16 , a__U32^#(X) -> c_21(X) 1007.28/297.16 , a__U32^#(tt()) -> c_22() 1007.28/297.16 , a__U41^#(X1, X2, X3) -> c_23(X1, X2, X3) 1007.28/297.16 , a__U41^#(tt(), V1, V2) -> c_24(a__U42^#(a__isNat(V1), V2)) 1007.28/297.16 , a__U42^#(X1, X2) -> c_25(X1, X2) 1007.28/297.16 , a__U42^#(tt(), V2) -> c_26(a__U43^#(a__isNatIList(V2))) 1007.28/297.16 , a__U43^#(X) -> c_27(X) 1007.28/297.16 , a__U43^#(tt()) -> c_28() 1007.28/297.16 , a__isNatIList^#(V) -> c_29(a__U31^#(a__isNatIListKind(V), V)) 1007.28/297.16 , a__isNatIList^#(X) -> c_30(X) 1007.28/297.16 , a__isNatIList^#(cons(V1, V2)) -> 1007.28/297.16 c_31(a__U41^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.16 V1, 1007.28/297.16 V2)) 1007.28/297.16 , a__isNatIList^#(zeros()) -> c_32() 1007.28/297.16 , a__U52^#(X1, X2) -> c_35(X1, X2) 1007.28/297.16 , a__U52^#(tt(), V2) -> c_36(a__U53^#(a__isNatList(V2))) 1007.28/297.16 , a__U53^#(X) -> c_37(X) 1007.28/297.16 , a__U53^#(tt()) -> c_38() 1007.28/297.16 , a__U62^#(X1, X2) -> c_41(X1, X2) 1007.28/297.16 , a__U62^#(tt(), V2) -> c_42(a__U63^#(a__isNatIList(V2))) 1007.28/297.16 , a__U63^#(X) -> c_43(X) 1007.28/297.16 , a__U63^#(tt()) -> c_44() 1007.28/297.16 , a__U71^#(X1, X2) -> c_45(X1, X2) 1007.28/297.16 , a__U71^#(tt(), L) -> c_46(a__length^#(mark(L))) 1007.28/297.16 , a__length^#(X) -> c_47(X) 1007.28/297.16 , a__length^#(cons(N, L)) -> 1007.28/297.16 c_48(a__U71^#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.16 and(isNat(N), isNatKind(N))), 1007.28/297.16 L)) 1007.28/297.16 , a__length^#(nil()) -> c_49() 1007.28/297.16 , mark^#(cons(X1, X2)) -> c_50(mark^#(X1), X2) 1007.28/297.16 , mark^#(0()) -> c_51() 1007.28/297.16 , mark^#(zeros()) -> c_52(a__zeros^#()) 1007.28/297.16 , mark^#(tt()) -> c_53() 1007.28/297.16 , mark^#(s(X)) -> c_54(mark^#(X)) 1007.28/297.16 , mark^#(nil()) -> c_55() 1007.28/297.16 , mark^#(take(X1, X2)) -> c_56(a__take^#(mark(X1), mark(X2))) 1007.28/297.16 , mark^#(length(X)) -> c_57(a__length^#(mark(X))) 1007.28/297.16 , mark^#(isNatIListKind(X)) -> c_58(a__isNatIListKind^#(X)) 1007.28/297.16 , mark^#(and(X1, X2)) -> c_59(a__and^#(mark(X1), X2)) 1007.28/297.16 , mark^#(isNat(X)) -> c_60(a__isNat^#(X)) 1007.28/297.16 , mark^#(isNatKind(X)) -> c_61(a__isNatKind^#(X)) 1007.28/297.16 , mark^#(U11(X1, X2)) -> c_62(a__U11^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U12(X)) -> c_63(a__U12^#(mark(X))) 1007.28/297.16 , mark^#(isNatList(X)) -> c_64(a__isNatList^#(X)) 1007.28/297.16 , mark^#(U21(X1, X2)) -> c_65(a__U21^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U22(X)) -> c_66(a__U22^#(mark(X))) 1007.28/297.16 , mark^#(U31(X1, X2)) -> c_67(a__U31^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U32(X)) -> c_68(a__U32^#(mark(X))) 1007.28/297.16 , mark^#(U41(X1, X2, X3)) -> c_69(a__U41^#(mark(X1), X2, X3)) 1007.28/297.16 , mark^#(U42(X1, X2)) -> c_70(a__U42^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U43(X)) -> c_71(a__U43^#(mark(X))) 1007.28/297.16 , mark^#(isNatIList(X)) -> c_72(a__isNatIList^#(X)) 1007.28/297.16 , mark^#(U51(X1, X2, X3)) -> c_73(a__U51^#(mark(X1), X2, X3)) 1007.28/297.16 , mark^#(U52(X1, X2)) -> c_74(a__U52^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U53(X)) -> c_75(a__U53^#(mark(X))) 1007.28/297.16 , mark^#(U61(X1, X2, X3)) -> c_76(a__U61^#(mark(X1), X2, X3)) 1007.28/297.16 , mark^#(U62(X1, X2)) -> c_77(a__U62^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U63(X)) -> c_78(a__U63^#(mark(X))) 1007.28/297.16 , mark^#(U71(X1, X2)) -> c_79(a__U71^#(mark(X1), X2)) 1007.28/297.16 , mark^#(U81(X)) -> c_80(a__U81^#(mark(X))) 1007.28/297.16 , mark^#(U91(X1, X2, X3, X4)) -> 1007.28/297.16 c_81(a__U91^#(mark(X1), X2, X3, X4)) 1007.28/297.16 , a__take^#(X1, X2) -> c_97(X1, X2) 1007.28/297.16 , a__take^#(0(), IL) -> 1007.28/297.16 c_98(a__U81^#(a__and(a__isNatIList(IL), isNatIListKind(IL)))) 1007.28/297.16 , a__take^#(s(M), cons(N, IL)) -> 1007.28/297.16 c_99(a__U91^#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.16 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.16 IL, 1007.28/297.16 M, 1007.28/297.16 N)) 1007.28/297.16 , a__isNatIListKind^#(X) -> c_88(X) 1007.28/297.16 , a__isNatIListKind^#(cons(V1, V2)) -> 1007.28/297.16 c_89(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.16 , a__isNatIListKind^#(zeros()) -> c_90() 1007.28/297.16 , a__isNatIListKind^#(nil()) -> c_91() 1007.28/297.16 , a__isNatIListKind^#(take(V1, V2)) -> 1007.28/297.16 c_92(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.16 , a__and^#(X1, X2) -> c_86(X1, X2) 1007.28/297.16 , a__and^#(tt(), X) -> c_87(mark^#(X)) 1007.28/297.16 , a__isNatKind^#(X) -> c_93(X) 1007.28/297.16 , a__isNatKind^#(0()) -> c_94() 1007.28/297.16 , a__isNatKind^#(s(V1)) -> c_95(a__isNatKind^#(V1)) 1007.28/297.16 , a__isNatKind^#(length(V1)) -> c_96(a__isNatIListKind^#(V1)) 1007.28/297.16 , a__U81^#(X) -> c_82(X) 1007.28/297.16 , a__U81^#(tt()) -> c_83() 1007.28/297.16 , a__U91^#(X1, X2, X3, X4) -> c_84(X1, X2, X3, X4) 1007.28/297.16 , a__U91^#(tt(), IL, M, N) -> c_85(mark^#(N), M, IL) } 1007.28/297.16 Strict Trs: 1007.28/297.16 { a__zeros() -> cons(0(), zeros()) 1007.28/297.16 , a__zeros() -> zeros() 1007.28/297.16 , a__U11(X1, X2) -> U11(X1, X2) 1007.28/297.16 , a__U11(tt(), V1) -> a__U12(a__isNatList(V1)) 1007.28/297.16 , a__U12(X) -> U12(X) 1007.28/297.16 , a__U12(tt()) -> tt() 1007.28/297.16 , a__isNatList(X) -> isNatList(X) 1007.28/297.16 , a__isNatList(cons(V1, V2)) -> 1007.28/297.16 a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.17 , a__isNatList(nil()) -> tt() 1007.28/297.17 , a__isNatList(take(V1, V2)) -> 1007.28/297.17 a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.17 , a__U21(X1, X2) -> U21(X1, X2) 1007.28/297.17 , a__U21(tt(), V1) -> a__U22(a__isNat(V1)) 1007.28/297.17 , a__U22(X) -> U22(X) 1007.28/297.17 , a__U22(tt()) -> tt() 1007.28/297.17 , a__isNat(X) -> isNat(X) 1007.28/297.17 , a__isNat(0()) -> tt() 1007.28/297.17 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1007.28/297.17 , a__isNat(length(V1)) -> a__U11(a__isNatIListKind(V1), V1) 1007.28/297.17 , a__U31(X1, X2) -> U31(X1, X2) 1007.28/297.17 , a__U31(tt(), V) -> a__U32(a__isNatList(V)) 1007.28/297.17 , a__U32(X) -> U32(X) 1007.28/297.17 , a__U32(tt()) -> tt() 1007.28/297.17 , a__U41(X1, X2, X3) -> U41(X1, X2, X3) 1007.28/297.17 , a__U41(tt(), V1, V2) -> a__U42(a__isNat(V1), V2) 1007.28/297.17 , a__U42(X1, X2) -> U42(X1, X2) 1007.28/297.17 , a__U42(tt(), V2) -> a__U43(a__isNatIList(V2)) 1007.28/297.17 , a__U43(X) -> U43(X) 1007.28/297.17 , a__U43(tt()) -> tt() 1007.28/297.17 , a__isNatIList(V) -> a__U31(a__isNatIListKind(V), V) 1007.28/297.17 , a__isNatIList(X) -> isNatIList(X) 1007.28/297.17 , a__isNatIList(cons(V1, V2)) -> 1007.28/297.17 a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.17 , a__isNatIList(zeros()) -> tt() 1007.28/297.17 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1007.28/297.17 , a__U51(tt(), V1, V2) -> a__U52(a__isNat(V1), V2) 1007.28/297.17 , a__U52(X1, X2) -> U52(X1, X2) 1007.28/297.17 , a__U52(tt(), V2) -> a__U53(a__isNatList(V2)) 1007.28/297.17 , a__U53(X) -> U53(X) 1007.28/297.17 , a__U53(tt()) -> tt() 1007.28/297.17 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 1007.28/297.17 , a__U61(tt(), V1, V2) -> a__U62(a__isNat(V1), V2) 1007.28/297.17 , a__U62(X1, X2) -> U62(X1, X2) 1007.28/297.17 , a__U62(tt(), V2) -> a__U63(a__isNatIList(V2)) 1007.28/297.17 , a__U63(X) -> U63(X) 1007.28/297.17 , a__U63(tt()) -> tt() 1007.28/297.17 , a__U71(X1, X2) -> U71(X1, X2) 1007.28/297.17 , a__U71(tt(), L) -> s(a__length(mark(L))) 1007.28/297.17 , a__length(X) -> length(X) 1007.28/297.17 , a__length(cons(N, L)) -> 1007.28/297.17 a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.17 and(isNat(N), isNatKind(N))), 1007.28/297.17 L) 1007.28/297.17 , a__length(nil()) -> 0() 1007.28/297.17 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1007.28/297.17 , mark(0()) -> 0() 1007.28/297.17 , mark(zeros()) -> a__zeros() 1007.28/297.17 , mark(tt()) -> tt() 1007.28/297.17 , mark(s(X)) -> s(mark(X)) 1007.28/297.17 , mark(nil()) -> nil() 1007.28/297.17 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1007.28/297.17 , mark(length(X)) -> a__length(mark(X)) 1007.28/297.17 , mark(isNatIListKind(X)) -> a__isNatIListKind(X) 1007.28/297.17 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1007.28/297.17 , mark(isNat(X)) -> a__isNat(X) 1007.28/297.17 , mark(isNatKind(X)) -> a__isNatKind(X) 1007.28/297.17 , mark(U11(X1, X2)) -> a__U11(mark(X1), X2) 1007.28/297.17 , mark(U12(X)) -> a__U12(mark(X)) 1007.28/297.17 , mark(isNatList(X)) -> a__isNatList(X) 1007.28/297.17 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1007.28/297.17 , mark(U22(X)) -> a__U22(mark(X)) 1007.28/297.17 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1007.28/297.17 , mark(U32(X)) -> a__U32(mark(X)) 1007.28/297.17 , mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3) 1007.28/297.17 , mark(U42(X1, X2)) -> a__U42(mark(X1), X2) 1007.28/297.17 , mark(U43(X)) -> a__U43(mark(X)) 1007.28/297.17 , mark(isNatIList(X)) -> a__isNatIList(X) 1007.28/297.17 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1007.28/297.17 , mark(U52(X1, X2)) -> a__U52(mark(X1), X2) 1007.28/297.17 , mark(U53(X)) -> a__U53(mark(X)) 1007.28/297.17 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 1007.28/297.17 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 1007.28/297.17 , mark(U63(X)) -> a__U63(mark(X)) 1007.28/297.17 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1007.28/297.17 , mark(U81(X)) -> a__U81(mark(X)) 1007.28/297.17 , mark(U91(X1, X2, X3, X4)) -> a__U91(mark(X1), X2, X3, X4) 1007.28/297.17 , a__U81(X) -> U81(X) 1007.28/297.17 , a__U81(tt()) -> nil() 1007.28/297.17 , a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4) 1007.28/297.17 , a__U91(tt(), IL, M, N) -> cons(mark(N), take(M, IL)) 1007.28/297.17 , a__and(X1, X2) -> and(X1, X2) 1007.28/297.17 , a__and(tt(), X) -> mark(X) 1007.28/297.17 , a__isNatIListKind(X) -> isNatIListKind(X) 1007.28/297.17 , a__isNatIListKind(cons(V1, V2)) -> 1007.28/297.17 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.17 , a__isNatIListKind(zeros()) -> tt() 1007.28/297.17 , a__isNatIListKind(nil()) -> tt() 1007.28/297.17 , a__isNatIListKind(take(V1, V2)) -> 1007.28/297.17 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.17 , a__isNatKind(X) -> isNatKind(X) 1007.28/297.17 , a__isNatKind(0()) -> tt() 1007.28/297.17 , a__isNatKind(s(V1)) -> a__isNatKind(V1) 1007.28/297.17 , a__isNatKind(length(V1)) -> a__isNatIListKind(V1) 1007.28/297.17 , a__take(X1, X2) -> take(X1, X2) 1007.28/297.17 , a__take(0(), IL) -> 1007.28/297.17 a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL))) 1007.28/297.17 , a__take(s(M), cons(N, IL)) -> 1007.28/297.17 a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.17 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.17 IL, 1007.28/297.17 M, 1007.28/297.17 N) } 1007.28/297.17 Obligation: 1007.28/297.17 runtime complexity 1007.28/297.17 Answer: 1007.28/297.17 MAYBE 1007.28/297.17 1007.28/297.17 We estimate the number of application of 1007.28/297.17 {1,2,6,9,18,20,26,32,36,40,44,49,51,53,55,87,88,93,97} by 1007.28/297.17 applications of 1007.28/297.17 Pre({1,2,6,9,18,20,26,32,36,40,44,49,51,53,55,87,88,93,97}) = 1007.28/297.17 {3,4,5,7,11,13,15,16,17,19,23,24,25,27,29,30,31,34,37,38,39,41,42,43,45,46,47,50,52,54,57,58,60,61,63,64,66,68,71,72,75,78,80,82,83,85,90,91,92,94,95,96,98,99}. 1007.28/297.17 Here rules are labeled as follows: 1007.28/297.17 1007.28/297.17 DPs: 1007.28/297.17 { 1: a__zeros^#() -> c_1() 1007.28/297.17 , 2: a__zeros^#() -> c_2() 1007.28/297.17 , 3: a__U11^#(X1, X2) -> c_3(X1, X2) 1007.28/297.17 , 4: a__U11^#(tt(), V1) -> c_4(a__U12^#(a__isNatList(V1))) 1007.28/297.17 , 5: a__U12^#(X) -> c_5(X) 1007.28/297.17 , 6: a__U12^#(tt()) -> c_6() 1007.28/297.17 , 7: a__isNatList^#(X) -> c_7(X) 1007.28/297.17 , 8: a__isNatList^#(cons(V1, V2)) -> 1007.28/297.17 c_8(a__U51^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1007.28/297.17 , 9: a__isNatList^#(nil()) -> c_9() 1007.28/297.17 , 10: a__isNatList^#(take(V1, V2)) -> 1007.28/297.17 c_10(a__U61^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.17 V1, 1007.28/297.17 V2)) 1007.28/297.17 , 11: a__U51^#(X1, X2, X3) -> c_33(X1, X2, X3) 1007.28/297.17 , 12: a__U51^#(tt(), V1, V2) -> c_34(a__U52^#(a__isNat(V1), V2)) 1007.28/297.17 , 13: a__U61^#(X1, X2, X3) -> c_39(X1, X2, X3) 1007.28/297.17 , 14: a__U61^#(tt(), V1, V2) -> c_40(a__U62^#(a__isNat(V1), V2)) 1007.28/297.17 , 15: a__U21^#(X1, X2) -> c_11(X1, X2) 1007.28/297.17 , 16: a__U21^#(tt(), V1) -> c_12(a__U22^#(a__isNat(V1))) 1007.28/297.17 , 17: a__U22^#(X) -> c_13(X) 1007.28/297.17 , 18: a__U22^#(tt()) -> c_14() 1007.28/297.17 , 19: a__isNat^#(X) -> c_15(X) 1007.28/297.17 , 20: a__isNat^#(0()) -> c_16() 1007.28/297.17 , 21: a__isNat^#(s(V1)) -> c_17(a__U21^#(a__isNatKind(V1), V1)) 1007.28/297.17 , 22: a__isNat^#(length(V1)) -> 1007.28/297.17 c_18(a__U11^#(a__isNatIListKind(V1), V1)) 1007.28/297.17 , 23: a__U31^#(X1, X2) -> c_19(X1, X2) 1007.28/297.17 , 24: a__U31^#(tt(), V) -> c_20(a__U32^#(a__isNatList(V))) 1007.28/297.17 , 25: a__U32^#(X) -> c_21(X) 1007.28/297.17 , 26: a__U32^#(tt()) -> c_22() 1007.28/297.17 , 27: a__U41^#(X1, X2, X3) -> c_23(X1, X2, X3) 1007.28/297.17 , 28: a__U41^#(tt(), V1, V2) -> c_24(a__U42^#(a__isNat(V1), V2)) 1007.28/297.17 , 29: a__U42^#(X1, X2) -> c_25(X1, X2) 1007.28/297.17 , 30: a__U42^#(tt(), V2) -> c_26(a__U43^#(a__isNatIList(V2))) 1007.28/297.17 , 31: a__U43^#(X) -> c_27(X) 1007.28/297.17 , 32: a__U43^#(tt()) -> c_28() 1007.28/297.17 , 33: a__isNatIList^#(V) -> c_29(a__U31^#(a__isNatIListKind(V), V)) 1007.28/297.17 , 34: a__isNatIList^#(X) -> c_30(X) 1007.28/297.17 , 35: a__isNatIList^#(cons(V1, V2)) -> 1007.28/297.17 c_31(a__U41^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.17 V1, 1007.28/297.17 V2)) 1007.28/297.17 , 36: a__isNatIList^#(zeros()) -> c_32() 1007.28/297.17 , 37: a__U52^#(X1, X2) -> c_35(X1, X2) 1007.28/297.17 , 38: a__U52^#(tt(), V2) -> c_36(a__U53^#(a__isNatList(V2))) 1007.28/297.17 , 39: a__U53^#(X) -> c_37(X) 1007.28/297.17 , 40: a__U53^#(tt()) -> c_38() 1007.28/297.17 , 41: a__U62^#(X1, X2) -> c_41(X1, X2) 1007.28/297.17 , 42: a__U62^#(tt(), V2) -> c_42(a__U63^#(a__isNatIList(V2))) 1007.28/297.17 , 43: a__U63^#(X) -> c_43(X) 1007.28/297.17 , 44: a__U63^#(tt()) -> c_44() 1007.28/297.17 , 45: a__U71^#(X1, X2) -> c_45(X1, X2) 1007.28/297.17 , 46: a__U71^#(tt(), L) -> c_46(a__length^#(mark(L))) 1007.28/297.17 , 47: a__length^#(X) -> c_47(X) 1007.28/297.17 , 48: a__length^#(cons(N, L)) -> 1007.28/297.17 c_48(a__U71^#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.17 and(isNat(N), isNatKind(N))), 1007.28/297.17 L)) 1007.28/297.17 , 49: a__length^#(nil()) -> c_49() 1007.28/297.17 , 50: mark^#(cons(X1, X2)) -> c_50(mark^#(X1), X2) 1007.28/297.17 , 51: mark^#(0()) -> c_51() 1007.28/297.17 , 52: mark^#(zeros()) -> c_52(a__zeros^#()) 1007.28/297.17 , 53: mark^#(tt()) -> c_53() 1007.28/297.17 , 54: mark^#(s(X)) -> c_54(mark^#(X)) 1007.28/297.17 , 55: mark^#(nil()) -> c_55() 1007.28/297.17 , 56: mark^#(take(X1, X2)) -> c_56(a__take^#(mark(X1), mark(X2))) 1007.28/297.17 , 57: mark^#(length(X)) -> c_57(a__length^#(mark(X))) 1007.28/297.17 , 58: mark^#(isNatIListKind(X)) -> c_58(a__isNatIListKind^#(X)) 1007.28/297.17 , 59: mark^#(and(X1, X2)) -> c_59(a__and^#(mark(X1), X2)) 1007.28/297.17 , 60: mark^#(isNat(X)) -> c_60(a__isNat^#(X)) 1007.28/297.17 , 61: mark^#(isNatKind(X)) -> c_61(a__isNatKind^#(X)) 1007.28/297.17 , 62: mark^#(U11(X1, X2)) -> c_62(a__U11^#(mark(X1), X2)) 1007.28/297.17 , 63: mark^#(U12(X)) -> c_63(a__U12^#(mark(X))) 1007.28/297.17 , 64: mark^#(isNatList(X)) -> c_64(a__isNatList^#(X)) 1007.28/297.17 , 65: mark^#(U21(X1, X2)) -> c_65(a__U21^#(mark(X1), X2)) 1007.28/297.17 , 66: mark^#(U22(X)) -> c_66(a__U22^#(mark(X))) 1007.28/297.17 , 67: mark^#(U31(X1, X2)) -> c_67(a__U31^#(mark(X1), X2)) 1007.28/297.17 , 68: mark^#(U32(X)) -> c_68(a__U32^#(mark(X))) 1007.28/297.17 , 69: mark^#(U41(X1, X2, X3)) -> c_69(a__U41^#(mark(X1), X2, X3)) 1007.28/297.17 , 70: mark^#(U42(X1, X2)) -> c_70(a__U42^#(mark(X1), X2)) 1007.28/297.17 , 71: mark^#(U43(X)) -> c_71(a__U43^#(mark(X))) 1007.28/297.17 , 72: mark^#(isNatIList(X)) -> c_72(a__isNatIList^#(X)) 1007.28/297.17 , 73: mark^#(U51(X1, X2, X3)) -> c_73(a__U51^#(mark(X1), X2, X3)) 1007.28/297.17 , 74: mark^#(U52(X1, X2)) -> c_74(a__U52^#(mark(X1), X2)) 1007.28/297.17 , 75: mark^#(U53(X)) -> c_75(a__U53^#(mark(X))) 1007.28/297.17 , 76: mark^#(U61(X1, X2, X3)) -> c_76(a__U61^#(mark(X1), X2, X3)) 1007.28/297.17 , 77: mark^#(U62(X1, X2)) -> c_77(a__U62^#(mark(X1), X2)) 1007.28/297.17 , 78: mark^#(U63(X)) -> c_78(a__U63^#(mark(X))) 1007.28/297.17 , 79: mark^#(U71(X1, X2)) -> c_79(a__U71^#(mark(X1), X2)) 1007.28/297.17 , 80: mark^#(U81(X)) -> c_80(a__U81^#(mark(X))) 1007.28/297.17 , 81: mark^#(U91(X1, X2, X3, X4)) -> 1007.28/297.17 c_81(a__U91^#(mark(X1), X2, X3, X4)) 1007.28/297.17 , 82: a__take^#(X1, X2) -> c_97(X1, X2) 1007.28/297.17 , 83: a__take^#(0(), IL) -> 1007.28/297.17 c_98(a__U81^#(a__and(a__isNatIList(IL), isNatIListKind(IL)))) 1007.28/297.17 , 84: a__take^#(s(M), cons(N, IL)) -> 1007.28/297.17 c_99(a__U91^#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.17 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.17 IL, 1007.28/297.17 M, 1007.28/297.17 N)) 1007.28/297.17 , 85: a__isNatIListKind^#(X) -> c_88(X) 1007.28/297.17 , 86: a__isNatIListKind^#(cons(V1, V2)) -> 1007.28/297.17 c_89(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.17 , 87: a__isNatIListKind^#(zeros()) -> c_90() 1007.28/297.17 , 88: a__isNatIListKind^#(nil()) -> c_91() 1007.28/297.17 , 89: a__isNatIListKind^#(take(V1, V2)) -> 1007.28/297.17 c_92(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.17 , 90: a__and^#(X1, X2) -> c_86(X1, X2) 1007.28/297.17 , 91: a__and^#(tt(), X) -> c_87(mark^#(X)) 1007.28/297.17 , 92: a__isNatKind^#(X) -> c_93(X) 1007.28/297.17 , 93: a__isNatKind^#(0()) -> c_94() 1007.28/297.17 , 94: a__isNatKind^#(s(V1)) -> c_95(a__isNatKind^#(V1)) 1007.28/297.17 , 95: a__isNatKind^#(length(V1)) -> c_96(a__isNatIListKind^#(V1)) 1007.28/297.17 , 96: a__U81^#(X) -> c_82(X) 1007.28/297.17 , 97: a__U81^#(tt()) -> c_83() 1007.28/297.17 , 98: a__U91^#(X1, X2, X3, X4) -> c_84(X1, X2, X3, X4) 1007.28/297.17 , 99: a__U91^#(tt(), IL, M, N) -> c_85(mark^#(N), M, IL) } 1007.28/297.17 1007.28/297.17 We are left with following problem, upon which TcT provides the 1007.28/297.17 certificate MAYBE. 1007.28/297.17 1007.28/297.17 Strict DPs: 1007.28/297.17 { a__U11^#(X1, X2) -> c_3(X1, X2) 1007.28/297.17 , a__U11^#(tt(), V1) -> c_4(a__U12^#(a__isNatList(V1))) 1007.28/297.17 , a__U12^#(X) -> c_5(X) 1007.28/297.17 , a__isNatList^#(X) -> c_7(X) 1007.28/297.17 , a__isNatList^#(cons(V1, V2)) -> 1007.28/297.17 c_8(a__U51^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1007.28/297.17 , a__isNatList^#(take(V1, V2)) -> 1007.28/297.17 c_10(a__U61^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.17 V1, 1007.28/297.17 V2)) 1007.28/297.17 , a__U51^#(X1, X2, X3) -> c_33(X1, X2, X3) 1007.28/297.17 , a__U51^#(tt(), V1, V2) -> c_34(a__U52^#(a__isNat(V1), V2)) 1007.28/297.17 , a__U61^#(X1, X2, X3) -> c_39(X1, X2, X3) 1007.28/297.17 , a__U61^#(tt(), V1, V2) -> c_40(a__U62^#(a__isNat(V1), V2)) 1007.28/297.17 , a__U21^#(X1, X2) -> c_11(X1, X2) 1007.28/297.17 , a__U21^#(tt(), V1) -> c_12(a__U22^#(a__isNat(V1))) 1007.28/297.17 , a__U22^#(X) -> c_13(X) 1007.28/297.17 , a__isNat^#(X) -> c_15(X) 1007.28/297.17 , a__isNat^#(s(V1)) -> c_17(a__U21^#(a__isNatKind(V1), V1)) 1007.28/297.17 , a__isNat^#(length(V1)) -> 1007.28/297.17 c_18(a__U11^#(a__isNatIListKind(V1), V1)) 1007.28/297.17 , a__U31^#(X1, X2) -> c_19(X1, X2) 1007.28/297.17 , a__U31^#(tt(), V) -> c_20(a__U32^#(a__isNatList(V))) 1007.28/297.17 , a__U32^#(X) -> c_21(X) 1007.28/297.17 , a__U41^#(X1, X2, X3) -> c_23(X1, X2, X3) 1007.28/297.17 , a__U41^#(tt(), V1, V2) -> c_24(a__U42^#(a__isNat(V1), V2)) 1007.28/297.17 , a__U42^#(X1, X2) -> c_25(X1, X2) 1007.28/297.17 , a__U42^#(tt(), V2) -> c_26(a__U43^#(a__isNatIList(V2))) 1007.28/297.17 , a__U43^#(X) -> c_27(X) 1007.28/297.17 , a__isNatIList^#(V) -> c_29(a__U31^#(a__isNatIListKind(V), V)) 1007.28/297.17 , a__isNatIList^#(X) -> c_30(X) 1007.28/297.17 , a__isNatIList^#(cons(V1, V2)) -> 1007.28/297.17 c_31(a__U41^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.17 V1, 1007.28/297.17 V2)) 1007.28/297.17 , a__U52^#(X1, X2) -> c_35(X1, X2) 1007.28/297.17 , a__U52^#(tt(), V2) -> c_36(a__U53^#(a__isNatList(V2))) 1007.28/297.17 , a__U53^#(X) -> c_37(X) 1007.28/297.17 , a__U62^#(X1, X2) -> c_41(X1, X2) 1007.28/297.17 , a__U62^#(tt(), V2) -> c_42(a__U63^#(a__isNatIList(V2))) 1007.28/297.17 , a__U63^#(X) -> c_43(X) 1007.28/297.17 , a__U71^#(X1, X2) -> c_45(X1, X2) 1007.28/297.17 , a__U71^#(tt(), L) -> c_46(a__length^#(mark(L))) 1007.28/297.17 , a__length^#(X) -> c_47(X) 1007.28/297.17 , a__length^#(cons(N, L)) -> 1007.28/297.17 c_48(a__U71^#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.17 and(isNat(N), isNatKind(N))), 1007.28/297.17 L)) 1007.28/297.17 , mark^#(cons(X1, X2)) -> c_50(mark^#(X1), X2) 1007.28/297.17 , mark^#(zeros()) -> c_52(a__zeros^#()) 1007.28/297.17 , mark^#(s(X)) -> c_54(mark^#(X)) 1007.28/297.17 , mark^#(take(X1, X2)) -> c_56(a__take^#(mark(X1), mark(X2))) 1007.28/297.17 , mark^#(length(X)) -> c_57(a__length^#(mark(X))) 1007.28/297.17 , mark^#(isNatIListKind(X)) -> c_58(a__isNatIListKind^#(X)) 1007.28/297.17 , mark^#(and(X1, X2)) -> c_59(a__and^#(mark(X1), X2)) 1007.28/297.17 , mark^#(isNat(X)) -> c_60(a__isNat^#(X)) 1007.28/297.17 , mark^#(isNatKind(X)) -> c_61(a__isNatKind^#(X)) 1007.28/297.17 , mark^#(U11(X1, X2)) -> c_62(a__U11^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U12(X)) -> c_63(a__U12^#(mark(X))) 1007.28/297.17 , mark^#(isNatList(X)) -> c_64(a__isNatList^#(X)) 1007.28/297.17 , mark^#(U21(X1, X2)) -> c_65(a__U21^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U22(X)) -> c_66(a__U22^#(mark(X))) 1007.28/297.17 , mark^#(U31(X1, X2)) -> c_67(a__U31^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U32(X)) -> c_68(a__U32^#(mark(X))) 1007.28/297.17 , mark^#(U41(X1, X2, X3)) -> c_69(a__U41^#(mark(X1), X2, X3)) 1007.28/297.17 , mark^#(U42(X1, X2)) -> c_70(a__U42^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U43(X)) -> c_71(a__U43^#(mark(X))) 1007.28/297.17 , mark^#(isNatIList(X)) -> c_72(a__isNatIList^#(X)) 1007.28/297.17 , mark^#(U51(X1, X2, X3)) -> c_73(a__U51^#(mark(X1), X2, X3)) 1007.28/297.17 , mark^#(U52(X1, X2)) -> c_74(a__U52^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U53(X)) -> c_75(a__U53^#(mark(X))) 1007.28/297.17 , mark^#(U61(X1, X2, X3)) -> c_76(a__U61^#(mark(X1), X2, X3)) 1007.28/297.17 , mark^#(U62(X1, X2)) -> c_77(a__U62^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U63(X)) -> c_78(a__U63^#(mark(X))) 1007.28/297.17 , mark^#(U71(X1, X2)) -> c_79(a__U71^#(mark(X1), X2)) 1007.28/297.17 , mark^#(U81(X)) -> c_80(a__U81^#(mark(X))) 1007.28/297.17 , mark^#(U91(X1, X2, X3, X4)) -> 1007.28/297.17 c_81(a__U91^#(mark(X1), X2, X3, X4)) 1007.28/297.17 , a__take^#(X1, X2) -> c_97(X1, X2) 1007.28/297.17 , a__take^#(0(), IL) -> 1007.28/297.17 c_98(a__U81^#(a__and(a__isNatIList(IL), isNatIListKind(IL)))) 1007.28/297.17 , a__take^#(s(M), cons(N, IL)) -> 1007.28/297.17 c_99(a__U91^#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.17 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.17 IL, 1007.28/297.17 M, 1007.28/297.17 N)) 1007.28/297.17 , a__isNatIListKind^#(X) -> c_88(X) 1007.28/297.17 , a__isNatIListKind^#(cons(V1, V2)) -> 1007.28/297.17 c_89(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.17 , a__isNatIListKind^#(take(V1, V2)) -> 1007.28/297.17 c_92(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.17 , a__and^#(X1, X2) -> c_86(X1, X2) 1007.28/297.17 , a__and^#(tt(), X) -> c_87(mark^#(X)) 1007.28/297.17 , a__isNatKind^#(X) -> c_93(X) 1007.28/297.17 , a__isNatKind^#(s(V1)) -> c_95(a__isNatKind^#(V1)) 1007.28/297.17 , a__isNatKind^#(length(V1)) -> c_96(a__isNatIListKind^#(V1)) 1007.28/297.17 , a__U81^#(X) -> c_82(X) 1007.28/297.17 , a__U91^#(X1, X2, X3, X4) -> c_84(X1, X2, X3, X4) 1007.28/297.17 , a__U91^#(tt(), IL, M, N) -> c_85(mark^#(N), M, IL) } 1007.28/297.17 Strict Trs: 1007.28/297.17 { a__zeros() -> cons(0(), zeros()) 1007.28/297.17 , a__zeros() -> zeros() 1007.28/297.17 , a__U11(X1, X2) -> U11(X1, X2) 1007.28/297.17 , a__U11(tt(), V1) -> a__U12(a__isNatList(V1)) 1007.28/297.17 , a__U12(X) -> U12(X) 1007.28/297.17 , a__U12(tt()) -> tt() 1007.28/297.17 , a__isNatList(X) -> isNatList(X) 1007.28/297.17 , a__isNatList(cons(V1, V2)) -> 1007.28/297.17 a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.17 , a__isNatList(nil()) -> tt() 1007.28/297.17 , a__isNatList(take(V1, V2)) -> 1007.28/297.17 a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.17 , a__U21(X1, X2) -> U21(X1, X2) 1007.28/297.17 , a__U21(tt(), V1) -> a__U22(a__isNat(V1)) 1007.28/297.17 , a__U22(X) -> U22(X) 1007.28/297.17 , a__U22(tt()) -> tt() 1007.28/297.17 , a__isNat(X) -> isNat(X) 1007.28/297.17 , a__isNat(0()) -> tt() 1007.28/297.17 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1007.28/297.17 , a__isNat(length(V1)) -> a__U11(a__isNatIListKind(V1), V1) 1007.28/297.17 , a__U31(X1, X2) -> U31(X1, X2) 1007.28/297.17 , a__U31(tt(), V) -> a__U32(a__isNatList(V)) 1007.28/297.17 , a__U32(X) -> U32(X) 1007.28/297.17 , a__U32(tt()) -> tt() 1007.28/297.17 , a__U41(X1, X2, X3) -> U41(X1, X2, X3) 1007.28/297.17 , a__U41(tt(), V1, V2) -> a__U42(a__isNat(V1), V2) 1007.28/297.17 , a__U42(X1, X2) -> U42(X1, X2) 1007.28/297.17 , a__U42(tt(), V2) -> a__U43(a__isNatIList(V2)) 1007.28/297.17 , a__U43(X) -> U43(X) 1007.28/297.17 , a__U43(tt()) -> tt() 1007.28/297.17 , a__isNatIList(V) -> a__U31(a__isNatIListKind(V), V) 1007.28/297.17 , a__isNatIList(X) -> isNatIList(X) 1007.28/297.17 , a__isNatIList(cons(V1, V2)) -> 1007.28/297.17 a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.17 , a__isNatIList(zeros()) -> tt() 1007.28/297.17 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1007.28/297.17 , a__U51(tt(), V1, V2) -> a__U52(a__isNat(V1), V2) 1007.28/297.17 , a__U52(X1, X2) -> U52(X1, X2) 1007.28/297.17 , a__U52(tt(), V2) -> a__U53(a__isNatList(V2)) 1007.28/297.17 , a__U53(X) -> U53(X) 1007.28/297.17 , a__U53(tt()) -> tt() 1007.28/297.17 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 1007.28/297.17 , a__U61(tt(), V1, V2) -> a__U62(a__isNat(V1), V2) 1007.28/297.17 , a__U62(X1, X2) -> U62(X1, X2) 1007.28/297.17 , a__U62(tt(), V2) -> a__U63(a__isNatIList(V2)) 1007.28/297.17 , a__U63(X) -> U63(X) 1007.28/297.17 , a__U63(tt()) -> tt() 1007.28/297.17 , a__U71(X1, X2) -> U71(X1, X2) 1007.28/297.17 , a__U71(tt(), L) -> s(a__length(mark(L))) 1007.28/297.17 , a__length(X) -> length(X) 1007.28/297.17 , a__length(cons(N, L)) -> 1007.28/297.17 a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.17 and(isNat(N), isNatKind(N))), 1007.28/297.17 L) 1007.28/297.17 , a__length(nil()) -> 0() 1007.28/297.17 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1007.28/297.17 , mark(0()) -> 0() 1007.28/297.17 , mark(zeros()) -> a__zeros() 1007.28/297.17 , mark(tt()) -> tt() 1007.28/297.17 , mark(s(X)) -> s(mark(X)) 1007.28/297.17 , mark(nil()) -> nil() 1007.28/297.17 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1007.28/297.17 , mark(length(X)) -> a__length(mark(X)) 1007.28/297.17 , mark(isNatIListKind(X)) -> a__isNatIListKind(X) 1007.28/297.17 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1007.28/297.17 , mark(isNat(X)) -> a__isNat(X) 1007.28/297.17 , mark(isNatKind(X)) -> a__isNatKind(X) 1007.28/297.17 , mark(U11(X1, X2)) -> a__U11(mark(X1), X2) 1007.28/297.17 , mark(U12(X)) -> a__U12(mark(X)) 1007.28/297.17 , mark(isNatList(X)) -> a__isNatList(X) 1007.28/297.17 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1007.28/297.17 , mark(U22(X)) -> a__U22(mark(X)) 1007.28/297.17 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1007.28/297.17 , mark(U32(X)) -> a__U32(mark(X)) 1007.28/297.17 , mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3) 1007.28/297.17 , mark(U42(X1, X2)) -> a__U42(mark(X1), X2) 1007.28/297.17 , mark(U43(X)) -> a__U43(mark(X)) 1007.28/297.17 , mark(isNatIList(X)) -> a__isNatIList(X) 1007.28/297.17 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1007.28/297.17 , mark(U52(X1, X2)) -> a__U52(mark(X1), X2) 1007.28/297.17 , mark(U53(X)) -> a__U53(mark(X)) 1007.28/297.17 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 1007.28/297.17 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 1007.28/297.17 , mark(U63(X)) -> a__U63(mark(X)) 1007.28/297.17 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1007.28/297.17 , mark(U81(X)) -> a__U81(mark(X)) 1007.28/297.17 , mark(U91(X1, X2, X3, X4)) -> a__U91(mark(X1), X2, X3, X4) 1007.28/297.17 , a__U81(X) -> U81(X) 1007.28/297.17 , a__U81(tt()) -> nil() 1007.28/297.17 , a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4) 1007.28/297.17 , a__U91(tt(), IL, M, N) -> cons(mark(N), take(M, IL)) 1007.28/297.17 , a__and(X1, X2) -> and(X1, X2) 1007.28/297.17 , a__and(tt(), X) -> mark(X) 1007.28/297.17 , a__isNatIListKind(X) -> isNatIListKind(X) 1007.28/297.17 , a__isNatIListKind(cons(V1, V2)) -> 1007.28/297.17 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.17 , a__isNatIListKind(zeros()) -> tt() 1007.28/297.17 , a__isNatIListKind(nil()) -> tt() 1007.28/297.17 , a__isNatIListKind(take(V1, V2)) -> 1007.28/297.17 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.17 , a__isNatKind(X) -> isNatKind(X) 1007.28/297.17 , a__isNatKind(0()) -> tt() 1007.28/297.17 , a__isNatKind(s(V1)) -> a__isNatKind(V1) 1007.28/297.17 , a__isNatKind(length(V1)) -> a__isNatIListKind(V1) 1007.28/297.17 , a__take(X1, X2) -> take(X1, X2) 1007.28/297.17 , a__take(0(), IL) -> 1007.28/297.17 a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL))) 1007.28/297.17 , a__take(s(M), cons(N, IL)) -> 1007.28/297.17 a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.17 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.17 IL, 1007.28/297.17 M, 1007.28/297.17 N) } 1007.28/297.17 Weak DPs: 1007.28/297.17 { a__zeros^#() -> c_1() 1007.28/297.17 , a__zeros^#() -> c_2() 1007.28/297.17 , a__U12^#(tt()) -> c_6() 1007.28/297.17 , a__isNatList^#(nil()) -> c_9() 1007.28/297.17 , a__U22^#(tt()) -> c_14() 1007.28/297.17 , a__isNat^#(0()) -> c_16() 1007.28/297.17 , a__U32^#(tt()) -> c_22() 1007.28/297.17 , a__U43^#(tt()) -> c_28() 1007.28/297.17 , a__isNatIList^#(zeros()) -> c_32() 1007.28/297.17 , a__U53^#(tt()) -> c_38() 1007.28/297.17 , a__U63^#(tt()) -> c_44() 1007.28/297.17 , a__length^#(nil()) -> c_49() 1007.28/297.17 , mark^#(0()) -> c_51() 1007.28/297.17 , mark^#(tt()) -> c_53() 1007.28/297.17 , mark^#(nil()) -> c_55() 1007.28/297.17 , a__isNatIListKind^#(zeros()) -> c_90() 1007.28/297.17 , a__isNatIListKind^#(nil()) -> c_91() 1007.28/297.17 , a__isNatKind^#(0()) -> c_94() 1007.28/297.17 , a__U81^#(tt()) -> c_83() } 1007.28/297.17 Obligation: 1007.28/297.17 runtime complexity 1007.28/297.17 Answer: 1007.28/297.17 MAYBE 1007.28/297.17 1007.28/297.17 We estimate the number of application of {39} by applications of 1007.28/297.17 Pre({39}) = 1007.28/297.17 {1,3,4,7,9,11,13,14,17,19,20,22,24,26,28,30,31,33,34,36,38,40,67,70,73,74,75,78,79,80}. 1007.28/297.17 Here rules are labeled as follows: 1007.28/297.17 1007.28/297.17 DPs: 1007.28/297.17 { 1: a__U11^#(X1, X2) -> c_3(X1, X2) 1007.28/297.17 , 2: a__U11^#(tt(), V1) -> c_4(a__U12^#(a__isNatList(V1))) 1007.28/297.17 , 3: a__U12^#(X) -> c_5(X) 1007.28/297.17 , 4: a__isNatList^#(X) -> c_7(X) 1007.28/297.17 , 5: a__isNatList^#(cons(V1, V2)) -> 1007.28/297.17 c_8(a__U51^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1007.28/297.17 , 6: a__isNatList^#(take(V1, V2)) -> 1007.28/297.18 c_10(a__U61^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.18 V1, 1007.28/297.18 V2)) 1007.28/297.18 , 7: a__U51^#(X1, X2, X3) -> c_33(X1, X2, X3) 1007.28/297.18 , 8: a__U51^#(tt(), V1, V2) -> c_34(a__U52^#(a__isNat(V1), V2)) 1007.28/297.18 , 9: a__U61^#(X1, X2, X3) -> c_39(X1, X2, X3) 1007.28/297.18 , 10: a__U61^#(tt(), V1, V2) -> c_40(a__U62^#(a__isNat(V1), V2)) 1007.28/297.18 , 11: a__U21^#(X1, X2) -> c_11(X1, X2) 1007.28/297.18 , 12: a__U21^#(tt(), V1) -> c_12(a__U22^#(a__isNat(V1))) 1007.28/297.18 , 13: a__U22^#(X) -> c_13(X) 1007.28/297.18 , 14: a__isNat^#(X) -> c_15(X) 1007.28/297.18 , 15: a__isNat^#(s(V1)) -> c_17(a__U21^#(a__isNatKind(V1), V1)) 1007.28/297.18 , 16: a__isNat^#(length(V1)) -> 1007.28/297.18 c_18(a__U11^#(a__isNatIListKind(V1), V1)) 1007.28/297.18 , 17: a__U31^#(X1, X2) -> c_19(X1, X2) 1007.28/297.18 , 18: a__U31^#(tt(), V) -> c_20(a__U32^#(a__isNatList(V))) 1007.28/297.18 , 19: a__U32^#(X) -> c_21(X) 1007.28/297.18 , 20: a__U41^#(X1, X2, X3) -> c_23(X1, X2, X3) 1007.28/297.18 , 21: a__U41^#(tt(), V1, V2) -> c_24(a__U42^#(a__isNat(V1), V2)) 1007.28/297.18 , 22: a__U42^#(X1, X2) -> c_25(X1, X2) 1007.28/297.18 , 23: a__U42^#(tt(), V2) -> c_26(a__U43^#(a__isNatIList(V2))) 1007.28/297.18 , 24: a__U43^#(X) -> c_27(X) 1007.28/297.18 , 25: a__isNatIList^#(V) -> c_29(a__U31^#(a__isNatIListKind(V), V)) 1007.28/297.18 , 26: a__isNatIList^#(X) -> c_30(X) 1007.28/297.18 , 27: a__isNatIList^#(cons(V1, V2)) -> 1007.28/297.18 c_31(a__U41^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.18 V1, 1007.28/297.18 V2)) 1007.28/297.18 , 28: a__U52^#(X1, X2) -> c_35(X1, X2) 1007.28/297.18 , 29: a__U52^#(tt(), V2) -> c_36(a__U53^#(a__isNatList(V2))) 1007.28/297.18 , 30: a__U53^#(X) -> c_37(X) 1007.28/297.18 , 31: a__U62^#(X1, X2) -> c_41(X1, X2) 1007.28/297.18 , 32: a__U62^#(tt(), V2) -> c_42(a__U63^#(a__isNatIList(V2))) 1007.28/297.18 , 33: a__U63^#(X) -> c_43(X) 1007.28/297.18 , 34: a__U71^#(X1, X2) -> c_45(X1, X2) 1007.28/297.18 , 35: a__U71^#(tt(), L) -> c_46(a__length^#(mark(L))) 1007.28/297.18 , 36: a__length^#(X) -> c_47(X) 1007.28/297.18 , 37: a__length^#(cons(N, L)) -> 1007.28/297.18 c_48(a__U71^#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.18 and(isNat(N), isNatKind(N))), 1007.28/297.18 L)) 1007.28/297.18 , 38: mark^#(cons(X1, X2)) -> c_50(mark^#(X1), X2) 1007.28/297.18 , 39: mark^#(zeros()) -> c_52(a__zeros^#()) 1007.28/297.18 , 40: mark^#(s(X)) -> c_54(mark^#(X)) 1007.28/297.18 , 41: mark^#(take(X1, X2)) -> c_56(a__take^#(mark(X1), mark(X2))) 1007.28/297.18 , 42: mark^#(length(X)) -> c_57(a__length^#(mark(X))) 1007.28/297.18 , 43: mark^#(isNatIListKind(X)) -> c_58(a__isNatIListKind^#(X)) 1007.28/297.18 , 44: mark^#(and(X1, X2)) -> c_59(a__and^#(mark(X1), X2)) 1007.28/297.18 , 45: mark^#(isNat(X)) -> c_60(a__isNat^#(X)) 1007.28/297.18 , 46: mark^#(isNatKind(X)) -> c_61(a__isNatKind^#(X)) 1007.28/297.18 , 47: mark^#(U11(X1, X2)) -> c_62(a__U11^#(mark(X1), X2)) 1007.28/297.18 , 48: mark^#(U12(X)) -> c_63(a__U12^#(mark(X))) 1007.28/297.18 , 49: mark^#(isNatList(X)) -> c_64(a__isNatList^#(X)) 1007.28/297.18 , 50: mark^#(U21(X1, X2)) -> c_65(a__U21^#(mark(X1), X2)) 1007.28/297.18 , 51: mark^#(U22(X)) -> c_66(a__U22^#(mark(X))) 1007.28/297.18 , 52: mark^#(U31(X1, X2)) -> c_67(a__U31^#(mark(X1), X2)) 1007.28/297.18 , 53: mark^#(U32(X)) -> c_68(a__U32^#(mark(X))) 1007.28/297.18 , 54: mark^#(U41(X1, X2, X3)) -> c_69(a__U41^#(mark(X1), X2, X3)) 1007.28/297.18 , 55: mark^#(U42(X1, X2)) -> c_70(a__U42^#(mark(X1), X2)) 1007.28/297.18 , 56: mark^#(U43(X)) -> c_71(a__U43^#(mark(X))) 1007.28/297.18 , 57: mark^#(isNatIList(X)) -> c_72(a__isNatIList^#(X)) 1007.28/297.18 , 58: mark^#(U51(X1, X2, X3)) -> c_73(a__U51^#(mark(X1), X2, X3)) 1007.28/297.18 , 59: mark^#(U52(X1, X2)) -> c_74(a__U52^#(mark(X1), X2)) 1007.28/297.18 , 60: mark^#(U53(X)) -> c_75(a__U53^#(mark(X))) 1007.28/297.18 , 61: mark^#(U61(X1, X2, X3)) -> c_76(a__U61^#(mark(X1), X2, X3)) 1007.28/297.18 , 62: mark^#(U62(X1, X2)) -> c_77(a__U62^#(mark(X1), X2)) 1007.28/297.18 , 63: mark^#(U63(X)) -> c_78(a__U63^#(mark(X))) 1007.28/297.18 , 64: mark^#(U71(X1, X2)) -> c_79(a__U71^#(mark(X1), X2)) 1007.28/297.18 , 65: mark^#(U81(X)) -> c_80(a__U81^#(mark(X))) 1007.28/297.18 , 66: mark^#(U91(X1, X2, X3, X4)) -> 1007.28/297.18 c_81(a__U91^#(mark(X1), X2, X3, X4)) 1007.28/297.18 , 67: a__take^#(X1, X2) -> c_97(X1, X2) 1007.28/297.18 , 68: a__take^#(0(), IL) -> 1007.28/297.18 c_98(a__U81^#(a__and(a__isNatIList(IL), isNatIListKind(IL)))) 1007.28/297.18 , 69: a__take^#(s(M), cons(N, IL)) -> 1007.28/297.18 c_99(a__U91^#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.18 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.18 IL, 1007.28/297.18 M, 1007.28/297.18 N)) 1007.28/297.18 , 70: a__isNatIListKind^#(X) -> c_88(X) 1007.28/297.18 , 71: a__isNatIListKind^#(cons(V1, V2)) -> 1007.28/297.18 c_89(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.18 , 72: a__isNatIListKind^#(take(V1, V2)) -> 1007.28/297.18 c_92(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.18 , 73: a__and^#(X1, X2) -> c_86(X1, X2) 1007.28/297.18 , 74: a__and^#(tt(), X) -> c_87(mark^#(X)) 1007.28/297.18 , 75: a__isNatKind^#(X) -> c_93(X) 1007.28/297.18 , 76: a__isNatKind^#(s(V1)) -> c_95(a__isNatKind^#(V1)) 1007.28/297.18 , 77: a__isNatKind^#(length(V1)) -> c_96(a__isNatIListKind^#(V1)) 1007.28/297.18 , 78: a__U81^#(X) -> c_82(X) 1007.28/297.18 , 79: a__U91^#(X1, X2, X3, X4) -> c_84(X1, X2, X3, X4) 1007.28/297.18 , 80: a__U91^#(tt(), IL, M, N) -> c_85(mark^#(N), M, IL) 1007.28/297.18 , 81: a__zeros^#() -> c_1() 1007.28/297.18 , 82: a__zeros^#() -> c_2() 1007.28/297.18 , 83: a__U12^#(tt()) -> c_6() 1007.28/297.18 , 84: a__isNatList^#(nil()) -> c_9() 1007.28/297.18 , 85: a__U22^#(tt()) -> c_14() 1007.28/297.18 , 86: a__isNat^#(0()) -> c_16() 1007.28/297.18 , 87: a__U32^#(tt()) -> c_22() 1007.28/297.18 , 88: a__U43^#(tt()) -> c_28() 1007.28/297.18 , 89: a__isNatIList^#(zeros()) -> c_32() 1007.28/297.18 , 90: a__U53^#(tt()) -> c_38() 1007.28/297.18 , 91: a__U63^#(tt()) -> c_44() 1007.28/297.18 , 92: a__length^#(nil()) -> c_49() 1007.28/297.18 , 93: mark^#(0()) -> c_51() 1007.28/297.18 , 94: mark^#(tt()) -> c_53() 1007.28/297.18 , 95: mark^#(nil()) -> c_55() 1007.28/297.18 , 96: a__isNatIListKind^#(zeros()) -> c_90() 1007.28/297.18 , 97: a__isNatIListKind^#(nil()) -> c_91() 1007.28/297.18 , 98: a__isNatKind^#(0()) -> c_94() 1007.28/297.18 , 99: a__U81^#(tt()) -> c_83() } 1007.28/297.18 1007.28/297.18 We are left with following problem, upon which TcT provides the 1007.28/297.18 certificate MAYBE. 1007.28/297.18 1007.28/297.18 Strict DPs: 1007.28/297.18 { a__U11^#(X1, X2) -> c_3(X1, X2) 1007.28/297.18 , a__U11^#(tt(), V1) -> c_4(a__U12^#(a__isNatList(V1))) 1007.28/297.18 , a__U12^#(X) -> c_5(X) 1007.28/297.18 , a__isNatList^#(X) -> c_7(X) 1007.28/297.18 , a__isNatList^#(cons(V1, V2)) -> 1007.28/297.18 c_8(a__U51^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1007.28/297.18 , a__isNatList^#(take(V1, V2)) -> 1007.28/297.18 c_10(a__U61^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.18 V1, 1007.28/297.18 V2)) 1007.28/297.18 , a__U51^#(X1, X2, X3) -> c_33(X1, X2, X3) 1007.28/297.18 , a__U51^#(tt(), V1, V2) -> c_34(a__U52^#(a__isNat(V1), V2)) 1007.28/297.18 , a__U61^#(X1, X2, X3) -> c_39(X1, X2, X3) 1007.28/297.18 , a__U61^#(tt(), V1, V2) -> c_40(a__U62^#(a__isNat(V1), V2)) 1007.28/297.18 , a__U21^#(X1, X2) -> c_11(X1, X2) 1007.28/297.18 , a__U21^#(tt(), V1) -> c_12(a__U22^#(a__isNat(V1))) 1007.28/297.18 , a__U22^#(X) -> c_13(X) 1007.28/297.18 , a__isNat^#(X) -> c_15(X) 1007.28/297.18 , a__isNat^#(s(V1)) -> c_17(a__U21^#(a__isNatKind(V1), V1)) 1007.28/297.18 , a__isNat^#(length(V1)) -> 1007.28/297.18 c_18(a__U11^#(a__isNatIListKind(V1), V1)) 1007.28/297.18 , a__U31^#(X1, X2) -> c_19(X1, X2) 1007.28/297.18 , a__U31^#(tt(), V) -> c_20(a__U32^#(a__isNatList(V))) 1007.28/297.18 , a__U32^#(X) -> c_21(X) 1007.28/297.18 , a__U41^#(X1, X2, X3) -> c_23(X1, X2, X3) 1007.28/297.18 , a__U41^#(tt(), V1, V2) -> c_24(a__U42^#(a__isNat(V1), V2)) 1007.28/297.18 , a__U42^#(X1, X2) -> c_25(X1, X2) 1007.28/297.18 , a__U42^#(tt(), V2) -> c_26(a__U43^#(a__isNatIList(V2))) 1007.28/297.18 , a__U43^#(X) -> c_27(X) 1007.28/297.18 , a__isNatIList^#(V) -> c_29(a__U31^#(a__isNatIListKind(V), V)) 1007.28/297.18 , a__isNatIList^#(X) -> c_30(X) 1007.28/297.18 , a__isNatIList^#(cons(V1, V2)) -> 1007.28/297.18 c_31(a__U41^#(a__and(a__isNatKind(V1), isNatIListKind(V2)), 1007.28/297.18 V1, 1007.28/297.18 V2)) 1007.28/297.18 , a__U52^#(X1, X2) -> c_35(X1, X2) 1007.28/297.18 , a__U52^#(tt(), V2) -> c_36(a__U53^#(a__isNatList(V2))) 1007.28/297.18 , a__U53^#(X) -> c_37(X) 1007.28/297.18 , a__U62^#(X1, X2) -> c_41(X1, X2) 1007.28/297.18 , a__U62^#(tt(), V2) -> c_42(a__U63^#(a__isNatIList(V2))) 1007.28/297.18 , a__U63^#(X) -> c_43(X) 1007.28/297.18 , a__U71^#(X1, X2) -> c_45(X1, X2) 1007.28/297.18 , a__U71^#(tt(), L) -> c_46(a__length^#(mark(L))) 1007.28/297.18 , a__length^#(X) -> c_47(X) 1007.28/297.18 , a__length^#(cons(N, L)) -> 1007.28/297.18 c_48(a__U71^#(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.18 and(isNat(N), isNatKind(N))), 1007.28/297.18 L)) 1007.28/297.18 , mark^#(cons(X1, X2)) -> c_50(mark^#(X1), X2) 1007.28/297.18 , mark^#(s(X)) -> c_54(mark^#(X)) 1007.28/297.18 , mark^#(take(X1, X2)) -> c_56(a__take^#(mark(X1), mark(X2))) 1007.28/297.18 , mark^#(length(X)) -> c_57(a__length^#(mark(X))) 1007.28/297.18 , mark^#(isNatIListKind(X)) -> c_58(a__isNatIListKind^#(X)) 1007.28/297.18 , mark^#(and(X1, X2)) -> c_59(a__and^#(mark(X1), X2)) 1007.28/297.18 , mark^#(isNat(X)) -> c_60(a__isNat^#(X)) 1007.28/297.18 , mark^#(isNatKind(X)) -> c_61(a__isNatKind^#(X)) 1007.28/297.18 , mark^#(U11(X1, X2)) -> c_62(a__U11^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U12(X)) -> c_63(a__U12^#(mark(X))) 1007.28/297.18 , mark^#(isNatList(X)) -> c_64(a__isNatList^#(X)) 1007.28/297.18 , mark^#(U21(X1, X2)) -> c_65(a__U21^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U22(X)) -> c_66(a__U22^#(mark(X))) 1007.28/297.18 , mark^#(U31(X1, X2)) -> c_67(a__U31^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U32(X)) -> c_68(a__U32^#(mark(X))) 1007.28/297.18 , mark^#(U41(X1, X2, X3)) -> c_69(a__U41^#(mark(X1), X2, X3)) 1007.28/297.18 , mark^#(U42(X1, X2)) -> c_70(a__U42^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U43(X)) -> c_71(a__U43^#(mark(X))) 1007.28/297.18 , mark^#(isNatIList(X)) -> c_72(a__isNatIList^#(X)) 1007.28/297.18 , mark^#(U51(X1, X2, X3)) -> c_73(a__U51^#(mark(X1), X2, X3)) 1007.28/297.18 , mark^#(U52(X1, X2)) -> c_74(a__U52^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U53(X)) -> c_75(a__U53^#(mark(X))) 1007.28/297.18 , mark^#(U61(X1, X2, X3)) -> c_76(a__U61^#(mark(X1), X2, X3)) 1007.28/297.18 , mark^#(U62(X1, X2)) -> c_77(a__U62^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U63(X)) -> c_78(a__U63^#(mark(X))) 1007.28/297.18 , mark^#(U71(X1, X2)) -> c_79(a__U71^#(mark(X1), X2)) 1007.28/297.18 , mark^#(U81(X)) -> c_80(a__U81^#(mark(X))) 1007.28/297.18 , mark^#(U91(X1, X2, X3, X4)) -> 1007.28/297.18 c_81(a__U91^#(mark(X1), X2, X3, X4)) 1007.28/297.18 , a__take^#(X1, X2) -> c_97(X1, X2) 1007.28/297.18 , a__take^#(0(), IL) -> 1007.28/297.18 c_98(a__U81^#(a__and(a__isNatIList(IL), isNatIListKind(IL)))) 1007.28/297.18 , a__take^#(s(M), cons(N, IL)) -> 1007.28/297.18 c_99(a__U91^#(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.18 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.18 IL, 1007.28/297.18 M, 1007.28/297.18 N)) 1007.28/297.18 , a__isNatIListKind^#(X) -> c_88(X) 1007.28/297.18 , a__isNatIListKind^#(cons(V1, V2)) -> 1007.28/297.18 c_89(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.18 , a__isNatIListKind^#(take(V1, V2)) -> 1007.28/297.18 c_92(a__and^#(a__isNatKind(V1), isNatIListKind(V2))) 1007.28/297.18 , a__and^#(X1, X2) -> c_86(X1, X2) 1007.28/297.18 , a__and^#(tt(), X) -> c_87(mark^#(X)) 1007.28/297.18 , a__isNatKind^#(X) -> c_93(X) 1007.28/297.18 , a__isNatKind^#(s(V1)) -> c_95(a__isNatKind^#(V1)) 1007.28/297.18 , a__isNatKind^#(length(V1)) -> c_96(a__isNatIListKind^#(V1)) 1007.28/297.18 , a__U81^#(X) -> c_82(X) 1007.28/297.18 , a__U91^#(X1, X2, X3, X4) -> c_84(X1, X2, X3, X4) 1007.28/297.18 , a__U91^#(tt(), IL, M, N) -> c_85(mark^#(N), M, IL) } 1007.28/297.18 Strict Trs: 1007.28/297.18 { a__zeros() -> cons(0(), zeros()) 1007.28/297.18 , a__zeros() -> zeros() 1007.28/297.18 , a__U11(X1, X2) -> U11(X1, X2) 1007.28/297.18 , a__U11(tt(), V1) -> a__U12(a__isNatList(V1)) 1007.28/297.18 , a__U12(X) -> U12(X) 1007.28/297.18 , a__U12(tt()) -> tt() 1007.28/297.18 , a__isNatList(X) -> isNatList(X) 1007.28/297.18 , a__isNatList(cons(V1, V2)) -> 1007.28/297.18 a__U51(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.18 , a__isNatList(nil()) -> tt() 1007.28/297.18 , a__isNatList(take(V1, V2)) -> 1007.28/297.18 a__U61(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.18 , a__U21(X1, X2) -> U21(X1, X2) 1007.28/297.18 , a__U21(tt(), V1) -> a__U22(a__isNat(V1)) 1007.28/297.18 , a__U22(X) -> U22(X) 1007.28/297.18 , a__U22(tt()) -> tt() 1007.28/297.18 , a__isNat(X) -> isNat(X) 1007.28/297.18 , a__isNat(0()) -> tt() 1007.28/297.18 , a__isNat(s(V1)) -> a__U21(a__isNatKind(V1), V1) 1007.28/297.18 , a__isNat(length(V1)) -> a__U11(a__isNatIListKind(V1), V1) 1007.28/297.18 , a__U31(X1, X2) -> U31(X1, X2) 1007.28/297.18 , a__U31(tt(), V) -> a__U32(a__isNatList(V)) 1007.28/297.18 , a__U32(X) -> U32(X) 1007.28/297.18 , a__U32(tt()) -> tt() 1007.28/297.18 , a__U41(X1, X2, X3) -> U41(X1, X2, X3) 1007.28/297.18 , a__U41(tt(), V1, V2) -> a__U42(a__isNat(V1), V2) 1007.28/297.18 , a__U42(X1, X2) -> U42(X1, X2) 1007.28/297.18 , a__U42(tt(), V2) -> a__U43(a__isNatIList(V2)) 1007.28/297.18 , a__U43(X) -> U43(X) 1007.28/297.18 , a__U43(tt()) -> tt() 1007.28/297.18 , a__isNatIList(V) -> a__U31(a__isNatIListKind(V), V) 1007.28/297.18 , a__isNatIList(X) -> isNatIList(X) 1007.28/297.18 , a__isNatIList(cons(V1, V2)) -> 1007.28/297.18 a__U41(a__and(a__isNatKind(V1), isNatIListKind(V2)), V1, V2) 1007.28/297.18 , a__isNatIList(zeros()) -> tt() 1007.28/297.18 , a__U51(X1, X2, X3) -> U51(X1, X2, X3) 1007.28/297.18 , a__U51(tt(), V1, V2) -> a__U52(a__isNat(V1), V2) 1007.28/297.18 , a__U52(X1, X2) -> U52(X1, X2) 1007.28/297.18 , a__U52(tt(), V2) -> a__U53(a__isNatList(V2)) 1007.28/297.18 , a__U53(X) -> U53(X) 1007.28/297.18 , a__U53(tt()) -> tt() 1007.28/297.18 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 1007.28/297.18 , a__U61(tt(), V1, V2) -> a__U62(a__isNat(V1), V2) 1007.28/297.18 , a__U62(X1, X2) -> U62(X1, X2) 1007.28/297.18 , a__U62(tt(), V2) -> a__U63(a__isNatIList(V2)) 1007.28/297.18 , a__U63(X) -> U63(X) 1007.28/297.18 , a__U63(tt()) -> tt() 1007.28/297.18 , a__U71(X1, X2) -> U71(X1, X2) 1007.28/297.18 , a__U71(tt(), L) -> s(a__length(mark(L))) 1007.28/297.18 , a__length(X) -> length(X) 1007.28/297.18 , a__length(cons(N, L)) -> 1007.28/297.18 a__U71(a__and(a__and(a__isNatList(L), isNatIListKind(L)), 1007.28/297.18 and(isNat(N), isNatKind(N))), 1007.28/297.18 L) 1007.28/297.18 , a__length(nil()) -> 0() 1007.28/297.18 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 1007.28/297.18 , mark(0()) -> 0() 1007.28/297.18 , mark(zeros()) -> a__zeros() 1007.28/297.18 , mark(tt()) -> tt() 1007.28/297.18 , mark(s(X)) -> s(mark(X)) 1007.28/297.18 , mark(nil()) -> nil() 1007.28/297.18 , mark(take(X1, X2)) -> a__take(mark(X1), mark(X2)) 1007.28/297.18 , mark(length(X)) -> a__length(mark(X)) 1007.28/297.18 , mark(isNatIListKind(X)) -> a__isNatIListKind(X) 1007.28/297.18 , mark(and(X1, X2)) -> a__and(mark(X1), X2) 1007.28/297.18 , mark(isNat(X)) -> a__isNat(X) 1007.28/297.18 , mark(isNatKind(X)) -> a__isNatKind(X) 1007.28/297.18 , mark(U11(X1, X2)) -> a__U11(mark(X1), X2) 1007.28/297.18 , mark(U12(X)) -> a__U12(mark(X)) 1007.28/297.18 , mark(isNatList(X)) -> a__isNatList(X) 1007.28/297.18 , mark(U21(X1, X2)) -> a__U21(mark(X1), X2) 1007.28/297.18 , mark(U22(X)) -> a__U22(mark(X)) 1007.28/297.18 , mark(U31(X1, X2)) -> a__U31(mark(X1), X2) 1007.28/297.18 , mark(U32(X)) -> a__U32(mark(X)) 1007.28/297.18 , mark(U41(X1, X2, X3)) -> a__U41(mark(X1), X2, X3) 1007.28/297.18 , mark(U42(X1, X2)) -> a__U42(mark(X1), X2) 1007.28/297.18 , mark(U43(X)) -> a__U43(mark(X)) 1007.28/297.18 , mark(isNatIList(X)) -> a__isNatIList(X) 1007.28/297.18 , mark(U51(X1, X2, X3)) -> a__U51(mark(X1), X2, X3) 1007.28/297.18 , mark(U52(X1, X2)) -> a__U52(mark(X1), X2) 1007.28/297.18 , mark(U53(X)) -> a__U53(mark(X)) 1007.28/297.18 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 1007.28/297.18 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 1007.28/297.18 , mark(U63(X)) -> a__U63(mark(X)) 1007.28/297.18 , mark(U71(X1, X2)) -> a__U71(mark(X1), X2) 1007.28/297.18 , mark(U81(X)) -> a__U81(mark(X)) 1007.28/297.18 , mark(U91(X1, X2, X3, X4)) -> a__U91(mark(X1), X2, X3, X4) 1007.28/297.18 , a__U81(X) -> U81(X) 1007.28/297.18 , a__U81(tt()) -> nil() 1007.28/297.18 , a__U91(X1, X2, X3, X4) -> U91(X1, X2, X3, X4) 1007.28/297.18 , a__U91(tt(), IL, M, N) -> cons(mark(N), take(M, IL)) 1007.28/297.18 , a__and(X1, X2) -> and(X1, X2) 1007.28/297.18 , a__and(tt(), X) -> mark(X) 1007.28/297.18 , a__isNatIListKind(X) -> isNatIListKind(X) 1007.28/297.18 , a__isNatIListKind(cons(V1, V2)) -> 1007.28/297.18 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.18 , a__isNatIListKind(zeros()) -> tt() 1007.28/297.18 , a__isNatIListKind(nil()) -> tt() 1007.28/297.18 , a__isNatIListKind(take(V1, V2)) -> 1007.28/297.18 a__and(a__isNatKind(V1), isNatIListKind(V2)) 1007.28/297.18 , a__isNatKind(X) -> isNatKind(X) 1007.28/297.18 , a__isNatKind(0()) -> tt() 1007.28/297.18 , a__isNatKind(s(V1)) -> a__isNatKind(V1) 1007.28/297.18 , a__isNatKind(length(V1)) -> a__isNatIListKind(V1) 1007.28/297.18 , a__take(X1, X2) -> take(X1, X2) 1007.28/297.18 , a__take(0(), IL) -> 1007.28/297.18 a__U81(a__and(a__isNatIList(IL), isNatIListKind(IL))) 1007.28/297.18 , a__take(s(M), cons(N, IL)) -> 1007.28/297.18 a__U91(a__and(a__and(a__isNatIList(IL), isNatIListKind(IL)), 1007.28/297.18 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1007.28/297.18 IL, 1007.28/297.18 M, 1007.28/297.18 N) } 1007.28/297.18 Weak DPs: 1007.28/297.18 { a__zeros^#() -> c_1() 1007.28/297.18 , a__zeros^#() -> c_2() 1007.28/297.18 , a__U12^#(tt()) -> c_6() 1007.28/297.18 , a__isNatList^#(nil()) -> c_9() 1007.28/297.18 , a__U22^#(tt()) -> c_14() 1007.28/297.18 , a__isNat^#(0()) -> c_16() 1007.28/297.18 , a__U32^#(tt()) -> c_22() 1007.28/297.18 , a__U43^#(tt()) -> c_28() 1007.28/297.18 , a__isNatIList^#(zeros()) -> c_32() 1007.28/297.18 , a__U53^#(tt()) -> c_38() 1007.28/297.18 , a__U63^#(tt()) -> c_44() 1007.28/297.18 , a__length^#(nil()) -> c_49() 1007.28/297.18 , mark^#(0()) -> c_51() 1007.28/297.18 , mark^#(zeros()) -> c_52(a__zeros^#()) 1007.28/297.18 , mark^#(tt()) -> c_53() 1007.28/297.18 , mark^#(nil()) -> c_55() 1007.28/297.18 , a__isNatIListKind^#(zeros()) -> c_90() 1007.28/297.18 , a__isNatIListKind^#(nil()) -> c_91() 1007.28/297.18 , a__isNatKind^#(0()) -> c_94() 1007.28/297.18 , a__U81^#(tt()) -> c_83() } 1007.28/297.18 Obligation: 1007.28/297.18 runtime complexity 1007.28/297.18 Answer: 1007.28/297.18 MAYBE 1007.28/297.18 1007.28/297.18 Empty strict component of the problem is NOT empty. 1007.28/297.18 1007.28/297.18 1007.28/297.18 Arrrr.. 1007.52/297.20 EOF