MAYBE We are left with following problem, upon which TcT provides the certificate MAYBE. Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), V1, V2)) -> mark(U102(isNatKind(V1), V1, V2)) , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) , active(U102(tt(), V1, V2)) -> mark(U103(isNatIListKind(V2), V1, V2)) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(s(V1))) -> mark(U81(isNatKind(V1))) , active(isNatKind(length(V1))) -> mark(U71(isNatIListKind(V1))) , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) , active(U103(tt(), V1, V2)) -> mark(U104(isNatIListKind(V2), V1, V2)) , active(isNatIListKind(zeros())) -> mark(tt()) , active(isNatIListKind(cons(V1, V2))) -> mark(U51(isNatKind(V1), V2)) , active(isNatIListKind(nil())) -> mark(tt()) , active(isNatIListKind(take(V1, V2))) -> mark(U61(isNatKind(V1), V2)) , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) , active(U104(tt(), V1, V2)) -> mark(U105(isNat(V1), V2)) , active(U105(X1, X2)) -> U105(active(X1), X2) , active(U105(tt(), V2)) -> mark(U106(isNatIList(V2))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) , active(U106(X)) -> U106(active(X)) , active(U106(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNatKind(V1), V1, V2)) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) , active(U111(X1, X2, X3)) -> U111(active(X1), X2, X3) , active(U111(tt(), L, N)) -> mark(U112(isNatIListKind(L), L, N)) , active(U112(X1, X2, X3)) -> U112(active(X1), X2, X3) , active(U112(tt(), L, N)) -> mark(U113(isNat(N), L, N)) , active(U113(X1, X2, X3)) -> U113(active(X1), X2, X3) , active(U113(tt(), L, N)) -> mark(U114(isNatKind(N), L)) , active(U114(X1, X2)) -> U114(active(X1), X2) , active(U114(tt(), L)) -> mark(s(length(L))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U111(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U91(isNatKind(V1), V1, V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U101(isNatKind(V1), V1, V2)) , active(U121(X1, X2)) -> U121(active(X1), X2) , active(U121(tt(), IL)) -> mark(U122(isNatIListKind(IL))) , active(U122(X)) -> U122(active(X)) , active(U122(tt())) -> mark(nil()) , active(U131(X1, X2, X3, X4)) -> U131(active(X1), X2, X3, X4) , active(U131(tt(), IL, M, N)) -> mark(U132(isNatIListKind(IL), IL, M, N)) , active(U132(X1, X2, X3, X4)) -> U132(active(X1), X2, X3, X4) , active(U132(tt(), IL, M, N)) -> mark(U133(isNat(M), IL, M, N)) , active(U133(X1, X2, X3, X4)) -> U133(active(X1), X2, X3, X4) , active(U133(tt(), IL, M, N)) -> mark(U134(isNatKind(M), IL, M, N)) , active(U134(X1, X2, X3, X4)) -> U134(active(X1), X2, X3, X4) , active(U134(tt(), IL, M, N)) -> mark(U135(isNat(N), IL, M, N)) , active(U135(X1, X2, X3, X4)) -> U135(active(X1), X2, X3, X4) , active(U135(tt(), IL, M, N)) -> mark(U136(isNatKind(N), IL, M, N)) , active(U136(X1, X2, X3, X4)) -> U136(active(X1), X2, X3, X4) , active(U136(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U121(isNatIList(IL), IL)) , active(take(s(M), cons(N, IL))) -> mark(U131(isNatIList(IL), IL, M, N)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isNatList(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isNatIListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isNatIListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIListKind(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X)) -> U71(active(X)) , active(U71(tt())) -> mark(tt()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(tt()) , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) , active(U91(tt(), V1, V2)) -> mark(U92(isNatKind(V1), V1, V2)) , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) , active(U92(tt(), V1, V2)) -> mark(U93(isNatIListKind(V2), V1, V2)) , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) , active(U93(tt(), V1, V2)) -> mark(U94(isNatIListKind(V2), V1, V2)) , active(U94(X1, X2, X3)) -> U94(active(X1), X2, X3) , active(U94(tt(), V1, V2)) -> mark(U95(isNat(V1), V2)) , active(U95(X1, X2)) -> U95(active(X1), X2) , active(U95(tt(), V2)) -> mark(U96(isNatList(V2))) , active(U96(X)) -> U96(active(X)) , active(U96(tt())) -> mark(tt()) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) , U105(mark(X1), X2) -> mark(U105(X1, X2)) , U105(ok(X1), ok(X2)) -> ok(U105(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U106(mark(X)) -> mark(U106(X)) , U106(ok(X)) -> ok(U106(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , U111(mark(X1), X2, X3) -> mark(U111(X1, X2, X3)) , U111(ok(X1), ok(X2), ok(X3)) -> ok(U111(X1, X2, X3)) , U112(mark(X1), X2, X3) -> mark(U112(X1, X2, X3)) , U112(ok(X1), ok(X2), ok(X3)) -> ok(U112(X1, X2, X3)) , U113(mark(X1), X2, X3) -> mark(U113(X1, X2, X3)) , U113(ok(X1), ok(X2), ok(X3)) -> ok(U113(X1, X2, X3)) , U114(mark(X1), X2) -> mark(U114(X1, X2)) , U114(ok(X1), ok(X2)) -> ok(U114(X1, X2)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U121(mark(X1), X2) -> mark(U121(X1, X2)) , U121(ok(X1), ok(X2)) -> ok(U121(X1, X2)) , U122(mark(X)) -> mark(U122(X)) , U122(ok(X)) -> ok(U122(X)) , U131(mark(X1), X2, X3, X4) -> mark(U131(X1, X2, X3, X4)) , U131(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U131(X1, X2, X3, X4)) , U132(mark(X1), X2, X3, X4) -> mark(U132(X1, X2, X3, X4)) , U132(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U132(X1, X2, X3, X4)) , U133(mark(X1), X2, X3, X4) -> mark(U133(X1, X2, X3, X4)) , U133(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U133(X1, X2, X3, X4)) , U134(mark(X1), X2, X3, X4) -> mark(U134(X1, X2, X3, X4)) , U134(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U134(X1, X2, X3, X4)) , U135(mark(X1), X2, X3, X4) -> mark(U135(X1, X2, X3, X4)) , U135(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U135(X1, X2, X3, X4)) , U136(mark(X1), X2, X3, X4) -> mark(U136(X1, X2, X3, X4)) , U136(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U136(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X1), X2) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X)) -> mark(U71(X)) , U71(ok(X)) -> ok(U71(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) , U94(mark(X1), X2, X3) -> mark(U94(X1, X2, X3)) , U94(ok(X1), ok(X2), ok(X3)) -> ok(U94(X1, X2, X3)) , U95(mark(X1), X2) -> mark(U95(X1, X2)) , U95(ok(X1), ok(X2)) -> ok(U95(X1, X2)) , U96(mark(X)) -> mark(U96(X)) , U96(ok(X)) -> ok(U96(X)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U102(X1, X2, X3)) -> U102(proper(X1), proper(X2), proper(X3)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , proper(U103(X1, X2, X3)) -> U103(proper(X1), proper(X2), proper(X3)) , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) , proper(U104(X1, X2, X3)) -> U104(proper(X1), proper(X2), proper(X3)) , proper(U105(X1, X2)) -> U105(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U106(X)) -> U106(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(U111(X1, X2, X3)) -> U111(proper(X1), proper(X2), proper(X3)) , proper(U112(X1, X2, X3)) -> U112(proper(X1), proper(X2), proper(X3)) , proper(U113(X1, X2, X3)) -> U113(proper(X1), proper(X2), proper(X3)) , proper(U114(X1, X2)) -> U114(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U121(X1, X2)) -> U121(proper(X1), proper(X2)) , proper(U122(X)) -> U122(proper(X)) , proper(nil()) -> ok(nil()) , proper(U131(X1, X2, X3, X4)) -> U131(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U132(X1, X2, X3, X4)) -> U132(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U133(X1, X2, X3, X4)) -> U133(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U134(X1, X2, X3, X4)) -> U134(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U135(X1, X2, X3, X4)) -> U135(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U136(X1, X2, X3, X4)) -> U136(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X)) -> U71(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(U91(X1, X2, X3)) -> U91(proper(X1), proper(X2), proper(X3)) , proper(U92(X1, X2, X3)) -> U92(proper(X1), proper(X2), proper(X3)) , proper(U93(X1, X2, X3)) -> U93(proper(X1), proper(X2), proper(X3)) , proper(U94(X1, X2, X3)) -> U94(proper(X1), proper(X2), proper(X3)) , proper(U95(X1, X2)) -> U95(proper(X1), proper(X2)) , proper(U96(X)) -> U96(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 60.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'WithProblem (timeout of 30 seconds) (timeout of 60 seconds)' failed due to the following reason: Computation stopped due to timeout after 30.0 seconds. 2) 'Best' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'bsearch-popstar (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 2) 'Polynomial Path Order (PS) (timeout of 60 seconds)' failed due to the following reason: The processor is inapplicable, reason: Processor only applicable for innermost runtime complexity analysis 3) 'Fastest (timeout of 5 seconds) (timeout of 60 seconds)' failed due to the following reason: None of the processors succeeded. Details of failed attempt(s): ----------------------------- 1) 'Bounds with minimal-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' failed due to the following reason: match-boundness of the problem could not be verified. 3) 'Innermost Weak Dependency Pairs (timeout of 60 seconds)' failed due to the following reason: We add the following weak dependency pairs: Strict DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) , active^#(U101(X1, X2, X3)) -> c_3(U101^#(active(X1), X2, X3)) , active^#(U101(tt(), V1, V2)) -> c_4(U102^#(isNatKind(V1), V1, V2)) , active^#(U102(X1, X2, X3)) -> c_5(U102^#(active(X1), X2, X3)) , active^#(U102(tt(), V1, V2)) -> c_6(U103^#(isNatIListKind(V2), V1, V2)) , active^#(isNatKind(0())) -> c_7() , active^#(isNatKind(s(V1))) -> c_8(U81^#(isNatKind(V1))) , active^#(isNatKind(length(V1))) -> c_9(U71^#(isNatIListKind(V1))) , active^#(U103(X1, X2, X3)) -> c_10(U103^#(active(X1), X2, X3)) , active^#(U103(tt(), V1, V2)) -> c_11(U104^#(isNatIListKind(V2), V1, V2)) , active^#(isNatIListKind(zeros())) -> c_12() , active^#(isNatIListKind(cons(V1, V2))) -> c_13(U51^#(isNatKind(V1), V2)) , active^#(isNatIListKind(nil())) -> c_14() , active^#(isNatIListKind(take(V1, V2))) -> c_15(U61^#(isNatKind(V1), V2)) , active^#(U104(X1, X2, X3)) -> c_16(U104^#(active(X1), X2, X3)) , active^#(U104(tt(), V1, V2)) -> c_17(U105^#(isNat(V1), V2)) , active^#(U105(X1, X2)) -> c_18(U105^#(active(X1), X2)) , active^#(U105(tt(), V2)) -> c_19(U106^#(isNatIList(V2))) , active^#(isNat(0())) -> c_20() , active^#(isNat(s(V1))) -> c_21(U21^#(isNatKind(V1), V1)) , active^#(isNat(length(V1))) -> c_22(U11^#(isNatIListKind(V1), V1)) , active^#(U106(X)) -> c_23(U106^#(active(X))) , active^#(U106(tt())) -> c_24() , active^#(isNatIList(V)) -> c_25(U31^#(isNatIListKind(V), V)) , active^#(isNatIList(zeros())) -> c_26() , active^#(isNatIList(cons(V1, V2))) -> c_27(U41^#(isNatKind(V1), V1, V2)) , active^#(U11(X1, X2)) -> c_28(U11^#(active(X1), X2)) , active^#(U11(tt(), V1)) -> c_29(U12^#(isNatIListKind(V1), V1)) , active^#(U12(X1, X2)) -> c_30(U12^#(active(X1), X2)) , active^#(U12(tt(), V1)) -> c_31(U13^#(isNatList(V1))) , active^#(U111(X1, X2, X3)) -> c_32(U111^#(active(X1), X2, X3)) , active^#(U111(tt(), L, N)) -> c_33(U112^#(isNatIListKind(L), L, N)) , active^#(U112(X1, X2, X3)) -> c_34(U112^#(active(X1), X2, X3)) , active^#(U112(tt(), L, N)) -> c_35(U113^#(isNat(N), L, N)) , active^#(U113(X1, X2, X3)) -> c_36(U113^#(active(X1), X2, X3)) , active^#(U113(tt(), L, N)) -> c_37(U114^#(isNatKind(N), L)) , active^#(U114(X1, X2)) -> c_38(U114^#(active(X1), X2)) , active^#(U114(tt(), L)) -> c_39(s^#(length(L))) , active^#(s(X)) -> c_40(s^#(active(X))) , active^#(length(X)) -> c_41(length^#(active(X))) , active^#(length(cons(N, L))) -> c_42(U111^#(isNatList(L), L, N)) , active^#(length(nil())) -> c_43() , active^#(U13(X)) -> c_44(U13^#(active(X))) , active^#(U13(tt())) -> c_45() , active^#(isNatList(cons(V1, V2))) -> c_46(U91^#(isNatKind(V1), V1, V2)) , active^#(isNatList(nil())) -> c_47() , active^#(isNatList(take(V1, V2))) -> c_48(U101^#(isNatKind(V1), V1, V2)) , active^#(U121(X1, X2)) -> c_49(U121^#(active(X1), X2)) , active^#(U121(tt(), IL)) -> c_50(U122^#(isNatIListKind(IL))) , active^#(U122(X)) -> c_51(U122^#(active(X))) , active^#(U122(tt())) -> c_52() , active^#(U131(X1, X2, X3, X4)) -> c_53(U131^#(active(X1), X2, X3, X4)) , active^#(U131(tt(), IL, M, N)) -> c_54(U132^#(isNatIListKind(IL), IL, M, N)) , active^#(U132(X1, X2, X3, X4)) -> c_55(U132^#(active(X1), X2, X3, X4)) , active^#(U132(tt(), IL, M, N)) -> c_56(U133^#(isNat(M), IL, M, N)) , active^#(U133(X1, X2, X3, X4)) -> c_57(U133^#(active(X1), X2, X3, X4)) , active^#(U133(tt(), IL, M, N)) -> c_58(U134^#(isNatKind(M), IL, M, N)) , active^#(U134(X1, X2, X3, X4)) -> c_59(U134^#(active(X1), X2, X3, X4)) , active^#(U134(tt(), IL, M, N)) -> c_60(U135^#(isNat(N), IL, M, N)) , active^#(U135(X1, X2, X3, X4)) -> c_61(U135^#(active(X1), X2, X3, X4)) , active^#(U135(tt(), IL, M, N)) -> c_62(U136^#(isNatKind(N), IL, M, N)) , active^#(U136(X1, X2, X3, X4)) -> c_63(U136^#(active(X1), X2, X3, X4)) , active^#(U136(tt(), IL, M, N)) -> c_64(cons^#(N, take(M, IL))) , active^#(take(X1, X2)) -> c_65(take^#(X1, active(X2))) , active^#(take(X1, X2)) -> c_66(take^#(active(X1), X2)) , active^#(take(0(), IL)) -> c_67(U121^#(isNatIList(IL), IL)) , active^#(take(s(M), cons(N, IL))) -> c_68(U131^#(isNatIList(IL), IL, M, N)) , active^#(U21(X1, X2)) -> c_69(U21^#(active(X1), X2)) , active^#(U21(tt(), V1)) -> c_70(U22^#(isNatKind(V1), V1)) , active^#(U22(X1, X2)) -> c_71(U22^#(active(X1), X2)) , active^#(U22(tt(), V1)) -> c_72(U23^#(isNat(V1))) , active^#(U23(X)) -> c_73(U23^#(active(X))) , active^#(U23(tt())) -> c_74() , active^#(U31(X1, X2)) -> c_75(U31^#(active(X1), X2)) , active^#(U31(tt(), V)) -> c_76(U32^#(isNatIListKind(V), V)) , active^#(U32(X1, X2)) -> c_77(U32^#(active(X1), X2)) , active^#(U32(tt(), V)) -> c_78(U33^#(isNatList(V))) , active^#(U33(X)) -> c_79(U33^#(active(X))) , active^#(U33(tt())) -> c_80() , active^#(U41(X1, X2, X3)) -> c_81(U41^#(active(X1), X2, X3)) , active^#(U41(tt(), V1, V2)) -> c_82(U42^#(isNatKind(V1), V1, V2)) , active^#(U42(X1, X2, X3)) -> c_83(U42^#(active(X1), X2, X3)) , active^#(U42(tt(), V1, V2)) -> c_84(U43^#(isNatIListKind(V2), V1, V2)) , active^#(U43(X1, X2, X3)) -> c_85(U43^#(active(X1), X2, X3)) , active^#(U43(tt(), V1, V2)) -> c_86(U44^#(isNatIListKind(V2), V1, V2)) , active^#(U44(X1, X2, X3)) -> c_87(U44^#(active(X1), X2, X3)) , active^#(U44(tt(), V1, V2)) -> c_88(U45^#(isNat(V1), V2)) , active^#(U45(X1, X2)) -> c_89(U45^#(active(X1), X2)) , active^#(U45(tt(), V2)) -> c_90(U46^#(isNatIList(V2))) , active^#(U46(X)) -> c_91(U46^#(active(X))) , active^#(U46(tt())) -> c_92() , active^#(U51(X1, X2)) -> c_93(U51^#(active(X1), X2)) , active^#(U51(tt(), V2)) -> c_94(U52^#(isNatIListKind(V2))) , active^#(U52(X)) -> c_95(U52^#(active(X))) , active^#(U52(tt())) -> c_96() , active^#(U61(X1, X2)) -> c_97(U61^#(active(X1), X2)) , active^#(U61(tt(), V2)) -> c_98(U62^#(isNatIListKind(V2))) , active^#(U62(X)) -> c_99(U62^#(active(X))) , active^#(U62(tt())) -> c_100() , active^#(U71(X)) -> c_101(U71^#(active(X))) , active^#(U71(tt())) -> c_102() , active^#(U81(X)) -> c_103(U81^#(active(X))) , active^#(U81(tt())) -> c_104() , active^#(U91(X1, X2, X3)) -> c_105(U91^#(active(X1), X2, X3)) , active^#(U91(tt(), V1, V2)) -> c_106(U92^#(isNatKind(V1), V1, V2)) , active^#(U92(X1, X2, X3)) -> c_107(U92^#(active(X1), X2, X3)) , active^#(U92(tt(), V1, V2)) -> c_108(U93^#(isNatIListKind(V2), V1, V2)) , active^#(U93(X1, X2, X3)) -> c_109(U93^#(active(X1), X2, X3)) , active^#(U93(tt(), V1, V2)) -> c_110(U94^#(isNatIListKind(V2), V1, V2)) , active^#(U94(X1, X2, X3)) -> c_111(U94^#(active(X1), X2, X3)) , active^#(U94(tt(), V1, V2)) -> c_112(U95^#(isNat(V1), V2)) , active^#(U95(X1, X2)) -> c_113(U95^#(active(X1), X2)) , active^#(U95(tt(), V2)) -> c_114(U96^#(isNatList(V2))) , active^#(U96(X)) -> c_115(U96^#(active(X))) , active^#(U96(tt())) -> c_116() , cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) , U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) , U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) , U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) , U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) , U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) , U81^#(mark(X)) -> c_207(U81^#(X)) , U81^#(ok(X)) -> c_208(U81^#(X)) , U71^#(mark(X)) -> c_205(U71^#(X)) , U71^#(ok(X)) -> c_206(U71^#(X)) , U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) , U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) , U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) , U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) , U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) , U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) , U106^#(mark(X)) -> c_132(U106^#(X)) , U106^#(ok(X)) -> c_133(U106^#(X)) , U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) , U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) , U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) , U13^#(mark(X)) -> c_151(U13^#(X)) , U13^#(ok(X)) -> c_152(U13^#(X)) , U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) , U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) , U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) , U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) , U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) , U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) , U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) , U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) , s^#(mark(X)) -> c_147(s^#(X)) , s^#(ok(X)) -> c_148(s^#(X)) , length^#(mark(X)) -> c_149(length^#(X)) , length^#(ok(X)) -> c_150(length^#(X)) , U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) , U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) , U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) , U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) , U122^#(mark(X)) -> c_156(U122^#(X)) , U122^#(ok(X)) -> c_157(U122^#(X)) , U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) , U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) , U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) , U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) , U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) , U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) , U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) , U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) , U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) , U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) , U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) , U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) , U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) , U23^#(mark(X)) -> c_177(U23^#(X)) , U23^#(ok(X)) -> c_178(U23^#(X)) , U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) , U33^#(mark(X)) -> c_183(U33^#(X)) , U33^#(ok(X)) -> c_184(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) , U46^#(mark(X)) -> c_195(U46^#(X)) , U46^#(ok(X)) -> c_196(U46^#(X)) , U52^#(mark(X)) -> c_199(U52^#(X)) , U52^#(ok(X)) -> c_200(U52^#(X)) , U62^#(mark(X)) -> c_203(U62^#(X)) , U62^#(ok(X)) -> c_204(U62^#(X)) , U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) , U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) , U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) , U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) , U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) , U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) , U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) , U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) , U96^#(mark(X)) -> c_219(U96^#(X)) , U96^#(ok(X)) -> c_220(U96^#(X)) , isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) , isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) , isNat^#(ok(X)) -> c_131(isNat^#(X)) , isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_153(isNatList^#(X)) , proper^#(zeros()) -> c_221() , proper^#(cons(X1, X2)) -> c_222(cons^#(proper(X1), proper(X2))) , proper^#(0()) -> c_223() , proper^#(U101(X1, X2, X3)) -> c_224(U101^#(proper(X1), proper(X2), proper(X3))) , proper^#(tt()) -> c_225() , proper^#(U102(X1, X2, X3)) -> c_226(U102^#(proper(X1), proper(X2), proper(X3))) , proper^#(isNatKind(X)) -> c_227(isNatKind^#(proper(X))) , proper^#(U103(X1, X2, X3)) -> c_228(U103^#(proper(X1), proper(X2), proper(X3))) , proper^#(isNatIListKind(X)) -> c_229(isNatIListKind^#(proper(X))) , proper^#(U104(X1, X2, X3)) -> c_230(U104^#(proper(X1), proper(X2), proper(X3))) , proper^#(U105(X1, X2)) -> c_231(U105^#(proper(X1), proper(X2))) , proper^#(isNat(X)) -> c_232(isNat^#(proper(X))) , proper^#(U106(X)) -> c_233(U106^#(proper(X))) , proper^#(isNatIList(X)) -> c_234(isNatIList^#(proper(X))) , proper^#(U11(X1, X2)) -> c_235(U11^#(proper(X1), proper(X2))) , proper^#(U12(X1, X2)) -> c_236(U12^#(proper(X1), proper(X2))) , proper^#(U111(X1, X2, X3)) -> c_237(U111^#(proper(X1), proper(X2), proper(X3))) , proper^#(U112(X1, X2, X3)) -> c_238(U112^#(proper(X1), proper(X2), proper(X3))) , proper^#(U113(X1, X2, X3)) -> c_239(U113^#(proper(X1), proper(X2), proper(X3))) , proper^#(U114(X1, X2)) -> c_240(U114^#(proper(X1), proper(X2))) , proper^#(s(X)) -> c_241(s^#(proper(X))) , proper^#(length(X)) -> c_242(length^#(proper(X))) , proper^#(U13(X)) -> c_243(U13^#(proper(X))) , proper^#(isNatList(X)) -> c_244(isNatList^#(proper(X))) , proper^#(U121(X1, X2)) -> c_245(U121^#(proper(X1), proper(X2))) , proper^#(U122(X)) -> c_246(U122^#(proper(X))) , proper^#(nil()) -> c_247() , proper^#(U131(X1, X2, X3, X4)) -> c_248(U131^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U132(X1, X2, X3, X4)) -> c_249(U132^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U133(X1, X2, X3, X4)) -> c_250(U133^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U134(X1, X2, X3, X4)) -> c_251(U134^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U135(X1, X2, X3, X4)) -> c_252(U135^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U136(X1, X2, X3, X4)) -> c_253(U136^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(take(X1, X2)) -> c_254(take^#(proper(X1), proper(X2))) , proper^#(U21(X1, X2)) -> c_255(U21^#(proper(X1), proper(X2))) , proper^#(U22(X1, X2)) -> c_256(U22^#(proper(X1), proper(X2))) , proper^#(U23(X)) -> c_257(U23^#(proper(X))) , proper^#(U31(X1, X2)) -> c_258(U31^#(proper(X1), proper(X2))) , proper^#(U32(X1, X2)) -> c_259(U32^#(proper(X1), proper(X2))) , proper^#(U33(X)) -> c_260(U33^#(proper(X))) , proper^#(U41(X1, X2, X3)) -> c_261(U41^#(proper(X1), proper(X2), proper(X3))) , proper^#(U42(X1, X2, X3)) -> c_262(U42^#(proper(X1), proper(X2), proper(X3))) , proper^#(U43(X1, X2, X3)) -> c_263(U43^#(proper(X1), proper(X2), proper(X3))) , proper^#(U44(X1, X2, X3)) -> c_264(U44^#(proper(X1), proper(X2), proper(X3))) , proper^#(U45(X1, X2)) -> c_265(U45^#(proper(X1), proper(X2))) , proper^#(U46(X)) -> c_266(U46^#(proper(X))) , proper^#(U51(X1, X2)) -> c_267(U51^#(proper(X1), proper(X2))) , proper^#(U52(X)) -> c_268(U52^#(proper(X))) , proper^#(U61(X1, X2)) -> c_269(U61^#(proper(X1), proper(X2))) , proper^#(U62(X)) -> c_270(U62^#(proper(X))) , proper^#(U71(X)) -> c_271(U71^#(proper(X))) , proper^#(U81(X)) -> c_272(U81^#(proper(X))) , proper^#(U91(X1, X2, X3)) -> c_273(U91^#(proper(X1), proper(X2), proper(X3))) , proper^#(U92(X1, X2, X3)) -> c_274(U92^#(proper(X1), proper(X2), proper(X3))) , proper^#(U93(X1, X2, X3)) -> c_275(U93^#(proper(X1), proper(X2), proper(X3))) , proper^#(U94(X1, X2, X3)) -> c_276(U94^#(proper(X1), proper(X2), proper(X3))) , proper^#(U95(X1, X2)) -> c_277(U95^#(proper(X1), proper(X2))) , proper^#(U96(X)) -> c_278(U96^#(proper(X))) , top^#(mark(X)) -> c_279(top^#(proper(X))) , top^#(ok(X)) -> c_280(top^#(active(X))) } and mark the set of starting terms. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) , active^#(U101(X1, X2, X3)) -> c_3(U101^#(active(X1), X2, X3)) , active^#(U101(tt(), V1, V2)) -> c_4(U102^#(isNatKind(V1), V1, V2)) , active^#(U102(X1, X2, X3)) -> c_5(U102^#(active(X1), X2, X3)) , active^#(U102(tt(), V1, V2)) -> c_6(U103^#(isNatIListKind(V2), V1, V2)) , active^#(isNatKind(0())) -> c_7() , active^#(isNatKind(s(V1))) -> c_8(U81^#(isNatKind(V1))) , active^#(isNatKind(length(V1))) -> c_9(U71^#(isNatIListKind(V1))) , active^#(U103(X1, X2, X3)) -> c_10(U103^#(active(X1), X2, X3)) , active^#(U103(tt(), V1, V2)) -> c_11(U104^#(isNatIListKind(V2), V1, V2)) , active^#(isNatIListKind(zeros())) -> c_12() , active^#(isNatIListKind(cons(V1, V2))) -> c_13(U51^#(isNatKind(V1), V2)) , active^#(isNatIListKind(nil())) -> c_14() , active^#(isNatIListKind(take(V1, V2))) -> c_15(U61^#(isNatKind(V1), V2)) , active^#(U104(X1, X2, X3)) -> c_16(U104^#(active(X1), X2, X3)) , active^#(U104(tt(), V1, V2)) -> c_17(U105^#(isNat(V1), V2)) , active^#(U105(X1, X2)) -> c_18(U105^#(active(X1), X2)) , active^#(U105(tt(), V2)) -> c_19(U106^#(isNatIList(V2))) , active^#(isNat(0())) -> c_20() , active^#(isNat(s(V1))) -> c_21(U21^#(isNatKind(V1), V1)) , active^#(isNat(length(V1))) -> c_22(U11^#(isNatIListKind(V1), V1)) , active^#(U106(X)) -> c_23(U106^#(active(X))) , active^#(U106(tt())) -> c_24() , active^#(isNatIList(V)) -> c_25(U31^#(isNatIListKind(V), V)) , active^#(isNatIList(zeros())) -> c_26() , active^#(isNatIList(cons(V1, V2))) -> c_27(U41^#(isNatKind(V1), V1, V2)) , active^#(U11(X1, X2)) -> c_28(U11^#(active(X1), X2)) , active^#(U11(tt(), V1)) -> c_29(U12^#(isNatIListKind(V1), V1)) , active^#(U12(X1, X2)) -> c_30(U12^#(active(X1), X2)) , active^#(U12(tt(), V1)) -> c_31(U13^#(isNatList(V1))) , active^#(U111(X1, X2, X3)) -> c_32(U111^#(active(X1), X2, X3)) , active^#(U111(tt(), L, N)) -> c_33(U112^#(isNatIListKind(L), L, N)) , active^#(U112(X1, X2, X3)) -> c_34(U112^#(active(X1), X2, X3)) , active^#(U112(tt(), L, N)) -> c_35(U113^#(isNat(N), L, N)) , active^#(U113(X1, X2, X3)) -> c_36(U113^#(active(X1), X2, X3)) , active^#(U113(tt(), L, N)) -> c_37(U114^#(isNatKind(N), L)) , active^#(U114(X1, X2)) -> c_38(U114^#(active(X1), X2)) , active^#(U114(tt(), L)) -> c_39(s^#(length(L))) , active^#(s(X)) -> c_40(s^#(active(X))) , active^#(length(X)) -> c_41(length^#(active(X))) , active^#(length(cons(N, L))) -> c_42(U111^#(isNatList(L), L, N)) , active^#(length(nil())) -> c_43() , active^#(U13(X)) -> c_44(U13^#(active(X))) , active^#(U13(tt())) -> c_45() , active^#(isNatList(cons(V1, V2))) -> c_46(U91^#(isNatKind(V1), V1, V2)) , active^#(isNatList(nil())) -> c_47() , active^#(isNatList(take(V1, V2))) -> c_48(U101^#(isNatKind(V1), V1, V2)) , active^#(U121(X1, X2)) -> c_49(U121^#(active(X1), X2)) , active^#(U121(tt(), IL)) -> c_50(U122^#(isNatIListKind(IL))) , active^#(U122(X)) -> c_51(U122^#(active(X))) , active^#(U122(tt())) -> c_52() , active^#(U131(X1, X2, X3, X4)) -> c_53(U131^#(active(X1), X2, X3, X4)) , active^#(U131(tt(), IL, M, N)) -> c_54(U132^#(isNatIListKind(IL), IL, M, N)) , active^#(U132(X1, X2, X3, X4)) -> c_55(U132^#(active(X1), X2, X3, X4)) , active^#(U132(tt(), IL, M, N)) -> c_56(U133^#(isNat(M), IL, M, N)) , active^#(U133(X1, X2, X3, X4)) -> c_57(U133^#(active(X1), X2, X3, X4)) , active^#(U133(tt(), IL, M, N)) -> c_58(U134^#(isNatKind(M), IL, M, N)) , active^#(U134(X1, X2, X3, X4)) -> c_59(U134^#(active(X1), X2, X3, X4)) , active^#(U134(tt(), IL, M, N)) -> c_60(U135^#(isNat(N), IL, M, N)) , active^#(U135(X1, X2, X3, X4)) -> c_61(U135^#(active(X1), X2, X3, X4)) , active^#(U135(tt(), IL, M, N)) -> c_62(U136^#(isNatKind(N), IL, M, N)) , active^#(U136(X1, X2, X3, X4)) -> c_63(U136^#(active(X1), X2, X3, X4)) , active^#(U136(tt(), IL, M, N)) -> c_64(cons^#(N, take(M, IL))) , active^#(take(X1, X2)) -> c_65(take^#(X1, active(X2))) , active^#(take(X1, X2)) -> c_66(take^#(active(X1), X2)) , active^#(take(0(), IL)) -> c_67(U121^#(isNatIList(IL), IL)) , active^#(take(s(M), cons(N, IL))) -> c_68(U131^#(isNatIList(IL), IL, M, N)) , active^#(U21(X1, X2)) -> c_69(U21^#(active(X1), X2)) , active^#(U21(tt(), V1)) -> c_70(U22^#(isNatKind(V1), V1)) , active^#(U22(X1, X2)) -> c_71(U22^#(active(X1), X2)) , active^#(U22(tt(), V1)) -> c_72(U23^#(isNat(V1))) , active^#(U23(X)) -> c_73(U23^#(active(X))) , active^#(U23(tt())) -> c_74() , active^#(U31(X1, X2)) -> c_75(U31^#(active(X1), X2)) , active^#(U31(tt(), V)) -> c_76(U32^#(isNatIListKind(V), V)) , active^#(U32(X1, X2)) -> c_77(U32^#(active(X1), X2)) , active^#(U32(tt(), V)) -> c_78(U33^#(isNatList(V))) , active^#(U33(X)) -> c_79(U33^#(active(X))) , active^#(U33(tt())) -> c_80() , active^#(U41(X1, X2, X3)) -> c_81(U41^#(active(X1), X2, X3)) , active^#(U41(tt(), V1, V2)) -> c_82(U42^#(isNatKind(V1), V1, V2)) , active^#(U42(X1, X2, X3)) -> c_83(U42^#(active(X1), X2, X3)) , active^#(U42(tt(), V1, V2)) -> c_84(U43^#(isNatIListKind(V2), V1, V2)) , active^#(U43(X1, X2, X3)) -> c_85(U43^#(active(X1), X2, X3)) , active^#(U43(tt(), V1, V2)) -> c_86(U44^#(isNatIListKind(V2), V1, V2)) , active^#(U44(X1, X2, X3)) -> c_87(U44^#(active(X1), X2, X3)) , active^#(U44(tt(), V1, V2)) -> c_88(U45^#(isNat(V1), V2)) , active^#(U45(X1, X2)) -> c_89(U45^#(active(X1), X2)) , active^#(U45(tt(), V2)) -> c_90(U46^#(isNatIList(V2))) , active^#(U46(X)) -> c_91(U46^#(active(X))) , active^#(U46(tt())) -> c_92() , active^#(U51(X1, X2)) -> c_93(U51^#(active(X1), X2)) , active^#(U51(tt(), V2)) -> c_94(U52^#(isNatIListKind(V2))) , active^#(U52(X)) -> c_95(U52^#(active(X))) , active^#(U52(tt())) -> c_96() , active^#(U61(X1, X2)) -> c_97(U61^#(active(X1), X2)) , active^#(U61(tt(), V2)) -> c_98(U62^#(isNatIListKind(V2))) , active^#(U62(X)) -> c_99(U62^#(active(X))) , active^#(U62(tt())) -> c_100() , active^#(U71(X)) -> c_101(U71^#(active(X))) , active^#(U71(tt())) -> c_102() , active^#(U81(X)) -> c_103(U81^#(active(X))) , active^#(U81(tt())) -> c_104() , active^#(U91(X1, X2, X3)) -> c_105(U91^#(active(X1), X2, X3)) , active^#(U91(tt(), V1, V2)) -> c_106(U92^#(isNatKind(V1), V1, V2)) , active^#(U92(X1, X2, X3)) -> c_107(U92^#(active(X1), X2, X3)) , active^#(U92(tt(), V1, V2)) -> c_108(U93^#(isNatIListKind(V2), V1, V2)) , active^#(U93(X1, X2, X3)) -> c_109(U93^#(active(X1), X2, X3)) , active^#(U93(tt(), V1, V2)) -> c_110(U94^#(isNatIListKind(V2), V1, V2)) , active^#(U94(X1, X2, X3)) -> c_111(U94^#(active(X1), X2, X3)) , active^#(U94(tt(), V1, V2)) -> c_112(U95^#(isNat(V1), V2)) , active^#(U95(X1, X2)) -> c_113(U95^#(active(X1), X2)) , active^#(U95(tt(), V2)) -> c_114(U96^#(isNatList(V2))) , active^#(U96(X)) -> c_115(U96^#(active(X))) , active^#(U96(tt())) -> c_116() , cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) , U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) , U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) , U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) , U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) , U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) , U81^#(mark(X)) -> c_207(U81^#(X)) , U81^#(ok(X)) -> c_208(U81^#(X)) , U71^#(mark(X)) -> c_205(U71^#(X)) , U71^#(ok(X)) -> c_206(U71^#(X)) , U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) , U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) , U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) , U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) , U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) , U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) , U106^#(mark(X)) -> c_132(U106^#(X)) , U106^#(ok(X)) -> c_133(U106^#(X)) , U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) , U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) , U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) , U13^#(mark(X)) -> c_151(U13^#(X)) , U13^#(ok(X)) -> c_152(U13^#(X)) , U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) , U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) , U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) , U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) , U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) , U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) , U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) , U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) , s^#(mark(X)) -> c_147(s^#(X)) , s^#(ok(X)) -> c_148(s^#(X)) , length^#(mark(X)) -> c_149(length^#(X)) , length^#(ok(X)) -> c_150(length^#(X)) , U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) , U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) , U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) , U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) , U122^#(mark(X)) -> c_156(U122^#(X)) , U122^#(ok(X)) -> c_157(U122^#(X)) , U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) , U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) , U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) , U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) , U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) , U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) , U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) , U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) , U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) , U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) , U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) , U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) , U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) , U23^#(mark(X)) -> c_177(U23^#(X)) , U23^#(ok(X)) -> c_178(U23^#(X)) , U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) , U33^#(mark(X)) -> c_183(U33^#(X)) , U33^#(ok(X)) -> c_184(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) , U46^#(mark(X)) -> c_195(U46^#(X)) , U46^#(ok(X)) -> c_196(U46^#(X)) , U52^#(mark(X)) -> c_199(U52^#(X)) , U52^#(ok(X)) -> c_200(U52^#(X)) , U62^#(mark(X)) -> c_203(U62^#(X)) , U62^#(ok(X)) -> c_204(U62^#(X)) , U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) , U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) , U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) , U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) , U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) , U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) , U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) , U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) , U96^#(mark(X)) -> c_219(U96^#(X)) , U96^#(ok(X)) -> c_220(U96^#(X)) , isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) , isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) , isNat^#(ok(X)) -> c_131(isNat^#(X)) , isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_153(isNatList^#(X)) , proper^#(zeros()) -> c_221() , proper^#(cons(X1, X2)) -> c_222(cons^#(proper(X1), proper(X2))) , proper^#(0()) -> c_223() , proper^#(U101(X1, X2, X3)) -> c_224(U101^#(proper(X1), proper(X2), proper(X3))) , proper^#(tt()) -> c_225() , proper^#(U102(X1, X2, X3)) -> c_226(U102^#(proper(X1), proper(X2), proper(X3))) , proper^#(isNatKind(X)) -> c_227(isNatKind^#(proper(X))) , proper^#(U103(X1, X2, X3)) -> c_228(U103^#(proper(X1), proper(X2), proper(X3))) , proper^#(isNatIListKind(X)) -> c_229(isNatIListKind^#(proper(X))) , proper^#(U104(X1, X2, X3)) -> c_230(U104^#(proper(X1), proper(X2), proper(X3))) , proper^#(U105(X1, X2)) -> c_231(U105^#(proper(X1), proper(X2))) , proper^#(isNat(X)) -> c_232(isNat^#(proper(X))) , proper^#(U106(X)) -> c_233(U106^#(proper(X))) , proper^#(isNatIList(X)) -> c_234(isNatIList^#(proper(X))) , proper^#(U11(X1, X2)) -> c_235(U11^#(proper(X1), proper(X2))) , proper^#(U12(X1, X2)) -> c_236(U12^#(proper(X1), proper(X2))) , proper^#(U111(X1, X2, X3)) -> c_237(U111^#(proper(X1), proper(X2), proper(X3))) , proper^#(U112(X1, X2, X3)) -> c_238(U112^#(proper(X1), proper(X2), proper(X3))) , proper^#(U113(X1, X2, X3)) -> c_239(U113^#(proper(X1), proper(X2), proper(X3))) , proper^#(U114(X1, X2)) -> c_240(U114^#(proper(X1), proper(X2))) , proper^#(s(X)) -> c_241(s^#(proper(X))) , proper^#(length(X)) -> c_242(length^#(proper(X))) , proper^#(U13(X)) -> c_243(U13^#(proper(X))) , proper^#(isNatList(X)) -> c_244(isNatList^#(proper(X))) , proper^#(U121(X1, X2)) -> c_245(U121^#(proper(X1), proper(X2))) , proper^#(U122(X)) -> c_246(U122^#(proper(X))) , proper^#(nil()) -> c_247() , proper^#(U131(X1, X2, X3, X4)) -> c_248(U131^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U132(X1, X2, X3, X4)) -> c_249(U132^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U133(X1, X2, X3, X4)) -> c_250(U133^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U134(X1, X2, X3, X4)) -> c_251(U134^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U135(X1, X2, X3, X4)) -> c_252(U135^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(U136(X1, X2, X3, X4)) -> c_253(U136^#(proper(X1), proper(X2), proper(X3), proper(X4))) , proper^#(take(X1, X2)) -> c_254(take^#(proper(X1), proper(X2))) , proper^#(U21(X1, X2)) -> c_255(U21^#(proper(X1), proper(X2))) , proper^#(U22(X1, X2)) -> c_256(U22^#(proper(X1), proper(X2))) , proper^#(U23(X)) -> c_257(U23^#(proper(X))) , proper^#(U31(X1, X2)) -> c_258(U31^#(proper(X1), proper(X2))) , proper^#(U32(X1, X2)) -> c_259(U32^#(proper(X1), proper(X2))) , proper^#(U33(X)) -> c_260(U33^#(proper(X))) , proper^#(U41(X1, X2, X3)) -> c_261(U41^#(proper(X1), proper(X2), proper(X3))) , proper^#(U42(X1, X2, X3)) -> c_262(U42^#(proper(X1), proper(X2), proper(X3))) , proper^#(U43(X1, X2, X3)) -> c_263(U43^#(proper(X1), proper(X2), proper(X3))) , proper^#(U44(X1, X2, X3)) -> c_264(U44^#(proper(X1), proper(X2), proper(X3))) , proper^#(U45(X1, X2)) -> c_265(U45^#(proper(X1), proper(X2))) , proper^#(U46(X)) -> c_266(U46^#(proper(X))) , proper^#(U51(X1, X2)) -> c_267(U51^#(proper(X1), proper(X2))) , proper^#(U52(X)) -> c_268(U52^#(proper(X))) , proper^#(U61(X1, X2)) -> c_269(U61^#(proper(X1), proper(X2))) , proper^#(U62(X)) -> c_270(U62^#(proper(X))) , proper^#(U71(X)) -> c_271(U71^#(proper(X))) , proper^#(U81(X)) -> c_272(U81^#(proper(X))) , proper^#(U91(X1, X2, X3)) -> c_273(U91^#(proper(X1), proper(X2), proper(X3))) , proper^#(U92(X1, X2, X3)) -> c_274(U92^#(proper(X1), proper(X2), proper(X3))) , proper^#(U93(X1, X2, X3)) -> c_275(U93^#(proper(X1), proper(X2), proper(X3))) , proper^#(U94(X1, X2, X3)) -> c_276(U94^#(proper(X1), proper(X2), proper(X3))) , proper^#(U95(X1, X2)) -> c_277(U95^#(proper(X1), proper(X2))) , proper^#(U96(X)) -> c_278(U96^#(proper(X))) , top^#(mark(X)) -> c_279(top^#(proper(X))) , top^#(ok(X)) -> c_280(top^#(active(X))) } Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), V1, V2)) -> mark(U102(isNatKind(V1), V1, V2)) , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) , active(U102(tt(), V1, V2)) -> mark(U103(isNatIListKind(V2), V1, V2)) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(s(V1))) -> mark(U81(isNatKind(V1))) , active(isNatKind(length(V1))) -> mark(U71(isNatIListKind(V1))) , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) , active(U103(tt(), V1, V2)) -> mark(U104(isNatIListKind(V2), V1, V2)) , active(isNatIListKind(zeros())) -> mark(tt()) , active(isNatIListKind(cons(V1, V2))) -> mark(U51(isNatKind(V1), V2)) , active(isNatIListKind(nil())) -> mark(tt()) , active(isNatIListKind(take(V1, V2))) -> mark(U61(isNatKind(V1), V2)) , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) , active(U104(tt(), V1, V2)) -> mark(U105(isNat(V1), V2)) , active(U105(X1, X2)) -> U105(active(X1), X2) , active(U105(tt(), V2)) -> mark(U106(isNatIList(V2))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) , active(U106(X)) -> U106(active(X)) , active(U106(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNatKind(V1), V1, V2)) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) , active(U111(X1, X2, X3)) -> U111(active(X1), X2, X3) , active(U111(tt(), L, N)) -> mark(U112(isNatIListKind(L), L, N)) , active(U112(X1, X2, X3)) -> U112(active(X1), X2, X3) , active(U112(tt(), L, N)) -> mark(U113(isNat(N), L, N)) , active(U113(X1, X2, X3)) -> U113(active(X1), X2, X3) , active(U113(tt(), L, N)) -> mark(U114(isNatKind(N), L)) , active(U114(X1, X2)) -> U114(active(X1), X2) , active(U114(tt(), L)) -> mark(s(length(L))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U111(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U91(isNatKind(V1), V1, V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U101(isNatKind(V1), V1, V2)) , active(U121(X1, X2)) -> U121(active(X1), X2) , active(U121(tt(), IL)) -> mark(U122(isNatIListKind(IL))) , active(U122(X)) -> U122(active(X)) , active(U122(tt())) -> mark(nil()) , active(U131(X1, X2, X3, X4)) -> U131(active(X1), X2, X3, X4) , active(U131(tt(), IL, M, N)) -> mark(U132(isNatIListKind(IL), IL, M, N)) , active(U132(X1, X2, X3, X4)) -> U132(active(X1), X2, X3, X4) , active(U132(tt(), IL, M, N)) -> mark(U133(isNat(M), IL, M, N)) , active(U133(X1, X2, X3, X4)) -> U133(active(X1), X2, X3, X4) , active(U133(tt(), IL, M, N)) -> mark(U134(isNatKind(M), IL, M, N)) , active(U134(X1, X2, X3, X4)) -> U134(active(X1), X2, X3, X4) , active(U134(tt(), IL, M, N)) -> mark(U135(isNat(N), IL, M, N)) , active(U135(X1, X2, X3, X4)) -> U135(active(X1), X2, X3, X4) , active(U135(tt(), IL, M, N)) -> mark(U136(isNatKind(N), IL, M, N)) , active(U136(X1, X2, X3, X4)) -> U136(active(X1), X2, X3, X4) , active(U136(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U121(isNatIList(IL), IL)) , active(take(s(M), cons(N, IL))) -> mark(U131(isNatIList(IL), IL, M, N)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isNatList(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isNatIListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isNatIListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIListKind(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X)) -> U71(active(X)) , active(U71(tt())) -> mark(tt()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(tt()) , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) , active(U91(tt(), V1, V2)) -> mark(U92(isNatKind(V1), V1, V2)) , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) , active(U92(tt(), V1, V2)) -> mark(U93(isNatIListKind(V2), V1, V2)) , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) , active(U93(tt(), V1, V2)) -> mark(U94(isNatIListKind(V2), V1, V2)) , active(U94(X1, X2, X3)) -> U94(active(X1), X2, X3) , active(U94(tt(), V1, V2)) -> mark(U95(isNat(V1), V2)) , active(U95(X1, X2)) -> U95(active(X1), X2) , active(U95(tt(), V2)) -> mark(U96(isNatList(V2))) , active(U96(X)) -> U96(active(X)) , active(U96(tt())) -> mark(tt()) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) , U105(mark(X1), X2) -> mark(U105(X1, X2)) , U105(ok(X1), ok(X2)) -> ok(U105(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U106(mark(X)) -> mark(U106(X)) , U106(ok(X)) -> ok(U106(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , U111(mark(X1), X2, X3) -> mark(U111(X1, X2, X3)) , U111(ok(X1), ok(X2), ok(X3)) -> ok(U111(X1, X2, X3)) , U112(mark(X1), X2, X3) -> mark(U112(X1, X2, X3)) , U112(ok(X1), ok(X2), ok(X3)) -> ok(U112(X1, X2, X3)) , U113(mark(X1), X2, X3) -> mark(U113(X1, X2, X3)) , U113(ok(X1), ok(X2), ok(X3)) -> ok(U113(X1, X2, X3)) , U114(mark(X1), X2) -> mark(U114(X1, X2)) , U114(ok(X1), ok(X2)) -> ok(U114(X1, X2)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U121(mark(X1), X2) -> mark(U121(X1, X2)) , U121(ok(X1), ok(X2)) -> ok(U121(X1, X2)) , U122(mark(X)) -> mark(U122(X)) , U122(ok(X)) -> ok(U122(X)) , U131(mark(X1), X2, X3, X4) -> mark(U131(X1, X2, X3, X4)) , U131(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U131(X1, X2, X3, X4)) , U132(mark(X1), X2, X3, X4) -> mark(U132(X1, X2, X3, X4)) , U132(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U132(X1, X2, X3, X4)) , U133(mark(X1), X2, X3, X4) -> mark(U133(X1, X2, X3, X4)) , U133(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U133(X1, X2, X3, X4)) , U134(mark(X1), X2, X3, X4) -> mark(U134(X1, X2, X3, X4)) , U134(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U134(X1, X2, X3, X4)) , U135(mark(X1), X2, X3, X4) -> mark(U135(X1, X2, X3, X4)) , U135(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U135(X1, X2, X3, X4)) , U136(mark(X1), X2, X3, X4) -> mark(U136(X1, X2, X3, X4)) , U136(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U136(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X1), X2) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X)) -> mark(U71(X)) , U71(ok(X)) -> ok(U71(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) , U94(mark(X1), X2, X3) -> mark(U94(X1, X2, X3)) , U94(ok(X1), ok(X2), ok(X3)) -> ok(U94(X1, X2, X3)) , U95(mark(X1), X2) -> mark(U95(X1, X2)) , U95(ok(X1), ok(X2)) -> ok(U95(X1, X2)) , U96(mark(X)) -> mark(U96(X)) , U96(ok(X)) -> ok(U96(X)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U102(X1, X2, X3)) -> U102(proper(X1), proper(X2), proper(X3)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , proper(U103(X1, X2, X3)) -> U103(proper(X1), proper(X2), proper(X3)) , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) , proper(U104(X1, X2, X3)) -> U104(proper(X1), proper(X2), proper(X3)) , proper(U105(X1, X2)) -> U105(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U106(X)) -> U106(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(U111(X1, X2, X3)) -> U111(proper(X1), proper(X2), proper(X3)) , proper(U112(X1, X2, X3)) -> U112(proper(X1), proper(X2), proper(X3)) , proper(U113(X1, X2, X3)) -> U113(proper(X1), proper(X2), proper(X3)) , proper(U114(X1, X2)) -> U114(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U121(X1, X2)) -> U121(proper(X1), proper(X2)) , proper(U122(X)) -> U122(proper(X)) , proper(nil()) -> ok(nil()) , proper(U131(X1, X2, X3, X4)) -> U131(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U132(X1, X2, X3, X4)) -> U132(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U133(X1, X2, X3, X4)) -> U133(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U134(X1, X2, X3, X4)) -> U134(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U135(X1, X2, X3, X4)) -> U135(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U136(X1, X2, X3, X4)) -> U136(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X)) -> U71(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(U91(X1, X2, X3)) -> U91(proper(X1), proper(X2), proper(X3)) , proper(U92(X1, X2, X3)) -> U92(proper(X1), proper(X2), proper(X3)) , proper(U93(X1, X2, X3)) -> U93(proper(X1), proper(X2), proper(X3)) , proper(U94(X1, X2, X3)) -> U94(proper(X1), proper(X2), proper(X3)) , proper(U95(X1, X2)) -> U95(proper(X1), proper(X2)) , proper(U96(X)) -> U96(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE Consider the dependency graph: 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) :118 -->_1 cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) :117 3: active^#(U101(X1, X2, X3)) -> c_3(U101^#(active(X1), X2, X3)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) :120 -->_1 U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) :119 4: active^#(U101(tt(), V1, V2)) -> c_4(U102^#(isNatKind(V1), V1, V2)) -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) :122 -->_1 U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) :121 5: active^#(U102(X1, X2, X3)) -> c_5(U102^#(active(X1), X2, X3)) -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) :122 -->_1 U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) :121 6: active^#(U102(tt(), V1, V2)) -> c_6(U103^#(isNatIListKind(V2), V1, V2)) -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) :124 -->_1 U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) :123 7: active^#(isNatKind(0())) -> c_7() 8: active^#(isNatKind(s(V1))) -> c_8(U81^#(isNatKind(V1))) -->_1 U81^#(ok(X)) -> c_208(U81^#(X)) :126 -->_1 U81^#(mark(X)) -> c_207(U81^#(X)) :125 9: active^#(isNatKind(length(V1))) -> c_9(U71^#(isNatIListKind(V1))) -->_1 U71^#(ok(X)) -> c_206(U71^#(X)) :128 -->_1 U71^#(mark(X)) -> c_205(U71^#(X)) :127 10: active^#(U103(X1, X2, X3)) -> c_10(U103^#(active(X1), X2, X3)) -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) :124 -->_1 U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) :123 11: active^#(U103(tt(), V1, V2)) -> c_11(U104^#(isNatIListKind(V2), V1, V2)) -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) :130 -->_1 U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) :129 12: active^#(isNatIListKind(zeros())) -> c_12() 13: active^#(isNatIListKind(cons(V1, V2))) -> c_13(U51^#(isNatKind(V1), V2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) :132 -->_1 U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) :131 14: active^#(isNatIListKind(nil())) -> c_14() 15: active^#(isNatIListKind(take(V1, V2))) -> c_15(U61^#(isNatKind(V1), V2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) :134 -->_1 U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) :133 16: active^#(U104(X1, X2, X3)) -> c_16(U104^#(active(X1), X2, X3)) -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) :130 -->_1 U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) :129 17: active^#(U104(tt(), V1, V2)) -> c_17(U105^#(isNat(V1), V2)) -->_1 U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) :136 -->_1 U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) :135 18: active^#(U105(X1, X2)) -> c_18(U105^#(active(X1), X2)) -->_1 U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) :136 -->_1 U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) :135 19: active^#(U105(tt(), V2)) -> c_19(U106^#(isNatIList(V2))) -->_1 U106^#(ok(X)) -> c_133(U106^#(X)) :138 -->_1 U106^#(mark(X)) -> c_132(U106^#(X)) :137 20: active^#(isNat(0())) -> c_20() 21: active^#(isNat(s(V1))) -> c_21(U21^#(isNatKind(V1), V1)) -->_1 U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) :140 -->_1 U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) :139 22: active^#(isNat(length(V1))) -> c_22(U11^#(isNatIListKind(V1), V1)) -->_1 U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) :142 -->_1 U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) :141 23: active^#(U106(X)) -> c_23(U106^#(active(X))) -->_1 U106^#(ok(X)) -> c_133(U106^#(X)) :138 -->_1 U106^#(mark(X)) -> c_132(U106^#(X)) :137 24: active^#(U106(tt())) -> c_24() 25: active^#(isNatIList(V)) -> c_25(U31^#(isNatIListKind(V), V)) -->_1 U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) :144 -->_1 U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) :143 26: active^#(isNatIList(zeros())) -> c_26() 27: active^#(isNatIList(cons(V1, V2))) -> c_27(U41^#(isNatKind(V1), V1, V2)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) :146 -->_1 U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) :145 28: active^#(U11(X1, X2)) -> c_28(U11^#(active(X1), X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) :142 -->_1 U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) :141 29: active^#(U11(tt(), V1)) -> c_29(U12^#(isNatIListKind(V1), V1)) -->_1 U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) :148 -->_1 U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) :147 30: active^#(U12(X1, X2)) -> c_30(U12^#(active(X1), X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) :148 -->_1 U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) :147 31: active^#(U12(tt(), V1)) -> c_31(U13^#(isNatList(V1))) -->_1 U13^#(ok(X)) -> c_152(U13^#(X)) :150 -->_1 U13^#(mark(X)) -> c_151(U13^#(X)) :149 32: active^#(U111(X1, X2, X3)) -> c_32(U111^#(active(X1), X2, X3)) -->_1 U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) :152 -->_1 U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) :151 33: active^#(U111(tt(), L, N)) -> c_33(U112^#(isNatIListKind(L), L, N)) -->_1 U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) :154 -->_1 U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) :153 34: active^#(U112(X1, X2, X3)) -> c_34(U112^#(active(X1), X2, X3)) -->_1 U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) :154 -->_1 U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) :153 35: active^#(U112(tt(), L, N)) -> c_35(U113^#(isNat(N), L, N)) -->_1 U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) :156 -->_1 U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) :155 36: active^#(U113(X1, X2, X3)) -> c_36(U113^#(active(X1), X2, X3)) -->_1 U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) :156 -->_1 U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) :155 37: active^#(U113(tt(), L, N)) -> c_37(U114^#(isNatKind(N), L)) -->_1 U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) :158 -->_1 U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) :157 38: active^#(U114(X1, X2)) -> c_38(U114^#(active(X1), X2)) -->_1 U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) :158 -->_1 U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) :157 39: active^#(U114(tt(), L)) -> c_39(s^#(length(L))) -->_1 s^#(ok(X)) -> c_148(s^#(X)) :160 -->_1 s^#(mark(X)) -> c_147(s^#(X)) :159 40: active^#(s(X)) -> c_40(s^#(active(X))) -->_1 s^#(ok(X)) -> c_148(s^#(X)) :160 -->_1 s^#(mark(X)) -> c_147(s^#(X)) :159 41: active^#(length(X)) -> c_41(length^#(active(X))) -->_1 length^#(ok(X)) -> c_150(length^#(X)) :162 -->_1 length^#(mark(X)) -> c_149(length^#(X)) :161 42: active^#(length(cons(N, L))) -> c_42(U111^#(isNatList(L), L, N)) -->_1 U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) :152 -->_1 U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) :151 43: active^#(length(nil())) -> c_43() 44: active^#(U13(X)) -> c_44(U13^#(active(X))) -->_1 U13^#(ok(X)) -> c_152(U13^#(X)) :150 -->_1 U13^#(mark(X)) -> c_151(U13^#(X)) :149 45: active^#(U13(tt())) -> c_45() 46: active^#(isNatList(cons(V1, V2))) -> c_46(U91^#(isNatKind(V1), V1, V2)) -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) :164 -->_1 U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) :163 47: active^#(isNatList(nil())) -> c_47() 48: active^#(isNatList(take(V1, V2))) -> c_48(U101^#(isNatKind(V1), V1, V2)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) :120 -->_1 U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) :119 49: active^#(U121(X1, X2)) -> c_49(U121^#(active(X1), X2)) -->_1 U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) :166 -->_1 U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) :165 50: active^#(U121(tt(), IL)) -> c_50(U122^#(isNatIListKind(IL))) -->_1 U122^#(ok(X)) -> c_157(U122^#(X)) :168 -->_1 U122^#(mark(X)) -> c_156(U122^#(X)) :167 51: active^#(U122(X)) -> c_51(U122^#(active(X))) -->_1 U122^#(ok(X)) -> c_157(U122^#(X)) :168 -->_1 U122^#(mark(X)) -> c_156(U122^#(X)) :167 52: active^#(U122(tt())) -> c_52() 53: active^#(U131(X1, X2, X3, X4)) -> c_53(U131^#(active(X1), X2, X3, X4)) -->_1 U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) :170 -->_1 U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) :169 54: active^#(U131(tt(), IL, M, N)) -> c_54(U132^#(isNatIListKind(IL), IL, M, N)) -->_1 U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) :172 -->_1 U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) :171 55: active^#(U132(X1, X2, X3, X4)) -> c_55(U132^#(active(X1), X2, X3, X4)) -->_1 U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) :172 -->_1 U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) :171 56: active^#(U132(tt(), IL, M, N)) -> c_56(U133^#(isNat(M), IL, M, N)) -->_1 U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) :174 -->_1 U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) :173 57: active^#(U133(X1, X2, X3, X4)) -> c_57(U133^#(active(X1), X2, X3, X4)) -->_1 U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) :174 -->_1 U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) :173 58: active^#(U133(tt(), IL, M, N)) -> c_58(U134^#(isNatKind(M), IL, M, N)) -->_1 U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) :176 -->_1 U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) :175 59: active^#(U134(X1, X2, X3, X4)) -> c_59(U134^#(active(X1), X2, X3, X4)) -->_1 U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) :176 -->_1 U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) :175 60: active^#(U134(tt(), IL, M, N)) -> c_60(U135^#(isNat(N), IL, M, N)) -->_1 U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) :178 -->_1 U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) :177 61: active^#(U135(X1, X2, X3, X4)) -> c_61(U135^#(active(X1), X2, X3, X4)) -->_1 U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) :178 -->_1 U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) :177 62: active^#(U135(tt(), IL, M, N)) -> c_62(U136^#(isNatKind(N), IL, M, N)) -->_1 U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) :180 -->_1 U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) :179 63: active^#(U136(X1, X2, X3, X4)) -> c_63(U136^#(active(X1), X2, X3, X4)) -->_1 U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) :180 -->_1 U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) :179 64: active^#(U136(tt(), IL, M, N)) -> c_64(cons^#(N, take(M, IL))) -->_1 cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) :118 -->_1 cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) :117 65: active^#(take(X1, X2)) -> c_65(take^#(X1, active(X2))) -->_1 take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) :183 -->_1 take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) :182 -->_1 take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) :181 66: active^#(take(X1, X2)) -> c_66(take^#(active(X1), X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) :183 -->_1 take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) :182 -->_1 take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) :181 67: active^#(take(0(), IL)) -> c_67(U121^#(isNatIList(IL), IL)) -->_1 U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) :166 -->_1 U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) :165 68: active^#(take(s(M), cons(N, IL))) -> c_68(U131^#(isNatIList(IL), IL, M, N)) -->_1 U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) :170 -->_1 U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) :169 69: active^#(U21(X1, X2)) -> c_69(U21^#(active(X1), X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) :140 -->_1 U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) :139 70: active^#(U21(tt(), V1)) -> c_70(U22^#(isNatKind(V1), V1)) -->_1 U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) :185 -->_1 U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) :184 71: active^#(U22(X1, X2)) -> c_71(U22^#(active(X1), X2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) :185 -->_1 U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) :184 72: active^#(U22(tt(), V1)) -> c_72(U23^#(isNat(V1))) -->_1 U23^#(ok(X)) -> c_178(U23^#(X)) :187 -->_1 U23^#(mark(X)) -> c_177(U23^#(X)) :186 73: active^#(U23(X)) -> c_73(U23^#(active(X))) -->_1 U23^#(ok(X)) -> c_178(U23^#(X)) :187 -->_1 U23^#(mark(X)) -> c_177(U23^#(X)) :186 74: active^#(U23(tt())) -> c_74() 75: active^#(U31(X1, X2)) -> c_75(U31^#(active(X1), X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) :144 -->_1 U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) :143 76: active^#(U31(tt(), V)) -> c_76(U32^#(isNatIListKind(V), V)) -->_1 U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) :189 -->_1 U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) :188 77: active^#(U32(X1, X2)) -> c_77(U32^#(active(X1), X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) :189 -->_1 U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) :188 78: active^#(U32(tt(), V)) -> c_78(U33^#(isNatList(V))) -->_1 U33^#(ok(X)) -> c_184(U33^#(X)) :191 -->_1 U33^#(mark(X)) -> c_183(U33^#(X)) :190 79: active^#(U33(X)) -> c_79(U33^#(active(X))) -->_1 U33^#(ok(X)) -> c_184(U33^#(X)) :191 -->_1 U33^#(mark(X)) -> c_183(U33^#(X)) :190 80: active^#(U33(tt())) -> c_80() 81: active^#(U41(X1, X2, X3)) -> c_81(U41^#(active(X1), X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) :146 -->_1 U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) :145 82: active^#(U41(tt(), V1, V2)) -> c_82(U42^#(isNatKind(V1), V1, V2)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) :193 -->_1 U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) :192 83: active^#(U42(X1, X2, X3)) -> c_83(U42^#(active(X1), X2, X3)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) :193 -->_1 U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) :192 84: active^#(U42(tt(), V1, V2)) -> c_84(U43^#(isNatIListKind(V2), V1, V2)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) :195 -->_1 U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) :194 85: active^#(U43(X1, X2, X3)) -> c_85(U43^#(active(X1), X2, X3)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) :195 -->_1 U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) :194 86: active^#(U43(tt(), V1, V2)) -> c_86(U44^#(isNatIListKind(V2), V1, V2)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) :197 -->_1 U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) :196 87: active^#(U44(X1, X2, X3)) -> c_87(U44^#(active(X1), X2, X3)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) :197 -->_1 U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) :196 88: active^#(U44(tt(), V1, V2)) -> c_88(U45^#(isNat(V1), V2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) :199 -->_1 U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) :198 89: active^#(U45(X1, X2)) -> c_89(U45^#(active(X1), X2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) :199 -->_1 U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) :198 90: active^#(U45(tt(), V2)) -> c_90(U46^#(isNatIList(V2))) -->_1 U46^#(ok(X)) -> c_196(U46^#(X)) :201 -->_1 U46^#(mark(X)) -> c_195(U46^#(X)) :200 91: active^#(U46(X)) -> c_91(U46^#(active(X))) -->_1 U46^#(ok(X)) -> c_196(U46^#(X)) :201 -->_1 U46^#(mark(X)) -> c_195(U46^#(X)) :200 92: active^#(U46(tt())) -> c_92() 93: active^#(U51(X1, X2)) -> c_93(U51^#(active(X1), X2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) :132 -->_1 U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) :131 94: active^#(U51(tt(), V2)) -> c_94(U52^#(isNatIListKind(V2))) -->_1 U52^#(ok(X)) -> c_200(U52^#(X)) :203 -->_1 U52^#(mark(X)) -> c_199(U52^#(X)) :202 95: active^#(U52(X)) -> c_95(U52^#(active(X))) -->_1 U52^#(ok(X)) -> c_200(U52^#(X)) :203 -->_1 U52^#(mark(X)) -> c_199(U52^#(X)) :202 96: active^#(U52(tt())) -> c_96() 97: active^#(U61(X1, X2)) -> c_97(U61^#(active(X1), X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) :134 -->_1 U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) :133 98: active^#(U61(tt(), V2)) -> c_98(U62^#(isNatIListKind(V2))) -->_1 U62^#(ok(X)) -> c_204(U62^#(X)) :205 -->_1 U62^#(mark(X)) -> c_203(U62^#(X)) :204 99: active^#(U62(X)) -> c_99(U62^#(active(X))) -->_1 U62^#(ok(X)) -> c_204(U62^#(X)) :205 -->_1 U62^#(mark(X)) -> c_203(U62^#(X)) :204 100: active^#(U62(tt())) -> c_100() 101: active^#(U71(X)) -> c_101(U71^#(active(X))) -->_1 U71^#(ok(X)) -> c_206(U71^#(X)) :128 -->_1 U71^#(mark(X)) -> c_205(U71^#(X)) :127 102: active^#(U71(tt())) -> c_102() 103: active^#(U81(X)) -> c_103(U81^#(active(X))) -->_1 U81^#(ok(X)) -> c_208(U81^#(X)) :126 -->_1 U81^#(mark(X)) -> c_207(U81^#(X)) :125 104: active^#(U81(tt())) -> c_104() 105: active^#(U91(X1, X2, X3)) -> c_105(U91^#(active(X1), X2, X3)) -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) :164 -->_1 U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) :163 106: active^#(U91(tt(), V1, V2)) -> c_106(U92^#(isNatKind(V1), V1, V2)) -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) :207 -->_1 U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) :206 107: active^#(U92(X1, X2, X3)) -> c_107(U92^#(active(X1), X2, X3)) -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) :207 -->_1 U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) :206 108: active^#(U92(tt(), V1, V2)) -> c_108(U93^#(isNatIListKind(V2), V1, V2)) -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) :209 -->_1 U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) :208 109: active^#(U93(X1, X2, X3)) -> c_109(U93^#(active(X1), X2, X3)) -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) :209 -->_1 U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) :208 110: active^#(U93(tt(), V1, V2)) -> c_110(U94^#(isNatIListKind(V2), V1, V2)) -->_1 U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) :211 -->_1 U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) :210 111: active^#(U94(X1, X2, X3)) -> c_111(U94^#(active(X1), X2, X3)) -->_1 U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) :211 -->_1 U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) :210 112: active^#(U94(tt(), V1, V2)) -> c_112(U95^#(isNat(V1), V2)) -->_1 U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) :213 -->_1 U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) :212 113: active^#(U95(X1, X2)) -> c_113(U95^#(active(X1), X2)) -->_1 U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) :213 -->_1 U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) :212 114: active^#(U95(tt(), V2)) -> c_114(U96^#(isNatList(V2))) -->_1 U96^#(ok(X)) -> c_220(U96^#(X)) :215 -->_1 U96^#(mark(X)) -> c_219(U96^#(X)) :214 115: active^#(U96(X)) -> c_115(U96^#(active(X))) -->_1 U96^#(ok(X)) -> c_220(U96^#(X)) :215 -->_1 U96^#(mark(X)) -> c_219(U96^#(X)) :214 116: active^#(U96(tt())) -> c_116() 117: cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) :118 -->_1 cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) :117 118: cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) -->_1 cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) :118 -->_1 cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) :117 119: U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) :120 -->_1 U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) :119 120: U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) :120 -->_1 U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) :119 121: U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) :122 -->_1 U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) :121 122: U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) :122 -->_1 U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) :121 123: U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) :124 -->_1 U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) :123 124: U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) :124 -->_1 U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) :123 125: U81^#(mark(X)) -> c_207(U81^#(X)) -->_1 U81^#(ok(X)) -> c_208(U81^#(X)) :126 -->_1 U81^#(mark(X)) -> c_207(U81^#(X)) :125 126: U81^#(ok(X)) -> c_208(U81^#(X)) -->_1 U81^#(ok(X)) -> c_208(U81^#(X)) :126 -->_1 U81^#(mark(X)) -> c_207(U81^#(X)) :125 127: U71^#(mark(X)) -> c_205(U71^#(X)) -->_1 U71^#(ok(X)) -> c_206(U71^#(X)) :128 -->_1 U71^#(mark(X)) -> c_205(U71^#(X)) :127 128: U71^#(ok(X)) -> c_206(U71^#(X)) -->_1 U71^#(ok(X)) -> c_206(U71^#(X)) :128 -->_1 U71^#(mark(X)) -> c_205(U71^#(X)) :127 129: U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) :130 -->_1 U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) :129 130: U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) :130 -->_1 U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) :129 131: U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) :132 -->_1 U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) :131 132: U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) -->_1 U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) :132 -->_1 U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) :131 133: U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) :134 -->_1 U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) :133 134: U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) -->_1 U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) :134 -->_1 U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) :133 135: U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) -->_1 U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) :136 -->_1 U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) :135 136: U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) -->_1 U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) :136 -->_1 U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) :135 137: U106^#(mark(X)) -> c_132(U106^#(X)) -->_1 U106^#(ok(X)) -> c_133(U106^#(X)) :138 -->_1 U106^#(mark(X)) -> c_132(U106^#(X)) :137 138: U106^#(ok(X)) -> c_133(U106^#(X)) -->_1 U106^#(ok(X)) -> c_133(U106^#(X)) :138 -->_1 U106^#(mark(X)) -> c_132(U106^#(X)) :137 139: U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) :140 -->_1 U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) :139 140: U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) -->_1 U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) :140 -->_1 U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) :139 141: U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) :142 -->_1 U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) :141 142: U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) -->_1 U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) :142 -->_1 U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) :141 143: U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) :144 -->_1 U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) :143 144: U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) -->_1 U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) :144 -->_1 U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) :143 145: U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) :146 -->_1 U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) :145 146: U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) :146 -->_1 U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) :145 147: U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) :148 -->_1 U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) :147 148: U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) -->_1 U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) :148 -->_1 U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) :147 149: U13^#(mark(X)) -> c_151(U13^#(X)) -->_1 U13^#(ok(X)) -> c_152(U13^#(X)) :150 -->_1 U13^#(mark(X)) -> c_151(U13^#(X)) :149 150: U13^#(ok(X)) -> c_152(U13^#(X)) -->_1 U13^#(ok(X)) -> c_152(U13^#(X)) :150 -->_1 U13^#(mark(X)) -> c_151(U13^#(X)) :149 151: U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) -->_1 U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) :152 -->_1 U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) :151 152: U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) -->_1 U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) :152 -->_1 U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) :151 153: U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) -->_1 U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) :154 -->_1 U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) :153 154: U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) -->_1 U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) :154 -->_1 U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) :153 155: U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) -->_1 U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) :156 -->_1 U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) :155 156: U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) -->_1 U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) :156 -->_1 U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) :155 157: U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) -->_1 U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) :158 -->_1 U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) :157 158: U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) -->_1 U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) :158 -->_1 U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) :157 159: s^#(mark(X)) -> c_147(s^#(X)) -->_1 s^#(ok(X)) -> c_148(s^#(X)) :160 -->_1 s^#(mark(X)) -> c_147(s^#(X)) :159 160: s^#(ok(X)) -> c_148(s^#(X)) -->_1 s^#(ok(X)) -> c_148(s^#(X)) :160 -->_1 s^#(mark(X)) -> c_147(s^#(X)) :159 161: length^#(mark(X)) -> c_149(length^#(X)) -->_1 length^#(ok(X)) -> c_150(length^#(X)) :162 -->_1 length^#(mark(X)) -> c_149(length^#(X)) :161 162: length^#(ok(X)) -> c_150(length^#(X)) -->_1 length^#(ok(X)) -> c_150(length^#(X)) :162 -->_1 length^#(mark(X)) -> c_149(length^#(X)) :161 163: U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) :164 -->_1 U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) :163 164: U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) :164 -->_1 U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) :163 165: U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) -->_1 U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) :166 -->_1 U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) :165 166: U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) -->_1 U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) :166 -->_1 U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) :165 167: U122^#(mark(X)) -> c_156(U122^#(X)) -->_1 U122^#(ok(X)) -> c_157(U122^#(X)) :168 -->_1 U122^#(mark(X)) -> c_156(U122^#(X)) :167 168: U122^#(ok(X)) -> c_157(U122^#(X)) -->_1 U122^#(ok(X)) -> c_157(U122^#(X)) :168 -->_1 U122^#(mark(X)) -> c_156(U122^#(X)) :167 169: U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) -->_1 U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) :170 -->_1 U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) :169 170: U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) -->_1 U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) :170 -->_1 U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) :169 171: U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) -->_1 U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) :172 -->_1 U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) :171 172: U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) -->_1 U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) :172 -->_1 U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) :171 173: U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) -->_1 U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) :174 -->_1 U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) :173 174: U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) -->_1 U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) :174 -->_1 U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) :173 175: U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) -->_1 U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) :176 -->_1 U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) :175 176: U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) -->_1 U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) :176 -->_1 U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) :175 177: U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) -->_1 U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) :178 -->_1 U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) :177 178: U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) -->_1 U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) :178 -->_1 U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) :177 179: U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) -->_1 U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) :180 -->_1 U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) :179 180: U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) -->_1 U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) :180 -->_1 U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) :179 181: take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) :183 -->_1 take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) :182 -->_1 take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) :181 182: take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) :183 -->_1 take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) :182 -->_1 take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) :181 183: take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) -->_1 take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) :183 -->_1 take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) :182 -->_1 take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) :181 184: U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) :185 -->_1 U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) :184 185: U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) -->_1 U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) :185 -->_1 U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) :184 186: U23^#(mark(X)) -> c_177(U23^#(X)) -->_1 U23^#(ok(X)) -> c_178(U23^#(X)) :187 -->_1 U23^#(mark(X)) -> c_177(U23^#(X)) :186 187: U23^#(ok(X)) -> c_178(U23^#(X)) -->_1 U23^#(ok(X)) -> c_178(U23^#(X)) :187 -->_1 U23^#(mark(X)) -> c_177(U23^#(X)) :186 188: U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) :189 -->_1 U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) :188 189: U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) -->_1 U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) :189 -->_1 U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) :188 190: U33^#(mark(X)) -> c_183(U33^#(X)) -->_1 U33^#(ok(X)) -> c_184(U33^#(X)) :191 -->_1 U33^#(mark(X)) -> c_183(U33^#(X)) :190 191: U33^#(ok(X)) -> c_184(U33^#(X)) -->_1 U33^#(ok(X)) -> c_184(U33^#(X)) :191 -->_1 U33^#(mark(X)) -> c_183(U33^#(X)) :190 192: U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) :193 -->_1 U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) :192 193: U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) :193 -->_1 U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) :192 194: U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) :195 -->_1 U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) :194 195: U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) :195 -->_1 U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) :194 196: U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) :197 -->_1 U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) :196 197: U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) :197 -->_1 U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) :196 198: U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) :199 -->_1 U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) :198 199: U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) -->_1 U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) :199 -->_1 U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) :198 200: U46^#(mark(X)) -> c_195(U46^#(X)) -->_1 U46^#(ok(X)) -> c_196(U46^#(X)) :201 -->_1 U46^#(mark(X)) -> c_195(U46^#(X)) :200 201: U46^#(ok(X)) -> c_196(U46^#(X)) -->_1 U46^#(ok(X)) -> c_196(U46^#(X)) :201 -->_1 U46^#(mark(X)) -> c_195(U46^#(X)) :200 202: U52^#(mark(X)) -> c_199(U52^#(X)) -->_1 U52^#(ok(X)) -> c_200(U52^#(X)) :203 -->_1 U52^#(mark(X)) -> c_199(U52^#(X)) :202 203: U52^#(ok(X)) -> c_200(U52^#(X)) -->_1 U52^#(ok(X)) -> c_200(U52^#(X)) :203 -->_1 U52^#(mark(X)) -> c_199(U52^#(X)) :202 204: U62^#(mark(X)) -> c_203(U62^#(X)) -->_1 U62^#(ok(X)) -> c_204(U62^#(X)) :205 -->_1 U62^#(mark(X)) -> c_203(U62^#(X)) :204 205: U62^#(ok(X)) -> c_204(U62^#(X)) -->_1 U62^#(ok(X)) -> c_204(U62^#(X)) :205 -->_1 U62^#(mark(X)) -> c_203(U62^#(X)) :204 206: U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) :207 -->_1 U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) :206 207: U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) :207 -->_1 U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) :206 208: U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) :209 -->_1 U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) :208 209: U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) :209 -->_1 U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) :208 210: U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) -->_1 U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) :211 -->_1 U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) :210 211: U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) -->_1 U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) :211 -->_1 U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) :210 212: U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) -->_1 U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) :213 -->_1 U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) :212 213: U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) -->_1 U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) :213 -->_1 U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) :212 214: U96^#(mark(X)) -> c_219(U96^#(X)) -->_1 U96^#(ok(X)) -> c_220(U96^#(X)) :215 -->_1 U96^#(mark(X)) -> c_219(U96^#(X)) :214 215: U96^#(ok(X)) -> c_220(U96^#(X)) -->_1 U96^#(ok(X)) -> c_220(U96^#(X)) :215 -->_1 U96^#(mark(X)) -> c_219(U96^#(X)) :214 216: isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) -->_1 isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) :216 217: isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) -->_1 isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) :217 218: isNat^#(ok(X)) -> c_131(isNat^#(X)) -->_1 isNat^#(ok(X)) -> c_131(isNat^#(X)) :218 219: isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) -->_1 isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) :219 220: isNatList^#(ok(X)) -> c_153(isNatList^#(X)) -->_1 isNatList^#(ok(X)) -> c_153(isNatList^#(X)) :220 221: proper^#(zeros()) -> c_221() 222: proper^#(cons(X1, X2)) -> c_222(cons^#(proper(X1), proper(X2))) -->_1 cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) :118 -->_1 cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) :117 223: proper^#(0()) -> c_223() 224: proper^#(U101(X1, X2, X3)) -> c_224(U101^#(proper(X1), proper(X2), proper(X3))) -->_1 U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) :120 -->_1 U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) :119 225: proper^#(tt()) -> c_225() 226: proper^#(U102(X1, X2, X3)) -> c_226(U102^#(proper(X1), proper(X2), proper(X3))) -->_1 U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) :122 -->_1 U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) :121 227: proper^#(isNatKind(X)) -> c_227(isNatKind^#(proper(X))) -->_1 isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) :216 228: proper^#(U103(X1, X2, X3)) -> c_228(U103^#(proper(X1), proper(X2), proper(X3))) -->_1 U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) :124 -->_1 U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) :123 229: proper^#(isNatIListKind(X)) -> c_229(isNatIListKind^#(proper(X))) -->_1 isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) :217 230: proper^#(U104(X1, X2, X3)) -> c_230(U104^#(proper(X1), proper(X2), proper(X3))) -->_1 U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) :130 -->_1 U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) :129 231: proper^#(U105(X1, X2)) -> c_231(U105^#(proper(X1), proper(X2))) -->_1 U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) :136 -->_1 U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) :135 232: proper^#(isNat(X)) -> c_232(isNat^#(proper(X))) -->_1 isNat^#(ok(X)) -> c_131(isNat^#(X)) :218 233: proper^#(U106(X)) -> c_233(U106^#(proper(X))) -->_1 U106^#(ok(X)) -> c_133(U106^#(X)) :138 -->_1 U106^#(mark(X)) -> c_132(U106^#(X)) :137 234: proper^#(isNatIList(X)) -> c_234(isNatIList^#(proper(X))) -->_1 isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) :219 235: proper^#(U11(X1, X2)) -> c_235(U11^#(proper(X1), proper(X2))) -->_1 U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) :142 -->_1 U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) :141 236: proper^#(U12(X1, X2)) -> c_236(U12^#(proper(X1), proper(X2))) -->_1 U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) :148 -->_1 U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) :147 237: proper^#(U111(X1, X2, X3)) -> c_237(U111^#(proper(X1), proper(X2), proper(X3))) -->_1 U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) :152 -->_1 U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) :151 238: proper^#(U112(X1, X2, X3)) -> c_238(U112^#(proper(X1), proper(X2), proper(X3))) -->_1 U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) :154 -->_1 U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) :153 239: proper^#(U113(X1, X2, X3)) -> c_239(U113^#(proper(X1), proper(X2), proper(X3))) -->_1 U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) :156 -->_1 U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) :155 240: proper^#(U114(X1, X2)) -> c_240(U114^#(proper(X1), proper(X2))) -->_1 U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) :158 -->_1 U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) :157 241: proper^#(s(X)) -> c_241(s^#(proper(X))) -->_1 s^#(ok(X)) -> c_148(s^#(X)) :160 -->_1 s^#(mark(X)) -> c_147(s^#(X)) :159 242: proper^#(length(X)) -> c_242(length^#(proper(X))) -->_1 length^#(ok(X)) -> c_150(length^#(X)) :162 -->_1 length^#(mark(X)) -> c_149(length^#(X)) :161 243: proper^#(U13(X)) -> c_243(U13^#(proper(X))) -->_1 U13^#(ok(X)) -> c_152(U13^#(X)) :150 -->_1 U13^#(mark(X)) -> c_151(U13^#(X)) :149 244: proper^#(isNatList(X)) -> c_244(isNatList^#(proper(X))) -->_1 isNatList^#(ok(X)) -> c_153(isNatList^#(X)) :220 245: proper^#(U121(X1, X2)) -> c_245(U121^#(proper(X1), proper(X2))) -->_1 U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) :166 -->_1 U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) :165 246: proper^#(U122(X)) -> c_246(U122^#(proper(X))) -->_1 U122^#(ok(X)) -> c_157(U122^#(X)) :168 -->_1 U122^#(mark(X)) -> c_156(U122^#(X)) :167 247: proper^#(nil()) -> c_247() 248: proper^#(U131(X1, X2, X3, X4)) -> c_248(U131^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) :170 -->_1 U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) :169 249: proper^#(U132(X1, X2, X3, X4)) -> c_249(U132^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) :172 -->_1 U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) :171 250: proper^#(U133(X1, X2, X3, X4)) -> c_250(U133^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) :174 -->_1 U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) :173 251: proper^#(U134(X1, X2, X3, X4)) -> c_251(U134^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) :176 -->_1 U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) :175 252: proper^#(U135(X1, X2, X3, X4)) -> c_252(U135^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) :178 -->_1 U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) :177 253: proper^#(U136(X1, X2, X3, X4)) -> c_253(U136^#(proper(X1), proper(X2), proper(X3), proper(X4))) -->_1 U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) :180 -->_1 U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) :179 254: proper^#(take(X1, X2)) -> c_254(take^#(proper(X1), proper(X2))) -->_1 take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) :183 -->_1 take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) :182 -->_1 take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) :181 255: proper^#(U21(X1, X2)) -> c_255(U21^#(proper(X1), proper(X2))) -->_1 U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) :140 -->_1 U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) :139 256: proper^#(U22(X1, X2)) -> c_256(U22^#(proper(X1), proper(X2))) -->_1 U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) :185 -->_1 U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) :184 257: proper^#(U23(X)) -> c_257(U23^#(proper(X))) -->_1 U23^#(ok(X)) -> c_178(U23^#(X)) :187 -->_1 U23^#(mark(X)) -> c_177(U23^#(X)) :186 258: proper^#(U31(X1, X2)) -> c_258(U31^#(proper(X1), proper(X2))) -->_1 U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) :144 -->_1 U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) :143 259: proper^#(U32(X1, X2)) -> c_259(U32^#(proper(X1), proper(X2))) -->_1 U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) :189 -->_1 U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) :188 260: proper^#(U33(X)) -> c_260(U33^#(proper(X))) -->_1 U33^#(ok(X)) -> c_184(U33^#(X)) :191 -->_1 U33^#(mark(X)) -> c_183(U33^#(X)) :190 261: proper^#(U41(X1, X2, X3)) -> c_261(U41^#(proper(X1), proper(X2), proper(X3))) -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) :146 -->_1 U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) :145 262: proper^#(U42(X1, X2, X3)) -> c_262(U42^#(proper(X1), proper(X2), proper(X3))) -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) :193 -->_1 U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) :192 263: proper^#(U43(X1, X2, X3)) -> c_263(U43^#(proper(X1), proper(X2), proper(X3))) -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) :195 -->_1 U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) :194 264: proper^#(U44(X1, X2, X3)) -> c_264(U44^#(proper(X1), proper(X2), proper(X3))) -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) :197 -->_1 U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) :196 265: proper^#(U45(X1, X2)) -> c_265(U45^#(proper(X1), proper(X2))) -->_1 U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) :199 -->_1 U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) :198 266: proper^#(U46(X)) -> c_266(U46^#(proper(X))) -->_1 U46^#(ok(X)) -> c_196(U46^#(X)) :201 -->_1 U46^#(mark(X)) -> c_195(U46^#(X)) :200 267: proper^#(U51(X1, X2)) -> c_267(U51^#(proper(X1), proper(X2))) -->_1 U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) :132 -->_1 U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) :131 268: proper^#(U52(X)) -> c_268(U52^#(proper(X))) -->_1 U52^#(ok(X)) -> c_200(U52^#(X)) :203 -->_1 U52^#(mark(X)) -> c_199(U52^#(X)) :202 269: proper^#(U61(X1, X2)) -> c_269(U61^#(proper(X1), proper(X2))) -->_1 U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) :134 -->_1 U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) :133 270: proper^#(U62(X)) -> c_270(U62^#(proper(X))) -->_1 U62^#(ok(X)) -> c_204(U62^#(X)) :205 -->_1 U62^#(mark(X)) -> c_203(U62^#(X)) :204 271: proper^#(U71(X)) -> c_271(U71^#(proper(X))) -->_1 U71^#(ok(X)) -> c_206(U71^#(X)) :128 -->_1 U71^#(mark(X)) -> c_205(U71^#(X)) :127 272: proper^#(U81(X)) -> c_272(U81^#(proper(X))) -->_1 U81^#(ok(X)) -> c_208(U81^#(X)) :126 -->_1 U81^#(mark(X)) -> c_207(U81^#(X)) :125 273: proper^#(U91(X1, X2, X3)) -> c_273(U91^#(proper(X1), proper(X2), proper(X3))) -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) :164 -->_1 U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) :163 274: proper^#(U92(X1, X2, X3)) -> c_274(U92^#(proper(X1), proper(X2), proper(X3))) -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) :207 -->_1 U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) :206 275: proper^#(U93(X1, X2, X3)) -> c_275(U93^#(proper(X1), proper(X2), proper(X3))) -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) :209 -->_1 U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) :208 276: proper^#(U94(X1, X2, X3)) -> c_276(U94^#(proper(X1), proper(X2), proper(X3))) -->_1 U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) :211 -->_1 U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) :210 277: proper^#(U95(X1, X2)) -> c_277(U95^#(proper(X1), proper(X2))) -->_1 U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) :213 -->_1 U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) :212 278: proper^#(U96(X)) -> c_278(U96^#(proper(X))) -->_1 U96^#(ok(X)) -> c_220(U96^#(X)) :215 -->_1 U96^#(mark(X)) -> c_219(U96^#(X)) :214 279: top^#(mark(X)) -> c_279(top^#(proper(X))) -->_1 top^#(ok(X)) -> c_280(top^#(active(X))) :280 -->_1 top^#(mark(X)) -> c_279(top^#(proper(X))) :279 280: top^#(ok(X)) -> c_280(top^#(active(X))) -->_1 top^#(ok(X)) -> c_280(top^#(active(X))) :280 -->_1 top^#(mark(X)) -> c_279(top^#(proper(X))) :279 Only the nodes {1,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,183,182,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,223,225,247,279,280} are reachable from nodes {1,117,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,149,150,151,152,153,154,155,156,157,158,159,160,161,162,163,164,165,166,167,168,169,170,171,172,173,174,175,176,177,178,179,180,181,182,183,184,185,186,187,188,189,190,191,192,193,194,195,196,197,198,199,200,201,202,203,204,205,206,207,208,209,210,211,212,213,214,215,216,217,218,219,220,221,223,225,247,279,280} that start derivation from marked basic terms. The nodes not reachable are removed from the problem. We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) , U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) , U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) , U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) , U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) , U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) , U81^#(mark(X)) -> c_207(U81^#(X)) , U81^#(ok(X)) -> c_208(U81^#(X)) , U71^#(mark(X)) -> c_205(U71^#(X)) , U71^#(ok(X)) -> c_206(U71^#(X)) , U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) , U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) , U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) , U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) , U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) , U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) , U106^#(mark(X)) -> c_132(U106^#(X)) , U106^#(ok(X)) -> c_133(U106^#(X)) , U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) , U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) , U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) , U13^#(mark(X)) -> c_151(U13^#(X)) , U13^#(ok(X)) -> c_152(U13^#(X)) , U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) , U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) , U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) , U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) , U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) , U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) , U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) , U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) , s^#(mark(X)) -> c_147(s^#(X)) , s^#(ok(X)) -> c_148(s^#(X)) , length^#(mark(X)) -> c_149(length^#(X)) , length^#(ok(X)) -> c_150(length^#(X)) , U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) , U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) , U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) , U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) , U122^#(mark(X)) -> c_156(U122^#(X)) , U122^#(ok(X)) -> c_157(U122^#(X)) , U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) , U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) , U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) , U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) , U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) , U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) , U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) , U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) , U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) , U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) , U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) , U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) , U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) , U23^#(mark(X)) -> c_177(U23^#(X)) , U23^#(ok(X)) -> c_178(U23^#(X)) , U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) , U33^#(mark(X)) -> c_183(U33^#(X)) , U33^#(ok(X)) -> c_184(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) , U46^#(mark(X)) -> c_195(U46^#(X)) , U46^#(ok(X)) -> c_196(U46^#(X)) , U52^#(mark(X)) -> c_199(U52^#(X)) , U52^#(ok(X)) -> c_200(U52^#(X)) , U62^#(mark(X)) -> c_203(U62^#(X)) , U62^#(ok(X)) -> c_204(U62^#(X)) , U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) , U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) , U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) , U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) , U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) , U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) , U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) , U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) , U96^#(mark(X)) -> c_219(U96^#(X)) , U96^#(ok(X)) -> c_220(U96^#(X)) , isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) , isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) , isNat^#(ok(X)) -> c_131(isNat^#(X)) , isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_153(isNatList^#(X)) , proper^#(zeros()) -> c_221() , proper^#(0()) -> c_223() , proper^#(tt()) -> c_225() , proper^#(nil()) -> c_247() , top^#(mark(X)) -> c_279(top^#(proper(X))) , top^#(ok(X)) -> c_280(top^#(active(X))) } Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), V1, V2)) -> mark(U102(isNatKind(V1), V1, V2)) , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) , active(U102(tt(), V1, V2)) -> mark(U103(isNatIListKind(V2), V1, V2)) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(s(V1))) -> mark(U81(isNatKind(V1))) , active(isNatKind(length(V1))) -> mark(U71(isNatIListKind(V1))) , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) , active(U103(tt(), V1, V2)) -> mark(U104(isNatIListKind(V2), V1, V2)) , active(isNatIListKind(zeros())) -> mark(tt()) , active(isNatIListKind(cons(V1, V2))) -> mark(U51(isNatKind(V1), V2)) , active(isNatIListKind(nil())) -> mark(tt()) , active(isNatIListKind(take(V1, V2))) -> mark(U61(isNatKind(V1), V2)) , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) , active(U104(tt(), V1, V2)) -> mark(U105(isNat(V1), V2)) , active(U105(X1, X2)) -> U105(active(X1), X2) , active(U105(tt(), V2)) -> mark(U106(isNatIList(V2))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) , active(U106(X)) -> U106(active(X)) , active(U106(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNatKind(V1), V1, V2)) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) , active(U111(X1, X2, X3)) -> U111(active(X1), X2, X3) , active(U111(tt(), L, N)) -> mark(U112(isNatIListKind(L), L, N)) , active(U112(X1, X2, X3)) -> U112(active(X1), X2, X3) , active(U112(tt(), L, N)) -> mark(U113(isNat(N), L, N)) , active(U113(X1, X2, X3)) -> U113(active(X1), X2, X3) , active(U113(tt(), L, N)) -> mark(U114(isNatKind(N), L)) , active(U114(X1, X2)) -> U114(active(X1), X2) , active(U114(tt(), L)) -> mark(s(length(L))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U111(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U91(isNatKind(V1), V1, V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U101(isNatKind(V1), V1, V2)) , active(U121(X1, X2)) -> U121(active(X1), X2) , active(U121(tt(), IL)) -> mark(U122(isNatIListKind(IL))) , active(U122(X)) -> U122(active(X)) , active(U122(tt())) -> mark(nil()) , active(U131(X1, X2, X3, X4)) -> U131(active(X1), X2, X3, X4) , active(U131(tt(), IL, M, N)) -> mark(U132(isNatIListKind(IL), IL, M, N)) , active(U132(X1, X2, X3, X4)) -> U132(active(X1), X2, X3, X4) , active(U132(tt(), IL, M, N)) -> mark(U133(isNat(M), IL, M, N)) , active(U133(X1, X2, X3, X4)) -> U133(active(X1), X2, X3, X4) , active(U133(tt(), IL, M, N)) -> mark(U134(isNatKind(M), IL, M, N)) , active(U134(X1, X2, X3, X4)) -> U134(active(X1), X2, X3, X4) , active(U134(tt(), IL, M, N)) -> mark(U135(isNat(N), IL, M, N)) , active(U135(X1, X2, X3, X4)) -> U135(active(X1), X2, X3, X4) , active(U135(tt(), IL, M, N)) -> mark(U136(isNatKind(N), IL, M, N)) , active(U136(X1, X2, X3, X4)) -> U136(active(X1), X2, X3, X4) , active(U136(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U121(isNatIList(IL), IL)) , active(take(s(M), cons(N, IL))) -> mark(U131(isNatIList(IL), IL, M, N)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isNatList(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isNatIListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isNatIListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIListKind(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X)) -> U71(active(X)) , active(U71(tt())) -> mark(tt()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(tt()) , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) , active(U91(tt(), V1, V2)) -> mark(U92(isNatKind(V1), V1, V2)) , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) , active(U92(tt(), V1, V2)) -> mark(U93(isNatIListKind(V2), V1, V2)) , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) , active(U93(tt(), V1, V2)) -> mark(U94(isNatIListKind(V2), V1, V2)) , active(U94(X1, X2, X3)) -> U94(active(X1), X2, X3) , active(U94(tt(), V1, V2)) -> mark(U95(isNat(V1), V2)) , active(U95(X1, X2)) -> U95(active(X1), X2) , active(U95(tt(), V2)) -> mark(U96(isNatList(V2))) , active(U96(X)) -> U96(active(X)) , active(U96(tt())) -> mark(tt()) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) , U105(mark(X1), X2) -> mark(U105(X1, X2)) , U105(ok(X1), ok(X2)) -> ok(U105(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U106(mark(X)) -> mark(U106(X)) , U106(ok(X)) -> ok(U106(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , U111(mark(X1), X2, X3) -> mark(U111(X1, X2, X3)) , U111(ok(X1), ok(X2), ok(X3)) -> ok(U111(X1, X2, X3)) , U112(mark(X1), X2, X3) -> mark(U112(X1, X2, X3)) , U112(ok(X1), ok(X2), ok(X3)) -> ok(U112(X1, X2, X3)) , U113(mark(X1), X2, X3) -> mark(U113(X1, X2, X3)) , U113(ok(X1), ok(X2), ok(X3)) -> ok(U113(X1, X2, X3)) , U114(mark(X1), X2) -> mark(U114(X1, X2)) , U114(ok(X1), ok(X2)) -> ok(U114(X1, X2)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U121(mark(X1), X2) -> mark(U121(X1, X2)) , U121(ok(X1), ok(X2)) -> ok(U121(X1, X2)) , U122(mark(X)) -> mark(U122(X)) , U122(ok(X)) -> ok(U122(X)) , U131(mark(X1), X2, X3, X4) -> mark(U131(X1, X2, X3, X4)) , U131(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U131(X1, X2, X3, X4)) , U132(mark(X1), X2, X3, X4) -> mark(U132(X1, X2, X3, X4)) , U132(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U132(X1, X2, X3, X4)) , U133(mark(X1), X2, X3, X4) -> mark(U133(X1, X2, X3, X4)) , U133(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U133(X1, X2, X3, X4)) , U134(mark(X1), X2, X3, X4) -> mark(U134(X1, X2, X3, X4)) , U134(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U134(X1, X2, X3, X4)) , U135(mark(X1), X2, X3, X4) -> mark(U135(X1, X2, X3, X4)) , U135(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U135(X1, X2, X3, X4)) , U136(mark(X1), X2, X3, X4) -> mark(U136(X1, X2, X3, X4)) , U136(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U136(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X1), X2) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X)) -> mark(U71(X)) , U71(ok(X)) -> ok(U71(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) , U94(mark(X1), X2, X3) -> mark(U94(X1, X2, X3)) , U94(ok(X1), ok(X2), ok(X3)) -> ok(U94(X1, X2, X3)) , U95(mark(X1), X2) -> mark(U95(X1, X2)) , U95(ok(X1), ok(X2)) -> ok(U95(X1, X2)) , U96(mark(X)) -> mark(U96(X)) , U96(ok(X)) -> ok(U96(X)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U102(X1, X2, X3)) -> U102(proper(X1), proper(X2), proper(X3)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , proper(U103(X1, X2, X3)) -> U103(proper(X1), proper(X2), proper(X3)) , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) , proper(U104(X1, X2, X3)) -> U104(proper(X1), proper(X2), proper(X3)) , proper(U105(X1, X2)) -> U105(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U106(X)) -> U106(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(U111(X1, X2, X3)) -> U111(proper(X1), proper(X2), proper(X3)) , proper(U112(X1, X2, X3)) -> U112(proper(X1), proper(X2), proper(X3)) , proper(U113(X1, X2, X3)) -> U113(proper(X1), proper(X2), proper(X3)) , proper(U114(X1, X2)) -> U114(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U121(X1, X2)) -> U121(proper(X1), proper(X2)) , proper(U122(X)) -> U122(proper(X)) , proper(nil()) -> ok(nil()) , proper(U131(X1, X2, X3, X4)) -> U131(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U132(X1, X2, X3, X4)) -> U132(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U133(X1, X2, X3, X4)) -> U133(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U134(X1, X2, X3, X4)) -> U134(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U135(X1, X2, X3, X4)) -> U135(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U136(X1, X2, X3, X4)) -> U136(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X)) -> U71(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(U91(X1, X2, X3)) -> U91(proper(X1), proper(X2), proper(X3)) , proper(U92(X1, X2, X3)) -> U92(proper(X1), proper(X2), proper(X3)) , proper(U93(X1, X2, X3)) -> U93(proper(X1), proper(X2), proper(X3)) , proper(U94(X1, X2, X3)) -> U94(proper(X1), proper(X2), proper(X3)) , proper(U95(X1, X2)) -> U95(proper(X1), proper(X2)) , proper(U96(X)) -> U96(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Obligation: runtime complexity Answer: MAYBE We estimate the number of application of {1,106,107,108,109} by applications of Pre({1,106,107,108,109}) = {}. Here rules are labeled as follows: DPs: { 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) , 2: cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) , 3: cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) , 4: U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) , 5: U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) , 6: U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) , 7: U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) , 8: U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) , 9: U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) , 10: U81^#(mark(X)) -> c_207(U81^#(X)) , 11: U81^#(ok(X)) -> c_208(U81^#(X)) , 12: U71^#(mark(X)) -> c_205(U71^#(X)) , 13: U71^#(ok(X)) -> c_206(U71^#(X)) , 14: U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) , 15: U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) , 16: U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) , 17: U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) , 18: U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) , 19: U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) , 20: U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) , 21: U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) , 22: U106^#(mark(X)) -> c_132(U106^#(X)) , 23: U106^#(ok(X)) -> c_133(U106^#(X)) , 24: U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) , 25: U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) , 26: U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) , 27: U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) , 28: U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) , 29: U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) , 30: U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) , 31: U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) , 32: U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) , 33: U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) , 34: U13^#(mark(X)) -> c_151(U13^#(X)) , 35: U13^#(ok(X)) -> c_152(U13^#(X)) , 36: U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) , 37: U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) , 38: U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) , 39: U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) , 40: U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) , 41: U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) , 42: U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) , 43: U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) , 44: s^#(mark(X)) -> c_147(s^#(X)) , 45: s^#(ok(X)) -> c_148(s^#(X)) , 46: length^#(mark(X)) -> c_149(length^#(X)) , 47: length^#(ok(X)) -> c_150(length^#(X)) , 48: U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) , 49: U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) , 50: U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) , 51: U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) , 52: U122^#(mark(X)) -> c_156(U122^#(X)) , 53: U122^#(ok(X)) -> c_157(U122^#(X)) , 54: U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) , 55: U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) , 56: U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) , 57: U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) , 58: U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) , 59: U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) , 60: U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) , 61: U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) , 62: U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) , 63: U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) , 64: U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) , 65: U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) , 66: take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) , 67: take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) , 68: take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) , 69: U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) , 70: U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) , 71: U23^#(mark(X)) -> c_177(U23^#(X)) , 72: U23^#(ok(X)) -> c_178(U23^#(X)) , 73: U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) , 74: U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) , 75: U33^#(mark(X)) -> c_183(U33^#(X)) , 76: U33^#(ok(X)) -> c_184(U33^#(X)) , 77: U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) , 78: U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) , 79: U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) , 80: U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) , 81: U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) , 82: U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) , 83: U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) , 84: U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) , 85: U46^#(mark(X)) -> c_195(U46^#(X)) , 86: U46^#(ok(X)) -> c_196(U46^#(X)) , 87: U52^#(mark(X)) -> c_199(U52^#(X)) , 88: U52^#(ok(X)) -> c_200(U52^#(X)) , 89: U62^#(mark(X)) -> c_203(U62^#(X)) , 90: U62^#(ok(X)) -> c_204(U62^#(X)) , 91: U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) , 92: U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) , 93: U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) , 94: U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) , 95: U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) , 96: U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) , 97: U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) , 98: U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) , 99: U96^#(mark(X)) -> c_219(U96^#(X)) , 100: U96^#(ok(X)) -> c_220(U96^#(X)) , 101: isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) , 102: isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) , 103: isNat^#(ok(X)) -> c_131(isNat^#(X)) , 104: isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) , 105: isNatList^#(ok(X)) -> c_153(isNatList^#(X)) , 106: proper^#(zeros()) -> c_221() , 107: proper^#(0()) -> c_223() , 108: proper^#(tt()) -> c_225() , 109: proper^#(nil()) -> c_247() , 110: top^#(mark(X)) -> c_279(top^#(proper(X))) , 111: top^#(ok(X)) -> c_280(top^#(active(X))) } We are left with following problem, upon which TcT provides the certificate MAYBE. Strict DPs: { cons^#(mark(X1), X2) -> c_117(cons^#(X1, X2)) , cons^#(ok(X1), ok(X2)) -> c_118(cons^#(X1, X2)) , U101^#(mark(X1), X2, X3) -> c_119(U101^#(X1, X2, X3)) , U101^#(ok(X1), ok(X2), ok(X3)) -> c_120(U101^#(X1, X2, X3)) , U102^#(mark(X1), X2, X3) -> c_121(U102^#(X1, X2, X3)) , U102^#(ok(X1), ok(X2), ok(X3)) -> c_122(U102^#(X1, X2, X3)) , U103^#(mark(X1), X2, X3) -> c_124(U103^#(X1, X2, X3)) , U103^#(ok(X1), ok(X2), ok(X3)) -> c_125(U103^#(X1, X2, X3)) , U81^#(mark(X)) -> c_207(U81^#(X)) , U81^#(ok(X)) -> c_208(U81^#(X)) , U71^#(mark(X)) -> c_205(U71^#(X)) , U71^#(ok(X)) -> c_206(U71^#(X)) , U104^#(mark(X1), X2, X3) -> c_127(U104^#(X1, X2, X3)) , U104^#(ok(X1), ok(X2), ok(X3)) -> c_128(U104^#(X1, X2, X3)) , U51^#(mark(X1), X2) -> c_197(U51^#(X1, X2)) , U51^#(ok(X1), ok(X2)) -> c_198(U51^#(X1, X2)) , U61^#(mark(X1), X2) -> c_201(U61^#(X1, X2)) , U61^#(ok(X1), ok(X2)) -> c_202(U61^#(X1, X2)) , U105^#(mark(X1), X2) -> c_129(U105^#(X1, X2)) , U105^#(ok(X1), ok(X2)) -> c_130(U105^#(X1, X2)) , U106^#(mark(X)) -> c_132(U106^#(X)) , U106^#(ok(X)) -> c_133(U106^#(X)) , U21^#(mark(X1), X2) -> c_173(U21^#(X1, X2)) , U21^#(ok(X1), ok(X2)) -> c_174(U21^#(X1, X2)) , U11^#(mark(X1), X2) -> c_135(U11^#(X1, X2)) , U11^#(ok(X1), ok(X2)) -> c_136(U11^#(X1, X2)) , U31^#(mark(X1), X2) -> c_179(U31^#(X1, X2)) , U31^#(ok(X1), ok(X2)) -> c_180(U31^#(X1, X2)) , U41^#(mark(X1), X2, X3) -> c_185(U41^#(X1, X2, X3)) , U41^#(ok(X1), ok(X2), ok(X3)) -> c_186(U41^#(X1, X2, X3)) , U12^#(mark(X1), X2) -> c_137(U12^#(X1, X2)) , U12^#(ok(X1), ok(X2)) -> c_138(U12^#(X1, X2)) , U13^#(mark(X)) -> c_151(U13^#(X)) , U13^#(ok(X)) -> c_152(U13^#(X)) , U111^#(mark(X1), X2, X3) -> c_139(U111^#(X1, X2, X3)) , U111^#(ok(X1), ok(X2), ok(X3)) -> c_140(U111^#(X1, X2, X3)) , U112^#(mark(X1), X2, X3) -> c_141(U112^#(X1, X2, X3)) , U112^#(ok(X1), ok(X2), ok(X3)) -> c_142(U112^#(X1, X2, X3)) , U113^#(mark(X1), X2, X3) -> c_143(U113^#(X1, X2, X3)) , U113^#(ok(X1), ok(X2), ok(X3)) -> c_144(U113^#(X1, X2, X3)) , U114^#(mark(X1), X2) -> c_145(U114^#(X1, X2)) , U114^#(ok(X1), ok(X2)) -> c_146(U114^#(X1, X2)) , s^#(mark(X)) -> c_147(s^#(X)) , s^#(ok(X)) -> c_148(s^#(X)) , length^#(mark(X)) -> c_149(length^#(X)) , length^#(ok(X)) -> c_150(length^#(X)) , U91^#(mark(X1), X2, X3) -> c_209(U91^#(X1, X2, X3)) , U91^#(ok(X1), ok(X2), ok(X3)) -> c_210(U91^#(X1, X2, X3)) , U121^#(mark(X1), X2) -> c_154(U121^#(X1, X2)) , U121^#(ok(X1), ok(X2)) -> c_155(U121^#(X1, X2)) , U122^#(mark(X)) -> c_156(U122^#(X)) , U122^#(ok(X)) -> c_157(U122^#(X)) , U131^#(mark(X1), X2, X3, X4) -> c_158(U131^#(X1, X2, X3, X4)) , U131^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_159(U131^#(X1, X2, X3, X4)) , U132^#(mark(X1), X2, X3, X4) -> c_160(U132^#(X1, X2, X3, X4)) , U132^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_161(U132^#(X1, X2, X3, X4)) , U133^#(mark(X1), X2, X3, X4) -> c_162(U133^#(X1, X2, X3, X4)) , U133^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_163(U133^#(X1, X2, X3, X4)) , U134^#(mark(X1), X2, X3, X4) -> c_164(U134^#(X1, X2, X3, X4)) , U134^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_165(U134^#(X1, X2, X3, X4)) , U135^#(mark(X1), X2, X3, X4) -> c_166(U135^#(X1, X2, X3, X4)) , U135^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_167(U135^#(X1, X2, X3, X4)) , U136^#(mark(X1), X2, X3, X4) -> c_168(U136^#(X1, X2, X3, X4)) , U136^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> c_169(U136^#(X1, X2, X3, X4)) , take^#(X1, mark(X2)) -> c_170(take^#(X1, X2)) , take^#(mark(X1), X2) -> c_171(take^#(X1, X2)) , take^#(ok(X1), ok(X2)) -> c_172(take^#(X1, X2)) , U22^#(mark(X1), X2) -> c_175(U22^#(X1, X2)) , U22^#(ok(X1), ok(X2)) -> c_176(U22^#(X1, X2)) , U23^#(mark(X)) -> c_177(U23^#(X)) , U23^#(ok(X)) -> c_178(U23^#(X)) , U32^#(mark(X1), X2) -> c_181(U32^#(X1, X2)) , U32^#(ok(X1), ok(X2)) -> c_182(U32^#(X1, X2)) , U33^#(mark(X)) -> c_183(U33^#(X)) , U33^#(ok(X)) -> c_184(U33^#(X)) , U42^#(mark(X1), X2, X3) -> c_187(U42^#(X1, X2, X3)) , U42^#(ok(X1), ok(X2), ok(X3)) -> c_188(U42^#(X1, X2, X3)) , U43^#(mark(X1), X2, X3) -> c_189(U43^#(X1, X2, X3)) , U43^#(ok(X1), ok(X2), ok(X3)) -> c_190(U43^#(X1, X2, X3)) , U44^#(mark(X1), X2, X3) -> c_191(U44^#(X1, X2, X3)) , U44^#(ok(X1), ok(X2), ok(X3)) -> c_192(U44^#(X1, X2, X3)) , U45^#(mark(X1), X2) -> c_193(U45^#(X1, X2)) , U45^#(ok(X1), ok(X2)) -> c_194(U45^#(X1, X2)) , U46^#(mark(X)) -> c_195(U46^#(X)) , U46^#(ok(X)) -> c_196(U46^#(X)) , U52^#(mark(X)) -> c_199(U52^#(X)) , U52^#(ok(X)) -> c_200(U52^#(X)) , U62^#(mark(X)) -> c_203(U62^#(X)) , U62^#(ok(X)) -> c_204(U62^#(X)) , U92^#(mark(X1), X2, X3) -> c_211(U92^#(X1, X2, X3)) , U92^#(ok(X1), ok(X2), ok(X3)) -> c_212(U92^#(X1, X2, X3)) , U93^#(mark(X1), X2, X3) -> c_213(U93^#(X1, X2, X3)) , U93^#(ok(X1), ok(X2), ok(X3)) -> c_214(U93^#(X1, X2, X3)) , U94^#(mark(X1), X2, X3) -> c_215(U94^#(X1, X2, X3)) , U94^#(ok(X1), ok(X2), ok(X3)) -> c_216(U94^#(X1, X2, X3)) , U95^#(mark(X1), X2) -> c_217(U95^#(X1, X2)) , U95^#(ok(X1), ok(X2)) -> c_218(U95^#(X1, X2)) , U96^#(mark(X)) -> c_219(U96^#(X)) , U96^#(ok(X)) -> c_220(U96^#(X)) , isNatKind^#(ok(X)) -> c_123(isNatKind^#(X)) , isNatIListKind^#(ok(X)) -> c_126(isNatIListKind^#(X)) , isNat^#(ok(X)) -> c_131(isNat^#(X)) , isNatIList^#(ok(X)) -> c_134(isNatIList^#(X)) , isNatList^#(ok(X)) -> c_153(isNatList^#(X)) , top^#(mark(X)) -> c_279(top^#(proper(X))) , top^#(ok(X)) -> c_280(top^#(active(X))) } Strict Trs: { active(zeros()) -> mark(cons(0(), zeros())) , active(cons(X1, X2)) -> cons(active(X1), X2) , active(U101(X1, X2, X3)) -> U101(active(X1), X2, X3) , active(U101(tt(), V1, V2)) -> mark(U102(isNatKind(V1), V1, V2)) , active(U102(X1, X2, X3)) -> U102(active(X1), X2, X3) , active(U102(tt(), V1, V2)) -> mark(U103(isNatIListKind(V2), V1, V2)) , active(isNatKind(0())) -> mark(tt()) , active(isNatKind(s(V1))) -> mark(U81(isNatKind(V1))) , active(isNatKind(length(V1))) -> mark(U71(isNatIListKind(V1))) , active(U103(X1, X2, X3)) -> U103(active(X1), X2, X3) , active(U103(tt(), V1, V2)) -> mark(U104(isNatIListKind(V2), V1, V2)) , active(isNatIListKind(zeros())) -> mark(tt()) , active(isNatIListKind(cons(V1, V2))) -> mark(U51(isNatKind(V1), V2)) , active(isNatIListKind(nil())) -> mark(tt()) , active(isNatIListKind(take(V1, V2))) -> mark(U61(isNatKind(V1), V2)) , active(U104(X1, X2, X3)) -> U104(active(X1), X2, X3) , active(U104(tt(), V1, V2)) -> mark(U105(isNat(V1), V2)) , active(U105(X1, X2)) -> U105(active(X1), X2) , active(U105(tt(), V2)) -> mark(U106(isNatIList(V2))) , active(isNat(0())) -> mark(tt()) , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) , active(U106(X)) -> U106(active(X)) , active(U106(tt())) -> mark(tt()) , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) , active(isNatIList(zeros())) -> mark(tt()) , active(isNatIList(cons(V1, V2))) -> mark(U41(isNatKind(V1), V1, V2)) , active(U11(X1, X2)) -> U11(active(X1), X2) , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) , active(U12(X1, X2)) -> U12(active(X1), X2) , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) , active(U111(X1, X2, X3)) -> U111(active(X1), X2, X3) , active(U111(tt(), L, N)) -> mark(U112(isNatIListKind(L), L, N)) , active(U112(X1, X2, X3)) -> U112(active(X1), X2, X3) , active(U112(tt(), L, N)) -> mark(U113(isNat(N), L, N)) , active(U113(X1, X2, X3)) -> U113(active(X1), X2, X3) , active(U113(tt(), L, N)) -> mark(U114(isNatKind(N), L)) , active(U114(X1, X2)) -> U114(active(X1), X2) , active(U114(tt(), L)) -> mark(s(length(L))) , active(s(X)) -> s(active(X)) , active(length(X)) -> length(active(X)) , active(length(cons(N, L))) -> mark(U111(isNatList(L), L, N)) , active(length(nil())) -> mark(0()) , active(U13(X)) -> U13(active(X)) , active(U13(tt())) -> mark(tt()) , active(isNatList(cons(V1, V2))) -> mark(U91(isNatKind(V1), V1, V2)) , active(isNatList(nil())) -> mark(tt()) , active(isNatList(take(V1, V2))) -> mark(U101(isNatKind(V1), V1, V2)) , active(U121(X1, X2)) -> U121(active(X1), X2) , active(U121(tt(), IL)) -> mark(U122(isNatIListKind(IL))) , active(U122(X)) -> U122(active(X)) , active(U122(tt())) -> mark(nil()) , active(U131(X1, X2, X3, X4)) -> U131(active(X1), X2, X3, X4) , active(U131(tt(), IL, M, N)) -> mark(U132(isNatIListKind(IL), IL, M, N)) , active(U132(X1, X2, X3, X4)) -> U132(active(X1), X2, X3, X4) , active(U132(tt(), IL, M, N)) -> mark(U133(isNat(M), IL, M, N)) , active(U133(X1, X2, X3, X4)) -> U133(active(X1), X2, X3, X4) , active(U133(tt(), IL, M, N)) -> mark(U134(isNatKind(M), IL, M, N)) , active(U134(X1, X2, X3, X4)) -> U134(active(X1), X2, X3, X4) , active(U134(tt(), IL, M, N)) -> mark(U135(isNat(N), IL, M, N)) , active(U135(X1, X2, X3, X4)) -> U135(active(X1), X2, X3, X4) , active(U135(tt(), IL, M, N)) -> mark(U136(isNatKind(N), IL, M, N)) , active(U136(X1, X2, X3, X4)) -> U136(active(X1), X2, X3, X4) , active(U136(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) , active(take(X1, X2)) -> take(X1, active(X2)) , active(take(X1, X2)) -> take(active(X1), X2) , active(take(0(), IL)) -> mark(U121(isNatIList(IL), IL)) , active(take(s(M), cons(N, IL))) -> mark(U131(isNatIList(IL), IL, M, N)) , active(U21(X1, X2)) -> U21(active(X1), X2) , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) , active(U22(X1, X2)) -> U22(active(X1), X2) , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) , active(U23(X)) -> U23(active(X)) , active(U23(tt())) -> mark(tt()) , active(U31(X1, X2)) -> U31(active(X1), X2) , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) , active(U32(X1, X2)) -> U32(active(X1), X2) , active(U32(tt(), V)) -> mark(U33(isNatList(V))) , active(U33(X)) -> U33(active(X)) , active(U33(tt())) -> mark(tt()) , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) , active(U42(tt(), V1, V2)) -> mark(U43(isNatIListKind(V2), V1, V2)) , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) , active(U43(tt(), V1, V2)) -> mark(U44(isNatIListKind(V2), V1, V2)) , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) , active(U45(X1, X2)) -> U45(active(X1), X2) , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) , active(U46(X)) -> U46(active(X)) , active(U46(tt())) -> mark(tt()) , active(U51(X1, X2)) -> U51(active(X1), X2) , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) , active(U52(X)) -> U52(active(X)) , active(U52(tt())) -> mark(tt()) , active(U61(X1, X2)) -> U61(active(X1), X2) , active(U61(tt(), V2)) -> mark(U62(isNatIListKind(V2))) , active(U62(X)) -> U62(active(X)) , active(U62(tt())) -> mark(tt()) , active(U71(X)) -> U71(active(X)) , active(U71(tt())) -> mark(tt()) , active(U81(X)) -> U81(active(X)) , active(U81(tt())) -> mark(tt()) , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) , active(U91(tt(), V1, V2)) -> mark(U92(isNatKind(V1), V1, V2)) , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) , active(U92(tt(), V1, V2)) -> mark(U93(isNatIListKind(V2), V1, V2)) , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) , active(U93(tt(), V1, V2)) -> mark(U94(isNatIListKind(V2), V1, V2)) , active(U94(X1, X2, X3)) -> U94(active(X1), X2, X3) , active(U94(tt(), V1, V2)) -> mark(U95(isNat(V1), V2)) , active(U95(X1, X2)) -> U95(active(X1), X2) , active(U95(tt(), V2)) -> mark(U96(isNatList(V2))) , active(U96(X)) -> U96(active(X)) , active(U96(tt())) -> mark(tt()) , cons(mark(X1), X2) -> mark(cons(X1, X2)) , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) , U101(mark(X1), X2, X3) -> mark(U101(X1, X2, X3)) , U101(ok(X1), ok(X2), ok(X3)) -> ok(U101(X1, X2, X3)) , U102(mark(X1), X2, X3) -> mark(U102(X1, X2, X3)) , U102(ok(X1), ok(X2), ok(X3)) -> ok(U102(X1, X2, X3)) , isNatKind(ok(X)) -> ok(isNatKind(X)) , U103(mark(X1), X2, X3) -> mark(U103(X1, X2, X3)) , U103(ok(X1), ok(X2), ok(X3)) -> ok(U103(X1, X2, X3)) , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) , U104(mark(X1), X2, X3) -> mark(U104(X1, X2, X3)) , U104(ok(X1), ok(X2), ok(X3)) -> ok(U104(X1, X2, X3)) , U105(mark(X1), X2) -> mark(U105(X1, X2)) , U105(ok(X1), ok(X2)) -> ok(U105(X1, X2)) , isNat(ok(X)) -> ok(isNat(X)) , U106(mark(X)) -> mark(U106(X)) , U106(ok(X)) -> ok(U106(X)) , isNatIList(ok(X)) -> ok(isNatIList(X)) , U11(mark(X1), X2) -> mark(U11(X1, X2)) , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) , U12(mark(X1), X2) -> mark(U12(X1, X2)) , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) , U111(mark(X1), X2, X3) -> mark(U111(X1, X2, X3)) , U111(ok(X1), ok(X2), ok(X3)) -> ok(U111(X1, X2, X3)) , U112(mark(X1), X2, X3) -> mark(U112(X1, X2, X3)) , U112(ok(X1), ok(X2), ok(X3)) -> ok(U112(X1, X2, X3)) , U113(mark(X1), X2, X3) -> mark(U113(X1, X2, X3)) , U113(ok(X1), ok(X2), ok(X3)) -> ok(U113(X1, X2, X3)) , U114(mark(X1), X2) -> mark(U114(X1, X2)) , U114(ok(X1), ok(X2)) -> ok(U114(X1, X2)) , s(mark(X)) -> mark(s(X)) , s(ok(X)) -> ok(s(X)) , length(mark(X)) -> mark(length(X)) , length(ok(X)) -> ok(length(X)) , U13(mark(X)) -> mark(U13(X)) , U13(ok(X)) -> ok(U13(X)) , isNatList(ok(X)) -> ok(isNatList(X)) , U121(mark(X1), X2) -> mark(U121(X1, X2)) , U121(ok(X1), ok(X2)) -> ok(U121(X1, X2)) , U122(mark(X)) -> mark(U122(X)) , U122(ok(X)) -> ok(U122(X)) , U131(mark(X1), X2, X3, X4) -> mark(U131(X1, X2, X3, X4)) , U131(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U131(X1, X2, X3, X4)) , U132(mark(X1), X2, X3, X4) -> mark(U132(X1, X2, X3, X4)) , U132(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U132(X1, X2, X3, X4)) , U133(mark(X1), X2, X3, X4) -> mark(U133(X1, X2, X3, X4)) , U133(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U133(X1, X2, X3, X4)) , U134(mark(X1), X2, X3, X4) -> mark(U134(X1, X2, X3, X4)) , U134(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U134(X1, X2, X3, X4)) , U135(mark(X1), X2, X3, X4) -> mark(U135(X1, X2, X3, X4)) , U135(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U135(X1, X2, X3, X4)) , U136(mark(X1), X2, X3, X4) -> mark(U136(X1, X2, X3, X4)) , U136(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U136(X1, X2, X3, X4)) , take(X1, mark(X2)) -> mark(take(X1, X2)) , take(mark(X1), X2) -> mark(take(X1, X2)) , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) , U21(mark(X1), X2) -> mark(U21(X1, X2)) , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) , U22(mark(X1), X2) -> mark(U22(X1, X2)) , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) , U23(mark(X)) -> mark(U23(X)) , U23(ok(X)) -> ok(U23(X)) , U31(mark(X1), X2) -> mark(U31(X1, X2)) , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) , U32(mark(X1), X2) -> mark(U32(X1, X2)) , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) , U33(mark(X)) -> mark(U33(X)) , U33(ok(X)) -> ok(U33(X)) , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) , U45(mark(X1), X2) -> mark(U45(X1, X2)) , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) , U46(mark(X)) -> mark(U46(X)) , U46(ok(X)) -> ok(U46(X)) , U51(mark(X1), X2) -> mark(U51(X1, X2)) , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) , U52(mark(X)) -> mark(U52(X)) , U52(ok(X)) -> ok(U52(X)) , U61(mark(X1), X2) -> mark(U61(X1, X2)) , U61(ok(X1), ok(X2)) -> ok(U61(X1, X2)) , U62(mark(X)) -> mark(U62(X)) , U62(ok(X)) -> ok(U62(X)) , U71(mark(X)) -> mark(U71(X)) , U71(ok(X)) -> ok(U71(X)) , U81(mark(X)) -> mark(U81(X)) , U81(ok(X)) -> ok(U81(X)) , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) , U94(mark(X1), X2, X3) -> mark(U94(X1, X2, X3)) , U94(ok(X1), ok(X2), ok(X3)) -> ok(U94(X1, X2, X3)) , U95(mark(X1), X2) -> mark(U95(X1, X2)) , U95(ok(X1), ok(X2)) -> ok(U95(X1, X2)) , U96(mark(X)) -> mark(U96(X)) , U96(ok(X)) -> ok(U96(X)) , proper(zeros()) -> ok(zeros()) , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) , proper(0()) -> ok(0()) , proper(U101(X1, X2, X3)) -> U101(proper(X1), proper(X2), proper(X3)) , proper(tt()) -> ok(tt()) , proper(U102(X1, X2, X3)) -> U102(proper(X1), proper(X2), proper(X3)) , proper(isNatKind(X)) -> isNatKind(proper(X)) , proper(U103(X1, X2, X3)) -> U103(proper(X1), proper(X2), proper(X3)) , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) , proper(U104(X1, X2, X3)) -> U104(proper(X1), proper(X2), proper(X3)) , proper(U105(X1, X2)) -> U105(proper(X1), proper(X2)) , proper(isNat(X)) -> isNat(proper(X)) , proper(U106(X)) -> U106(proper(X)) , proper(isNatIList(X)) -> isNatIList(proper(X)) , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) , proper(U111(X1, X2, X3)) -> U111(proper(X1), proper(X2), proper(X3)) , proper(U112(X1, X2, X3)) -> U112(proper(X1), proper(X2), proper(X3)) , proper(U113(X1, X2, X3)) -> U113(proper(X1), proper(X2), proper(X3)) , proper(U114(X1, X2)) -> U114(proper(X1), proper(X2)) , proper(s(X)) -> s(proper(X)) , proper(length(X)) -> length(proper(X)) , proper(U13(X)) -> U13(proper(X)) , proper(isNatList(X)) -> isNatList(proper(X)) , proper(U121(X1, X2)) -> U121(proper(X1), proper(X2)) , proper(U122(X)) -> U122(proper(X)) , proper(nil()) -> ok(nil()) , proper(U131(X1, X2, X3, X4)) -> U131(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U132(X1, X2, X3, X4)) -> U132(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U133(X1, X2, X3, X4)) -> U133(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U134(X1, X2, X3, X4)) -> U134(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U135(X1, X2, X3, X4)) -> U135(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(U136(X1, X2, X3, X4)) -> U136(proper(X1), proper(X2), proper(X3), proper(X4)) , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) , proper(U23(X)) -> U23(proper(X)) , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) , proper(U33(X)) -> U33(proper(X)) , proper(U41(X1, X2, X3)) -> U41(proper(X1), proper(X2), proper(X3)) , proper(U42(X1, X2, X3)) -> U42(proper(X1), proper(X2), proper(X3)) , proper(U43(X1, X2, X3)) -> U43(proper(X1), proper(X2), proper(X3)) , proper(U44(X1, X2, X3)) -> U44(proper(X1), proper(X2), proper(X3)) , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) , proper(U46(X)) -> U46(proper(X)) , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) , proper(U52(X)) -> U52(proper(X)) , proper(U61(X1, X2)) -> U61(proper(X1), proper(X2)) , proper(U62(X)) -> U62(proper(X)) , proper(U71(X)) -> U71(proper(X)) , proper(U81(X)) -> U81(proper(X)) , proper(U91(X1, X2, X3)) -> U91(proper(X1), proper(X2), proper(X3)) , proper(U92(X1, X2, X3)) -> U92(proper(X1), proper(X2), proper(X3)) , proper(U93(X1, X2, X3)) -> U93(proper(X1), proper(X2), proper(X3)) , proper(U94(X1, X2, X3)) -> U94(proper(X1), proper(X2), proper(X3)) , proper(U95(X1, X2)) -> U95(proper(X1), proper(X2)) , proper(U96(X)) -> U96(proper(X)) , top(mark(X)) -> top(proper(X)) , top(ok(X)) -> top(active(X)) } Weak DPs: { active^#(zeros()) -> c_1(cons^#(0(), zeros())) , proper^#(zeros()) -> c_221() , proper^#(0()) -> c_223() , proper^#(tt()) -> c_225() , proper^#(nil()) -> c_247() } Obligation: runtime complexity Answer: MAYBE Empty strict component of the problem is NOT empty. Arrrr..