MAYBE 1123.22/297.08 MAYBE 1123.22/297.08 1123.22/297.08 We are left with following problem, upon which TcT provides the 1123.22/297.08 certificate MAYBE. 1123.22/297.08 1123.22/297.08 Strict Trs: 1123.22/297.08 { active(zeros()) -> mark(cons(0(), zeros())) 1123.22/297.08 , active(cons(X1, X2)) -> cons(active(X1), X2) 1123.22/297.08 , active(U11(X1, X2)) -> U11(active(X1), X2) 1123.22/297.08 , active(U11(tt(), V1)) -> mark(U12(isNatList(V1))) 1123.22/297.08 , active(U12(X)) -> U12(active(X)) 1123.22/297.08 , active(U12(tt())) -> mark(tt()) 1123.22/297.08 , active(isNatList(cons(V1, V2))) -> 1123.22/297.08 mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.08 , active(isNatList(nil())) -> mark(tt()) 1123.22/297.08 , active(isNatList(take(V1, V2))) -> 1123.22/297.08 mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.08 , active(U21(X1, X2)) -> U21(active(X1), X2) 1123.22/297.08 , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) 1123.22/297.08 , active(U22(X)) -> U22(active(X)) 1123.22/297.08 , active(U22(tt())) -> mark(tt()) 1123.22/297.08 , active(isNat(0())) -> mark(tt()) 1123.22/297.08 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1123.22/297.08 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 1123.22/297.08 , active(U31(X1, X2)) -> U31(active(X1), X2) 1123.22/297.08 , active(U31(tt(), V)) -> mark(U32(isNatList(V))) 1123.22/297.08 , active(U32(X)) -> U32(active(X)) 1123.22/297.08 , active(U32(tt())) -> mark(tt()) 1123.22/297.08 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 1123.22/297.08 , active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2)) 1123.22/297.08 , active(U42(X1, X2)) -> U42(active(X1), X2) 1123.22/297.08 , active(U42(tt(), V2)) -> mark(U43(isNatIList(V2))) 1123.22/297.08 , active(U43(X)) -> U43(active(X)) 1123.22/297.08 , active(U43(tt())) -> mark(tt()) 1123.22/297.08 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 1123.22/297.08 , active(isNatIList(zeros())) -> mark(tt()) 1123.22/297.08 , active(isNatIList(cons(V1, V2))) -> 1123.22/297.08 mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.08 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 1123.22/297.08 , active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2)) 1123.22/297.08 , active(U52(X1, X2)) -> U52(active(X1), X2) 1123.22/297.08 , active(U52(tt(), V2)) -> mark(U53(isNatList(V2))) 1123.22/297.08 , active(U53(X)) -> U53(active(X)) 1123.22/297.08 , active(U53(tt())) -> mark(tt()) 1123.22/297.08 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1123.22/297.08 , active(U61(tt(), V1, V2)) -> mark(U62(isNat(V1), V2)) 1123.22/297.08 , active(U62(X1, X2)) -> U62(active(X1), X2) 1123.22/297.08 , active(U62(tt(), V2)) -> mark(U63(isNatIList(V2))) 1123.22/297.08 , active(U63(X)) -> U63(active(X)) 1123.22/297.08 , active(U63(tt())) -> mark(tt()) 1123.22/297.08 , active(U71(X1, X2)) -> U71(active(X1), X2) 1123.22/297.08 , active(U71(tt(), L)) -> mark(s(length(L))) 1123.22/297.08 , active(s(X)) -> s(active(X)) 1123.22/297.08 , active(length(X)) -> length(active(X)) 1123.22/297.08 , active(length(cons(N, L))) -> 1123.22/297.08 mark(U71(and(and(isNatList(L), isNatIListKind(L)), 1123.22/297.08 and(isNat(N), isNatKind(N))), 1123.22/297.08 L)) 1123.22/297.08 , active(length(nil())) -> mark(0()) 1123.22/297.08 , active(U81(X)) -> U81(active(X)) 1123.22/297.08 , active(U81(tt())) -> mark(nil()) 1123.22/297.08 , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) 1123.22/297.08 , active(U91(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 1123.22/297.08 , active(take(X1, X2)) -> take(X1, active(X2)) 1123.22/297.08 , active(take(X1, X2)) -> take(active(X1), X2) 1123.22/297.08 , active(take(0(), IL)) -> 1123.22/297.08 mark(U81(and(isNatIList(IL), isNatIListKind(IL)))) 1123.22/297.08 , active(take(s(M), cons(N, IL))) -> 1123.22/297.08 mark(U91(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.22/297.08 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.22/297.08 IL, 1123.22/297.08 M, 1123.22/297.08 N)) 1123.22/297.08 , active(and(X1, X2)) -> and(active(X1), X2) 1123.22/297.08 , active(and(tt(), X)) -> mark(X) 1123.22/297.08 , active(isNatIListKind(zeros())) -> mark(tt()) 1123.22/297.08 , active(isNatIListKind(cons(V1, V2))) -> 1123.22/297.08 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.08 , active(isNatIListKind(nil())) -> mark(tt()) 1123.22/297.08 , active(isNatIListKind(take(V1, V2))) -> 1123.22/297.08 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.08 , active(isNatKind(0())) -> mark(tt()) 1123.22/297.08 , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) 1123.22/297.08 , active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)) 1123.22/297.08 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1123.22/297.08 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1123.22/297.08 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 1123.22/297.08 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 1123.22/297.08 , U12(mark(X)) -> mark(U12(X)) 1123.22/297.08 , U12(ok(X)) -> ok(U12(X)) 1123.22/297.08 , isNatList(ok(X)) -> ok(isNatList(X)) 1123.22/297.08 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1123.22/297.08 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1123.22/297.08 , U22(mark(X)) -> mark(U22(X)) 1123.22/297.08 , U22(ok(X)) -> ok(U22(X)) 1123.22/297.08 , isNat(ok(X)) -> ok(isNat(X)) 1123.22/297.08 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1123.22/297.08 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1123.22/297.08 , U32(mark(X)) -> mark(U32(X)) 1123.22/297.08 , U32(ok(X)) -> ok(U32(X)) 1123.22/297.08 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 1123.22/297.08 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 1123.22/297.08 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 1123.22/297.08 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 1123.22/297.08 , U43(mark(X)) -> mark(U43(X)) 1123.22/297.08 , U43(ok(X)) -> ok(U43(X)) 1123.22/297.08 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1123.22/297.08 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 1123.22/297.08 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 1123.22/297.08 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1123.22/297.08 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1123.22/297.08 , U53(mark(X)) -> mark(U53(X)) 1123.22/297.08 , U53(ok(X)) -> ok(U53(X)) 1123.22/297.08 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1123.22/297.08 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1123.22/297.08 , U62(mark(X1), X2) -> mark(U62(X1, X2)) 1123.22/297.08 , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) 1123.22/297.08 , U63(mark(X)) -> mark(U63(X)) 1123.22/297.08 , U63(ok(X)) -> ok(U63(X)) 1123.22/297.08 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1123.22/297.08 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1123.22/297.08 , s(mark(X)) -> mark(s(X)) 1123.22/297.08 , s(ok(X)) -> ok(s(X)) 1123.22/297.08 , length(mark(X)) -> mark(length(X)) 1123.22/297.08 , length(ok(X)) -> ok(length(X)) 1123.22/297.08 , U81(mark(X)) -> mark(U81(X)) 1123.22/297.08 , U81(ok(X)) -> ok(U81(X)) 1123.22/297.08 , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) 1123.22/297.08 , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) 1123.22/297.08 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1123.22/297.08 , take(mark(X1), X2) -> mark(take(X1, X2)) 1123.22/297.08 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1123.22/297.08 , and(mark(X1), X2) -> mark(and(X1, X2)) 1123.22/297.08 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1123.22/297.08 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 1123.22/297.08 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1123.22/297.08 , proper(zeros()) -> ok(zeros()) 1123.22/297.08 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1123.22/297.08 , proper(0()) -> ok(0()) 1123.22/297.08 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 1123.22/297.08 , proper(tt()) -> ok(tt()) 1123.22/297.08 , proper(U12(X)) -> U12(proper(X)) 1123.22/297.08 , proper(isNatList(X)) -> isNatList(proper(X)) 1123.22/297.08 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1123.22/297.08 , proper(U22(X)) -> U22(proper(X)) 1123.22/297.08 , proper(isNat(X)) -> isNat(proper(X)) 1123.22/297.08 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1123.22/297.08 , proper(U32(X)) -> U32(proper(X)) 1123.22/297.08 , proper(U41(X1, X2, X3)) -> 1123.22/297.08 U41(proper(X1), proper(X2), proper(X3)) 1123.22/297.08 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 1123.22/297.08 , proper(U43(X)) -> U43(proper(X)) 1123.22/297.08 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1123.22/297.08 , proper(U51(X1, X2, X3)) -> 1123.22/297.08 U51(proper(X1), proper(X2), proper(X3)) 1123.22/297.08 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1123.22/297.08 , proper(U53(X)) -> U53(proper(X)) 1123.22/297.08 , proper(U61(X1, X2, X3)) -> 1123.22/297.08 U61(proper(X1), proper(X2), proper(X3)) 1123.22/297.08 , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) 1123.22/297.08 , proper(U63(X)) -> U63(proper(X)) 1123.22/297.08 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1123.22/297.08 , proper(s(X)) -> s(proper(X)) 1123.22/297.08 , proper(length(X)) -> length(proper(X)) 1123.22/297.08 , proper(U81(X)) -> U81(proper(X)) 1123.22/297.08 , proper(nil()) -> ok(nil()) 1123.22/297.08 , proper(U91(X1, X2, X3, X4)) -> 1123.22/297.08 U91(proper(X1), proper(X2), proper(X3), proper(X4)) 1123.22/297.08 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1123.22/297.08 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1123.22/297.08 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 1123.22/297.08 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1123.22/297.08 , top(mark(X)) -> top(proper(X)) 1123.22/297.08 , top(ok(X)) -> top(active(X)) } 1123.22/297.08 Obligation: 1123.22/297.08 runtime complexity 1123.22/297.08 Answer: 1123.22/297.08 MAYBE 1123.22/297.08 1123.22/297.08 None of the processors succeeded. 1123.22/297.08 1123.22/297.08 Details of failed attempt(s): 1123.22/297.08 ----------------------------- 1123.22/297.08 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 1123.22/297.08 following reason: 1123.22/297.08 1123.22/297.08 Computation stopped due to timeout after 297.0 seconds. 1123.22/297.08 1123.22/297.08 2) 'Best' failed due to the following reason: 1123.22/297.08 1123.22/297.08 None of the processors succeeded. 1123.22/297.08 1123.22/297.08 Details of failed attempt(s): 1123.22/297.08 ----------------------------- 1123.22/297.08 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 1123.22/297.08 seconds)' failed due to the following reason: 1123.22/297.08 1123.22/297.08 Computation stopped due to timeout after 148.0 seconds. 1123.22/297.09 1123.22/297.09 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 1123.22/297.09 failed due to the following reason: 1123.22/297.09 1123.22/297.09 None of the processors succeeded. 1123.22/297.09 1123.22/297.09 Details of failed attempt(s): 1123.22/297.09 ----------------------------- 1123.22/297.09 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 1123.22/297.09 failed due to the following reason: 1123.22/297.09 1123.22/297.09 match-boundness of the problem could not be verified. 1123.22/297.09 1123.22/297.09 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 1123.22/297.09 failed due to the following reason: 1123.22/297.09 1123.22/297.09 match-boundness of the problem could not be verified. 1123.22/297.09 1123.22/297.09 1123.22/297.09 3) 'Best' failed due to the following reason: 1123.22/297.09 1123.22/297.09 None of the processors succeeded. 1123.22/297.09 1123.22/297.09 Details of failed attempt(s): 1123.22/297.09 ----------------------------- 1123.22/297.09 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 1123.22/297.09 following reason: 1123.22/297.09 1123.22/297.09 The processor is inapplicable, reason: 1123.22/297.09 Processor only applicable for innermost runtime complexity analysis 1123.22/297.09 1123.22/297.09 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 1123.22/297.09 to the following reason: 1123.22/297.09 1123.22/297.09 The processor is inapplicable, reason: 1123.22/297.09 Processor only applicable for innermost runtime complexity analysis 1123.22/297.09 1123.22/297.09 1123.22/297.09 1123.22/297.09 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 1123.22/297.09 the following reason: 1123.22/297.09 1123.22/297.09 We add the following weak dependency pairs: 1123.22/297.09 1123.22/297.09 Strict DPs: 1123.22/297.09 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 1123.22/297.09 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 1123.22/297.09 , active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 1123.22/297.09 , active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1))) 1123.22/297.09 , active^#(U12(X)) -> c_5(U12^#(active(X))) 1123.22/297.09 , active^#(U12(tt())) -> c_6() 1123.22/297.09 , active^#(isNatList(cons(V1, V2))) -> 1123.22/297.09 c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.09 , active^#(isNatList(nil())) -> c_8() 1123.22/297.09 , active^#(isNatList(take(V1, V2))) -> 1123.22/297.09 c_9(U61^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.09 , active^#(U21(X1, X2)) -> c_10(U21^#(active(X1), X2)) 1123.22/297.09 , active^#(U21(tt(), V1)) -> c_11(U22^#(isNat(V1))) 1123.22/297.09 , active^#(U22(X)) -> c_12(U22^#(active(X))) 1123.22/297.09 , active^#(U22(tt())) -> c_13() 1123.22/297.09 , active^#(isNat(0())) -> c_14() 1123.22/297.09 , active^#(isNat(s(V1))) -> c_15(U21^#(isNatKind(V1), V1)) 1123.22/297.09 , active^#(isNat(length(V1))) -> 1123.22/297.09 c_16(U11^#(isNatIListKind(V1), V1)) 1123.22/297.09 , active^#(U31(X1, X2)) -> c_17(U31^#(active(X1), X2)) 1123.22/297.09 , active^#(U31(tt(), V)) -> c_18(U32^#(isNatList(V))) 1123.22/297.09 , active^#(U32(X)) -> c_19(U32^#(active(X))) 1123.22/297.09 , active^#(U32(tt())) -> c_20() 1123.22/297.09 , active^#(U41(X1, X2, X3)) -> c_21(U41^#(active(X1), X2, X3)) 1123.22/297.09 , active^#(U41(tt(), V1, V2)) -> c_22(U42^#(isNat(V1), V2)) 1123.22/297.09 , active^#(U42(X1, X2)) -> c_23(U42^#(active(X1), X2)) 1123.22/297.09 , active^#(U42(tt(), V2)) -> c_24(U43^#(isNatIList(V2))) 1123.22/297.09 , active^#(U43(X)) -> c_25(U43^#(active(X))) 1123.22/297.09 , active^#(U43(tt())) -> c_26() 1123.22/297.09 , active^#(isNatIList(V)) -> c_27(U31^#(isNatIListKind(V), V)) 1123.22/297.09 , active^#(isNatIList(zeros())) -> c_28() 1123.22/297.09 , active^#(isNatIList(cons(V1, V2))) -> 1123.22/297.09 c_29(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.09 , active^#(U51(X1, X2, X3)) -> c_30(U51^#(active(X1), X2, X3)) 1123.22/297.09 , active^#(U51(tt(), V1, V2)) -> c_31(U52^#(isNat(V1), V2)) 1123.22/297.09 , active^#(U52(X1, X2)) -> c_32(U52^#(active(X1), X2)) 1123.22/297.09 , active^#(U52(tt(), V2)) -> c_33(U53^#(isNatList(V2))) 1123.22/297.09 , active^#(U53(X)) -> c_34(U53^#(active(X))) 1123.22/297.09 , active^#(U53(tt())) -> c_35() 1123.22/297.09 , active^#(U61(X1, X2, X3)) -> c_36(U61^#(active(X1), X2, X3)) 1123.22/297.09 , active^#(U61(tt(), V1, V2)) -> c_37(U62^#(isNat(V1), V2)) 1123.22/297.09 , active^#(U62(X1, X2)) -> c_38(U62^#(active(X1), X2)) 1123.22/297.09 , active^#(U62(tt(), V2)) -> c_39(U63^#(isNatIList(V2))) 1123.22/297.09 , active^#(U63(X)) -> c_40(U63^#(active(X))) 1123.22/297.09 , active^#(U63(tt())) -> c_41() 1123.22/297.09 , active^#(U71(X1, X2)) -> c_42(U71^#(active(X1), X2)) 1123.22/297.09 , active^#(U71(tt(), L)) -> c_43(s^#(length(L))) 1123.22/297.09 , active^#(s(X)) -> c_44(s^#(active(X))) 1123.22/297.09 , active^#(length(X)) -> c_45(length^#(active(X))) 1123.22/297.09 , active^#(length(cons(N, L))) -> 1123.22/297.09 c_46(U71^#(and(and(isNatList(L), isNatIListKind(L)), 1123.22/297.09 and(isNat(N), isNatKind(N))), 1123.22/297.09 L)) 1123.22/297.09 , active^#(length(nil())) -> c_47() 1123.22/297.09 , active^#(U81(X)) -> c_48(U81^#(active(X))) 1123.22/297.09 , active^#(U81(tt())) -> c_49() 1123.22/297.09 , active^#(U91(X1, X2, X3, X4)) -> 1123.22/297.09 c_50(U91^#(active(X1), X2, X3, X4)) 1123.22/297.09 , active^#(U91(tt(), IL, M, N)) -> c_51(cons^#(N, take(M, IL))) 1123.22/297.09 , active^#(take(X1, X2)) -> c_52(take^#(X1, active(X2))) 1123.22/297.09 , active^#(take(X1, X2)) -> c_53(take^#(active(X1), X2)) 1123.22/297.09 , active^#(take(0(), IL)) -> 1123.22/297.09 c_54(U81^#(and(isNatIList(IL), isNatIListKind(IL)))) 1123.22/297.09 , active^#(take(s(M), cons(N, IL))) -> 1123.22/297.09 c_55(U91^#(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.22/297.09 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.22/297.09 IL, 1123.22/297.09 M, 1123.22/297.09 N)) 1123.22/297.09 , active^#(and(X1, X2)) -> c_56(and^#(active(X1), X2)) 1123.22/297.09 , active^#(and(tt(), X)) -> c_57(X) 1123.22/297.09 , active^#(isNatIListKind(zeros())) -> c_58() 1123.22/297.09 , active^#(isNatIListKind(cons(V1, V2))) -> 1123.22/297.09 c_59(and^#(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.09 , active^#(isNatIListKind(nil())) -> c_60() 1123.22/297.09 , active^#(isNatIListKind(take(V1, V2))) -> 1123.22/297.09 c_61(and^#(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.09 , active^#(isNatKind(0())) -> c_62() 1123.22/297.09 , active^#(isNatKind(s(V1))) -> c_63(isNatKind^#(V1)) 1123.22/297.09 , active^#(isNatKind(length(V1))) -> c_64(isNatIListKind^#(V1)) 1123.22/297.09 , cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) 1123.22/297.09 , cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) 1123.22/297.09 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 1123.22/297.09 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 1123.22/297.09 , U12^#(mark(X)) -> c_69(U12^#(X)) 1123.22/297.09 , U12^#(ok(X)) -> c_70(U12^#(X)) 1123.22/297.09 , U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) 1123.22/297.09 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) 1123.22/297.09 , U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) 1123.22/297.09 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) 1123.22/297.09 , U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) 1123.22/297.09 , U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) 1123.22/297.09 , U22^#(mark(X)) -> c_74(U22^#(X)) 1123.22/297.09 , U22^#(ok(X)) -> c_75(U22^#(X)) 1123.22/297.09 , U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) 1123.22/297.09 , U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) 1123.22/297.09 , U32^#(mark(X)) -> c_79(U32^#(X)) 1123.22/297.09 , U32^#(ok(X)) -> c_80(U32^#(X)) 1123.22/297.09 , U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) 1123.22/297.09 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) 1123.22/297.09 , U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) 1123.22/297.09 , U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) 1123.22/297.09 , U43^#(mark(X)) -> c_85(U43^#(X)) 1123.22/297.09 , U43^#(ok(X)) -> c_86(U43^#(X)) 1123.22/297.09 , U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) 1123.22/297.09 , U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) 1123.22/297.09 , U53^#(mark(X)) -> c_92(U53^#(X)) 1123.22/297.09 , U53^#(ok(X)) -> c_93(U53^#(X)) 1123.22/297.09 , U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) 1123.22/297.09 , U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) 1123.22/297.09 , U63^#(mark(X)) -> c_98(U63^#(X)) 1123.22/297.09 , U63^#(ok(X)) -> c_99(U63^#(X)) 1123.22/297.09 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 1123.22/297.09 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 1123.22/297.09 , s^#(mark(X)) -> c_102(s^#(X)) 1123.22/297.09 , s^#(ok(X)) -> c_103(s^#(X)) 1123.22/297.09 , length^#(mark(X)) -> c_104(length^#(X)) 1123.22/297.09 , length^#(ok(X)) -> c_105(length^#(X)) 1123.22/297.09 , U81^#(mark(X)) -> c_106(U81^#(X)) 1123.22/297.09 , U81^#(ok(X)) -> c_107(U81^#(X)) 1123.22/297.09 , U91^#(mark(X1), X2, X3, X4) -> c_108(U91^#(X1, X2, X3, X4)) 1123.22/297.09 , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.22/297.09 c_109(U91^#(X1, X2, X3, X4)) 1123.22/297.09 , take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) 1123.22/297.09 , take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) 1123.22/297.09 , take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) 1123.22/297.09 , and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) 1123.22/297.09 , and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) 1123.22/297.09 , isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) 1123.22/297.09 , isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) 1123.22/297.09 , isNatList^#(ok(X)) -> c_71(isNatList^#(X)) 1123.22/297.09 , isNat^#(ok(X)) -> c_76(isNat^#(X)) 1123.22/297.09 , isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) 1123.22/297.09 , proper^#(zeros()) -> c_117() 1123.22/297.09 , proper^#(cons(X1, X2)) -> c_118(cons^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(0()) -> c_119() 1123.22/297.09 , proper^#(U11(X1, X2)) -> c_120(U11^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(tt()) -> c_121() 1123.22/297.09 , proper^#(U12(X)) -> c_122(U12^#(proper(X))) 1123.22/297.09 , proper^#(isNatList(X)) -> c_123(isNatList^#(proper(X))) 1123.22/297.09 , proper^#(U21(X1, X2)) -> c_124(U21^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U22(X)) -> c_125(U22^#(proper(X))) 1123.22/297.09 , proper^#(isNat(X)) -> c_126(isNat^#(proper(X))) 1123.22/297.09 , proper^#(U31(X1, X2)) -> c_127(U31^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U32(X)) -> c_128(U32^#(proper(X))) 1123.22/297.09 , proper^#(U41(X1, X2, X3)) -> 1123.22/297.09 c_129(U41^#(proper(X1), proper(X2), proper(X3))) 1123.22/297.09 , proper^#(U42(X1, X2)) -> c_130(U42^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U43(X)) -> c_131(U43^#(proper(X))) 1123.22/297.09 , proper^#(isNatIList(X)) -> c_132(isNatIList^#(proper(X))) 1123.22/297.09 , proper^#(U51(X1, X2, X3)) -> 1123.22/297.09 c_133(U51^#(proper(X1), proper(X2), proper(X3))) 1123.22/297.09 , proper^#(U52(X1, X2)) -> c_134(U52^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U53(X)) -> c_135(U53^#(proper(X))) 1123.22/297.09 , proper^#(U61(X1, X2, X3)) -> 1123.22/297.09 c_136(U61^#(proper(X1), proper(X2), proper(X3))) 1123.22/297.09 , proper^#(U62(X1, X2)) -> c_137(U62^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U63(X)) -> c_138(U63^#(proper(X))) 1123.22/297.09 , proper^#(U71(X1, X2)) -> c_139(U71^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(s(X)) -> c_140(s^#(proper(X))) 1123.22/297.09 , proper^#(length(X)) -> c_141(length^#(proper(X))) 1123.22/297.09 , proper^#(U81(X)) -> c_142(U81^#(proper(X))) 1123.22/297.09 , proper^#(nil()) -> c_143() 1123.22/297.09 , proper^#(U91(X1, X2, X3, X4)) -> 1123.22/297.09 c_144(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) 1123.22/297.09 , proper^#(take(X1, X2)) -> c_145(take^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(and(X1, X2)) -> c_146(and^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(isNatIListKind(X)) -> c_147(isNatIListKind^#(proper(X))) 1123.22/297.09 , proper^#(isNatKind(X)) -> c_148(isNatKind^#(proper(X))) 1123.22/297.09 , top^#(mark(X)) -> c_149(top^#(proper(X))) 1123.22/297.09 , top^#(ok(X)) -> c_150(top^#(active(X))) } 1123.22/297.09 1123.22/297.09 and mark the set of starting terms. 1123.22/297.09 1123.22/297.09 We are left with following problem, upon which TcT provides the 1123.22/297.09 certificate MAYBE. 1123.22/297.09 1123.22/297.09 Strict DPs: 1123.22/297.09 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 1123.22/297.09 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 1123.22/297.09 , active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 1123.22/297.09 , active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1))) 1123.22/297.09 , active^#(U12(X)) -> c_5(U12^#(active(X))) 1123.22/297.09 , active^#(U12(tt())) -> c_6() 1123.22/297.09 , active^#(isNatList(cons(V1, V2))) -> 1123.22/297.09 c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.09 , active^#(isNatList(nil())) -> c_8() 1123.22/297.09 , active^#(isNatList(take(V1, V2))) -> 1123.22/297.09 c_9(U61^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.09 , active^#(U21(X1, X2)) -> c_10(U21^#(active(X1), X2)) 1123.22/297.09 , active^#(U21(tt(), V1)) -> c_11(U22^#(isNat(V1))) 1123.22/297.09 , active^#(U22(X)) -> c_12(U22^#(active(X))) 1123.22/297.09 , active^#(U22(tt())) -> c_13() 1123.22/297.09 , active^#(isNat(0())) -> c_14() 1123.22/297.09 , active^#(isNat(s(V1))) -> c_15(U21^#(isNatKind(V1), V1)) 1123.22/297.09 , active^#(isNat(length(V1))) -> 1123.22/297.09 c_16(U11^#(isNatIListKind(V1), V1)) 1123.22/297.09 , active^#(U31(X1, X2)) -> c_17(U31^#(active(X1), X2)) 1123.22/297.09 , active^#(U31(tt(), V)) -> c_18(U32^#(isNatList(V))) 1123.22/297.09 , active^#(U32(X)) -> c_19(U32^#(active(X))) 1123.22/297.09 , active^#(U32(tt())) -> c_20() 1123.22/297.09 , active^#(U41(X1, X2, X3)) -> c_21(U41^#(active(X1), X2, X3)) 1123.22/297.09 , active^#(U41(tt(), V1, V2)) -> c_22(U42^#(isNat(V1), V2)) 1123.22/297.09 , active^#(U42(X1, X2)) -> c_23(U42^#(active(X1), X2)) 1123.22/297.09 , active^#(U42(tt(), V2)) -> c_24(U43^#(isNatIList(V2))) 1123.22/297.09 , active^#(U43(X)) -> c_25(U43^#(active(X))) 1123.22/297.09 , active^#(U43(tt())) -> c_26() 1123.22/297.09 , active^#(isNatIList(V)) -> c_27(U31^#(isNatIListKind(V), V)) 1123.22/297.09 , active^#(isNatIList(zeros())) -> c_28() 1123.22/297.09 , active^#(isNatIList(cons(V1, V2))) -> 1123.22/297.09 c_29(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.09 , active^#(U51(X1, X2, X3)) -> c_30(U51^#(active(X1), X2, X3)) 1123.22/297.09 , active^#(U51(tt(), V1, V2)) -> c_31(U52^#(isNat(V1), V2)) 1123.22/297.09 , active^#(U52(X1, X2)) -> c_32(U52^#(active(X1), X2)) 1123.22/297.09 , active^#(U52(tt(), V2)) -> c_33(U53^#(isNatList(V2))) 1123.22/297.09 , active^#(U53(X)) -> c_34(U53^#(active(X))) 1123.22/297.09 , active^#(U53(tt())) -> c_35() 1123.22/297.09 , active^#(U61(X1, X2, X3)) -> c_36(U61^#(active(X1), X2, X3)) 1123.22/297.09 , active^#(U61(tt(), V1, V2)) -> c_37(U62^#(isNat(V1), V2)) 1123.22/297.09 , active^#(U62(X1, X2)) -> c_38(U62^#(active(X1), X2)) 1123.22/297.09 , active^#(U62(tt(), V2)) -> c_39(U63^#(isNatIList(V2))) 1123.22/297.09 , active^#(U63(X)) -> c_40(U63^#(active(X))) 1123.22/297.09 , active^#(U63(tt())) -> c_41() 1123.22/297.09 , active^#(U71(X1, X2)) -> c_42(U71^#(active(X1), X2)) 1123.22/297.09 , active^#(U71(tt(), L)) -> c_43(s^#(length(L))) 1123.22/297.09 , active^#(s(X)) -> c_44(s^#(active(X))) 1123.22/297.09 , active^#(length(X)) -> c_45(length^#(active(X))) 1123.22/297.09 , active^#(length(cons(N, L))) -> 1123.22/297.09 c_46(U71^#(and(and(isNatList(L), isNatIListKind(L)), 1123.22/297.09 and(isNat(N), isNatKind(N))), 1123.22/297.09 L)) 1123.22/297.09 , active^#(length(nil())) -> c_47() 1123.22/297.09 , active^#(U81(X)) -> c_48(U81^#(active(X))) 1123.22/297.09 , active^#(U81(tt())) -> c_49() 1123.22/297.09 , active^#(U91(X1, X2, X3, X4)) -> 1123.22/297.09 c_50(U91^#(active(X1), X2, X3, X4)) 1123.22/297.09 , active^#(U91(tt(), IL, M, N)) -> c_51(cons^#(N, take(M, IL))) 1123.22/297.09 , active^#(take(X1, X2)) -> c_52(take^#(X1, active(X2))) 1123.22/297.09 , active^#(take(X1, X2)) -> c_53(take^#(active(X1), X2)) 1123.22/297.09 , active^#(take(0(), IL)) -> 1123.22/297.09 c_54(U81^#(and(isNatIList(IL), isNatIListKind(IL)))) 1123.22/297.09 , active^#(take(s(M), cons(N, IL))) -> 1123.22/297.09 c_55(U91^#(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.22/297.09 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.22/297.09 IL, 1123.22/297.09 M, 1123.22/297.09 N)) 1123.22/297.09 , active^#(and(X1, X2)) -> c_56(and^#(active(X1), X2)) 1123.22/297.09 , active^#(and(tt(), X)) -> c_57(X) 1123.22/297.09 , active^#(isNatIListKind(zeros())) -> c_58() 1123.22/297.09 , active^#(isNatIListKind(cons(V1, V2))) -> 1123.22/297.09 c_59(and^#(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.09 , active^#(isNatIListKind(nil())) -> c_60() 1123.22/297.09 , active^#(isNatIListKind(take(V1, V2))) -> 1123.22/297.09 c_61(and^#(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.09 , active^#(isNatKind(0())) -> c_62() 1123.22/297.09 , active^#(isNatKind(s(V1))) -> c_63(isNatKind^#(V1)) 1123.22/297.09 , active^#(isNatKind(length(V1))) -> c_64(isNatIListKind^#(V1)) 1123.22/297.09 , cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) 1123.22/297.09 , cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) 1123.22/297.09 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 1123.22/297.09 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 1123.22/297.09 , U12^#(mark(X)) -> c_69(U12^#(X)) 1123.22/297.09 , U12^#(ok(X)) -> c_70(U12^#(X)) 1123.22/297.09 , U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) 1123.22/297.09 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) 1123.22/297.09 , U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) 1123.22/297.09 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) 1123.22/297.09 , U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) 1123.22/297.09 , U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) 1123.22/297.09 , U22^#(mark(X)) -> c_74(U22^#(X)) 1123.22/297.09 , U22^#(ok(X)) -> c_75(U22^#(X)) 1123.22/297.09 , U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) 1123.22/297.09 , U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) 1123.22/297.09 , U32^#(mark(X)) -> c_79(U32^#(X)) 1123.22/297.09 , U32^#(ok(X)) -> c_80(U32^#(X)) 1123.22/297.09 , U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) 1123.22/297.09 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) 1123.22/297.09 , U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) 1123.22/297.09 , U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) 1123.22/297.09 , U43^#(mark(X)) -> c_85(U43^#(X)) 1123.22/297.09 , U43^#(ok(X)) -> c_86(U43^#(X)) 1123.22/297.09 , U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) 1123.22/297.09 , U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) 1123.22/297.09 , U53^#(mark(X)) -> c_92(U53^#(X)) 1123.22/297.09 , U53^#(ok(X)) -> c_93(U53^#(X)) 1123.22/297.09 , U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) 1123.22/297.09 , U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) 1123.22/297.09 , U63^#(mark(X)) -> c_98(U63^#(X)) 1123.22/297.09 , U63^#(ok(X)) -> c_99(U63^#(X)) 1123.22/297.09 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 1123.22/297.09 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 1123.22/297.09 , s^#(mark(X)) -> c_102(s^#(X)) 1123.22/297.09 , s^#(ok(X)) -> c_103(s^#(X)) 1123.22/297.09 , length^#(mark(X)) -> c_104(length^#(X)) 1123.22/297.09 , length^#(ok(X)) -> c_105(length^#(X)) 1123.22/297.09 , U81^#(mark(X)) -> c_106(U81^#(X)) 1123.22/297.09 , U81^#(ok(X)) -> c_107(U81^#(X)) 1123.22/297.09 , U91^#(mark(X1), X2, X3, X4) -> c_108(U91^#(X1, X2, X3, X4)) 1123.22/297.09 , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.22/297.09 c_109(U91^#(X1, X2, X3, X4)) 1123.22/297.09 , take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) 1123.22/297.09 , take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) 1123.22/297.09 , take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) 1123.22/297.09 , and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) 1123.22/297.09 , and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) 1123.22/297.09 , isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) 1123.22/297.09 , isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) 1123.22/297.09 , isNatList^#(ok(X)) -> c_71(isNatList^#(X)) 1123.22/297.09 , isNat^#(ok(X)) -> c_76(isNat^#(X)) 1123.22/297.09 , isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) 1123.22/297.09 , proper^#(zeros()) -> c_117() 1123.22/297.09 , proper^#(cons(X1, X2)) -> c_118(cons^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(0()) -> c_119() 1123.22/297.09 , proper^#(U11(X1, X2)) -> c_120(U11^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(tt()) -> c_121() 1123.22/297.09 , proper^#(U12(X)) -> c_122(U12^#(proper(X))) 1123.22/297.09 , proper^#(isNatList(X)) -> c_123(isNatList^#(proper(X))) 1123.22/297.09 , proper^#(U21(X1, X2)) -> c_124(U21^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U22(X)) -> c_125(U22^#(proper(X))) 1123.22/297.09 , proper^#(isNat(X)) -> c_126(isNat^#(proper(X))) 1123.22/297.09 , proper^#(U31(X1, X2)) -> c_127(U31^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U32(X)) -> c_128(U32^#(proper(X))) 1123.22/297.09 , proper^#(U41(X1, X2, X3)) -> 1123.22/297.09 c_129(U41^#(proper(X1), proper(X2), proper(X3))) 1123.22/297.09 , proper^#(U42(X1, X2)) -> c_130(U42^#(proper(X1), proper(X2))) 1123.22/297.09 , proper^#(U43(X)) -> c_131(U43^#(proper(X))) 1123.22/297.09 , proper^#(isNatIList(X)) -> c_132(isNatIList^#(proper(X))) 1123.22/297.09 , proper^#(U51(X1, X2, X3)) -> 1123.22/297.09 c_133(U51^#(proper(X1), proper(X2), proper(X3))) 1123.22/297.09 , proper^#(U52(X1, X2)) -> c_134(U52^#(proper(X1), proper(X2))) 1123.22/297.10 , proper^#(U53(X)) -> c_135(U53^#(proper(X))) 1123.22/297.10 , proper^#(U61(X1, X2, X3)) -> 1123.22/297.10 c_136(U61^#(proper(X1), proper(X2), proper(X3))) 1123.22/297.10 , proper^#(U62(X1, X2)) -> c_137(U62^#(proper(X1), proper(X2))) 1123.22/297.10 , proper^#(U63(X)) -> c_138(U63^#(proper(X))) 1123.22/297.10 , proper^#(U71(X1, X2)) -> c_139(U71^#(proper(X1), proper(X2))) 1123.22/297.10 , proper^#(s(X)) -> c_140(s^#(proper(X))) 1123.22/297.10 , proper^#(length(X)) -> c_141(length^#(proper(X))) 1123.22/297.10 , proper^#(U81(X)) -> c_142(U81^#(proper(X))) 1123.22/297.10 , proper^#(nil()) -> c_143() 1123.22/297.10 , proper^#(U91(X1, X2, X3, X4)) -> 1123.22/297.10 c_144(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) 1123.22/297.10 , proper^#(take(X1, X2)) -> c_145(take^#(proper(X1), proper(X2))) 1123.22/297.10 , proper^#(and(X1, X2)) -> c_146(and^#(proper(X1), proper(X2))) 1123.22/297.10 , proper^#(isNatIListKind(X)) -> c_147(isNatIListKind^#(proper(X))) 1123.22/297.10 , proper^#(isNatKind(X)) -> c_148(isNatKind^#(proper(X))) 1123.22/297.10 , top^#(mark(X)) -> c_149(top^#(proper(X))) 1123.22/297.10 , top^#(ok(X)) -> c_150(top^#(active(X))) } 1123.22/297.10 Strict Trs: 1123.22/297.10 { active(zeros()) -> mark(cons(0(), zeros())) 1123.22/297.10 , active(cons(X1, X2)) -> cons(active(X1), X2) 1123.22/297.10 , active(U11(X1, X2)) -> U11(active(X1), X2) 1123.22/297.10 , active(U11(tt(), V1)) -> mark(U12(isNatList(V1))) 1123.22/297.10 , active(U12(X)) -> U12(active(X)) 1123.22/297.10 , active(U12(tt())) -> mark(tt()) 1123.22/297.10 , active(isNatList(cons(V1, V2))) -> 1123.22/297.10 mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.10 , active(isNatList(nil())) -> mark(tt()) 1123.22/297.10 , active(isNatList(take(V1, V2))) -> 1123.22/297.10 mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.10 , active(U21(X1, X2)) -> U21(active(X1), X2) 1123.22/297.10 , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) 1123.22/297.10 , active(U22(X)) -> U22(active(X)) 1123.22/297.10 , active(U22(tt())) -> mark(tt()) 1123.22/297.10 , active(isNat(0())) -> mark(tt()) 1123.22/297.10 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1123.22/297.10 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 1123.22/297.10 , active(U31(X1, X2)) -> U31(active(X1), X2) 1123.22/297.10 , active(U31(tt(), V)) -> mark(U32(isNatList(V))) 1123.22/297.10 , active(U32(X)) -> U32(active(X)) 1123.22/297.10 , active(U32(tt())) -> mark(tt()) 1123.22/297.10 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 1123.22/297.10 , active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2)) 1123.22/297.10 , active(U42(X1, X2)) -> U42(active(X1), X2) 1123.22/297.10 , active(U42(tt(), V2)) -> mark(U43(isNatIList(V2))) 1123.22/297.10 , active(U43(X)) -> U43(active(X)) 1123.22/297.10 , active(U43(tt())) -> mark(tt()) 1123.22/297.10 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 1123.22/297.10 , active(isNatIList(zeros())) -> mark(tt()) 1123.22/297.10 , active(isNatIList(cons(V1, V2))) -> 1123.22/297.10 mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.22/297.10 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 1123.22/297.10 , active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2)) 1123.22/297.10 , active(U52(X1, X2)) -> U52(active(X1), X2) 1123.22/297.10 , active(U52(tt(), V2)) -> mark(U53(isNatList(V2))) 1123.22/297.10 , active(U53(X)) -> U53(active(X)) 1123.22/297.10 , active(U53(tt())) -> mark(tt()) 1123.22/297.10 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1123.22/297.10 , active(U61(tt(), V1, V2)) -> mark(U62(isNat(V1), V2)) 1123.22/297.10 , active(U62(X1, X2)) -> U62(active(X1), X2) 1123.22/297.10 , active(U62(tt(), V2)) -> mark(U63(isNatIList(V2))) 1123.22/297.10 , active(U63(X)) -> U63(active(X)) 1123.22/297.10 , active(U63(tt())) -> mark(tt()) 1123.22/297.10 , active(U71(X1, X2)) -> U71(active(X1), X2) 1123.22/297.10 , active(U71(tt(), L)) -> mark(s(length(L))) 1123.22/297.10 , active(s(X)) -> s(active(X)) 1123.22/297.10 , active(length(X)) -> length(active(X)) 1123.22/297.10 , active(length(cons(N, L))) -> 1123.22/297.10 mark(U71(and(and(isNatList(L), isNatIListKind(L)), 1123.22/297.10 and(isNat(N), isNatKind(N))), 1123.22/297.10 L)) 1123.22/297.10 , active(length(nil())) -> mark(0()) 1123.22/297.10 , active(U81(X)) -> U81(active(X)) 1123.22/297.10 , active(U81(tt())) -> mark(nil()) 1123.22/297.10 , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) 1123.22/297.10 , active(U91(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 1123.22/297.10 , active(take(X1, X2)) -> take(X1, active(X2)) 1123.22/297.10 , active(take(X1, X2)) -> take(active(X1), X2) 1123.22/297.10 , active(take(0(), IL)) -> 1123.22/297.10 mark(U81(and(isNatIList(IL), isNatIListKind(IL)))) 1123.22/297.10 , active(take(s(M), cons(N, IL))) -> 1123.22/297.10 mark(U91(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.22/297.10 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.22/297.10 IL, 1123.22/297.10 M, 1123.22/297.10 N)) 1123.22/297.10 , active(and(X1, X2)) -> and(active(X1), X2) 1123.22/297.10 , active(and(tt(), X)) -> mark(X) 1123.22/297.10 , active(isNatIListKind(zeros())) -> mark(tt()) 1123.22/297.10 , active(isNatIListKind(cons(V1, V2))) -> 1123.22/297.10 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.10 , active(isNatIListKind(nil())) -> mark(tt()) 1123.22/297.10 , active(isNatIListKind(take(V1, V2))) -> 1123.22/297.10 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.22/297.10 , active(isNatKind(0())) -> mark(tt()) 1123.22/297.10 , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) 1123.22/297.10 , active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)) 1123.22/297.10 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1123.22/297.10 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1123.22/297.10 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 1123.22/297.10 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 1123.22/297.10 , U12(mark(X)) -> mark(U12(X)) 1123.22/297.10 , U12(ok(X)) -> ok(U12(X)) 1123.22/297.10 , isNatList(ok(X)) -> ok(isNatList(X)) 1123.22/297.10 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1123.22/297.10 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1123.22/297.10 , U22(mark(X)) -> mark(U22(X)) 1123.22/297.10 , U22(ok(X)) -> ok(U22(X)) 1123.22/297.10 , isNat(ok(X)) -> ok(isNat(X)) 1123.22/297.10 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1123.22/297.10 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1123.22/297.10 , U32(mark(X)) -> mark(U32(X)) 1123.22/297.10 , U32(ok(X)) -> ok(U32(X)) 1123.22/297.10 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 1123.22/297.10 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 1123.22/297.10 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 1123.22/297.10 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 1123.22/297.10 , U43(mark(X)) -> mark(U43(X)) 1123.22/297.10 , U43(ok(X)) -> ok(U43(X)) 1123.22/297.10 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1123.22/297.10 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 1123.22/297.10 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 1123.22/297.10 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1123.22/297.10 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1123.22/297.10 , U53(mark(X)) -> mark(U53(X)) 1123.48/297.10 , U53(ok(X)) -> ok(U53(X)) 1123.48/297.10 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1123.48/297.10 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1123.48/297.10 , U62(mark(X1), X2) -> mark(U62(X1, X2)) 1123.48/297.10 , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) 1123.48/297.10 , U63(mark(X)) -> mark(U63(X)) 1123.48/297.10 , U63(ok(X)) -> ok(U63(X)) 1123.48/297.10 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1123.48/297.10 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1123.48/297.10 , s(mark(X)) -> mark(s(X)) 1123.48/297.10 , s(ok(X)) -> ok(s(X)) 1123.48/297.10 , length(mark(X)) -> mark(length(X)) 1123.48/297.10 , length(ok(X)) -> ok(length(X)) 1123.48/297.10 , U81(mark(X)) -> mark(U81(X)) 1123.48/297.10 , U81(ok(X)) -> ok(U81(X)) 1123.48/297.10 , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) 1123.48/297.10 , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) 1123.48/297.10 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1123.48/297.10 , take(mark(X1), X2) -> mark(take(X1, X2)) 1123.48/297.10 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1123.48/297.10 , and(mark(X1), X2) -> mark(and(X1, X2)) 1123.48/297.10 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1123.48/297.10 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 1123.48/297.10 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1123.48/297.10 , proper(zeros()) -> ok(zeros()) 1123.48/297.10 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1123.48/297.10 , proper(0()) -> ok(0()) 1123.48/297.10 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 1123.48/297.10 , proper(tt()) -> ok(tt()) 1123.48/297.10 , proper(U12(X)) -> U12(proper(X)) 1123.48/297.10 , proper(isNatList(X)) -> isNatList(proper(X)) 1123.48/297.10 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1123.48/297.10 , proper(U22(X)) -> U22(proper(X)) 1123.48/297.10 , proper(isNat(X)) -> isNat(proper(X)) 1123.48/297.10 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1123.48/297.10 , proper(U32(X)) -> U32(proper(X)) 1123.48/297.10 , proper(U41(X1, X2, X3)) -> 1123.48/297.10 U41(proper(X1), proper(X2), proper(X3)) 1123.48/297.10 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 1123.48/297.10 , proper(U43(X)) -> U43(proper(X)) 1123.48/297.10 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1123.48/297.10 , proper(U51(X1, X2, X3)) -> 1123.48/297.10 U51(proper(X1), proper(X2), proper(X3)) 1123.48/297.10 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1123.48/297.10 , proper(U53(X)) -> U53(proper(X)) 1123.48/297.10 , proper(U61(X1, X2, X3)) -> 1123.48/297.10 U61(proper(X1), proper(X2), proper(X3)) 1123.48/297.10 , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) 1123.48/297.10 , proper(U63(X)) -> U63(proper(X)) 1123.48/297.10 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1123.48/297.10 , proper(s(X)) -> s(proper(X)) 1123.48/297.10 , proper(length(X)) -> length(proper(X)) 1123.48/297.10 , proper(U81(X)) -> U81(proper(X)) 1123.48/297.10 , proper(nil()) -> ok(nil()) 1123.48/297.10 , proper(U91(X1, X2, X3, X4)) -> 1123.48/297.10 U91(proper(X1), proper(X2), proper(X3), proper(X4)) 1123.48/297.10 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1123.48/297.10 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1123.48/297.10 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 1123.48/297.10 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1123.48/297.10 , top(mark(X)) -> top(proper(X)) 1123.48/297.10 , top(ok(X)) -> top(active(X)) } 1123.48/297.10 Obligation: 1123.48/297.10 runtime complexity 1123.48/297.10 Answer: 1123.48/297.10 MAYBE 1123.48/297.10 1123.48/297.10 Consider the dependency graph: 1123.48/297.10 1123.48/297.10 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 1123.48/297.10 1123.48/297.10 2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 1123.48/297.10 -->_1 cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) :66 1123.48/297.10 -->_1 cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) :65 1123.48/297.10 1123.48/297.10 3: active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 1123.48/297.10 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 1123.48/297.10 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 1123.48/297.10 1123.48/297.10 4: active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1))) 1123.48/297.10 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 1123.48/297.10 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 1123.48/297.10 1123.48/297.10 5: active^#(U12(X)) -> c_5(U12^#(active(X))) 1123.48/297.10 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 1123.48/297.10 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 1123.48/297.10 1123.48/297.10 6: active^#(U12(tt())) -> c_6() 1123.48/297.10 1123.48/297.10 7: active^#(isNatList(cons(V1, V2))) -> 1123.48/297.10 c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.10 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) :72 1123.48/297.10 -->_1 U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) :71 1123.48/297.10 1123.48/297.10 8: active^#(isNatList(nil())) -> c_8() 1123.48/297.10 1123.48/297.10 9: active^#(isNatList(take(V1, V2))) -> 1123.48/297.10 c_9(U61^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.10 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) :74 1123.48/297.10 -->_1 U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) :73 1123.48/297.10 1123.48/297.10 10: active^#(U21(X1, X2)) -> c_10(U21^#(active(X1), X2)) 1123.48/297.10 -->_1 U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) :76 1123.48/297.10 -->_1 U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) :75 1123.48/297.10 1123.48/297.10 11: active^#(U21(tt(), V1)) -> c_11(U22^#(isNat(V1))) 1123.48/297.10 -->_1 U22^#(ok(X)) -> c_75(U22^#(X)) :78 1123.48/297.10 -->_1 U22^#(mark(X)) -> c_74(U22^#(X)) :77 1123.48/297.10 1123.48/297.10 12: active^#(U22(X)) -> c_12(U22^#(active(X))) 1123.48/297.10 -->_1 U22^#(ok(X)) -> c_75(U22^#(X)) :78 1123.48/297.10 -->_1 U22^#(mark(X)) -> c_74(U22^#(X)) :77 1123.48/297.10 1123.48/297.10 13: active^#(U22(tt())) -> c_13() 1123.48/297.10 1123.48/297.10 14: active^#(isNat(0())) -> c_14() 1123.48/297.10 1123.48/297.10 15: active^#(isNat(s(V1))) -> c_15(U21^#(isNatKind(V1), V1)) 1123.48/297.10 -->_1 U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) :76 1123.48/297.10 -->_1 U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) :75 1123.48/297.10 1123.48/297.10 16: active^#(isNat(length(V1))) -> 1123.48/297.10 c_16(U11^#(isNatIListKind(V1), V1)) 1123.48/297.10 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 1123.48/297.10 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 1123.48/297.10 1123.48/297.10 17: active^#(U31(X1, X2)) -> c_17(U31^#(active(X1), X2)) 1123.48/297.10 -->_1 U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) :80 1123.48/297.10 -->_1 U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) :79 1123.48/297.10 1123.48/297.10 18: active^#(U31(tt(), V)) -> c_18(U32^#(isNatList(V))) 1123.48/297.10 -->_1 U32^#(ok(X)) -> c_80(U32^#(X)) :82 1123.48/297.10 -->_1 U32^#(mark(X)) -> c_79(U32^#(X)) :81 1123.48/297.10 1123.48/297.10 19: active^#(U32(X)) -> c_19(U32^#(active(X))) 1123.48/297.10 -->_1 U32^#(ok(X)) -> c_80(U32^#(X)) :82 1123.48/297.10 -->_1 U32^#(mark(X)) -> c_79(U32^#(X)) :81 1123.48/297.10 1123.48/297.10 20: active^#(U32(tt())) -> c_20() 1123.48/297.10 1123.48/297.10 21: active^#(U41(X1, X2, X3)) -> c_21(U41^#(active(X1), X2, X3)) 1123.48/297.10 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) :84 1123.48/297.10 -->_1 U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) :83 1123.48/297.10 1123.48/297.10 22: active^#(U41(tt(), V1, V2)) -> c_22(U42^#(isNat(V1), V2)) 1123.48/297.10 -->_1 U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) :86 1123.48/297.10 -->_1 U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) :85 1123.48/297.10 1123.48/297.10 23: active^#(U42(X1, X2)) -> c_23(U42^#(active(X1), X2)) 1123.48/297.10 -->_1 U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) :86 1123.48/297.10 -->_1 U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) :85 1123.48/297.10 1123.48/297.10 24: active^#(U42(tt(), V2)) -> c_24(U43^#(isNatIList(V2))) 1123.48/297.10 -->_1 U43^#(ok(X)) -> c_86(U43^#(X)) :88 1123.48/297.10 -->_1 U43^#(mark(X)) -> c_85(U43^#(X)) :87 1123.48/297.10 1123.48/297.10 25: active^#(U43(X)) -> c_25(U43^#(active(X))) 1123.48/297.10 -->_1 U43^#(ok(X)) -> c_86(U43^#(X)) :88 1123.48/297.10 -->_1 U43^#(mark(X)) -> c_85(U43^#(X)) :87 1123.48/297.10 1123.48/297.10 26: active^#(U43(tt())) -> c_26() 1123.48/297.10 1123.48/297.10 27: active^#(isNatIList(V)) -> c_27(U31^#(isNatIListKind(V), V)) 1123.48/297.10 -->_1 U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) :80 1123.48/297.10 -->_1 U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) :79 1123.48/297.10 1123.48/297.10 28: active^#(isNatIList(zeros())) -> c_28() 1123.48/297.10 1123.48/297.10 29: active^#(isNatIList(cons(V1, V2))) -> 1123.48/297.10 c_29(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.10 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) :84 1123.48/297.10 -->_1 U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) :83 1123.48/297.10 1123.48/297.10 30: active^#(U51(X1, X2, X3)) -> c_30(U51^#(active(X1), X2, X3)) 1123.48/297.10 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) :72 1123.48/297.10 -->_1 U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) :71 1123.48/297.10 1123.48/297.10 31: active^#(U51(tt(), V1, V2)) -> c_31(U52^#(isNat(V1), V2)) 1123.48/297.10 -->_1 U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) :90 1123.48/297.10 -->_1 U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) :89 1123.48/297.10 1123.48/297.10 32: active^#(U52(X1, X2)) -> c_32(U52^#(active(X1), X2)) 1123.48/297.10 -->_1 U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) :90 1123.48/297.10 -->_1 U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) :89 1123.48/297.10 1123.48/297.10 33: active^#(U52(tt(), V2)) -> c_33(U53^#(isNatList(V2))) 1123.48/297.10 -->_1 U53^#(ok(X)) -> c_93(U53^#(X)) :92 1123.48/297.11 -->_1 U53^#(mark(X)) -> c_92(U53^#(X)) :91 1123.48/297.11 1123.48/297.11 34: active^#(U53(X)) -> c_34(U53^#(active(X))) 1123.48/297.11 -->_1 U53^#(ok(X)) -> c_93(U53^#(X)) :92 1123.48/297.11 -->_1 U53^#(mark(X)) -> c_92(U53^#(X)) :91 1123.48/297.11 1123.48/297.11 35: active^#(U53(tt())) -> c_35() 1123.48/297.11 1123.48/297.11 36: active^#(U61(X1, X2, X3)) -> c_36(U61^#(active(X1), X2, X3)) 1123.48/297.11 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) :74 1123.48/297.11 -->_1 U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) :73 1123.48/297.11 1123.48/297.11 37: active^#(U61(tt(), V1, V2)) -> c_37(U62^#(isNat(V1), V2)) 1123.48/297.11 -->_1 U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) :94 1123.48/297.11 -->_1 U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) :93 1123.48/297.11 1123.48/297.11 38: active^#(U62(X1, X2)) -> c_38(U62^#(active(X1), X2)) 1123.48/297.11 -->_1 U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) :94 1123.48/297.11 -->_1 U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) :93 1123.48/297.11 1123.48/297.11 39: active^#(U62(tt(), V2)) -> c_39(U63^#(isNatIList(V2))) 1123.48/297.11 -->_1 U63^#(ok(X)) -> c_99(U63^#(X)) :96 1123.48/297.11 -->_1 U63^#(mark(X)) -> c_98(U63^#(X)) :95 1123.48/297.11 1123.48/297.11 40: active^#(U63(X)) -> c_40(U63^#(active(X))) 1123.48/297.11 -->_1 U63^#(ok(X)) -> c_99(U63^#(X)) :96 1123.48/297.11 -->_1 U63^#(mark(X)) -> c_98(U63^#(X)) :95 1123.48/297.11 1123.48/297.11 41: active^#(U63(tt())) -> c_41() 1123.48/297.11 1123.48/297.11 42: active^#(U71(X1, X2)) -> c_42(U71^#(active(X1), X2)) 1123.48/297.11 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 1123.48/297.11 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 1123.48/297.11 1123.48/297.11 43: active^#(U71(tt(), L)) -> c_43(s^#(length(L))) 1123.48/297.11 -->_1 s^#(ok(X)) -> c_103(s^#(X)) :100 1123.48/297.11 -->_1 s^#(mark(X)) -> c_102(s^#(X)) :99 1123.48/297.11 1123.48/297.11 44: active^#(s(X)) -> c_44(s^#(active(X))) 1123.48/297.11 -->_1 s^#(ok(X)) -> c_103(s^#(X)) :100 1123.48/297.11 -->_1 s^#(mark(X)) -> c_102(s^#(X)) :99 1123.48/297.11 1123.48/297.11 45: active^#(length(X)) -> c_45(length^#(active(X))) 1123.48/297.11 -->_1 length^#(ok(X)) -> c_105(length^#(X)) :102 1123.48/297.11 -->_1 length^#(mark(X)) -> c_104(length^#(X)) :101 1123.48/297.11 1123.48/297.11 46: active^#(length(cons(N, L))) -> 1123.48/297.11 c_46(U71^#(and(and(isNatList(L), isNatIListKind(L)), 1123.48/297.11 and(isNat(N), isNatKind(N))), 1123.48/297.11 L)) 1123.48/297.11 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 1123.48/297.11 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 1123.48/297.11 1123.48/297.11 47: active^#(length(nil())) -> c_47() 1123.48/297.11 1123.48/297.11 48: active^#(U81(X)) -> c_48(U81^#(active(X))) 1123.48/297.11 -->_1 U81^#(ok(X)) -> c_107(U81^#(X)) :104 1123.48/297.11 -->_1 U81^#(mark(X)) -> c_106(U81^#(X)) :103 1123.48/297.11 1123.48/297.11 49: active^#(U81(tt())) -> c_49() 1123.48/297.11 1123.48/297.11 50: active^#(U91(X1, X2, X3, X4)) -> 1123.48/297.11 c_50(U91^#(active(X1), X2, X3, X4)) 1123.48/297.11 -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.11 c_109(U91^#(X1, X2, X3, X4)) :106 1123.48/297.11 -->_1 U91^#(mark(X1), X2, X3, X4) -> 1123.48/297.11 c_108(U91^#(X1, X2, X3, X4)) :105 1123.48/297.11 1123.48/297.11 51: active^#(U91(tt(), IL, M, N)) -> c_51(cons^#(N, take(M, IL))) 1123.48/297.11 -->_1 cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) :66 1123.48/297.11 -->_1 cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) :65 1123.48/297.11 1123.48/297.11 52: active^#(take(X1, X2)) -> c_52(take^#(X1, active(X2))) 1123.48/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.11 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.11 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.11 1123.48/297.11 53: active^#(take(X1, X2)) -> c_53(take^#(active(X1), X2)) 1123.48/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.11 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.11 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.11 1123.48/297.11 54: active^#(take(0(), IL)) -> 1123.48/297.11 c_54(U81^#(and(isNatIList(IL), isNatIListKind(IL)))) 1123.48/297.11 -->_1 U81^#(ok(X)) -> c_107(U81^#(X)) :104 1123.48/297.11 -->_1 U81^#(mark(X)) -> c_106(U81^#(X)) :103 1123.48/297.11 1123.48/297.11 55: active^#(take(s(M), cons(N, IL))) -> 1123.48/297.11 c_55(U91^#(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.48/297.11 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.48/297.11 IL, 1123.48/297.11 M, 1123.48/297.11 N)) 1123.48/297.11 -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.11 c_109(U91^#(X1, X2, X3, X4)) :106 1123.48/297.11 -->_1 U91^#(mark(X1), X2, X3, X4) -> 1123.48/297.11 c_108(U91^#(X1, X2, X3, X4)) :105 1123.48/297.11 1123.48/297.11 56: active^#(and(X1, X2)) -> c_56(and^#(active(X1), X2)) 1123.48/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.11 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.11 1123.48/297.11 57: active^#(and(tt(), X)) -> c_57(X) 1123.48/297.11 -->_1 top^#(ok(X)) -> c_150(top^#(active(X))) :150 1123.48/297.11 -->_1 top^#(mark(X)) -> c_149(top^#(proper(X))) :149 1123.48/297.11 -->_1 proper^#(isNatKind(X)) -> c_148(isNatKind^#(proper(X))) :148 1123.48/297.11 -->_1 proper^#(isNatIListKind(X)) -> 1123.48/297.11 c_147(isNatIListKind^#(proper(X))) :147 1123.48/297.11 -->_1 proper^#(and(X1, X2)) -> 1123.48/297.11 c_146(and^#(proper(X1), proper(X2))) :146 1123.48/297.11 -->_1 proper^#(take(X1, X2)) -> 1123.48/297.11 c_145(take^#(proper(X1), proper(X2))) :145 1123.48/297.11 -->_1 proper^#(U91(X1, X2, X3, X4)) -> 1123.48/297.11 c_144(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) :144 1123.48/297.11 -->_1 proper^#(U81(X)) -> c_142(U81^#(proper(X))) :142 1123.48/297.11 -->_1 proper^#(length(X)) -> c_141(length^#(proper(X))) :141 1123.48/297.11 -->_1 proper^#(s(X)) -> c_140(s^#(proper(X))) :140 1123.48/297.11 -->_1 proper^#(U71(X1, X2)) -> 1123.48/297.11 c_139(U71^#(proper(X1), proper(X2))) :139 1123.48/297.11 -->_1 proper^#(U63(X)) -> c_138(U63^#(proper(X))) :138 1123.48/297.11 -->_1 proper^#(U62(X1, X2)) -> 1123.48/297.11 c_137(U62^#(proper(X1), proper(X2))) :137 1123.48/297.11 -->_1 proper^#(U61(X1, X2, X3)) -> 1123.48/297.11 c_136(U61^#(proper(X1), proper(X2), proper(X3))) :136 1123.48/297.11 -->_1 proper^#(U53(X)) -> c_135(U53^#(proper(X))) :135 1123.48/297.11 -->_1 proper^#(U52(X1, X2)) -> 1123.48/297.11 c_134(U52^#(proper(X1), proper(X2))) :134 1123.48/297.11 -->_1 proper^#(U51(X1, X2, X3)) -> 1123.48/297.11 c_133(U51^#(proper(X1), proper(X2), proper(X3))) :133 1123.48/297.11 -->_1 proper^#(isNatIList(X)) -> 1123.48/297.11 c_132(isNatIList^#(proper(X))) :132 1123.48/297.11 -->_1 proper^#(U43(X)) -> c_131(U43^#(proper(X))) :131 1123.48/297.11 -->_1 proper^#(U42(X1, X2)) -> 1123.48/297.11 c_130(U42^#(proper(X1), proper(X2))) :130 1123.48/297.11 -->_1 proper^#(U41(X1, X2, X3)) -> 1123.48/297.11 c_129(U41^#(proper(X1), proper(X2), proper(X3))) :129 1123.48/297.11 -->_1 proper^#(U32(X)) -> c_128(U32^#(proper(X))) :128 1123.48/297.11 -->_1 proper^#(U31(X1, X2)) -> 1123.48/297.11 c_127(U31^#(proper(X1), proper(X2))) :127 1123.48/297.11 -->_1 proper^#(isNat(X)) -> c_126(isNat^#(proper(X))) :126 1123.48/297.11 -->_1 proper^#(U22(X)) -> c_125(U22^#(proper(X))) :125 1123.48/297.11 -->_1 proper^#(U21(X1, X2)) -> 1123.48/297.11 c_124(U21^#(proper(X1), proper(X2))) :124 1123.48/297.11 -->_1 proper^#(isNatList(X)) -> c_123(isNatList^#(proper(X))) :123 1123.48/297.11 -->_1 proper^#(U12(X)) -> c_122(U12^#(proper(X))) :122 1123.48/297.11 -->_1 proper^#(U11(X1, X2)) -> 1123.48/297.11 c_120(U11^#(proper(X1), proper(X2))) :120 1123.48/297.11 -->_1 proper^#(cons(X1, X2)) -> 1123.48/297.11 c_118(cons^#(proper(X1), proper(X2))) :118 1123.48/297.11 -->_1 isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) :116 1123.48/297.11 -->_1 isNat^#(ok(X)) -> c_76(isNat^#(X)) :115 1123.48/297.11 -->_1 isNatList^#(ok(X)) -> c_71(isNatList^#(X)) :114 1123.48/297.11 -->_1 isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) :113 1123.48/297.11 -->_1 isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) :112 1123.48/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.11 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.11 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.11 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.11 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.11 -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.11 c_109(U91^#(X1, X2, X3, X4)) :106 1123.48/297.11 -->_1 U91^#(mark(X1), X2, X3, X4) -> 1123.48/297.11 c_108(U91^#(X1, X2, X3, X4)) :105 1123.48/297.11 -->_1 U81^#(ok(X)) -> c_107(U81^#(X)) :104 1123.48/297.11 -->_1 U81^#(mark(X)) -> c_106(U81^#(X)) :103 1123.48/297.11 -->_1 length^#(ok(X)) -> c_105(length^#(X)) :102 1123.48/297.11 -->_1 length^#(mark(X)) -> c_104(length^#(X)) :101 1123.48/297.11 -->_1 s^#(ok(X)) -> c_103(s^#(X)) :100 1123.48/297.11 -->_1 s^#(mark(X)) -> c_102(s^#(X)) :99 1123.48/297.11 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 1123.48/297.11 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 1123.48/297.11 -->_1 U63^#(ok(X)) -> c_99(U63^#(X)) :96 1123.48/297.11 -->_1 U63^#(mark(X)) -> c_98(U63^#(X)) :95 1123.48/297.11 -->_1 U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) :94 1123.48/297.11 -->_1 U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) :93 1123.48/297.11 -->_1 U53^#(ok(X)) -> c_93(U53^#(X)) :92 1123.48/297.11 -->_1 U53^#(mark(X)) -> c_92(U53^#(X)) :91 1123.48/297.11 -->_1 U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) :90 1123.48/297.11 -->_1 U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) :89 1123.48/297.11 -->_1 U43^#(ok(X)) -> c_86(U43^#(X)) :88 1123.48/297.11 -->_1 U43^#(mark(X)) -> c_85(U43^#(X)) :87 1123.48/297.11 -->_1 U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) :86 1123.48/297.11 -->_1 U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) :85 1123.48/297.11 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) :84 1123.48/297.11 -->_1 U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) :83 1123.48/297.11 -->_1 U32^#(ok(X)) -> c_80(U32^#(X)) :82 1123.48/297.11 -->_1 U32^#(mark(X)) -> c_79(U32^#(X)) :81 1123.48/297.11 -->_1 U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) :80 1123.48/297.11 -->_1 U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) :79 1123.48/297.11 -->_1 U22^#(ok(X)) -> c_75(U22^#(X)) :78 1123.48/297.11 -->_1 U22^#(mark(X)) -> c_74(U22^#(X)) :77 1123.48/297.11 -->_1 U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) :76 1123.48/297.11 -->_1 U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) :75 1123.48/297.11 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) :74 1123.48/297.11 -->_1 U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) :73 1123.48/297.11 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) :72 1123.48/297.11 -->_1 U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) :71 1123.48/297.11 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 1123.48/297.11 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 1123.48/297.11 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 1123.48/297.11 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 1123.48/297.11 -->_1 cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) :66 1123.48/297.11 -->_1 cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) :65 1123.48/297.11 -->_1 active^#(isNatKind(length(V1))) -> 1123.48/297.11 c_64(isNatIListKind^#(V1)) :64 1123.48/297.11 -->_1 active^#(isNatKind(s(V1))) -> c_63(isNatKind^#(V1)) :63 1123.48/297.11 -->_1 active^#(isNatIListKind(take(V1, V2))) -> 1123.48/297.11 c_61(and^#(isNatKind(V1), isNatIListKind(V2))) :61 1123.48/297.11 -->_1 active^#(isNatIListKind(cons(V1, V2))) -> 1123.48/297.11 c_59(and^#(isNatKind(V1), isNatIListKind(V2))) :59 1123.48/297.11 -->_1 proper^#(nil()) -> c_143() :143 1123.48/297.11 -->_1 proper^#(tt()) -> c_121() :121 1123.48/297.11 -->_1 proper^#(0()) -> c_119() :119 1123.48/297.11 -->_1 proper^#(zeros()) -> c_117() :117 1123.48/297.11 -->_1 active^#(isNatKind(0())) -> c_62() :62 1123.48/297.11 -->_1 active^#(isNatIListKind(nil())) -> c_60() :60 1123.48/297.11 -->_1 active^#(isNatIListKind(zeros())) -> c_58() :58 1123.48/297.11 -->_1 active^#(and(tt(), X)) -> c_57(X) :57 1123.48/297.11 -->_1 active^#(and(X1, X2)) -> c_56(and^#(active(X1), X2)) :56 1123.48/297.11 -->_1 active^#(take(s(M), cons(N, IL))) -> 1123.48/297.11 c_55(U91^#(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.48/297.11 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.48/297.11 IL, 1123.48/297.11 M, 1123.48/297.11 N)) :55 1123.48/297.11 -->_1 active^#(take(0(), IL)) -> 1123.48/297.11 c_54(U81^#(and(isNatIList(IL), isNatIListKind(IL)))) :54 1123.48/297.11 -->_1 active^#(take(X1, X2)) -> c_53(take^#(active(X1), X2)) :53 1123.48/297.11 -->_1 active^#(take(X1, X2)) -> c_52(take^#(X1, active(X2))) :52 1123.48/297.11 -->_1 active^#(U91(tt(), IL, M, N)) -> 1123.48/297.11 c_51(cons^#(N, take(M, IL))) :51 1123.48/297.11 -->_1 active^#(U91(X1, X2, X3, X4)) -> 1123.48/297.11 c_50(U91^#(active(X1), X2, X3, X4)) :50 1123.48/297.11 -->_1 active^#(U81(tt())) -> c_49() :49 1123.48/297.11 -->_1 active^#(U81(X)) -> c_48(U81^#(active(X))) :48 1123.48/297.11 -->_1 active^#(length(nil())) -> c_47() :47 1123.48/297.11 -->_1 active^#(length(cons(N, L))) -> 1123.48/297.11 c_46(U71^#(and(and(isNatList(L), isNatIListKind(L)), 1123.48/297.11 and(isNat(N), isNatKind(N))), 1123.48/297.11 L)) :46 1123.48/297.11 -->_1 active^#(length(X)) -> c_45(length^#(active(X))) :45 1123.48/297.11 -->_1 active^#(s(X)) -> c_44(s^#(active(X))) :44 1123.48/297.11 -->_1 active^#(U71(tt(), L)) -> c_43(s^#(length(L))) :43 1123.48/297.11 -->_1 active^#(U71(X1, X2)) -> c_42(U71^#(active(X1), X2)) :42 1123.48/297.11 -->_1 active^#(U63(tt())) -> c_41() :41 1123.48/297.11 -->_1 active^#(U63(X)) -> c_40(U63^#(active(X))) :40 1123.48/297.11 -->_1 active^#(U62(tt(), V2)) -> c_39(U63^#(isNatIList(V2))) :39 1123.48/297.11 -->_1 active^#(U62(X1, X2)) -> c_38(U62^#(active(X1), X2)) :38 1123.48/297.11 -->_1 active^#(U61(tt(), V1, V2)) -> c_37(U62^#(isNat(V1), V2)) :37 1123.48/297.11 -->_1 active^#(U61(X1, X2, X3)) -> 1123.48/297.11 c_36(U61^#(active(X1), X2, X3)) :36 1123.48/297.11 -->_1 active^#(U53(tt())) -> c_35() :35 1123.48/297.11 -->_1 active^#(U53(X)) -> c_34(U53^#(active(X))) :34 1123.48/297.11 -->_1 active^#(U52(tt(), V2)) -> c_33(U53^#(isNatList(V2))) :33 1123.48/297.11 -->_1 active^#(U52(X1, X2)) -> c_32(U52^#(active(X1), X2)) :32 1123.48/297.11 -->_1 active^#(U51(tt(), V1, V2)) -> c_31(U52^#(isNat(V1), V2)) :31 1123.48/297.11 -->_1 active^#(U51(X1, X2, X3)) -> 1123.48/297.11 c_30(U51^#(active(X1), X2, X3)) :30 1123.48/297.11 -->_1 active^#(isNatIList(cons(V1, V2))) -> 1123.48/297.11 c_29(U41^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) :29 1123.48/297.11 -->_1 active^#(isNatIList(zeros())) -> c_28() :28 1123.48/297.11 -->_1 active^#(isNatIList(V)) -> 1123.48/297.11 c_27(U31^#(isNatIListKind(V), V)) :27 1123.48/297.11 -->_1 active^#(U43(tt())) -> c_26() :26 1123.48/297.11 -->_1 active^#(U43(X)) -> c_25(U43^#(active(X))) :25 1123.48/297.11 -->_1 active^#(U42(tt(), V2)) -> c_24(U43^#(isNatIList(V2))) :24 1123.48/297.11 -->_1 active^#(U42(X1, X2)) -> c_23(U42^#(active(X1), X2)) :23 1123.48/297.11 -->_1 active^#(U41(tt(), V1, V2)) -> c_22(U42^#(isNat(V1), V2)) :22 1123.48/297.11 -->_1 active^#(U41(X1, X2, X3)) -> 1123.48/297.11 c_21(U41^#(active(X1), X2, X3)) :21 1123.48/297.11 -->_1 active^#(U32(tt())) -> c_20() :20 1123.48/297.11 -->_1 active^#(U32(X)) -> c_19(U32^#(active(X))) :19 1123.48/297.11 -->_1 active^#(U31(tt(), V)) -> c_18(U32^#(isNatList(V))) :18 1123.48/297.11 -->_1 active^#(U31(X1, X2)) -> c_17(U31^#(active(X1), X2)) :17 1123.48/297.11 -->_1 active^#(isNat(length(V1))) -> 1123.48/297.11 c_16(U11^#(isNatIListKind(V1), V1)) :16 1123.48/297.11 -->_1 active^#(isNat(s(V1))) -> c_15(U21^#(isNatKind(V1), V1)) :15 1123.48/297.11 -->_1 active^#(isNat(0())) -> c_14() :14 1123.48/297.11 -->_1 active^#(U22(tt())) -> c_13() :13 1123.48/297.11 -->_1 active^#(U22(X)) -> c_12(U22^#(active(X))) :12 1123.48/297.11 -->_1 active^#(U21(tt(), V1)) -> c_11(U22^#(isNat(V1))) :11 1123.48/297.11 -->_1 active^#(U21(X1, X2)) -> c_10(U21^#(active(X1), X2)) :10 1123.48/297.11 -->_1 active^#(isNatList(take(V1, V2))) -> 1123.48/297.11 c_9(U61^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) :9 1123.48/297.11 -->_1 active^#(isNatList(nil())) -> c_8() :8 1123.48/297.11 -->_1 active^#(isNatList(cons(V1, V2))) -> 1123.48/297.11 c_7(U51^#(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) :7 1123.48/297.11 -->_1 active^#(U12(tt())) -> c_6() :6 1123.48/297.11 -->_1 active^#(U12(X)) -> c_5(U12^#(active(X))) :5 1123.48/297.11 -->_1 active^#(U11(tt(), V1)) -> c_4(U12^#(isNatList(V1))) :4 1123.48/297.11 -->_1 active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) :3 1123.48/297.11 -->_1 active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) :2 1123.48/297.11 -->_1 active^#(zeros()) -> c_1(cons^#(0(), zeros())) :1 1123.48/297.11 1123.48/297.11 58: active^#(isNatIListKind(zeros())) -> c_58() 1123.48/297.11 1123.48/297.11 59: active^#(isNatIListKind(cons(V1, V2))) -> 1123.48/297.11 c_59(and^#(isNatKind(V1), isNatIListKind(V2))) 1123.48/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.11 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.11 1123.48/297.11 60: active^#(isNatIListKind(nil())) -> c_60() 1123.48/297.11 1123.48/297.11 61: active^#(isNatIListKind(take(V1, V2))) -> 1123.48/297.11 c_61(and^#(isNatKind(V1), isNatIListKind(V2))) 1123.48/297.11 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.11 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.11 1123.48/297.11 62: active^#(isNatKind(0())) -> c_62() 1123.48/297.11 1123.48/297.11 63: active^#(isNatKind(s(V1))) -> c_63(isNatKind^#(V1)) 1123.48/297.11 -->_1 isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) :112 1123.48/297.11 1123.48/297.11 64: active^#(isNatKind(length(V1))) -> c_64(isNatIListKind^#(V1)) 1123.48/297.12 -->_1 isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) :113 1123.48/297.12 1123.48/297.12 65: cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) 1123.48/297.12 -->_1 cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) :66 1123.48/297.12 -->_1 cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) :65 1123.48/297.12 1123.48/297.12 66: cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) 1123.48/297.12 -->_1 cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) :66 1123.48/297.12 -->_1 cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) :65 1123.48/297.12 1123.48/297.12 67: U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 1123.48/297.12 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 1123.48/297.12 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 1123.48/297.12 1123.48/297.12 68: U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 1123.48/297.12 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 1123.48/297.12 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 1123.48/297.12 1123.48/297.12 69: U12^#(mark(X)) -> c_69(U12^#(X)) 1123.48/297.12 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 1123.48/297.12 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 1123.48/297.12 1123.48/297.12 70: U12^#(ok(X)) -> c_70(U12^#(X)) 1123.48/297.12 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 1123.48/297.12 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 1123.48/297.12 1123.48/297.12 71: U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) 1123.48/297.12 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) :72 1123.48/297.12 -->_1 U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) :71 1123.48/297.12 1123.48/297.12 72: U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) 1123.48/297.12 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) :72 1123.48/297.12 -->_1 U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) :71 1123.48/297.12 1123.48/297.12 73: U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) 1123.48/297.12 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) :74 1123.48/297.12 -->_1 U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) :73 1123.48/297.12 1123.48/297.12 74: U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) 1123.48/297.12 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) :74 1123.48/297.12 -->_1 U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) :73 1123.48/297.12 1123.48/297.12 75: U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) 1123.48/297.12 -->_1 U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) :76 1123.48/297.12 -->_1 U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) :75 1123.48/297.12 1123.48/297.12 76: U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) 1123.48/297.12 -->_1 U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) :76 1123.48/297.12 -->_1 U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) :75 1123.48/297.12 1123.48/297.12 77: U22^#(mark(X)) -> c_74(U22^#(X)) 1123.48/297.12 -->_1 U22^#(ok(X)) -> c_75(U22^#(X)) :78 1123.48/297.12 -->_1 U22^#(mark(X)) -> c_74(U22^#(X)) :77 1123.48/297.12 1123.48/297.12 78: U22^#(ok(X)) -> c_75(U22^#(X)) 1123.48/297.12 -->_1 U22^#(ok(X)) -> c_75(U22^#(X)) :78 1123.48/297.12 -->_1 U22^#(mark(X)) -> c_74(U22^#(X)) :77 1123.48/297.12 1123.48/297.12 79: U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) 1123.48/297.12 -->_1 U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) :80 1123.48/297.12 -->_1 U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) :79 1123.48/297.12 1123.48/297.12 80: U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) 1123.48/297.12 -->_1 U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) :80 1123.48/297.12 -->_1 U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) :79 1123.48/297.12 1123.48/297.12 81: U32^#(mark(X)) -> c_79(U32^#(X)) 1123.48/297.12 -->_1 U32^#(ok(X)) -> c_80(U32^#(X)) :82 1123.48/297.12 -->_1 U32^#(mark(X)) -> c_79(U32^#(X)) :81 1123.48/297.12 1123.48/297.12 82: U32^#(ok(X)) -> c_80(U32^#(X)) 1123.48/297.12 -->_1 U32^#(ok(X)) -> c_80(U32^#(X)) :82 1123.48/297.12 -->_1 U32^#(mark(X)) -> c_79(U32^#(X)) :81 1123.48/297.12 1123.48/297.12 83: U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) 1123.48/297.12 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) :84 1123.48/297.12 -->_1 U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) :83 1123.48/297.12 1123.48/297.12 84: U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) 1123.48/297.12 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) :84 1123.48/297.12 -->_1 U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) :83 1123.48/297.12 1123.48/297.12 85: U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) 1123.48/297.12 -->_1 U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) :86 1123.48/297.12 -->_1 U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) :85 1123.48/297.12 1123.48/297.12 86: U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) 1123.48/297.12 -->_1 U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) :86 1123.48/297.12 -->_1 U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) :85 1123.48/297.12 1123.48/297.12 87: U43^#(mark(X)) -> c_85(U43^#(X)) 1123.48/297.12 -->_1 U43^#(ok(X)) -> c_86(U43^#(X)) :88 1123.48/297.12 -->_1 U43^#(mark(X)) -> c_85(U43^#(X)) :87 1123.48/297.12 1123.48/297.12 88: U43^#(ok(X)) -> c_86(U43^#(X)) 1123.48/297.12 -->_1 U43^#(ok(X)) -> c_86(U43^#(X)) :88 1123.48/297.12 -->_1 U43^#(mark(X)) -> c_85(U43^#(X)) :87 1123.48/297.12 1123.48/297.12 89: U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) 1123.48/297.12 -->_1 U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) :90 1123.48/297.12 -->_1 U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) :89 1123.48/297.12 1123.48/297.12 90: U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) 1123.48/297.12 -->_1 U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) :90 1123.48/297.12 -->_1 U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) :89 1123.48/297.12 1123.48/297.12 91: U53^#(mark(X)) -> c_92(U53^#(X)) 1123.48/297.12 -->_1 U53^#(ok(X)) -> c_93(U53^#(X)) :92 1123.48/297.12 -->_1 U53^#(mark(X)) -> c_92(U53^#(X)) :91 1123.48/297.12 1123.48/297.12 92: U53^#(ok(X)) -> c_93(U53^#(X)) 1123.48/297.12 -->_1 U53^#(ok(X)) -> c_93(U53^#(X)) :92 1123.48/297.12 -->_1 U53^#(mark(X)) -> c_92(U53^#(X)) :91 1123.48/297.12 1123.48/297.12 93: U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) 1123.48/297.12 -->_1 U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) :94 1123.48/297.12 -->_1 U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) :93 1123.48/297.12 1123.48/297.12 94: U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) 1123.48/297.12 -->_1 U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) :94 1123.48/297.12 -->_1 U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) :93 1123.48/297.12 1123.48/297.12 95: U63^#(mark(X)) -> c_98(U63^#(X)) 1123.48/297.12 -->_1 U63^#(ok(X)) -> c_99(U63^#(X)) :96 1123.48/297.12 -->_1 U63^#(mark(X)) -> c_98(U63^#(X)) :95 1123.48/297.12 1123.48/297.12 96: U63^#(ok(X)) -> c_99(U63^#(X)) 1123.48/297.12 -->_1 U63^#(ok(X)) -> c_99(U63^#(X)) :96 1123.48/297.12 -->_1 U63^#(mark(X)) -> c_98(U63^#(X)) :95 1123.48/297.12 1123.48/297.12 97: U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 1123.48/297.12 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 1123.48/297.12 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 1123.48/297.12 1123.48/297.12 98: U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 1123.48/297.12 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 1123.48/297.12 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 1123.48/297.12 1123.48/297.12 99: s^#(mark(X)) -> c_102(s^#(X)) 1123.48/297.12 -->_1 s^#(ok(X)) -> c_103(s^#(X)) :100 1123.48/297.12 -->_1 s^#(mark(X)) -> c_102(s^#(X)) :99 1123.48/297.12 1123.48/297.12 100: s^#(ok(X)) -> c_103(s^#(X)) 1123.48/297.12 -->_1 s^#(ok(X)) -> c_103(s^#(X)) :100 1123.48/297.12 -->_1 s^#(mark(X)) -> c_102(s^#(X)) :99 1123.48/297.12 1123.48/297.12 101: length^#(mark(X)) -> c_104(length^#(X)) 1123.48/297.12 -->_1 length^#(ok(X)) -> c_105(length^#(X)) :102 1123.48/297.12 -->_1 length^#(mark(X)) -> c_104(length^#(X)) :101 1123.48/297.12 1123.48/297.12 102: length^#(ok(X)) -> c_105(length^#(X)) 1123.48/297.12 -->_1 length^#(ok(X)) -> c_105(length^#(X)) :102 1123.48/297.12 -->_1 length^#(mark(X)) -> c_104(length^#(X)) :101 1123.48/297.12 1123.48/297.12 103: U81^#(mark(X)) -> c_106(U81^#(X)) 1123.48/297.12 -->_1 U81^#(ok(X)) -> c_107(U81^#(X)) :104 1123.48/297.12 -->_1 U81^#(mark(X)) -> c_106(U81^#(X)) :103 1123.48/297.12 1123.48/297.12 104: U81^#(ok(X)) -> c_107(U81^#(X)) 1123.48/297.12 -->_1 U81^#(ok(X)) -> c_107(U81^#(X)) :104 1123.48/297.12 -->_1 U81^#(mark(X)) -> c_106(U81^#(X)) :103 1123.48/297.12 1123.48/297.12 105: U91^#(mark(X1), X2, X3, X4) -> c_108(U91^#(X1, X2, X3, X4)) 1123.48/297.12 -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.12 c_109(U91^#(X1, X2, X3, X4)) :106 1123.48/297.12 -->_1 U91^#(mark(X1), X2, X3, X4) -> 1123.48/297.12 c_108(U91^#(X1, X2, X3, X4)) :105 1123.48/297.12 1123.48/297.12 106: U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.12 c_109(U91^#(X1, X2, X3, X4)) 1123.48/297.12 -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.12 c_109(U91^#(X1, X2, X3, X4)) :106 1123.48/297.12 -->_1 U91^#(mark(X1), X2, X3, X4) -> 1123.48/297.12 c_108(U91^#(X1, X2, X3, X4)) :105 1123.48/297.12 1123.48/297.12 107: take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) 1123.48/297.12 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.12 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.12 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.12 1123.48/297.12 108: take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) 1123.48/297.12 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.12 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.12 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.12 1123.48/297.12 109: take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) 1123.48/297.12 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.12 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.12 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.12 1123.48/297.12 110: and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) 1123.48/297.12 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.12 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.12 1123.48/297.12 111: and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) 1123.48/297.12 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.12 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.12 1123.48/297.12 112: isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) 1123.48/297.12 -->_1 isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) :112 1123.48/297.12 1123.48/297.12 113: isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) 1123.48/297.12 -->_1 isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) :113 1123.48/297.12 1123.48/297.12 114: isNatList^#(ok(X)) -> c_71(isNatList^#(X)) 1123.48/297.12 -->_1 isNatList^#(ok(X)) -> c_71(isNatList^#(X)) :114 1123.48/297.12 1123.48/297.12 115: isNat^#(ok(X)) -> c_76(isNat^#(X)) 1123.48/297.12 -->_1 isNat^#(ok(X)) -> c_76(isNat^#(X)) :115 1123.48/297.12 1123.48/297.12 116: isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) 1123.48/297.12 -->_1 isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) :116 1123.48/297.12 1123.48/297.12 117: proper^#(zeros()) -> c_117() 1123.48/297.12 1123.48/297.12 118: proper^#(cons(X1, X2)) -> 1123.48/297.12 c_118(cons^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) :66 1123.48/297.12 -->_1 cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) :65 1123.48/297.12 1123.48/297.12 119: proper^#(0()) -> c_119() 1123.48/297.12 1123.48/297.12 120: proper^#(U11(X1, X2)) -> c_120(U11^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) :68 1123.48/297.12 -->_1 U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) :67 1123.48/297.12 1123.48/297.12 121: proper^#(tt()) -> c_121() 1123.48/297.12 1123.48/297.12 122: proper^#(U12(X)) -> c_122(U12^#(proper(X))) 1123.48/297.12 -->_1 U12^#(ok(X)) -> c_70(U12^#(X)) :70 1123.48/297.12 -->_1 U12^#(mark(X)) -> c_69(U12^#(X)) :69 1123.48/297.12 1123.48/297.12 123: proper^#(isNatList(X)) -> c_123(isNatList^#(proper(X))) 1123.48/297.12 -->_1 isNatList^#(ok(X)) -> c_71(isNatList^#(X)) :114 1123.48/297.12 1123.48/297.12 124: proper^#(U21(X1, X2)) -> c_124(U21^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) :76 1123.48/297.12 -->_1 U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) :75 1123.48/297.12 1123.48/297.12 125: proper^#(U22(X)) -> c_125(U22^#(proper(X))) 1123.48/297.12 -->_1 U22^#(ok(X)) -> c_75(U22^#(X)) :78 1123.48/297.12 -->_1 U22^#(mark(X)) -> c_74(U22^#(X)) :77 1123.48/297.12 1123.48/297.12 126: proper^#(isNat(X)) -> c_126(isNat^#(proper(X))) 1123.48/297.12 -->_1 isNat^#(ok(X)) -> c_76(isNat^#(X)) :115 1123.48/297.12 1123.48/297.12 127: proper^#(U31(X1, X2)) -> c_127(U31^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) :80 1123.48/297.12 -->_1 U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) :79 1123.48/297.12 1123.48/297.12 128: proper^#(U32(X)) -> c_128(U32^#(proper(X))) 1123.48/297.12 -->_1 U32^#(ok(X)) -> c_80(U32^#(X)) :82 1123.48/297.12 -->_1 U32^#(mark(X)) -> c_79(U32^#(X)) :81 1123.48/297.12 1123.48/297.12 129: proper^#(U41(X1, X2, X3)) -> 1123.48/297.12 c_129(U41^#(proper(X1), proper(X2), proper(X3))) 1123.48/297.12 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) :84 1123.48/297.12 -->_1 U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) :83 1123.48/297.12 1123.48/297.12 130: proper^#(U42(X1, X2)) -> c_130(U42^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) :86 1123.48/297.12 -->_1 U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) :85 1123.48/297.12 1123.48/297.12 131: proper^#(U43(X)) -> c_131(U43^#(proper(X))) 1123.48/297.12 -->_1 U43^#(ok(X)) -> c_86(U43^#(X)) :88 1123.48/297.12 -->_1 U43^#(mark(X)) -> c_85(U43^#(X)) :87 1123.48/297.12 1123.48/297.12 132: proper^#(isNatIList(X)) -> c_132(isNatIList^#(proper(X))) 1123.48/297.12 -->_1 isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) :116 1123.48/297.12 1123.48/297.12 133: proper^#(U51(X1, X2, X3)) -> 1123.48/297.12 c_133(U51^#(proper(X1), proper(X2), proper(X3))) 1123.48/297.12 -->_1 U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) :72 1123.48/297.12 -->_1 U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) :71 1123.48/297.12 1123.48/297.12 134: proper^#(U52(X1, X2)) -> c_134(U52^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) :90 1123.48/297.12 -->_1 U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) :89 1123.48/297.12 1123.48/297.12 135: proper^#(U53(X)) -> c_135(U53^#(proper(X))) 1123.48/297.12 -->_1 U53^#(ok(X)) -> c_93(U53^#(X)) :92 1123.48/297.12 -->_1 U53^#(mark(X)) -> c_92(U53^#(X)) :91 1123.48/297.12 1123.48/297.12 136: proper^#(U61(X1, X2, X3)) -> 1123.48/297.12 c_136(U61^#(proper(X1), proper(X2), proper(X3))) 1123.48/297.12 -->_1 U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) :74 1123.48/297.12 -->_1 U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) :73 1123.48/297.12 1123.48/297.12 137: proper^#(U62(X1, X2)) -> c_137(U62^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) :94 1123.48/297.12 -->_1 U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) :93 1123.48/297.12 1123.48/297.12 138: proper^#(U63(X)) -> c_138(U63^#(proper(X))) 1123.48/297.12 -->_1 U63^#(ok(X)) -> c_99(U63^#(X)) :96 1123.48/297.12 -->_1 U63^#(mark(X)) -> c_98(U63^#(X)) :95 1123.48/297.12 1123.48/297.12 139: proper^#(U71(X1, X2)) -> c_139(U71^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) :98 1123.48/297.12 -->_1 U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) :97 1123.48/297.12 1123.48/297.12 140: proper^#(s(X)) -> c_140(s^#(proper(X))) 1123.48/297.12 -->_1 s^#(ok(X)) -> c_103(s^#(X)) :100 1123.48/297.12 -->_1 s^#(mark(X)) -> c_102(s^#(X)) :99 1123.48/297.12 1123.48/297.12 141: proper^#(length(X)) -> c_141(length^#(proper(X))) 1123.48/297.12 -->_1 length^#(ok(X)) -> c_105(length^#(X)) :102 1123.48/297.12 -->_1 length^#(mark(X)) -> c_104(length^#(X)) :101 1123.48/297.12 1123.48/297.12 142: proper^#(U81(X)) -> c_142(U81^#(proper(X))) 1123.48/297.12 -->_1 U81^#(ok(X)) -> c_107(U81^#(X)) :104 1123.48/297.12 -->_1 U81^#(mark(X)) -> c_106(U81^#(X)) :103 1123.48/297.12 1123.48/297.12 143: proper^#(nil()) -> c_143() 1123.48/297.12 1123.48/297.12 144: proper^#(U91(X1, X2, X3, X4)) -> 1123.48/297.12 c_144(U91^#(proper(X1), proper(X2), proper(X3), proper(X4))) 1123.48/297.12 -->_1 U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.12 c_109(U91^#(X1, X2, X3, X4)) :106 1123.48/297.12 -->_1 U91^#(mark(X1), X2, X3, X4) -> 1123.48/297.12 c_108(U91^#(X1, X2, X3, X4)) :105 1123.48/297.12 1123.48/297.12 145: proper^#(take(X1, X2)) -> 1123.48/297.12 c_145(take^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) :109 1123.48/297.12 -->_1 take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) :108 1123.48/297.12 -->_1 take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) :107 1123.48/297.12 1123.48/297.12 146: proper^#(and(X1, X2)) -> c_146(and^#(proper(X1), proper(X2))) 1123.48/297.12 -->_1 and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) :111 1123.48/297.12 -->_1 and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) :110 1123.48/297.12 1123.48/297.12 147: proper^#(isNatIListKind(X)) -> 1123.48/297.12 c_147(isNatIListKind^#(proper(X))) 1123.48/297.12 -->_1 isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) :113 1123.48/297.12 1123.48/297.12 148: proper^#(isNatKind(X)) -> c_148(isNatKind^#(proper(X))) 1123.48/297.12 -->_1 isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) :112 1123.48/297.12 1123.48/297.12 149: top^#(mark(X)) -> c_149(top^#(proper(X))) 1123.48/297.12 -->_1 top^#(ok(X)) -> c_150(top^#(active(X))) :150 1123.48/297.12 -->_1 top^#(mark(X)) -> c_149(top^#(proper(X))) :149 1123.48/297.12 1123.48/297.12 150: top^#(ok(X)) -> c_150(top^#(active(X))) 1123.48/297.12 -->_1 top^#(ok(X)) -> c_150(top^#(active(X))) :150 1123.48/297.12 -->_1 top^#(mark(X)) -> c_149(top^#(proper(X))) :149 1123.48/297.12 1123.48/297.12 1123.48/297.12 Only the nodes 1123.48/297.12 {1,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,109,108,110,111,112,113,114,115,116,117,119,121,143,149,150} 1123.48/297.12 are reachable from nodes 1123.48/297.12 {1,65,66,67,68,69,70,71,72,73,74,75,76,77,78,79,80,81,82,83,84,85,86,87,88,89,90,91,92,93,94,95,96,97,98,99,100,101,102,103,104,105,106,107,108,109,110,111,112,113,114,115,116,117,119,121,143,149,150} 1123.48/297.12 that start derivation from marked basic terms. The nodes not 1123.48/297.12 reachable are removed from the problem. 1123.48/297.12 1123.48/297.12 We are left with following problem, upon which TcT provides the 1123.48/297.12 certificate MAYBE. 1123.48/297.12 1123.48/297.12 Strict DPs: 1123.48/297.12 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 1123.48/297.12 , cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) 1123.48/297.12 , cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) 1123.48/297.12 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 1123.48/297.12 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 1123.48/297.12 , U12^#(mark(X)) -> c_69(U12^#(X)) 1123.48/297.13 , U12^#(ok(X)) -> c_70(U12^#(X)) 1123.48/297.13 , U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) 1123.48/297.13 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) 1123.48/297.13 , U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) 1123.48/297.13 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) 1123.48/297.13 , U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) 1123.48/297.13 , U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) 1123.48/297.13 , U22^#(mark(X)) -> c_74(U22^#(X)) 1123.48/297.13 , U22^#(ok(X)) -> c_75(U22^#(X)) 1123.48/297.13 , U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) 1123.48/297.13 , U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) 1123.48/297.13 , U32^#(mark(X)) -> c_79(U32^#(X)) 1123.48/297.13 , U32^#(ok(X)) -> c_80(U32^#(X)) 1123.48/297.13 , U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) 1123.48/297.13 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) 1123.48/297.13 , U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) 1123.48/297.13 , U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) 1123.48/297.13 , U43^#(mark(X)) -> c_85(U43^#(X)) 1123.48/297.13 , U43^#(ok(X)) -> c_86(U43^#(X)) 1123.48/297.13 , U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) 1123.48/297.13 , U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) 1123.48/297.13 , U53^#(mark(X)) -> c_92(U53^#(X)) 1123.48/297.13 , U53^#(ok(X)) -> c_93(U53^#(X)) 1123.48/297.13 , U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) 1123.48/297.13 , U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) 1123.48/297.13 , U63^#(mark(X)) -> c_98(U63^#(X)) 1123.48/297.13 , U63^#(ok(X)) -> c_99(U63^#(X)) 1123.48/297.13 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 1123.48/297.13 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 1123.48/297.13 , s^#(mark(X)) -> c_102(s^#(X)) 1123.48/297.13 , s^#(ok(X)) -> c_103(s^#(X)) 1123.48/297.13 , length^#(mark(X)) -> c_104(length^#(X)) 1123.48/297.13 , length^#(ok(X)) -> c_105(length^#(X)) 1123.48/297.13 , U81^#(mark(X)) -> c_106(U81^#(X)) 1123.48/297.13 , U81^#(ok(X)) -> c_107(U81^#(X)) 1123.48/297.13 , U91^#(mark(X1), X2, X3, X4) -> c_108(U91^#(X1, X2, X3, X4)) 1123.48/297.13 , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.13 c_109(U91^#(X1, X2, X3, X4)) 1123.48/297.13 , take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) 1123.48/297.13 , take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) 1123.48/297.13 , take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) 1123.48/297.13 , and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) 1123.48/297.13 , and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) 1123.48/297.13 , isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) 1123.48/297.13 , isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) 1123.48/297.13 , isNatList^#(ok(X)) -> c_71(isNatList^#(X)) 1123.48/297.13 , isNat^#(ok(X)) -> c_76(isNat^#(X)) 1123.48/297.13 , isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) 1123.48/297.13 , proper^#(zeros()) -> c_117() 1123.48/297.13 , proper^#(0()) -> c_119() 1123.48/297.13 , proper^#(tt()) -> c_121() 1123.48/297.13 , proper^#(nil()) -> c_143() 1123.48/297.13 , top^#(mark(X)) -> c_149(top^#(proper(X))) 1123.48/297.13 , top^#(ok(X)) -> c_150(top^#(active(X))) } 1123.48/297.13 Strict Trs: 1123.48/297.13 { active(zeros()) -> mark(cons(0(), zeros())) 1123.48/297.13 , active(cons(X1, X2)) -> cons(active(X1), X2) 1123.48/297.13 , active(U11(X1, X2)) -> U11(active(X1), X2) 1123.48/297.13 , active(U11(tt(), V1)) -> mark(U12(isNatList(V1))) 1123.48/297.13 , active(U12(X)) -> U12(active(X)) 1123.48/297.13 , active(U12(tt())) -> mark(tt()) 1123.48/297.13 , active(isNatList(cons(V1, V2))) -> 1123.48/297.13 mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.13 , active(isNatList(nil())) -> mark(tt()) 1123.48/297.13 , active(isNatList(take(V1, V2))) -> 1123.48/297.13 mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.13 , active(U21(X1, X2)) -> U21(active(X1), X2) 1123.48/297.13 , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) 1123.48/297.13 , active(U22(X)) -> U22(active(X)) 1123.48/297.13 , active(U22(tt())) -> mark(tt()) 1123.48/297.13 , active(isNat(0())) -> mark(tt()) 1123.48/297.13 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1123.48/297.13 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 1123.48/297.13 , active(U31(X1, X2)) -> U31(active(X1), X2) 1123.48/297.13 , active(U31(tt(), V)) -> mark(U32(isNatList(V))) 1123.48/297.13 , active(U32(X)) -> U32(active(X)) 1123.48/297.13 , active(U32(tt())) -> mark(tt()) 1123.48/297.13 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 1123.48/297.13 , active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2)) 1123.48/297.13 , active(U42(X1, X2)) -> U42(active(X1), X2) 1123.48/297.13 , active(U42(tt(), V2)) -> mark(U43(isNatIList(V2))) 1123.48/297.13 , active(U43(X)) -> U43(active(X)) 1123.48/297.13 , active(U43(tt())) -> mark(tt()) 1123.48/297.13 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 1123.48/297.13 , active(isNatIList(zeros())) -> mark(tt()) 1123.48/297.13 , active(isNatIList(cons(V1, V2))) -> 1123.48/297.13 mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.13 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 1123.48/297.13 , active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2)) 1123.48/297.13 , active(U52(X1, X2)) -> U52(active(X1), X2) 1123.48/297.13 , active(U52(tt(), V2)) -> mark(U53(isNatList(V2))) 1123.48/297.13 , active(U53(X)) -> U53(active(X)) 1123.48/297.13 , active(U53(tt())) -> mark(tt()) 1123.48/297.13 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1123.48/297.13 , active(U61(tt(), V1, V2)) -> mark(U62(isNat(V1), V2)) 1123.48/297.13 , active(U62(X1, X2)) -> U62(active(X1), X2) 1123.48/297.13 , active(U62(tt(), V2)) -> mark(U63(isNatIList(V2))) 1123.48/297.13 , active(U63(X)) -> U63(active(X)) 1123.48/297.13 , active(U63(tt())) -> mark(tt()) 1123.48/297.13 , active(U71(X1, X2)) -> U71(active(X1), X2) 1123.48/297.13 , active(U71(tt(), L)) -> mark(s(length(L))) 1123.48/297.13 , active(s(X)) -> s(active(X)) 1123.48/297.13 , active(length(X)) -> length(active(X)) 1123.48/297.13 , active(length(cons(N, L))) -> 1123.48/297.13 mark(U71(and(and(isNatList(L), isNatIListKind(L)), 1123.48/297.13 and(isNat(N), isNatKind(N))), 1123.48/297.13 L)) 1123.48/297.13 , active(length(nil())) -> mark(0()) 1123.48/297.13 , active(U81(X)) -> U81(active(X)) 1123.48/297.13 , active(U81(tt())) -> mark(nil()) 1123.48/297.13 , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) 1123.48/297.13 , active(U91(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 1123.48/297.13 , active(take(X1, X2)) -> take(X1, active(X2)) 1123.48/297.13 , active(take(X1, X2)) -> take(active(X1), X2) 1123.48/297.13 , active(take(0(), IL)) -> 1123.48/297.13 mark(U81(and(isNatIList(IL), isNatIListKind(IL)))) 1123.48/297.13 , active(take(s(M), cons(N, IL))) -> 1123.48/297.13 mark(U91(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.48/297.13 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.48/297.13 IL, 1123.48/297.13 M, 1123.48/297.13 N)) 1123.48/297.13 , active(and(X1, X2)) -> and(active(X1), X2) 1123.48/297.13 , active(and(tt(), X)) -> mark(X) 1123.48/297.13 , active(isNatIListKind(zeros())) -> mark(tt()) 1123.48/297.13 , active(isNatIListKind(cons(V1, V2))) -> 1123.48/297.13 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.48/297.13 , active(isNatIListKind(nil())) -> mark(tt()) 1123.48/297.13 , active(isNatIListKind(take(V1, V2))) -> 1123.48/297.13 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.48/297.13 , active(isNatKind(0())) -> mark(tt()) 1123.48/297.13 , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) 1123.48/297.13 , active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)) 1123.48/297.13 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1123.48/297.13 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1123.48/297.13 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 1123.48/297.13 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 1123.48/297.13 , U12(mark(X)) -> mark(U12(X)) 1123.48/297.13 , U12(ok(X)) -> ok(U12(X)) 1123.48/297.13 , isNatList(ok(X)) -> ok(isNatList(X)) 1123.48/297.13 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1123.48/297.13 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1123.48/297.13 , U22(mark(X)) -> mark(U22(X)) 1123.48/297.13 , U22(ok(X)) -> ok(U22(X)) 1123.48/297.13 , isNat(ok(X)) -> ok(isNat(X)) 1123.48/297.13 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1123.48/297.13 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1123.48/297.13 , U32(mark(X)) -> mark(U32(X)) 1123.48/297.13 , U32(ok(X)) -> ok(U32(X)) 1123.48/297.13 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 1123.48/297.13 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 1123.48/297.13 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 1123.48/297.13 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 1123.48/297.13 , U43(mark(X)) -> mark(U43(X)) 1123.48/297.13 , U43(ok(X)) -> ok(U43(X)) 1123.48/297.13 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1123.48/297.13 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 1123.48/297.13 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 1123.48/297.13 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1123.48/297.13 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1123.48/297.13 , U53(mark(X)) -> mark(U53(X)) 1123.48/297.13 , U53(ok(X)) -> ok(U53(X)) 1123.48/297.13 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1123.48/297.13 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1123.48/297.13 , U62(mark(X1), X2) -> mark(U62(X1, X2)) 1123.48/297.13 , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) 1123.48/297.13 , U63(mark(X)) -> mark(U63(X)) 1123.48/297.13 , U63(ok(X)) -> ok(U63(X)) 1123.48/297.13 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1123.48/297.13 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1123.48/297.13 , s(mark(X)) -> mark(s(X)) 1123.48/297.13 , s(ok(X)) -> ok(s(X)) 1123.48/297.13 , length(mark(X)) -> mark(length(X)) 1123.48/297.13 , length(ok(X)) -> ok(length(X)) 1123.48/297.13 , U81(mark(X)) -> mark(U81(X)) 1123.48/297.13 , U81(ok(X)) -> ok(U81(X)) 1123.48/297.13 , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) 1123.48/297.13 , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) 1123.48/297.13 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1123.48/297.13 , take(mark(X1), X2) -> mark(take(X1, X2)) 1123.48/297.13 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1123.48/297.13 , and(mark(X1), X2) -> mark(and(X1, X2)) 1123.48/297.13 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1123.48/297.13 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 1123.48/297.13 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1123.48/297.13 , proper(zeros()) -> ok(zeros()) 1123.48/297.13 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1123.48/297.13 , proper(0()) -> ok(0()) 1123.48/297.13 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 1123.48/297.13 , proper(tt()) -> ok(tt()) 1123.48/297.13 , proper(U12(X)) -> U12(proper(X)) 1123.48/297.13 , proper(isNatList(X)) -> isNatList(proper(X)) 1123.48/297.13 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1123.48/297.13 , proper(U22(X)) -> U22(proper(X)) 1123.48/297.13 , proper(isNat(X)) -> isNat(proper(X)) 1123.48/297.13 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1123.48/297.13 , proper(U32(X)) -> U32(proper(X)) 1123.48/297.13 , proper(U41(X1, X2, X3)) -> 1123.48/297.13 U41(proper(X1), proper(X2), proper(X3)) 1123.48/297.13 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 1123.48/297.13 , proper(U43(X)) -> U43(proper(X)) 1123.48/297.13 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1123.48/297.13 , proper(U51(X1, X2, X3)) -> 1123.48/297.13 U51(proper(X1), proper(X2), proper(X3)) 1123.48/297.13 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1123.48/297.13 , proper(U53(X)) -> U53(proper(X)) 1123.48/297.13 , proper(U61(X1, X2, X3)) -> 1123.48/297.13 U61(proper(X1), proper(X2), proper(X3)) 1123.48/297.13 , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) 1123.48/297.13 , proper(U63(X)) -> U63(proper(X)) 1123.48/297.13 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1123.48/297.13 , proper(s(X)) -> s(proper(X)) 1123.48/297.13 , proper(length(X)) -> length(proper(X)) 1123.48/297.13 , proper(U81(X)) -> U81(proper(X)) 1123.48/297.13 , proper(nil()) -> ok(nil()) 1123.48/297.13 , proper(U91(X1, X2, X3, X4)) -> 1123.48/297.13 U91(proper(X1), proper(X2), proper(X3), proper(X4)) 1123.48/297.13 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1123.48/297.13 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1123.48/297.13 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 1123.48/297.13 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1123.48/297.13 , top(mark(X)) -> top(proper(X)) 1123.48/297.13 , top(ok(X)) -> top(active(X)) } 1123.48/297.13 Obligation: 1123.48/297.13 runtime complexity 1123.48/297.13 Answer: 1123.48/297.13 MAYBE 1123.48/297.13 1123.48/297.13 We estimate the number of application of {1,54,55,56,57} by 1123.48/297.13 applications of Pre({1,54,55,56,57}) = {}. Here rules are labeled 1123.48/297.13 as follows: 1123.48/297.13 1123.48/297.13 DPs: 1123.48/297.13 { 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 1123.48/297.13 , 2: cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) 1123.48/297.13 , 3: cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) 1123.48/297.13 , 4: U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 1123.48/297.13 , 5: U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 1123.48/297.13 , 6: U12^#(mark(X)) -> c_69(U12^#(X)) 1123.48/297.13 , 7: U12^#(ok(X)) -> c_70(U12^#(X)) 1123.48/297.13 , 8: U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) 1123.48/297.13 , 9: U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) 1123.48/297.13 , 10: U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) 1123.48/297.13 , 11: U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) 1123.48/297.13 , 12: U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) 1123.48/297.13 , 13: U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) 1123.48/297.13 , 14: U22^#(mark(X)) -> c_74(U22^#(X)) 1123.48/297.13 , 15: U22^#(ok(X)) -> c_75(U22^#(X)) 1123.48/297.13 , 16: U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) 1123.48/297.13 , 17: U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) 1123.48/297.13 , 18: U32^#(mark(X)) -> c_79(U32^#(X)) 1123.48/297.13 , 19: U32^#(ok(X)) -> c_80(U32^#(X)) 1123.48/297.13 , 20: U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) 1123.48/297.13 , 21: U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) 1123.48/297.13 , 22: U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) 1123.48/297.13 , 23: U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) 1123.48/297.13 , 24: U43^#(mark(X)) -> c_85(U43^#(X)) 1123.48/297.13 , 25: U43^#(ok(X)) -> c_86(U43^#(X)) 1123.48/297.13 , 26: U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) 1123.48/297.13 , 27: U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) 1123.48/297.13 , 28: U53^#(mark(X)) -> c_92(U53^#(X)) 1123.48/297.13 , 29: U53^#(ok(X)) -> c_93(U53^#(X)) 1123.48/297.13 , 30: U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) 1123.48/297.13 , 31: U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) 1123.48/297.13 , 32: U63^#(mark(X)) -> c_98(U63^#(X)) 1123.48/297.13 , 33: U63^#(ok(X)) -> c_99(U63^#(X)) 1123.48/297.13 , 34: U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 1123.48/297.13 , 35: U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 1123.48/297.13 , 36: s^#(mark(X)) -> c_102(s^#(X)) 1123.48/297.13 , 37: s^#(ok(X)) -> c_103(s^#(X)) 1123.48/297.13 , 38: length^#(mark(X)) -> c_104(length^#(X)) 1123.48/297.13 , 39: length^#(ok(X)) -> c_105(length^#(X)) 1123.48/297.13 , 40: U81^#(mark(X)) -> c_106(U81^#(X)) 1123.48/297.13 , 41: U81^#(ok(X)) -> c_107(U81^#(X)) 1123.48/297.13 , 42: U91^#(mark(X1), X2, X3, X4) -> c_108(U91^#(X1, X2, X3, X4)) 1123.48/297.13 , 43: U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.13 c_109(U91^#(X1, X2, X3, X4)) 1123.48/297.13 , 44: take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) 1123.48/297.13 , 45: take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) 1123.48/297.13 , 46: take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) 1123.48/297.13 , 47: and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) 1123.48/297.13 , 48: and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) 1123.48/297.13 , 49: isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) 1123.48/297.13 , 50: isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) 1123.48/297.13 , 51: isNatList^#(ok(X)) -> c_71(isNatList^#(X)) 1123.48/297.13 , 52: isNat^#(ok(X)) -> c_76(isNat^#(X)) 1123.48/297.13 , 53: isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) 1123.48/297.13 , 54: proper^#(zeros()) -> c_117() 1123.48/297.13 , 55: proper^#(0()) -> c_119() 1123.48/297.13 , 56: proper^#(tt()) -> c_121() 1123.48/297.13 , 57: proper^#(nil()) -> c_143() 1123.48/297.13 , 58: top^#(mark(X)) -> c_149(top^#(proper(X))) 1123.48/297.13 , 59: top^#(ok(X)) -> c_150(top^#(active(X))) } 1123.48/297.13 1123.48/297.13 We are left with following problem, upon which TcT provides the 1123.48/297.13 certificate MAYBE. 1123.48/297.13 1123.48/297.13 Strict DPs: 1123.48/297.13 { cons^#(mark(X1), X2) -> c_65(cons^#(X1, X2)) 1123.48/297.13 , cons^#(ok(X1), ok(X2)) -> c_66(cons^#(X1, X2)) 1123.48/297.13 , U11^#(mark(X1), X2) -> c_67(U11^#(X1, X2)) 1123.48/297.13 , U11^#(ok(X1), ok(X2)) -> c_68(U11^#(X1, X2)) 1123.48/297.13 , U12^#(mark(X)) -> c_69(U12^#(X)) 1123.48/297.13 , U12^#(ok(X)) -> c_70(U12^#(X)) 1123.48/297.13 , U51^#(mark(X1), X2, X3) -> c_88(U51^#(X1, X2, X3)) 1123.48/297.13 , U51^#(ok(X1), ok(X2), ok(X3)) -> c_89(U51^#(X1, X2, X3)) 1123.48/297.13 , U61^#(mark(X1), X2, X3) -> c_94(U61^#(X1, X2, X3)) 1123.48/297.13 , U61^#(ok(X1), ok(X2), ok(X3)) -> c_95(U61^#(X1, X2, X3)) 1123.48/297.13 , U21^#(mark(X1), X2) -> c_72(U21^#(X1, X2)) 1123.48/297.13 , U21^#(ok(X1), ok(X2)) -> c_73(U21^#(X1, X2)) 1123.48/297.13 , U22^#(mark(X)) -> c_74(U22^#(X)) 1123.48/297.13 , U22^#(ok(X)) -> c_75(U22^#(X)) 1123.48/297.13 , U31^#(mark(X1), X2) -> c_77(U31^#(X1, X2)) 1123.48/297.13 , U31^#(ok(X1), ok(X2)) -> c_78(U31^#(X1, X2)) 1123.48/297.13 , U32^#(mark(X)) -> c_79(U32^#(X)) 1123.48/297.13 , U32^#(ok(X)) -> c_80(U32^#(X)) 1123.48/297.13 , U41^#(mark(X1), X2, X3) -> c_81(U41^#(X1, X2, X3)) 1123.48/297.13 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_82(U41^#(X1, X2, X3)) 1123.48/297.13 , U42^#(mark(X1), X2) -> c_83(U42^#(X1, X2)) 1123.48/297.13 , U42^#(ok(X1), ok(X2)) -> c_84(U42^#(X1, X2)) 1123.48/297.13 , U43^#(mark(X)) -> c_85(U43^#(X)) 1123.48/297.13 , U43^#(ok(X)) -> c_86(U43^#(X)) 1123.48/297.13 , U52^#(mark(X1), X2) -> c_90(U52^#(X1, X2)) 1123.48/297.13 , U52^#(ok(X1), ok(X2)) -> c_91(U52^#(X1, X2)) 1123.48/297.13 , U53^#(mark(X)) -> c_92(U53^#(X)) 1123.48/297.13 , U53^#(ok(X)) -> c_93(U53^#(X)) 1123.48/297.13 , U62^#(mark(X1), X2) -> c_96(U62^#(X1, X2)) 1123.48/297.13 , U62^#(ok(X1), ok(X2)) -> c_97(U62^#(X1, X2)) 1123.48/297.13 , U63^#(mark(X)) -> c_98(U63^#(X)) 1123.48/297.13 , U63^#(ok(X)) -> c_99(U63^#(X)) 1123.48/297.13 , U71^#(mark(X1), X2) -> c_100(U71^#(X1, X2)) 1123.48/297.13 , U71^#(ok(X1), ok(X2)) -> c_101(U71^#(X1, X2)) 1123.48/297.13 , s^#(mark(X)) -> c_102(s^#(X)) 1123.48/297.13 , s^#(ok(X)) -> c_103(s^#(X)) 1123.48/297.13 , length^#(mark(X)) -> c_104(length^#(X)) 1123.48/297.13 , length^#(ok(X)) -> c_105(length^#(X)) 1123.48/297.13 , U81^#(mark(X)) -> c_106(U81^#(X)) 1123.48/297.13 , U81^#(ok(X)) -> c_107(U81^#(X)) 1123.48/297.13 , U91^#(mark(X1), X2, X3, X4) -> c_108(U91^#(X1, X2, X3, X4)) 1123.48/297.13 , U91^#(ok(X1), ok(X2), ok(X3), ok(X4)) -> 1123.48/297.13 c_109(U91^#(X1, X2, X3, X4)) 1123.48/297.13 , take^#(X1, mark(X2)) -> c_110(take^#(X1, X2)) 1123.48/297.13 , take^#(mark(X1), X2) -> c_111(take^#(X1, X2)) 1123.48/297.13 , take^#(ok(X1), ok(X2)) -> c_112(take^#(X1, X2)) 1123.48/297.14 , and^#(mark(X1), X2) -> c_113(and^#(X1, X2)) 1123.48/297.14 , and^#(ok(X1), ok(X2)) -> c_114(and^#(X1, X2)) 1123.48/297.14 , isNatKind^#(ok(X)) -> c_116(isNatKind^#(X)) 1123.48/297.14 , isNatIListKind^#(ok(X)) -> c_115(isNatIListKind^#(X)) 1123.48/297.14 , isNatList^#(ok(X)) -> c_71(isNatList^#(X)) 1123.48/297.14 , isNat^#(ok(X)) -> c_76(isNat^#(X)) 1123.48/297.14 , isNatIList^#(ok(X)) -> c_87(isNatIList^#(X)) 1123.48/297.14 , top^#(mark(X)) -> c_149(top^#(proper(X))) 1123.48/297.14 , top^#(ok(X)) -> c_150(top^#(active(X))) } 1123.48/297.14 Strict Trs: 1123.48/297.14 { active(zeros()) -> mark(cons(0(), zeros())) 1123.48/297.14 , active(cons(X1, X2)) -> cons(active(X1), X2) 1123.48/297.14 , active(U11(X1, X2)) -> U11(active(X1), X2) 1123.48/297.14 , active(U11(tt(), V1)) -> mark(U12(isNatList(V1))) 1123.48/297.14 , active(U12(X)) -> U12(active(X)) 1123.48/297.14 , active(U12(tt())) -> mark(tt()) 1123.48/297.14 , active(isNatList(cons(V1, V2))) -> 1123.48/297.14 mark(U51(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.14 , active(isNatList(nil())) -> mark(tt()) 1123.48/297.14 , active(isNatList(take(V1, V2))) -> 1123.48/297.14 mark(U61(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.14 , active(U21(X1, X2)) -> U21(active(X1), X2) 1123.48/297.14 , active(U21(tt(), V1)) -> mark(U22(isNat(V1))) 1123.48/297.14 , active(U22(X)) -> U22(active(X)) 1123.48/297.14 , active(U22(tt())) -> mark(tt()) 1123.48/297.14 , active(isNat(0())) -> mark(tt()) 1123.48/297.14 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 1123.48/297.14 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 1123.48/297.14 , active(U31(X1, X2)) -> U31(active(X1), X2) 1123.48/297.14 , active(U31(tt(), V)) -> mark(U32(isNatList(V))) 1123.48/297.14 , active(U32(X)) -> U32(active(X)) 1123.48/297.14 , active(U32(tt())) -> mark(tt()) 1123.48/297.14 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 1123.48/297.14 , active(U41(tt(), V1, V2)) -> mark(U42(isNat(V1), V2)) 1123.48/297.14 , active(U42(X1, X2)) -> U42(active(X1), X2) 1123.48/297.14 , active(U42(tt(), V2)) -> mark(U43(isNatIList(V2))) 1123.48/297.14 , active(U43(X)) -> U43(active(X)) 1123.48/297.14 , active(U43(tt())) -> mark(tt()) 1123.48/297.14 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 1123.48/297.14 , active(isNatIList(zeros())) -> mark(tt()) 1123.48/297.14 , active(isNatIList(cons(V1, V2))) -> 1123.48/297.14 mark(U41(and(isNatKind(V1), isNatIListKind(V2)), V1, V2)) 1123.48/297.14 , active(U51(X1, X2, X3)) -> U51(active(X1), X2, X3) 1123.48/297.14 , active(U51(tt(), V1, V2)) -> mark(U52(isNat(V1), V2)) 1123.48/297.14 , active(U52(X1, X2)) -> U52(active(X1), X2) 1123.48/297.14 , active(U52(tt(), V2)) -> mark(U53(isNatList(V2))) 1123.48/297.14 , active(U53(X)) -> U53(active(X)) 1123.48/297.14 , active(U53(tt())) -> mark(tt()) 1123.48/297.14 , active(U61(X1, X2, X3)) -> U61(active(X1), X2, X3) 1123.48/297.14 , active(U61(tt(), V1, V2)) -> mark(U62(isNat(V1), V2)) 1123.48/297.14 , active(U62(X1, X2)) -> U62(active(X1), X2) 1123.48/297.14 , active(U62(tt(), V2)) -> mark(U63(isNatIList(V2))) 1123.48/297.14 , active(U63(X)) -> U63(active(X)) 1123.48/297.14 , active(U63(tt())) -> mark(tt()) 1123.48/297.14 , active(U71(X1, X2)) -> U71(active(X1), X2) 1123.48/297.14 , active(U71(tt(), L)) -> mark(s(length(L))) 1123.48/297.14 , active(s(X)) -> s(active(X)) 1123.48/297.14 , active(length(X)) -> length(active(X)) 1123.48/297.14 , active(length(cons(N, L))) -> 1123.48/297.14 mark(U71(and(and(isNatList(L), isNatIListKind(L)), 1123.48/297.14 and(isNat(N), isNatKind(N))), 1123.48/297.14 L)) 1123.48/297.14 , active(length(nil())) -> mark(0()) 1123.48/297.14 , active(U81(X)) -> U81(active(X)) 1123.48/297.14 , active(U81(tt())) -> mark(nil()) 1123.48/297.14 , active(U91(X1, X2, X3, X4)) -> U91(active(X1), X2, X3, X4) 1123.48/297.14 , active(U91(tt(), IL, M, N)) -> mark(cons(N, take(M, IL))) 1123.48/297.14 , active(take(X1, X2)) -> take(X1, active(X2)) 1123.48/297.14 , active(take(X1, X2)) -> take(active(X1), X2) 1123.48/297.14 , active(take(0(), IL)) -> 1123.48/297.14 mark(U81(and(isNatIList(IL), isNatIListKind(IL)))) 1123.48/297.14 , active(take(s(M), cons(N, IL))) -> 1123.48/297.14 mark(U91(and(and(isNatIList(IL), isNatIListKind(IL)), 1123.48/297.14 and(and(isNat(M), isNatKind(M)), and(isNat(N), isNatKind(N)))), 1123.48/297.14 IL, 1123.48/297.14 M, 1123.48/297.14 N)) 1123.48/297.14 , active(and(X1, X2)) -> and(active(X1), X2) 1123.48/297.14 , active(and(tt(), X)) -> mark(X) 1123.48/297.14 , active(isNatIListKind(zeros())) -> mark(tt()) 1123.48/297.14 , active(isNatIListKind(cons(V1, V2))) -> 1123.48/297.14 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.48/297.14 , active(isNatIListKind(nil())) -> mark(tt()) 1123.48/297.14 , active(isNatIListKind(take(V1, V2))) -> 1123.48/297.14 mark(and(isNatKind(V1), isNatIListKind(V2))) 1123.48/297.14 , active(isNatKind(0())) -> mark(tt()) 1123.48/297.14 , active(isNatKind(s(V1))) -> mark(isNatKind(V1)) 1123.48/297.14 , active(isNatKind(length(V1))) -> mark(isNatIListKind(V1)) 1123.48/297.14 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 1123.48/297.14 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 1123.48/297.14 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 1123.48/297.14 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 1123.48/297.14 , U12(mark(X)) -> mark(U12(X)) 1123.48/297.14 , U12(ok(X)) -> ok(U12(X)) 1123.48/297.14 , isNatList(ok(X)) -> ok(isNatList(X)) 1123.48/297.14 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 1123.48/297.14 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 1123.48/297.14 , U22(mark(X)) -> mark(U22(X)) 1123.48/297.14 , U22(ok(X)) -> ok(U22(X)) 1123.48/297.14 , isNat(ok(X)) -> ok(isNat(X)) 1123.48/297.14 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 1123.48/297.14 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 1123.48/297.14 , U32(mark(X)) -> mark(U32(X)) 1123.48/297.14 , U32(ok(X)) -> ok(U32(X)) 1123.48/297.14 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 1123.48/297.14 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 1123.48/297.14 , U42(mark(X1), X2) -> mark(U42(X1, X2)) 1123.48/297.14 , U42(ok(X1), ok(X2)) -> ok(U42(X1, X2)) 1123.48/297.14 , U43(mark(X)) -> mark(U43(X)) 1123.48/297.14 , U43(ok(X)) -> ok(U43(X)) 1123.48/297.14 , isNatIList(ok(X)) -> ok(isNatIList(X)) 1123.48/297.14 , U51(mark(X1), X2, X3) -> mark(U51(X1, X2, X3)) 1123.48/297.14 , U51(ok(X1), ok(X2), ok(X3)) -> ok(U51(X1, X2, X3)) 1123.48/297.14 , U52(mark(X1), X2) -> mark(U52(X1, X2)) 1123.48/297.14 , U52(ok(X1), ok(X2)) -> ok(U52(X1, X2)) 1123.48/297.14 , U53(mark(X)) -> mark(U53(X)) 1123.48/297.14 , U53(ok(X)) -> ok(U53(X)) 1123.48/297.14 , U61(mark(X1), X2, X3) -> mark(U61(X1, X2, X3)) 1123.48/297.14 , U61(ok(X1), ok(X2), ok(X3)) -> ok(U61(X1, X2, X3)) 1123.48/297.14 , U62(mark(X1), X2) -> mark(U62(X1, X2)) 1123.48/297.14 , U62(ok(X1), ok(X2)) -> ok(U62(X1, X2)) 1123.48/297.14 , U63(mark(X)) -> mark(U63(X)) 1123.48/297.14 , U63(ok(X)) -> ok(U63(X)) 1123.48/297.14 , U71(mark(X1), X2) -> mark(U71(X1, X2)) 1123.48/297.14 , U71(ok(X1), ok(X2)) -> ok(U71(X1, X2)) 1123.48/297.14 , s(mark(X)) -> mark(s(X)) 1123.48/297.14 , s(ok(X)) -> ok(s(X)) 1123.48/297.14 , length(mark(X)) -> mark(length(X)) 1123.48/297.14 , length(ok(X)) -> ok(length(X)) 1123.48/297.14 , U81(mark(X)) -> mark(U81(X)) 1123.48/297.14 , U81(ok(X)) -> ok(U81(X)) 1123.48/297.14 , U91(mark(X1), X2, X3, X4) -> mark(U91(X1, X2, X3, X4)) 1123.48/297.14 , U91(ok(X1), ok(X2), ok(X3), ok(X4)) -> ok(U91(X1, X2, X3, X4)) 1123.48/297.14 , take(X1, mark(X2)) -> mark(take(X1, X2)) 1123.48/297.14 , take(mark(X1), X2) -> mark(take(X1, X2)) 1123.48/297.14 , take(ok(X1), ok(X2)) -> ok(take(X1, X2)) 1123.48/297.14 , and(mark(X1), X2) -> mark(and(X1, X2)) 1123.48/297.14 , and(ok(X1), ok(X2)) -> ok(and(X1, X2)) 1123.48/297.14 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 1123.48/297.14 , isNatKind(ok(X)) -> ok(isNatKind(X)) 1123.48/297.14 , proper(zeros()) -> ok(zeros()) 1123.48/297.14 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 1123.48/297.14 , proper(0()) -> ok(0()) 1123.48/297.14 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 1123.48/297.14 , proper(tt()) -> ok(tt()) 1123.48/297.14 , proper(U12(X)) -> U12(proper(X)) 1123.48/297.14 , proper(isNatList(X)) -> isNatList(proper(X)) 1123.48/297.14 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 1123.48/297.14 , proper(U22(X)) -> U22(proper(X)) 1123.48/297.14 , proper(isNat(X)) -> isNat(proper(X)) 1123.48/297.14 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 1123.48/297.14 , proper(U32(X)) -> U32(proper(X)) 1123.48/297.14 , proper(U41(X1, X2, X3)) -> 1123.48/297.14 U41(proper(X1), proper(X2), proper(X3)) 1123.48/297.14 , proper(U42(X1, X2)) -> U42(proper(X1), proper(X2)) 1123.48/297.14 , proper(U43(X)) -> U43(proper(X)) 1123.48/297.14 , proper(isNatIList(X)) -> isNatIList(proper(X)) 1123.48/297.14 , proper(U51(X1, X2, X3)) -> 1123.48/297.14 U51(proper(X1), proper(X2), proper(X3)) 1123.48/297.14 , proper(U52(X1, X2)) -> U52(proper(X1), proper(X2)) 1123.48/297.14 , proper(U53(X)) -> U53(proper(X)) 1123.48/297.14 , proper(U61(X1, X2, X3)) -> 1123.48/297.14 U61(proper(X1), proper(X2), proper(X3)) 1123.48/297.14 , proper(U62(X1, X2)) -> U62(proper(X1), proper(X2)) 1123.48/297.14 , proper(U63(X)) -> U63(proper(X)) 1123.48/297.14 , proper(U71(X1, X2)) -> U71(proper(X1), proper(X2)) 1123.48/297.14 , proper(s(X)) -> s(proper(X)) 1123.48/297.14 , proper(length(X)) -> length(proper(X)) 1123.48/297.14 , proper(U81(X)) -> U81(proper(X)) 1123.48/297.14 , proper(nil()) -> ok(nil()) 1123.48/297.14 , proper(U91(X1, X2, X3, X4)) -> 1123.48/297.14 U91(proper(X1), proper(X2), proper(X3), proper(X4)) 1123.48/297.14 , proper(take(X1, X2)) -> take(proper(X1), proper(X2)) 1123.48/297.14 , proper(and(X1, X2)) -> and(proper(X1), proper(X2)) 1123.48/297.14 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 1123.48/297.14 , proper(isNatKind(X)) -> isNatKind(proper(X)) 1123.48/297.14 , top(mark(X)) -> top(proper(X)) 1123.48/297.14 , top(ok(X)) -> top(active(X)) } 1123.48/297.14 Weak DPs: 1123.48/297.14 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 1123.48/297.14 , proper^#(zeros()) -> c_117() 1123.48/297.14 , proper^#(0()) -> c_119() 1123.48/297.14 , proper^#(tt()) -> c_121() 1123.48/297.14 , proper^#(nil()) -> c_143() } 1123.48/297.14 Obligation: 1123.48/297.14 runtime complexity 1123.48/297.14 Answer: 1123.48/297.14 MAYBE 1123.48/297.14 1123.48/297.14 Empty strict component of the problem is NOT empty. 1123.48/297.14 1123.48/297.14 1123.48/297.14 Arrrr.. 1123.93/297.59 EOF