MAYBE 840.00/297.13 MAYBE 840.00/297.13 840.00/297.13 We are left with following problem, upon which TcT provides the 840.00/297.13 certificate MAYBE. 840.00/297.13 840.00/297.13 Strict Trs: 840.00/297.13 { active(zeros()) -> mark(cons(0(), zeros())) 840.00/297.13 , active(cons(X1, X2)) -> cons(active(X1), X2) 840.00/297.13 , active(U11(X1, X2)) -> U11(active(X1), X2) 840.00/297.13 , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) 840.00/297.13 , active(U12(X1, X2)) -> U12(active(X1), X2) 840.00/297.13 , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) 840.00/297.13 , active(isNatIListKind(zeros())) -> mark(tt()) 840.00/297.13 , active(isNatIListKind(cons(V1, V2))) -> 840.00/297.13 mark(U51(isNatKind(V1), V2)) 840.00/297.13 , active(isNatIListKind(nil())) -> mark(tt()) 840.00/297.13 , active(U13(X)) -> U13(active(X)) 840.00/297.13 , active(U13(tt())) -> mark(tt()) 840.00/297.13 , active(isNatList(cons(V1, V2))) -> 840.00/297.13 mark(U81(isNatKind(V1), V1, V2)) 840.00/297.13 , active(isNatList(nil())) -> mark(tt()) 840.00/297.13 , active(U21(X1, X2)) -> U21(active(X1), X2) 840.00/297.13 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 840.00/297.13 , active(U22(X1, X2)) -> U22(active(X1), X2) 840.00/297.13 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 840.00/297.13 , active(isNatKind(0())) -> mark(tt()) 840.00/297.13 , active(isNatKind(s(V1))) -> mark(U71(isNatKind(V1))) 840.00/297.13 , active(isNatKind(length(V1))) -> mark(U61(isNatIListKind(V1))) 840.00/297.13 , active(U23(X)) -> U23(active(X)) 840.00/297.13 , active(U23(tt())) -> mark(tt()) 840.00/297.13 , active(isNat(0())) -> mark(tt()) 840.00/297.13 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 840.00/297.13 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 840.00/297.13 , active(U31(X1, X2)) -> U31(active(X1), X2) 840.00/297.13 , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) 840.00/297.13 , active(U32(X1, X2)) -> U32(active(X1), X2) 840.00/297.13 , active(U32(tt(), V)) -> mark(U33(isNatList(V))) 840.00/297.13 , active(U33(X)) -> U33(active(X)) 840.00/297.13 , active(U33(tt())) -> mark(tt()) 840.00/297.13 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 840.00/297.13 , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) 840.00/297.13 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 840.00/297.13 , active(U42(tt(), V1, V2)) -> 840.00/297.13 mark(U43(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) 840.00/297.13 , active(U43(tt(), V1, V2)) -> 840.00/297.13 mark(U44(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) 840.00/297.13 , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) 840.00/297.13 , active(U45(X1, X2)) -> U45(active(X1), X2) 840.00/297.13 , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) 840.00/297.13 , active(U46(X)) -> U46(active(X)) 840.00/297.13 , active(U46(tt())) -> mark(tt()) 840.00/297.13 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 840.00/297.13 , active(isNatIList(zeros())) -> mark(tt()) 840.00/297.13 , active(isNatIList(cons(V1, V2))) -> 840.00/297.13 mark(U41(isNatKind(V1), V1, V2)) 840.00/297.13 , active(U51(X1, X2)) -> U51(active(X1), X2) 840.00/297.13 , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) 840.00/297.13 , active(U52(X)) -> U52(active(X)) 840.00/297.13 , active(U52(tt())) -> mark(tt()) 840.00/297.13 , active(U61(X)) -> U61(active(X)) 840.00/297.13 , active(U61(tt())) -> mark(tt()) 840.00/297.13 , active(U71(X)) -> U71(active(X)) 840.00/297.13 , active(U71(tt())) -> mark(tt()) 840.00/297.13 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 840.00/297.13 , active(U81(tt(), V1, V2)) -> mark(U82(isNatKind(V1), V1, V2)) 840.00/297.13 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 840.00/297.13 , active(U82(tt(), V1, V2)) -> 840.00/297.13 mark(U83(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 840.00/297.13 , active(U83(tt(), V1, V2)) -> 840.00/297.13 mark(U84(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 840.00/297.13 , active(U84(tt(), V1, V2)) -> mark(U85(isNat(V1), V2)) 840.00/297.13 , active(U85(X1, X2)) -> U85(active(X1), X2) 840.00/297.13 , active(U85(tt(), V2)) -> mark(U86(isNatList(V2))) 840.00/297.13 , active(U86(X)) -> U86(active(X)) 840.00/297.13 , active(U86(tt())) -> mark(tt()) 840.00/297.13 , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) 840.00/297.13 , active(U91(tt(), L, N)) -> mark(U92(isNatIListKind(L), L, N)) 840.00/297.13 , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) 840.00/297.13 , active(U92(tt(), L, N)) -> mark(U93(isNat(N), L, N)) 840.00/297.13 , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) 840.00/297.13 , active(U93(tt(), L, N)) -> mark(U94(isNatKind(N), L)) 840.00/297.13 , active(U94(X1, X2)) -> U94(active(X1), X2) 840.00/297.13 , active(U94(tt(), L)) -> mark(s(length(L))) 840.00/297.13 , active(s(X)) -> s(active(X)) 840.00/297.13 , active(length(X)) -> length(active(X)) 840.00/297.13 , active(length(cons(N, L))) -> mark(U91(isNatList(L), L, N)) 840.00/297.13 , active(length(nil())) -> mark(0()) 840.00/297.13 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 840.00/297.13 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 840.00/297.13 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 840.00/297.13 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 840.00/297.13 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 840.00/297.13 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 840.00/297.13 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 840.00/297.13 , U13(mark(X)) -> mark(U13(X)) 840.00/297.13 , U13(ok(X)) -> ok(U13(X)) 840.00/297.13 , isNatList(ok(X)) -> ok(isNatList(X)) 840.00/297.13 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 840.00/297.13 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 840.00/297.13 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 840.00/297.13 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 840.00/297.13 , isNatKind(ok(X)) -> ok(isNatKind(X)) 840.00/297.13 , U23(mark(X)) -> mark(U23(X)) 840.00/297.13 , U23(ok(X)) -> ok(U23(X)) 840.00/297.13 , isNat(ok(X)) -> ok(isNat(X)) 840.00/297.13 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 840.00/297.13 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 840.00/297.13 , U32(mark(X1), X2) -> mark(U32(X1, X2)) 840.00/297.13 , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) 840.00/297.13 , U33(mark(X)) -> mark(U33(X)) 840.00/297.13 , U33(ok(X)) -> ok(U33(X)) 840.00/297.13 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 840.00/297.13 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 840.00/297.13 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 840.00/297.13 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 840.00/297.13 , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) 840.00/297.13 , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) 840.00/297.13 , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) 840.00/297.13 , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) 840.00/297.13 , U45(mark(X1), X2) -> mark(U45(X1, X2)) 840.00/297.13 , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) 840.00/297.13 , U46(mark(X)) -> mark(U46(X)) 840.00/297.13 , U46(ok(X)) -> ok(U46(X)) 840.00/297.13 , isNatIList(ok(X)) -> ok(isNatIList(X)) 840.00/297.13 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 840.00/297.13 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 840.00/297.13 , U52(mark(X)) -> mark(U52(X)) 840.00/297.13 , U52(ok(X)) -> ok(U52(X)) 840.00/297.13 , U61(mark(X)) -> mark(U61(X)) 840.00/297.13 , U61(ok(X)) -> ok(U61(X)) 840.00/297.13 , U71(mark(X)) -> mark(U71(X)) 840.00/297.13 , U71(ok(X)) -> ok(U71(X)) 840.00/297.13 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 840.00/297.13 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 840.00/297.13 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 840.00/297.13 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 840.00/297.13 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 840.00/297.13 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 840.00/297.13 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 840.00/297.13 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 840.00/297.13 , U85(mark(X1), X2) -> mark(U85(X1, X2)) 840.00/297.13 , U85(ok(X1), ok(X2)) -> ok(U85(X1, X2)) 840.00/297.13 , U86(mark(X)) -> mark(U86(X)) 840.00/297.13 , U86(ok(X)) -> ok(U86(X)) 840.00/297.13 , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) 840.00/297.13 , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) 840.00/297.13 , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) 840.00/297.13 , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) 840.00/297.13 , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) 840.00/297.13 , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) 840.00/297.13 , U94(mark(X1), X2) -> mark(U94(X1, X2)) 840.00/297.13 , U94(ok(X1), ok(X2)) -> ok(U94(X1, X2)) 840.00/297.13 , s(mark(X)) -> mark(s(X)) 840.00/297.13 , s(ok(X)) -> ok(s(X)) 840.00/297.13 , length(mark(X)) -> mark(length(X)) 840.00/297.13 , length(ok(X)) -> ok(length(X)) 840.00/297.13 , proper(zeros()) -> ok(zeros()) 840.00/297.13 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 840.00/297.13 , proper(0()) -> ok(0()) 840.00/297.13 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 840.00/297.13 , proper(tt()) -> ok(tt()) 840.00/297.13 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 840.00/297.13 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 840.00/297.13 , proper(U13(X)) -> U13(proper(X)) 840.00/297.13 , proper(isNatList(X)) -> isNatList(proper(X)) 840.00/297.13 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 840.00/297.13 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 840.00/297.13 , proper(isNatKind(X)) -> isNatKind(proper(X)) 840.00/297.13 , proper(U23(X)) -> U23(proper(X)) 840.00/297.13 , proper(isNat(X)) -> isNat(proper(X)) 840.00/297.13 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 840.00/297.13 , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) 840.00/297.13 , proper(U33(X)) -> U33(proper(X)) 840.00/297.13 , proper(U41(X1, X2, X3)) -> 840.00/297.13 U41(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U42(X1, X2, X3)) -> 840.00/297.13 U42(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U43(X1, X2, X3)) -> 840.00/297.13 U43(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U44(X1, X2, X3)) -> 840.00/297.13 U44(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) 840.00/297.13 , proper(U46(X)) -> U46(proper(X)) 840.00/297.13 , proper(isNatIList(X)) -> isNatIList(proper(X)) 840.00/297.13 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 840.00/297.13 , proper(U52(X)) -> U52(proper(X)) 840.00/297.13 , proper(U61(X)) -> U61(proper(X)) 840.00/297.13 , proper(U71(X)) -> U71(proper(X)) 840.00/297.13 , proper(U81(X1, X2, X3)) -> 840.00/297.13 U81(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U82(X1, X2, X3)) -> 840.00/297.13 U82(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U83(X1, X2, X3)) -> 840.00/297.13 U83(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U84(X1, X2, X3)) -> 840.00/297.13 U84(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U85(X1, X2)) -> U85(proper(X1), proper(X2)) 840.00/297.13 , proper(U86(X)) -> U86(proper(X)) 840.00/297.13 , proper(U91(X1, X2, X3)) -> 840.00/297.13 U91(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U92(X1, X2, X3)) -> 840.00/297.13 U92(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U93(X1, X2, X3)) -> 840.00/297.13 U93(proper(X1), proper(X2), proper(X3)) 840.00/297.13 , proper(U94(X1, X2)) -> U94(proper(X1), proper(X2)) 840.00/297.13 , proper(s(X)) -> s(proper(X)) 840.00/297.13 , proper(length(X)) -> length(proper(X)) 840.00/297.13 , proper(nil()) -> ok(nil()) 840.00/297.13 , top(mark(X)) -> top(proper(X)) 840.00/297.13 , top(ok(X)) -> top(active(X)) } 840.00/297.13 Obligation: 840.00/297.13 runtime complexity 840.00/297.13 Answer: 840.00/297.13 MAYBE 840.00/297.13 840.00/297.13 None of the processors succeeded. 840.00/297.13 840.00/297.13 Details of failed attempt(s): 840.00/297.13 ----------------------------- 840.00/297.13 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 840.00/297.13 following reason: 840.00/297.13 840.00/297.13 Computation stopped due to timeout after 297.0 seconds. 840.00/297.13 840.00/297.13 2) 'Best' failed due to the following reason: 840.00/297.13 840.00/297.13 None of the processors succeeded. 840.00/297.13 840.00/297.13 Details of failed attempt(s): 840.00/297.13 ----------------------------- 840.00/297.13 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 840.00/297.13 seconds)' failed due to the following reason: 840.00/297.13 840.00/297.13 Computation stopped due to timeout after 148.0 seconds. 840.00/297.13 840.00/297.13 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 840.00/297.13 failed due to the following reason: 840.00/297.13 840.00/297.13 None of the processors succeeded. 840.00/297.13 840.00/297.13 Details of failed attempt(s): 840.00/297.13 ----------------------------- 840.00/297.13 1) 'Bounds with minimal-enrichment and initial automaton 'match'' 840.00/297.13 failed due to the following reason: 840.00/297.13 840.00/297.13 match-boundness of the problem could not be verified. 840.00/297.13 840.00/297.13 2) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 840.00/297.13 failed due to the following reason: 840.00/297.13 840.00/297.13 match-boundness of the problem could not be verified. 840.00/297.13 840.00/297.13 840.00/297.13 3) 'Best' failed due to the following reason: 840.00/297.13 840.00/297.13 None of the processors succeeded. 840.00/297.13 840.00/297.13 Details of failed attempt(s): 840.00/297.13 ----------------------------- 840.00/297.13 1) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 840.00/297.13 following reason: 840.00/297.13 840.00/297.13 The processor is inapplicable, reason: 840.00/297.13 Processor only applicable for innermost runtime complexity analysis 840.00/297.13 840.00/297.13 2) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 840.00/297.13 to the following reason: 840.00/297.13 840.00/297.13 The processor is inapplicable, reason: 840.00/297.13 Processor only applicable for innermost runtime complexity analysis 840.00/297.13 840.00/297.13 840.00/297.13 840.00/297.13 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 840.00/297.13 the following reason: 840.00/297.13 840.00/297.13 We add the following weak dependency pairs: 840.00/297.13 840.00/297.13 Strict DPs: 840.00/297.13 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 840.00/297.13 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 840.00/297.13 , active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 840.00/297.13 , active^#(U11(tt(), V1)) -> c_4(U12^#(isNatIListKind(V1), V1)) 840.00/297.13 , active^#(U12(X1, X2)) -> c_5(U12^#(active(X1), X2)) 840.00/297.13 , active^#(U12(tt(), V1)) -> c_6(U13^#(isNatList(V1))) 840.00/297.13 , active^#(isNatIListKind(zeros())) -> c_7() 840.00/297.13 , active^#(isNatIListKind(cons(V1, V2))) -> 840.00/297.13 c_8(U51^#(isNatKind(V1), V2)) 840.00/297.13 , active^#(isNatIListKind(nil())) -> c_9() 840.00/297.13 , active^#(U13(X)) -> c_10(U13^#(active(X))) 840.00/297.13 , active^#(U13(tt())) -> c_11() 840.00/297.13 , active^#(isNatList(cons(V1, V2))) -> 840.00/297.13 c_12(U81^#(isNatKind(V1), V1, V2)) 840.00/297.13 , active^#(isNatList(nil())) -> c_13() 840.00/297.13 , active^#(U21(X1, X2)) -> c_14(U21^#(active(X1), X2)) 840.00/297.13 , active^#(U21(tt(), V1)) -> c_15(U22^#(isNatKind(V1), V1)) 840.00/297.13 , active^#(U22(X1, X2)) -> c_16(U22^#(active(X1), X2)) 840.00/297.13 , active^#(U22(tt(), V1)) -> c_17(U23^#(isNat(V1))) 840.00/297.13 , active^#(isNatKind(0())) -> c_18() 840.00/297.13 , active^#(isNatKind(s(V1))) -> c_19(U71^#(isNatKind(V1))) 840.00/297.13 , active^#(isNatKind(length(V1))) -> 840.00/297.13 c_20(U61^#(isNatIListKind(V1))) 840.00/297.13 , active^#(U23(X)) -> c_21(U23^#(active(X))) 840.00/297.13 , active^#(U23(tt())) -> c_22() 840.00/297.13 , active^#(isNat(0())) -> c_23() 840.00/297.13 , active^#(isNat(s(V1))) -> c_24(U21^#(isNatKind(V1), V1)) 840.00/297.13 , active^#(isNat(length(V1))) -> 840.00/297.13 c_25(U11^#(isNatIListKind(V1), V1)) 840.00/297.13 , active^#(U31(X1, X2)) -> c_26(U31^#(active(X1), X2)) 840.00/297.13 , active^#(U31(tt(), V)) -> c_27(U32^#(isNatIListKind(V), V)) 840.00/297.13 , active^#(U32(X1, X2)) -> c_28(U32^#(active(X1), X2)) 840.00/297.13 , active^#(U32(tt(), V)) -> c_29(U33^#(isNatList(V))) 840.00/297.13 , active^#(U33(X)) -> c_30(U33^#(active(X))) 840.00/297.13 , active^#(U33(tt())) -> c_31() 840.00/297.13 , active^#(U41(X1, X2, X3)) -> c_32(U41^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U41(tt(), V1, V2)) -> c_33(U42^#(isNatKind(V1), V1, V2)) 840.00/297.13 , active^#(U42(X1, X2, X3)) -> c_34(U42^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U42(tt(), V1, V2)) -> 840.00/297.13 c_35(U43^#(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active^#(U43(X1, X2, X3)) -> c_36(U43^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U43(tt(), V1, V2)) -> 840.00/297.13 c_37(U44^#(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active^#(U44(X1, X2, X3)) -> c_38(U44^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U44(tt(), V1, V2)) -> c_39(U45^#(isNat(V1), V2)) 840.00/297.13 , active^#(U45(X1, X2)) -> c_40(U45^#(active(X1), X2)) 840.00/297.13 , active^#(U45(tt(), V2)) -> c_41(U46^#(isNatIList(V2))) 840.00/297.13 , active^#(U46(X)) -> c_42(U46^#(active(X))) 840.00/297.13 , active^#(U46(tt())) -> c_43() 840.00/297.13 , active^#(isNatIList(V)) -> c_44(U31^#(isNatIListKind(V), V)) 840.00/297.13 , active^#(isNatIList(zeros())) -> c_45() 840.00/297.13 , active^#(isNatIList(cons(V1, V2))) -> 840.00/297.13 c_46(U41^#(isNatKind(V1), V1, V2)) 840.00/297.13 , active^#(U51(X1, X2)) -> c_47(U51^#(active(X1), X2)) 840.00/297.13 , active^#(U51(tt(), V2)) -> c_48(U52^#(isNatIListKind(V2))) 840.00/297.13 , active^#(U52(X)) -> c_49(U52^#(active(X))) 840.00/297.13 , active^#(U52(tt())) -> c_50() 840.00/297.13 , active^#(U61(X)) -> c_51(U61^#(active(X))) 840.00/297.13 , active^#(U61(tt())) -> c_52() 840.00/297.13 , active^#(U71(X)) -> c_53(U71^#(active(X))) 840.00/297.13 , active^#(U71(tt())) -> c_54() 840.00/297.13 , active^#(U81(X1, X2, X3)) -> c_55(U81^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U81(tt(), V1, V2)) -> c_56(U82^#(isNatKind(V1), V1, V2)) 840.00/297.13 , active^#(U82(X1, X2, X3)) -> c_57(U82^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U82(tt(), V1, V2)) -> 840.00/297.13 c_58(U83^#(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active^#(U83(X1, X2, X3)) -> c_59(U83^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U83(tt(), V1, V2)) -> 840.00/297.13 c_60(U84^#(isNatIListKind(V2), V1, V2)) 840.00/297.13 , active^#(U84(X1, X2, X3)) -> c_61(U84^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U84(tt(), V1, V2)) -> c_62(U85^#(isNat(V1), V2)) 840.00/297.13 , active^#(U85(X1, X2)) -> c_63(U85^#(active(X1), X2)) 840.00/297.13 , active^#(U85(tt(), V2)) -> c_64(U86^#(isNatList(V2))) 840.00/297.13 , active^#(U86(X)) -> c_65(U86^#(active(X))) 840.00/297.13 , active^#(U86(tt())) -> c_66() 840.00/297.13 , active^#(U91(X1, X2, X3)) -> c_67(U91^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U91(tt(), L, N)) -> c_68(U92^#(isNatIListKind(L), L, N)) 840.00/297.13 , active^#(U92(X1, X2, X3)) -> c_69(U92^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U92(tt(), L, N)) -> c_70(U93^#(isNat(N), L, N)) 840.00/297.13 , active^#(U93(X1, X2, X3)) -> c_71(U93^#(active(X1), X2, X3)) 840.00/297.13 , active^#(U93(tt(), L, N)) -> c_72(U94^#(isNatKind(N), L)) 840.00/297.13 , active^#(U94(X1, X2)) -> c_73(U94^#(active(X1), X2)) 840.00/297.13 , active^#(U94(tt(), L)) -> c_74(s^#(length(L))) 840.00/297.13 , active^#(s(X)) -> c_75(s^#(active(X))) 840.00/297.13 , active^#(length(X)) -> c_76(length^#(active(X))) 840.00/297.13 , active^#(length(cons(N, L))) -> c_77(U91^#(isNatList(L), L, N)) 840.00/297.13 , active^#(length(nil())) -> c_78() 840.00/297.13 , cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) 840.00/297.13 , cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) 840.00/297.14 , U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) 840.00/297.14 , U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) 840.00/297.14 , U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) 840.00/297.14 , U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) 840.00/297.14 , U13^#(mark(X)) -> c_86(U13^#(X)) 840.00/297.14 , U13^#(ok(X)) -> c_87(U13^#(X)) 840.00/297.14 , U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) 840.00/297.14 , U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) 840.00/297.14 , U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) 840.00/297.14 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) 840.00/297.14 , U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) 840.00/297.14 , U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) 840.00/297.14 , U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) 840.00/297.14 , U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) 840.00/297.14 , U23^#(mark(X)) -> c_94(U23^#(X)) 840.00/297.14 , U23^#(ok(X)) -> c_95(U23^#(X)) 840.00/297.14 , U71^#(mark(X)) -> c_122(U71^#(X)) 840.00/297.14 , U71^#(ok(X)) -> c_123(U71^#(X)) 840.00/297.14 , U61^#(mark(X)) -> c_120(U61^#(X)) 840.00/297.14 , U61^#(ok(X)) -> c_121(U61^#(X)) 840.00/297.14 , U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) 840.00/297.14 , U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) 840.00/297.14 , U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) 840.00/297.14 , U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) 840.00/297.14 , U33^#(mark(X)) -> c_101(U33^#(X)) 840.00/297.14 , U33^#(ok(X)) -> c_102(U33^#(X)) 840.00/297.14 , U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) 840.00/297.14 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_104(U41^#(X1, X2, X3)) 840.00/297.14 , U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) 840.00/297.14 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_106(U42^#(X1, X2, X3)) 840.00/297.14 , U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) 840.00/297.14 , U43^#(ok(X1), ok(X2), ok(X3)) -> c_108(U43^#(X1, X2, X3)) 840.00/297.14 , U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) 840.00/297.14 , U44^#(ok(X1), ok(X2), ok(X3)) -> c_110(U44^#(X1, X2, X3)) 840.00/297.14 , U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) 840.00/297.14 , U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) 840.00/297.14 , U46^#(mark(X)) -> c_113(U46^#(X)) 840.00/297.14 , U46^#(ok(X)) -> c_114(U46^#(X)) 840.00/297.14 , U52^#(mark(X)) -> c_118(U52^#(X)) 840.00/297.14 , U52^#(ok(X)) -> c_119(U52^#(X)) 840.00/297.14 , U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) 840.00/297.14 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_127(U82^#(X1, X2, X3)) 840.00/297.14 , U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) 840.00/297.14 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_129(U83^#(X1, X2, X3)) 840.00/297.14 , U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) 840.00/297.14 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_131(U84^#(X1, X2, X3)) 840.00/297.14 , U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) 840.00/297.14 , U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) 840.00/297.14 , U86^#(mark(X)) -> c_134(U86^#(X)) 840.00/297.14 , U86^#(ok(X)) -> c_135(U86^#(X)) 840.00/297.14 , U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) 840.00/297.14 , U91^#(ok(X1), ok(X2), ok(X3)) -> c_137(U91^#(X1, X2, X3)) 840.00/297.14 , U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) 840.00/297.14 , U92^#(ok(X1), ok(X2), ok(X3)) -> c_139(U92^#(X1, X2, X3)) 840.00/297.14 , U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) 840.00/297.14 , U93^#(ok(X1), ok(X2), ok(X3)) -> c_141(U93^#(X1, X2, X3)) 840.00/297.14 , U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) 840.00/297.14 , U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) 840.00/297.14 , s^#(mark(X)) -> c_144(s^#(X)) 840.00/297.14 , s^#(ok(X)) -> c_145(s^#(X)) 840.00/297.14 , length^#(mark(X)) -> c_146(length^#(X)) 840.00/297.14 , length^#(ok(X)) -> c_147(length^#(X)) 840.00/297.14 , isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) 840.00/297.14 , isNatList^#(ok(X)) -> c_88(isNatList^#(X)) 840.00/297.14 , isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) 840.00/297.14 , isNat^#(ok(X)) -> c_96(isNat^#(X)) 840.00/297.14 , isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) 840.00/297.14 , proper^#(zeros()) -> c_148() 840.00/297.14 , proper^#(cons(X1, X2)) -> c_149(cons^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(0()) -> c_150() 840.00/297.14 , proper^#(U11(X1, X2)) -> c_151(U11^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(tt()) -> c_152() 840.00/297.14 , proper^#(U12(X1, X2)) -> c_153(U12^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(isNatIListKind(X)) -> c_154(isNatIListKind^#(proper(X))) 840.00/297.14 , proper^#(U13(X)) -> c_155(U13^#(proper(X))) 840.00/297.14 , proper^#(isNatList(X)) -> c_156(isNatList^#(proper(X))) 840.00/297.14 , proper^#(U21(X1, X2)) -> c_157(U21^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U22(X1, X2)) -> c_158(U22^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) 840.00/297.14 , proper^#(U23(X)) -> c_160(U23^#(proper(X))) 840.00/297.14 , proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) 840.00/297.14 , proper^#(U31(X1, X2)) -> c_162(U31^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U32(X1, X2)) -> c_163(U32^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U33(X)) -> c_164(U33^#(proper(X))) 840.00/297.14 , proper^#(U41(X1, X2, X3)) -> 840.00/297.14 c_165(U41^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U42(X1, X2, X3)) -> 840.00/297.14 c_166(U42^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U43(X1, X2, X3)) -> 840.00/297.14 c_167(U43^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U44(X1, X2, X3)) -> 840.00/297.14 c_168(U44^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U45(X1, X2)) -> c_169(U45^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U46(X)) -> c_170(U46^#(proper(X))) 840.00/297.14 , proper^#(isNatIList(X)) -> c_171(isNatIList^#(proper(X))) 840.00/297.14 , proper^#(U51(X1, X2)) -> c_172(U51^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U52(X)) -> c_173(U52^#(proper(X))) 840.00/297.14 , proper^#(U61(X)) -> c_174(U61^#(proper(X))) 840.00/297.14 , proper^#(U71(X)) -> c_175(U71^#(proper(X))) 840.00/297.14 , proper^#(U81(X1, X2, X3)) -> 840.00/297.14 c_176(U81^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U82(X1, X2, X3)) -> 840.00/297.14 c_177(U82^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U83(X1, X2, X3)) -> 840.00/297.14 c_178(U83^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U84(X1, X2, X3)) -> 840.00/297.14 c_179(U84^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U85(X1, X2)) -> c_180(U85^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U86(X)) -> c_181(U86^#(proper(X))) 840.00/297.14 , proper^#(U91(X1, X2, X3)) -> 840.00/297.14 c_182(U91^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U92(X1, X2, X3)) -> 840.00/297.14 c_183(U92^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U93(X1, X2, X3)) -> 840.00/297.14 c_184(U93^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U94(X1, X2)) -> c_185(U94^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(s(X)) -> c_186(s^#(proper(X))) 840.00/297.14 , proper^#(length(X)) -> c_187(length^#(proper(X))) 840.00/297.14 , proper^#(nil()) -> c_188() 840.00/297.14 , top^#(mark(X)) -> c_189(top^#(proper(X))) 840.00/297.14 , top^#(ok(X)) -> c_190(top^#(active(X))) } 840.00/297.14 840.00/297.14 and mark the set of starting terms. 840.00/297.14 840.00/297.14 We are left with following problem, upon which TcT provides the 840.00/297.14 certificate MAYBE. 840.00/297.14 840.00/297.14 Strict DPs: 840.00/297.14 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 840.00/297.14 , active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 840.00/297.14 , active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 840.00/297.14 , active^#(U11(tt(), V1)) -> c_4(U12^#(isNatIListKind(V1), V1)) 840.00/297.14 , active^#(U12(X1, X2)) -> c_5(U12^#(active(X1), X2)) 840.00/297.14 , active^#(U12(tt(), V1)) -> c_6(U13^#(isNatList(V1))) 840.00/297.14 , active^#(isNatIListKind(zeros())) -> c_7() 840.00/297.14 , active^#(isNatIListKind(cons(V1, V2))) -> 840.00/297.14 c_8(U51^#(isNatKind(V1), V2)) 840.00/297.14 , active^#(isNatIListKind(nil())) -> c_9() 840.00/297.14 , active^#(U13(X)) -> c_10(U13^#(active(X))) 840.00/297.14 , active^#(U13(tt())) -> c_11() 840.00/297.14 , active^#(isNatList(cons(V1, V2))) -> 840.00/297.14 c_12(U81^#(isNatKind(V1), V1, V2)) 840.00/297.14 , active^#(isNatList(nil())) -> c_13() 840.00/297.14 , active^#(U21(X1, X2)) -> c_14(U21^#(active(X1), X2)) 840.00/297.14 , active^#(U21(tt(), V1)) -> c_15(U22^#(isNatKind(V1), V1)) 840.00/297.14 , active^#(U22(X1, X2)) -> c_16(U22^#(active(X1), X2)) 840.00/297.14 , active^#(U22(tt(), V1)) -> c_17(U23^#(isNat(V1))) 840.00/297.14 , active^#(isNatKind(0())) -> c_18() 840.00/297.14 , active^#(isNatKind(s(V1))) -> c_19(U71^#(isNatKind(V1))) 840.00/297.14 , active^#(isNatKind(length(V1))) -> 840.00/297.14 c_20(U61^#(isNatIListKind(V1))) 840.00/297.14 , active^#(U23(X)) -> c_21(U23^#(active(X))) 840.00/297.14 , active^#(U23(tt())) -> c_22() 840.00/297.14 , active^#(isNat(0())) -> c_23() 840.00/297.14 , active^#(isNat(s(V1))) -> c_24(U21^#(isNatKind(V1), V1)) 840.00/297.14 , active^#(isNat(length(V1))) -> 840.00/297.14 c_25(U11^#(isNatIListKind(V1), V1)) 840.00/297.14 , active^#(U31(X1, X2)) -> c_26(U31^#(active(X1), X2)) 840.00/297.14 , active^#(U31(tt(), V)) -> c_27(U32^#(isNatIListKind(V), V)) 840.00/297.14 , active^#(U32(X1, X2)) -> c_28(U32^#(active(X1), X2)) 840.00/297.14 , active^#(U32(tt(), V)) -> c_29(U33^#(isNatList(V))) 840.00/297.14 , active^#(U33(X)) -> c_30(U33^#(active(X))) 840.00/297.14 , active^#(U33(tt())) -> c_31() 840.00/297.14 , active^#(U41(X1, X2, X3)) -> c_32(U41^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U41(tt(), V1, V2)) -> c_33(U42^#(isNatKind(V1), V1, V2)) 840.00/297.14 , active^#(U42(X1, X2, X3)) -> c_34(U42^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U42(tt(), V1, V2)) -> 840.00/297.14 c_35(U43^#(isNatIListKind(V2), V1, V2)) 840.00/297.14 , active^#(U43(X1, X2, X3)) -> c_36(U43^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U43(tt(), V1, V2)) -> 840.00/297.14 c_37(U44^#(isNatIListKind(V2), V1, V2)) 840.00/297.14 , active^#(U44(X1, X2, X3)) -> c_38(U44^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U44(tt(), V1, V2)) -> c_39(U45^#(isNat(V1), V2)) 840.00/297.14 , active^#(U45(X1, X2)) -> c_40(U45^#(active(X1), X2)) 840.00/297.14 , active^#(U45(tt(), V2)) -> c_41(U46^#(isNatIList(V2))) 840.00/297.14 , active^#(U46(X)) -> c_42(U46^#(active(X))) 840.00/297.14 , active^#(U46(tt())) -> c_43() 840.00/297.14 , active^#(isNatIList(V)) -> c_44(U31^#(isNatIListKind(V), V)) 840.00/297.14 , active^#(isNatIList(zeros())) -> c_45() 840.00/297.14 , active^#(isNatIList(cons(V1, V2))) -> 840.00/297.14 c_46(U41^#(isNatKind(V1), V1, V2)) 840.00/297.14 , active^#(U51(X1, X2)) -> c_47(U51^#(active(X1), X2)) 840.00/297.14 , active^#(U51(tt(), V2)) -> c_48(U52^#(isNatIListKind(V2))) 840.00/297.14 , active^#(U52(X)) -> c_49(U52^#(active(X))) 840.00/297.14 , active^#(U52(tt())) -> c_50() 840.00/297.14 , active^#(U61(X)) -> c_51(U61^#(active(X))) 840.00/297.14 , active^#(U61(tt())) -> c_52() 840.00/297.14 , active^#(U71(X)) -> c_53(U71^#(active(X))) 840.00/297.14 , active^#(U71(tt())) -> c_54() 840.00/297.14 , active^#(U81(X1, X2, X3)) -> c_55(U81^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U81(tt(), V1, V2)) -> c_56(U82^#(isNatKind(V1), V1, V2)) 840.00/297.14 , active^#(U82(X1, X2, X3)) -> c_57(U82^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U82(tt(), V1, V2)) -> 840.00/297.14 c_58(U83^#(isNatIListKind(V2), V1, V2)) 840.00/297.14 , active^#(U83(X1, X2, X3)) -> c_59(U83^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U83(tt(), V1, V2)) -> 840.00/297.14 c_60(U84^#(isNatIListKind(V2), V1, V2)) 840.00/297.14 , active^#(U84(X1, X2, X3)) -> c_61(U84^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U84(tt(), V1, V2)) -> c_62(U85^#(isNat(V1), V2)) 840.00/297.14 , active^#(U85(X1, X2)) -> c_63(U85^#(active(X1), X2)) 840.00/297.14 , active^#(U85(tt(), V2)) -> c_64(U86^#(isNatList(V2))) 840.00/297.14 , active^#(U86(X)) -> c_65(U86^#(active(X))) 840.00/297.14 , active^#(U86(tt())) -> c_66() 840.00/297.14 , active^#(U91(X1, X2, X3)) -> c_67(U91^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U91(tt(), L, N)) -> c_68(U92^#(isNatIListKind(L), L, N)) 840.00/297.14 , active^#(U92(X1, X2, X3)) -> c_69(U92^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U92(tt(), L, N)) -> c_70(U93^#(isNat(N), L, N)) 840.00/297.14 , active^#(U93(X1, X2, X3)) -> c_71(U93^#(active(X1), X2, X3)) 840.00/297.14 , active^#(U93(tt(), L, N)) -> c_72(U94^#(isNatKind(N), L)) 840.00/297.14 , active^#(U94(X1, X2)) -> c_73(U94^#(active(X1), X2)) 840.00/297.14 , active^#(U94(tt(), L)) -> c_74(s^#(length(L))) 840.00/297.14 , active^#(s(X)) -> c_75(s^#(active(X))) 840.00/297.14 , active^#(length(X)) -> c_76(length^#(active(X))) 840.00/297.14 , active^#(length(cons(N, L))) -> c_77(U91^#(isNatList(L), L, N)) 840.00/297.14 , active^#(length(nil())) -> c_78() 840.00/297.14 , cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) 840.00/297.14 , cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) 840.00/297.14 , U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) 840.00/297.14 , U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) 840.00/297.14 , U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) 840.00/297.14 , U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) 840.00/297.14 , U13^#(mark(X)) -> c_86(U13^#(X)) 840.00/297.14 , U13^#(ok(X)) -> c_87(U13^#(X)) 840.00/297.14 , U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) 840.00/297.14 , U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) 840.00/297.14 , U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) 840.00/297.14 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) 840.00/297.14 , U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) 840.00/297.14 , U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) 840.00/297.14 , U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) 840.00/297.14 , U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) 840.00/297.14 , U23^#(mark(X)) -> c_94(U23^#(X)) 840.00/297.14 , U23^#(ok(X)) -> c_95(U23^#(X)) 840.00/297.14 , U71^#(mark(X)) -> c_122(U71^#(X)) 840.00/297.14 , U71^#(ok(X)) -> c_123(U71^#(X)) 840.00/297.14 , U61^#(mark(X)) -> c_120(U61^#(X)) 840.00/297.14 , U61^#(ok(X)) -> c_121(U61^#(X)) 840.00/297.14 , U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) 840.00/297.14 , U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) 840.00/297.14 , U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) 840.00/297.14 , U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) 840.00/297.14 , U33^#(mark(X)) -> c_101(U33^#(X)) 840.00/297.14 , U33^#(ok(X)) -> c_102(U33^#(X)) 840.00/297.14 , U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) 840.00/297.14 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_104(U41^#(X1, X2, X3)) 840.00/297.14 , U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) 840.00/297.14 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_106(U42^#(X1, X2, X3)) 840.00/297.14 , U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) 840.00/297.14 , U43^#(ok(X1), ok(X2), ok(X3)) -> c_108(U43^#(X1, X2, X3)) 840.00/297.14 , U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) 840.00/297.14 , U44^#(ok(X1), ok(X2), ok(X3)) -> c_110(U44^#(X1, X2, X3)) 840.00/297.14 , U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) 840.00/297.14 , U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) 840.00/297.14 , U46^#(mark(X)) -> c_113(U46^#(X)) 840.00/297.14 , U46^#(ok(X)) -> c_114(U46^#(X)) 840.00/297.14 , U52^#(mark(X)) -> c_118(U52^#(X)) 840.00/297.14 , U52^#(ok(X)) -> c_119(U52^#(X)) 840.00/297.14 , U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) 840.00/297.14 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_127(U82^#(X1, X2, X3)) 840.00/297.14 , U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) 840.00/297.14 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_129(U83^#(X1, X2, X3)) 840.00/297.14 , U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) 840.00/297.14 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_131(U84^#(X1, X2, X3)) 840.00/297.14 , U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) 840.00/297.14 , U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) 840.00/297.14 , U86^#(mark(X)) -> c_134(U86^#(X)) 840.00/297.14 , U86^#(ok(X)) -> c_135(U86^#(X)) 840.00/297.14 , U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) 840.00/297.14 , U91^#(ok(X1), ok(X2), ok(X3)) -> c_137(U91^#(X1, X2, X3)) 840.00/297.14 , U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) 840.00/297.14 , U92^#(ok(X1), ok(X2), ok(X3)) -> c_139(U92^#(X1, X2, X3)) 840.00/297.14 , U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) 840.00/297.14 , U93^#(ok(X1), ok(X2), ok(X3)) -> c_141(U93^#(X1, X2, X3)) 840.00/297.14 , U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) 840.00/297.14 , U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) 840.00/297.14 , s^#(mark(X)) -> c_144(s^#(X)) 840.00/297.14 , s^#(ok(X)) -> c_145(s^#(X)) 840.00/297.14 , length^#(mark(X)) -> c_146(length^#(X)) 840.00/297.14 , length^#(ok(X)) -> c_147(length^#(X)) 840.00/297.14 , isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) 840.00/297.14 , isNatList^#(ok(X)) -> c_88(isNatList^#(X)) 840.00/297.14 , isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) 840.00/297.14 , isNat^#(ok(X)) -> c_96(isNat^#(X)) 840.00/297.14 , isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) 840.00/297.14 , proper^#(zeros()) -> c_148() 840.00/297.14 , proper^#(cons(X1, X2)) -> c_149(cons^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(0()) -> c_150() 840.00/297.14 , proper^#(U11(X1, X2)) -> c_151(U11^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(tt()) -> c_152() 840.00/297.14 , proper^#(U12(X1, X2)) -> c_153(U12^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(isNatIListKind(X)) -> c_154(isNatIListKind^#(proper(X))) 840.00/297.14 , proper^#(U13(X)) -> c_155(U13^#(proper(X))) 840.00/297.14 , proper^#(isNatList(X)) -> c_156(isNatList^#(proper(X))) 840.00/297.14 , proper^#(U21(X1, X2)) -> c_157(U21^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U22(X1, X2)) -> c_158(U22^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) 840.00/297.14 , proper^#(U23(X)) -> c_160(U23^#(proper(X))) 840.00/297.14 , proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) 840.00/297.14 , proper^#(U31(X1, X2)) -> c_162(U31^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U32(X1, X2)) -> c_163(U32^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U33(X)) -> c_164(U33^#(proper(X))) 840.00/297.14 , proper^#(U41(X1, X2, X3)) -> 840.00/297.14 c_165(U41^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U42(X1, X2, X3)) -> 840.00/297.14 c_166(U42^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U43(X1, X2, X3)) -> 840.00/297.14 c_167(U43^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U44(X1, X2, X3)) -> 840.00/297.14 c_168(U44^#(proper(X1), proper(X2), proper(X3))) 840.00/297.14 , proper^#(U45(X1, X2)) -> c_169(U45^#(proper(X1), proper(X2))) 840.00/297.14 , proper^#(U46(X)) -> c_170(U46^#(proper(X))) 840.00/297.15 , proper^#(isNatIList(X)) -> c_171(isNatIList^#(proper(X))) 840.00/297.15 , proper^#(U51(X1, X2)) -> c_172(U51^#(proper(X1), proper(X2))) 840.00/297.15 , proper^#(U52(X)) -> c_173(U52^#(proper(X))) 840.00/297.15 , proper^#(U61(X)) -> c_174(U61^#(proper(X))) 840.00/297.15 , proper^#(U71(X)) -> c_175(U71^#(proper(X))) 840.00/297.15 , proper^#(U81(X1, X2, X3)) -> 840.00/297.15 c_176(U81^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U82(X1, X2, X3)) -> 840.00/297.15 c_177(U82^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U83(X1, X2, X3)) -> 840.00/297.15 c_178(U83^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U84(X1, X2, X3)) -> 840.00/297.15 c_179(U84^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U85(X1, X2)) -> c_180(U85^#(proper(X1), proper(X2))) 840.00/297.15 , proper^#(U86(X)) -> c_181(U86^#(proper(X))) 840.00/297.15 , proper^#(U91(X1, X2, X3)) -> 840.00/297.15 c_182(U91^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U92(X1, X2, X3)) -> 840.00/297.15 c_183(U92^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U93(X1, X2, X3)) -> 840.00/297.15 c_184(U93^#(proper(X1), proper(X2), proper(X3))) 840.00/297.15 , proper^#(U94(X1, X2)) -> c_185(U94^#(proper(X1), proper(X2))) 840.00/297.15 , proper^#(s(X)) -> c_186(s^#(proper(X))) 840.00/297.15 , proper^#(length(X)) -> c_187(length^#(proper(X))) 840.00/297.15 , proper^#(nil()) -> c_188() 840.00/297.15 , top^#(mark(X)) -> c_189(top^#(proper(X))) 840.00/297.15 , top^#(ok(X)) -> c_190(top^#(active(X))) } 840.00/297.15 Strict Trs: 840.00/297.15 { active(zeros()) -> mark(cons(0(), zeros())) 840.00/297.15 , active(cons(X1, X2)) -> cons(active(X1), X2) 840.00/297.15 , active(U11(X1, X2)) -> U11(active(X1), X2) 840.00/297.15 , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) 840.00/297.15 , active(U12(X1, X2)) -> U12(active(X1), X2) 840.00/297.15 , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) 840.00/297.15 , active(isNatIListKind(zeros())) -> mark(tt()) 840.00/297.15 , active(isNatIListKind(cons(V1, V2))) -> 840.00/297.15 mark(U51(isNatKind(V1), V2)) 840.00/297.15 , active(isNatIListKind(nil())) -> mark(tt()) 840.00/297.15 , active(U13(X)) -> U13(active(X)) 840.00/297.15 , active(U13(tt())) -> mark(tt()) 840.00/297.15 , active(isNatList(cons(V1, V2))) -> 840.00/297.15 mark(U81(isNatKind(V1), V1, V2)) 840.00/297.15 , active(isNatList(nil())) -> mark(tt()) 840.00/297.15 , active(U21(X1, X2)) -> U21(active(X1), X2) 840.00/297.15 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 840.00/297.15 , active(U22(X1, X2)) -> U22(active(X1), X2) 840.00/297.15 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 840.00/297.15 , active(isNatKind(0())) -> mark(tt()) 840.00/297.15 , active(isNatKind(s(V1))) -> mark(U71(isNatKind(V1))) 840.00/297.15 , active(isNatKind(length(V1))) -> mark(U61(isNatIListKind(V1))) 840.00/297.15 , active(U23(X)) -> U23(active(X)) 840.00/297.15 , active(U23(tt())) -> mark(tt()) 840.00/297.15 , active(isNat(0())) -> mark(tt()) 840.00/297.15 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 840.00/297.15 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 840.00/297.15 , active(U31(X1, X2)) -> U31(active(X1), X2) 840.00/297.15 , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) 840.00/297.15 , active(U32(X1, X2)) -> U32(active(X1), X2) 840.00/297.15 , active(U32(tt(), V)) -> mark(U33(isNatList(V))) 840.00/297.15 , active(U33(X)) -> U33(active(X)) 840.00/297.15 , active(U33(tt())) -> mark(tt()) 840.00/297.15 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 840.00/297.15 , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) 840.00/297.15 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 840.00/297.15 , active(U42(tt(), V1, V2)) -> 840.00/297.15 mark(U43(isNatIListKind(V2), V1, V2)) 840.00/297.15 , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) 840.00/297.15 , active(U43(tt(), V1, V2)) -> 840.00/297.15 mark(U44(isNatIListKind(V2), V1, V2)) 840.00/297.15 , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) 840.00/297.15 , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) 840.00/297.15 , active(U45(X1, X2)) -> U45(active(X1), X2) 840.00/297.15 , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) 840.00/297.15 , active(U46(X)) -> U46(active(X)) 840.00/297.15 , active(U46(tt())) -> mark(tt()) 840.00/297.15 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 840.00/297.15 , active(isNatIList(zeros())) -> mark(tt()) 840.00/297.15 , active(isNatIList(cons(V1, V2))) -> 840.00/297.15 mark(U41(isNatKind(V1), V1, V2)) 840.00/297.15 , active(U51(X1, X2)) -> U51(active(X1), X2) 840.00/297.15 , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) 840.00/297.15 , active(U52(X)) -> U52(active(X)) 840.00/297.15 , active(U52(tt())) -> mark(tt()) 840.00/297.15 , active(U61(X)) -> U61(active(X)) 840.00/297.15 , active(U61(tt())) -> mark(tt()) 840.00/297.15 , active(U71(X)) -> U71(active(X)) 840.00/297.15 , active(U71(tt())) -> mark(tt()) 840.00/297.15 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 840.00/297.15 , active(U81(tt(), V1, V2)) -> mark(U82(isNatKind(V1), V1, V2)) 840.00/297.15 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 840.00/297.15 , active(U82(tt(), V1, V2)) -> 840.00/297.15 mark(U83(isNatIListKind(V2), V1, V2)) 840.00/297.15 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 840.00/297.15 , active(U83(tt(), V1, V2)) -> 840.00/297.15 mark(U84(isNatIListKind(V2), V1, V2)) 840.00/297.15 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 840.00/297.15 , active(U84(tt(), V1, V2)) -> mark(U85(isNat(V1), V2)) 840.00/297.15 , active(U85(X1, X2)) -> U85(active(X1), X2) 840.00/297.15 , active(U85(tt(), V2)) -> mark(U86(isNatList(V2))) 840.00/297.15 , active(U86(X)) -> U86(active(X)) 840.00/297.15 , active(U86(tt())) -> mark(tt()) 840.00/297.15 , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) 840.00/297.15 , active(U91(tt(), L, N)) -> mark(U92(isNatIListKind(L), L, N)) 840.00/297.15 , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) 840.00/297.15 , active(U92(tt(), L, N)) -> mark(U93(isNat(N), L, N)) 840.00/297.15 , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) 840.00/297.15 , active(U93(tt(), L, N)) -> mark(U94(isNatKind(N), L)) 840.00/297.15 , active(U94(X1, X2)) -> U94(active(X1), X2) 840.00/297.15 , active(U94(tt(), L)) -> mark(s(length(L))) 840.00/297.15 , active(s(X)) -> s(active(X)) 840.00/297.15 , active(length(X)) -> length(active(X)) 840.00/297.15 , active(length(cons(N, L))) -> mark(U91(isNatList(L), L, N)) 840.00/297.15 , active(length(nil())) -> mark(0()) 840.00/297.15 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 840.00/297.15 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 840.00/297.15 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 840.00/297.15 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 840.00/297.15 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 840.00/297.15 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 840.00/297.15 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 840.00/297.15 , U13(mark(X)) -> mark(U13(X)) 840.00/297.15 , U13(ok(X)) -> ok(U13(X)) 840.00/297.15 , isNatList(ok(X)) -> ok(isNatList(X)) 840.00/297.15 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 840.00/297.15 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 840.00/297.15 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 840.00/297.15 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 840.00/297.15 , isNatKind(ok(X)) -> ok(isNatKind(X)) 840.00/297.15 , U23(mark(X)) -> mark(U23(X)) 840.00/297.15 , U23(ok(X)) -> ok(U23(X)) 840.00/297.15 , isNat(ok(X)) -> ok(isNat(X)) 840.00/297.15 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 840.00/297.15 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 840.00/297.15 , U32(mark(X1), X2) -> mark(U32(X1, X2)) 840.00/297.15 , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) 840.00/297.15 , U33(mark(X)) -> mark(U33(X)) 840.00/297.15 , U33(ok(X)) -> ok(U33(X)) 840.00/297.15 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 840.00/297.15 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 840.00/297.15 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 840.00/297.15 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 840.00/297.15 , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) 840.00/297.15 , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) 840.00/297.15 , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) 840.00/297.15 , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) 840.00/297.15 , U45(mark(X1), X2) -> mark(U45(X1, X2)) 840.00/297.15 , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) 840.00/297.15 , U46(mark(X)) -> mark(U46(X)) 840.00/297.15 , U46(ok(X)) -> ok(U46(X)) 840.00/297.15 , isNatIList(ok(X)) -> ok(isNatIList(X)) 840.00/297.15 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 840.00/297.15 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 840.00/297.15 , U52(mark(X)) -> mark(U52(X)) 840.00/297.15 , U52(ok(X)) -> ok(U52(X)) 840.00/297.15 , U61(mark(X)) -> mark(U61(X)) 840.00/297.15 , U61(ok(X)) -> ok(U61(X)) 840.00/297.15 , U71(mark(X)) -> mark(U71(X)) 840.00/297.15 , U71(ok(X)) -> ok(U71(X)) 840.00/297.15 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 840.00/297.15 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 840.00/297.15 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 840.00/297.15 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 840.00/297.15 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 840.00/297.15 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 840.00/297.15 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 840.00/297.15 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 840.00/297.15 , U85(mark(X1), X2) -> mark(U85(X1, X2)) 840.00/297.15 , U85(ok(X1), ok(X2)) -> ok(U85(X1, X2)) 840.00/297.15 , U86(mark(X)) -> mark(U86(X)) 840.00/297.15 , U86(ok(X)) -> ok(U86(X)) 840.00/297.15 , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) 840.00/297.15 , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) 840.00/297.15 , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) 840.00/297.15 , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) 840.00/297.15 , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) 840.00/297.15 , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) 840.00/297.15 , U94(mark(X1), X2) -> mark(U94(X1, X2)) 840.00/297.15 , U94(ok(X1), ok(X2)) -> ok(U94(X1, X2)) 840.00/297.15 , s(mark(X)) -> mark(s(X)) 840.00/297.15 , s(ok(X)) -> ok(s(X)) 840.00/297.15 , length(mark(X)) -> mark(length(X)) 840.00/297.15 , length(ok(X)) -> ok(length(X)) 840.00/297.15 , proper(zeros()) -> ok(zeros()) 840.00/297.15 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 840.00/297.15 , proper(0()) -> ok(0()) 840.00/297.15 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 840.00/297.15 , proper(tt()) -> ok(tt()) 840.00/297.15 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 840.00/297.15 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 840.00/297.15 , proper(U13(X)) -> U13(proper(X)) 840.00/297.15 , proper(isNatList(X)) -> isNatList(proper(X)) 840.00/297.15 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 840.00/297.15 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 840.00/297.15 , proper(isNatKind(X)) -> isNatKind(proper(X)) 840.00/297.15 , proper(U23(X)) -> U23(proper(X)) 840.00/297.15 , proper(isNat(X)) -> isNat(proper(X)) 840.00/297.15 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 840.00/297.15 , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) 840.00/297.15 , proper(U33(X)) -> U33(proper(X)) 840.00/297.15 , proper(U41(X1, X2, X3)) -> 840.00/297.15 U41(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U42(X1, X2, X3)) -> 840.00/297.15 U42(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U43(X1, X2, X3)) -> 840.00/297.15 U43(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U44(X1, X2, X3)) -> 840.00/297.15 U44(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) 840.00/297.15 , proper(U46(X)) -> U46(proper(X)) 840.00/297.15 , proper(isNatIList(X)) -> isNatIList(proper(X)) 840.00/297.15 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 840.00/297.15 , proper(U52(X)) -> U52(proper(X)) 840.00/297.15 , proper(U61(X)) -> U61(proper(X)) 840.00/297.15 , proper(U71(X)) -> U71(proper(X)) 840.00/297.15 , proper(U81(X1, X2, X3)) -> 840.00/297.15 U81(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U82(X1, X2, X3)) -> 840.00/297.15 U82(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U83(X1, X2, X3)) -> 840.00/297.15 U83(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U84(X1, X2, X3)) -> 840.00/297.15 U84(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U85(X1, X2)) -> U85(proper(X1), proper(X2)) 840.00/297.15 , proper(U86(X)) -> U86(proper(X)) 840.00/297.15 , proper(U91(X1, X2, X3)) -> 840.00/297.15 U91(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U92(X1, X2, X3)) -> 840.00/297.15 U92(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U93(X1, X2, X3)) -> 840.00/297.15 U93(proper(X1), proper(X2), proper(X3)) 840.00/297.15 , proper(U94(X1, X2)) -> U94(proper(X1), proper(X2)) 840.00/297.15 , proper(s(X)) -> s(proper(X)) 840.00/297.15 , proper(length(X)) -> length(proper(X)) 840.00/297.15 , proper(nil()) -> ok(nil()) 840.00/297.15 , top(mark(X)) -> top(proper(X)) 840.00/297.15 , top(ok(X)) -> top(active(X)) } 840.00/297.15 Obligation: 840.00/297.15 runtime complexity 840.00/297.15 Answer: 840.00/297.15 MAYBE 840.00/297.15 840.00/297.15 Consider the dependency graph: 840.00/297.15 840.00/297.15 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 840.00/297.15 840.00/297.15 2: active^#(cons(X1, X2)) -> c_2(cons^#(active(X1), X2)) 840.00/297.15 -->_1 cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) :80 840.00/297.15 -->_1 cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) :79 840.00/297.15 840.00/297.15 3: active^#(U11(X1, X2)) -> c_3(U11^#(active(X1), X2)) 840.00/297.15 -->_1 U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) :82 840.00/297.15 -->_1 U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) :81 840.00/297.15 840.00/297.15 4: active^#(U11(tt(), V1)) -> c_4(U12^#(isNatIListKind(V1), V1)) 840.00/297.15 -->_1 U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) :84 840.00/297.15 -->_1 U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) :83 840.00/297.15 840.00/297.15 5: active^#(U12(X1, X2)) -> c_5(U12^#(active(X1), X2)) 840.00/297.15 -->_1 U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) :84 840.00/297.15 -->_1 U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) :83 840.00/297.15 840.00/297.15 6: active^#(U12(tt(), V1)) -> c_6(U13^#(isNatList(V1))) 840.00/297.15 -->_1 U13^#(ok(X)) -> c_87(U13^#(X)) :86 840.00/297.15 -->_1 U13^#(mark(X)) -> c_86(U13^#(X)) :85 840.00/297.15 840.00/297.15 7: active^#(isNatIListKind(zeros())) -> c_7() 840.00/297.15 840.00/297.15 8: active^#(isNatIListKind(cons(V1, V2))) -> 840.00/297.15 c_8(U51^#(isNatKind(V1), V2)) 840.00/297.15 -->_1 U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) :88 840.00/297.15 -->_1 U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) :87 840.00/297.15 840.00/297.15 9: active^#(isNatIListKind(nil())) -> c_9() 840.00/297.15 840.00/297.15 10: active^#(U13(X)) -> c_10(U13^#(active(X))) 840.00/297.15 -->_1 U13^#(ok(X)) -> c_87(U13^#(X)) :86 840.00/297.15 -->_1 U13^#(mark(X)) -> c_86(U13^#(X)) :85 840.00/297.15 840.00/297.15 11: active^#(U13(tt())) -> c_11() 840.00/297.15 840.00/297.15 12: active^#(isNatList(cons(V1, V2))) -> 840.00/297.15 c_12(U81^#(isNatKind(V1), V1, V2)) 840.00/297.15 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) :90 840.00/297.15 -->_1 U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) :89 840.00/297.15 840.00/297.15 13: active^#(isNatList(nil())) -> c_13() 840.00/297.15 840.00/297.15 14: active^#(U21(X1, X2)) -> c_14(U21^#(active(X1), X2)) 840.00/297.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) :92 840.00/297.15 -->_1 U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) :91 840.00/297.15 840.00/297.15 15: active^#(U21(tt(), V1)) -> c_15(U22^#(isNatKind(V1), V1)) 840.00/297.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) :94 840.00/297.15 -->_1 U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) :93 840.00/297.15 840.00/297.15 16: active^#(U22(X1, X2)) -> c_16(U22^#(active(X1), X2)) 840.00/297.15 -->_1 U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) :94 840.00/297.15 -->_1 U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) :93 840.00/297.15 840.00/297.15 17: active^#(U22(tt(), V1)) -> c_17(U23^#(isNat(V1))) 840.00/297.15 -->_1 U23^#(ok(X)) -> c_95(U23^#(X)) :96 840.00/297.15 -->_1 U23^#(mark(X)) -> c_94(U23^#(X)) :95 840.00/297.15 840.00/297.15 18: active^#(isNatKind(0())) -> c_18() 840.00/297.15 840.00/297.15 19: active^#(isNatKind(s(V1))) -> c_19(U71^#(isNatKind(V1))) 840.00/297.15 -->_1 U71^#(ok(X)) -> c_123(U71^#(X)) :98 840.00/297.15 -->_1 U71^#(mark(X)) -> c_122(U71^#(X)) :97 840.00/297.15 840.00/297.15 20: active^#(isNatKind(length(V1))) -> 840.00/297.15 c_20(U61^#(isNatIListKind(V1))) 840.00/297.15 -->_1 U61^#(ok(X)) -> c_121(U61^#(X)) :100 840.00/297.15 -->_1 U61^#(mark(X)) -> c_120(U61^#(X)) :99 840.00/297.15 840.00/297.15 21: active^#(U23(X)) -> c_21(U23^#(active(X))) 840.00/297.15 -->_1 U23^#(ok(X)) -> c_95(U23^#(X)) :96 840.00/297.15 -->_1 U23^#(mark(X)) -> c_94(U23^#(X)) :95 840.00/297.15 840.00/297.15 22: active^#(U23(tt())) -> c_22() 840.00/297.15 840.00/297.15 23: active^#(isNat(0())) -> c_23() 840.00/297.15 840.00/297.15 24: active^#(isNat(s(V1))) -> c_24(U21^#(isNatKind(V1), V1)) 840.00/297.15 -->_1 U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) :92 840.00/297.15 -->_1 U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) :91 840.00/297.15 840.00/297.15 25: active^#(isNat(length(V1))) -> 840.00/297.15 c_25(U11^#(isNatIListKind(V1), V1)) 840.00/297.15 -->_1 U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) :82 840.00/297.15 -->_1 U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) :81 840.00/297.15 840.00/297.15 26: active^#(U31(X1, X2)) -> c_26(U31^#(active(X1), X2)) 840.00/297.15 -->_1 U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) :102 840.00/297.15 -->_1 U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) :101 840.00/297.15 840.00/297.15 27: active^#(U31(tt(), V)) -> c_27(U32^#(isNatIListKind(V), V)) 840.00/297.15 -->_1 U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) :104 840.00/297.15 -->_1 U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) :103 840.00/297.15 840.00/297.15 28: active^#(U32(X1, X2)) -> c_28(U32^#(active(X1), X2)) 840.00/297.15 -->_1 U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) :104 840.00/297.15 -->_1 U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) :103 840.00/297.15 840.00/297.15 29: active^#(U32(tt(), V)) -> c_29(U33^#(isNatList(V))) 840.00/297.15 -->_1 U33^#(ok(X)) -> c_102(U33^#(X)) :106 840.00/297.15 -->_1 U33^#(mark(X)) -> c_101(U33^#(X)) :105 840.00/297.15 840.00/297.15 30: active^#(U33(X)) -> c_30(U33^#(active(X))) 840.00/297.15 -->_1 U33^#(ok(X)) -> c_102(U33^#(X)) :106 840.00/297.15 -->_1 U33^#(mark(X)) -> c_101(U33^#(X)) :105 840.00/297.15 840.00/297.15 31: active^#(U33(tt())) -> c_31() 840.00/297.15 840.00/297.15 32: active^#(U41(X1, X2, X3)) -> c_32(U41^#(active(X1), X2, X3)) 840.00/297.15 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.15 c_104(U41^#(X1, X2, X3)) :108 840.00/297.15 -->_1 U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) :107 840.00/297.15 840.00/297.15 33: active^#(U41(tt(), V1, V2)) -> 840.00/297.16 c_33(U42^#(isNatKind(V1), V1, V2)) 840.00/297.16 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_106(U42^#(X1, X2, X3)) :110 840.00/297.16 -->_1 U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) :109 840.00/297.16 840.00/297.16 34: active^#(U42(X1, X2, X3)) -> c_34(U42^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_106(U42^#(X1, X2, X3)) :110 840.00/297.16 -->_1 U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) :109 840.00/297.16 840.00/297.16 35: active^#(U42(tt(), V1, V2)) -> 840.00/297.16 c_35(U43^#(isNatIListKind(V2), V1, V2)) 840.00/297.16 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_108(U43^#(X1, X2, X3)) :112 840.00/297.16 -->_1 U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) :111 840.00/297.16 840.00/297.16 36: active^#(U43(X1, X2, X3)) -> c_36(U43^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_108(U43^#(X1, X2, X3)) :112 840.00/297.16 -->_1 U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) :111 840.00/297.16 840.00/297.16 37: active^#(U43(tt(), V1, V2)) -> 840.00/297.16 c_37(U44^#(isNatIListKind(V2), V1, V2)) 840.00/297.16 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_110(U44^#(X1, X2, X3)) :114 840.00/297.16 -->_1 U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) :113 840.00/297.16 840.00/297.16 38: active^#(U44(X1, X2, X3)) -> c_38(U44^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_110(U44^#(X1, X2, X3)) :114 840.00/297.16 -->_1 U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) :113 840.00/297.16 840.00/297.16 39: active^#(U44(tt(), V1, V2)) -> c_39(U45^#(isNat(V1), V2)) 840.00/297.16 -->_1 U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) :116 840.00/297.16 -->_1 U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) :115 840.00/297.16 840.00/297.16 40: active^#(U45(X1, X2)) -> c_40(U45^#(active(X1), X2)) 840.00/297.16 -->_1 U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) :116 840.00/297.16 -->_1 U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) :115 840.00/297.16 840.00/297.16 41: active^#(U45(tt(), V2)) -> c_41(U46^#(isNatIList(V2))) 840.00/297.16 -->_1 U46^#(ok(X)) -> c_114(U46^#(X)) :118 840.00/297.16 -->_1 U46^#(mark(X)) -> c_113(U46^#(X)) :117 840.00/297.16 840.00/297.16 42: active^#(U46(X)) -> c_42(U46^#(active(X))) 840.00/297.16 -->_1 U46^#(ok(X)) -> c_114(U46^#(X)) :118 840.00/297.16 -->_1 U46^#(mark(X)) -> c_113(U46^#(X)) :117 840.00/297.16 840.00/297.16 43: active^#(U46(tt())) -> c_43() 840.00/297.16 840.00/297.16 44: active^#(isNatIList(V)) -> c_44(U31^#(isNatIListKind(V), V)) 840.00/297.16 -->_1 U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) :102 840.00/297.16 -->_1 U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) :101 840.00/297.16 840.00/297.16 45: active^#(isNatIList(zeros())) -> c_45() 840.00/297.16 840.00/297.16 46: active^#(isNatIList(cons(V1, V2))) -> 840.00/297.16 c_46(U41^#(isNatKind(V1), V1, V2)) 840.00/297.16 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_104(U41^#(X1, X2, X3)) :108 840.00/297.16 -->_1 U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) :107 840.00/297.16 840.00/297.16 47: active^#(U51(X1, X2)) -> c_47(U51^#(active(X1), X2)) 840.00/297.16 -->_1 U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) :88 840.00/297.16 -->_1 U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) :87 840.00/297.16 840.00/297.16 48: active^#(U51(tt(), V2)) -> c_48(U52^#(isNatIListKind(V2))) 840.00/297.16 -->_1 U52^#(ok(X)) -> c_119(U52^#(X)) :120 840.00/297.16 -->_1 U52^#(mark(X)) -> c_118(U52^#(X)) :119 840.00/297.16 840.00/297.16 49: active^#(U52(X)) -> c_49(U52^#(active(X))) 840.00/297.16 -->_1 U52^#(ok(X)) -> c_119(U52^#(X)) :120 840.00/297.16 -->_1 U52^#(mark(X)) -> c_118(U52^#(X)) :119 840.00/297.16 840.00/297.16 50: active^#(U52(tt())) -> c_50() 840.00/297.16 840.00/297.16 51: active^#(U61(X)) -> c_51(U61^#(active(X))) 840.00/297.16 -->_1 U61^#(ok(X)) -> c_121(U61^#(X)) :100 840.00/297.16 -->_1 U61^#(mark(X)) -> c_120(U61^#(X)) :99 840.00/297.16 840.00/297.16 52: active^#(U61(tt())) -> c_52() 840.00/297.16 840.00/297.16 53: active^#(U71(X)) -> c_53(U71^#(active(X))) 840.00/297.16 -->_1 U71^#(ok(X)) -> c_123(U71^#(X)) :98 840.00/297.16 -->_1 U71^#(mark(X)) -> c_122(U71^#(X)) :97 840.00/297.16 840.00/297.16 54: active^#(U71(tt())) -> c_54() 840.00/297.16 840.00/297.16 55: active^#(U81(X1, X2, X3)) -> c_55(U81^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) :90 840.00/297.16 -->_1 U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) :89 840.00/297.16 840.00/297.16 56: active^#(U81(tt(), V1, V2)) -> 840.00/297.16 c_56(U82^#(isNatKind(V1), V1, V2)) 840.00/297.16 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_127(U82^#(X1, X2, X3)) :122 840.00/297.16 -->_1 U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) :121 840.00/297.16 840.00/297.16 57: active^#(U82(X1, X2, X3)) -> c_57(U82^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_127(U82^#(X1, X2, X3)) :122 840.00/297.16 -->_1 U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) :121 840.00/297.16 840.00/297.16 58: active^#(U82(tt(), V1, V2)) -> 840.00/297.16 c_58(U83^#(isNatIListKind(V2), V1, V2)) 840.00/297.16 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_129(U83^#(X1, X2, X3)) :124 840.00/297.16 -->_1 U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) :123 840.00/297.16 840.00/297.16 59: active^#(U83(X1, X2, X3)) -> c_59(U83^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_129(U83^#(X1, X2, X3)) :124 840.00/297.16 -->_1 U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) :123 840.00/297.16 840.00/297.16 60: active^#(U83(tt(), V1, V2)) -> 840.00/297.16 c_60(U84^#(isNatIListKind(V2), V1, V2)) 840.00/297.16 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_131(U84^#(X1, X2, X3)) :126 840.00/297.16 -->_1 U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) :125 840.00/297.16 840.00/297.16 61: active^#(U84(X1, X2, X3)) -> c_61(U84^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_131(U84^#(X1, X2, X3)) :126 840.00/297.16 -->_1 U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) :125 840.00/297.16 840.00/297.16 62: active^#(U84(tt(), V1, V2)) -> c_62(U85^#(isNat(V1), V2)) 840.00/297.16 -->_1 U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) :128 840.00/297.16 -->_1 U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) :127 840.00/297.16 840.00/297.16 63: active^#(U85(X1, X2)) -> c_63(U85^#(active(X1), X2)) 840.00/297.16 -->_1 U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) :128 840.00/297.16 -->_1 U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) :127 840.00/297.16 840.00/297.16 64: active^#(U85(tt(), V2)) -> c_64(U86^#(isNatList(V2))) 840.00/297.16 -->_1 U86^#(ok(X)) -> c_135(U86^#(X)) :130 840.00/297.16 -->_1 U86^#(mark(X)) -> c_134(U86^#(X)) :129 840.00/297.16 840.00/297.16 65: active^#(U86(X)) -> c_65(U86^#(active(X))) 840.00/297.16 -->_1 U86^#(ok(X)) -> c_135(U86^#(X)) :130 840.00/297.16 -->_1 U86^#(mark(X)) -> c_134(U86^#(X)) :129 840.00/297.16 840.00/297.16 66: active^#(U86(tt())) -> c_66() 840.00/297.16 840.00/297.16 67: active^#(U91(X1, X2, X3)) -> c_67(U91^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_137(U91^#(X1, X2, X3)) :132 840.00/297.16 -->_1 U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) :131 840.00/297.16 840.00/297.16 68: active^#(U91(tt(), L, N)) -> 840.00/297.16 c_68(U92^#(isNatIListKind(L), L, N)) 840.00/297.16 -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_139(U92^#(X1, X2, X3)) :134 840.00/297.16 -->_1 U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) :133 840.00/297.16 840.00/297.16 69: active^#(U92(X1, X2, X3)) -> c_69(U92^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_139(U92^#(X1, X2, X3)) :134 840.00/297.16 -->_1 U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) :133 840.00/297.16 840.00/297.16 70: active^#(U92(tt(), L, N)) -> c_70(U93^#(isNat(N), L, N)) 840.00/297.16 -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_141(U93^#(X1, X2, X3)) :136 840.00/297.16 -->_1 U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) :135 840.00/297.16 840.00/297.16 71: active^#(U93(X1, X2, X3)) -> c_71(U93^#(active(X1), X2, X3)) 840.00/297.16 -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_141(U93^#(X1, X2, X3)) :136 840.00/297.16 -->_1 U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) :135 840.00/297.16 840.00/297.16 72: active^#(U93(tt(), L, N)) -> c_72(U94^#(isNatKind(N), L)) 840.00/297.16 -->_1 U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) :138 840.00/297.16 -->_1 U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) :137 840.00/297.16 840.00/297.16 73: active^#(U94(X1, X2)) -> c_73(U94^#(active(X1), X2)) 840.00/297.16 -->_1 U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) :138 840.00/297.16 -->_1 U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) :137 840.00/297.16 840.00/297.16 74: active^#(U94(tt(), L)) -> c_74(s^#(length(L))) 840.00/297.16 -->_1 s^#(ok(X)) -> c_145(s^#(X)) :140 840.00/297.16 -->_1 s^#(mark(X)) -> c_144(s^#(X)) :139 840.00/297.16 840.00/297.16 75: active^#(s(X)) -> c_75(s^#(active(X))) 840.00/297.16 -->_1 s^#(ok(X)) -> c_145(s^#(X)) :140 840.00/297.16 -->_1 s^#(mark(X)) -> c_144(s^#(X)) :139 840.00/297.16 840.00/297.16 76: active^#(length(X)) -> c_76(length^#(active(X))) 840.00/297.16 -->_1 length^#(ok(X)) -> c_147(length^#(X)) :142 840.00/297.16 -->_1 length^#(mark(X)) -> c_146(length^#(X)) :141 840.00/297.16 840.00/297.16 77: active^#(length(cons(N, L))) -> c_77(U91^#(isNatList(L), L, N)) 840.00/297.16 -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_137(U91^#(X1, X2, X3)) :132 840.00/297.16 -->_1 U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) :131 840.00/297.16 840.00/297.16 78: active^#(length(nil())) -> c_78() 840.00/297.16 840.00/297.16 79: cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) 840.00/297.16 -->_1 cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) :80 840.00/297.16 -->_1 cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) :79 840.00/297.16 840.00/297.16 80: cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) 840.00/297.16 -->_1 cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) :80 840.00/297.16 -->_1 cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) :79 840.00/297.16 840.00/297.16 81: U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) 840.00/297.16 -->_1 U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) :82 840.00/297.16 -->_1 U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) :81 840.00/297.16 840.00/297.16 82: U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) 840.00/297.16 -->_1 U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) :82 840.00/297.16 -->_1 U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) :81 840.00/297.16 840.00/297.16 83: U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) 840.00/297.16 -->_1 U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) :84 840.00/297.16 -->_1 U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) :83 840.00/297.16 840.00/297.16 84: U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) 840.00/297.16 -->_1 U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) :84 840.00/297.16 -->_1 U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) :83 840.00/297.16 840.00/297.16 85: U13^#(mark(X)) -> c_86(U13^#(X)) 840.00/297.16 -->_1 U13^#(ok(X)) -> c_87(U13^#(X)) :86 840.00/297.16 -->_1 U13^#(mark(X)) -> c_86(U13^#(X)) :85 840.00/297.16 840.00/297.16 86: U13^#(ok(X)) -> c_87(U13^#(X)) 840.00/297.16 -->_1 U13^#(ok(X)) -> c_87(U13^#(X)) :86 840.00/297.16 -->_1 U13^#(mark(X)) -> c_86(U13^#(X)) :85 840.00/297.16 840.00/297.16 87: U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) 840.00/297.16 -->_1 U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) :88 840.00/297.16 -->_1 U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) :87 840.00/297.16 840.00/297.16 88: U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) 840.00/297.16 -->_1 U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) :88 840.00/297.16 -->_1 U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) :87 840.00/297.16 840.00/297.16 89: U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) 840.00/297.16 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) :90 840.00/297.16 -->_1 U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) :89 840.00/297.16 840.00/297.16 90: U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) 840.00/297.16 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) :90 840.00/297.16 -->_1 U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) :89 840.00/297.16 840.00/297.16 91: U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) 840.00/297.16 -->_1 U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) :92 840.00/297.16 -->_1 U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) :91 840.00/297.16 840.00/297.16 92: U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) 840.00/297.16 -->_1 U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) :92 840.00/297.16 -->_1 U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) :91 840.00/297.16 840.00/297.16 93: U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) 840.00/297.16 -->_1 U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) :94 840.00/297.16 -->_1 U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) :93 840.00/297.16 840.00/297.16 94: U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) 840.00/297.16 -->_1 U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) :94 840.00/297.16 -->_1 U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) :93 840.00/297.16 840.00/297.16 95: U23^#(mark(X)) -> c_94(U23^#(X)) 840.00/297.16 -->_1 U23^#(ok(X)) -> c_95(U23^#(X)) :96 840.00/297.16 -->_1 U23^#(mark(X)) -> c_94(U23^#(X)) :95 840.00/297.16 840.00/297.16 96: U23^#(ok(X)) -> c_95(U23^#(X)) 840.00/297.16 -->_1 U23^#(ok(X)) -> c_95(U23^#(X)) :96 840.00/297.16 -->_1 U23^#(mark(X)) -> c_94(U23^#(X)) :95 840.00/297.16 840.00/297.16 97: U71^#(mark(X)) -> c_122(U71^#(X)) 840.00/297.16 -->_1 U71^#(ok(X)) -> c_123(U71^#(X)) :98 840.00/297.16 -->_1 U71^#(mark(X)) -> c_122(U71^#(X)) :97 840.00/297.16 840.00/297.16 98: U71^#(ok(X)) -> c_123(U71^#(X)) 840.00/297.16 -->_1 U71^#(ok(X)) -> c_123(U71^#(X)) :98 840.00/297.16 -->_1 U71^#(mark(X)) -> c_122(U71^#(X)) :97 840.00/297.16 840.00/297.16 99: U61^#(mark(X)) -> c_120(U61^#(X)) 840.00/297.16 -->_1 U61^#(ok(X)) -> c_121(U61^#(X)) :100 840.00/297.16 -->_1 U61^#(mark(X)) -> c_120(U61^#(X)) :99 840.00/297.16 840.00/297.16 100: U61^#(ok(X)) -> c_121(U61^#(X)) 840.00/297.16 -->_1 U61^#(ok(X)) -> c_121(U61^#(X)) :100 840.00/297.16 -->_1 U61^#(mark(X)) -> c_120(U61^#(X)) :99 840.00/297.16 840.00/297.16 101: U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) 840.00/297.16 -->_1 U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) :102 840.00/297.16 -->_1 U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) :101 840.00/297.16 840.00/297.16 102: U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) 840.00/297.16 -->_1 U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) :102 840.00/297.16 -->_1 U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) :101 840.00/297.16 840.00/297.16 103: U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) 840.00/297.16 -->_1 U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) :104 840.00/297.16 -->_1 U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) :103 840.00/297.16 840.00/297.16 104: U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) 840.00/297.16 -->_1 U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) :104 840.00/297.16 -->_1 U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) :103 840.00/297.16 840.00/297.16 105: U33^#(mark(X)) -> c_101(U33^#(X)) 840.00/297.16 -->_1 U33^#(ok(X)) -> c_102(U33^#(X)) :106 840.00/297.16 -->_1 U33^#(mark(X)) -> c_101(U33^#(X)) :105 840.00/297.16 840.00/297.16 106: U33^#(ok(X)) -> c_102(U33^#(X)) 840.00/297.16 -->_1 U33^#(ok(X)) -> c_102(U33^#(X)) :106 840.00/297.16 -->_1 U33^#(mark(X)) -> c_101(U33^#(X)) :105 840.00/297.16 840.00/297.16 107: U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) 840.00/297.16 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_104(U41^#(X1, X2, X3)) :108 840.00/297.16 -->_1 U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) :107 840.00/297.16 840.00/297.16 108: U41^#(ok(X1), ok(X2), ok(X3)) -> c_104(U41^#(X1, X2, X3)) 840.00/297.16 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_104(U41^#(X1, X2, X3)) :108 840.00/297.16 -->_1 U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) :107 840.00/297.16 840.00/297.16 109: U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) 840.00/297.16 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_106(U42^#(X1, X2, X3)) :110 840.00/297.16 -->_1 U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) :109 840.00/297.16 840.00/297.16 110: U42^#(ok(X1), ok(X2), ok(X3)) -> c_106(U42^#(X1, X2, X3)) 840.00/297.16 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_106(U42^#(X1, X2, X3)) :110 840.00/297.16 -->_1 U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) :109 840.00/297.16 840.00/297.16 111: U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) 840.00/297.16 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_108(U43^#(X1, X2, X3)) :112 840.00/297.16 -->_1 U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) :111 840.00/297.16 840.00/297.16 112: U43^#(ok(X1), ok(X2), ok(X3)) -> c_108(U43^#(X1, X2, X3)) 840.00/297.16 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_108(U43^#(X1, X2, X3)) :112 840.00/297.16 -->_1 U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) :111 840.00/297.16 840.00/297.16 113: U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) 840.00/297.16 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_110(U44^#(X1, X2, X3)) :114 840.00/297.16 -->_1 U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) :113 840.00/297.16 840.00/297.16 114: U44^#(ok(X1), ok(X2), ok(X3)) -> c_110(U44^#(X1, X2, X3)) 840.00/297.16 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_110(U44^#(X1, X2, X3)) :114 840.00/297.16 -->_1 U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) :113 840.00/297.16 840.00/297.16 115: U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) 840.00/297.16 -->_1 U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) :116 840.00/297.16 -->_1 U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) :115 840.00/297.16 840.00/297.16 116: U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) 840.00/297.16 -->_1 U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) :116 840.00/297.16 -->_1 U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) :115 840.00/297.16 840.00/297.16 117: U46^#(mark(X)) -> c_113(U46^#(X)) 840.00/297.16 -->_1 U46^#(ok(X)) -> c_114(U46^#(X)) :118 840.00/297.16 -->_1 U46^#(mark(X)) -> c_113(U46^#(X)) :117 840.00/297.16 840.00/297.16 118: U46^#(ok(X)) -> c_114(U46^#(X)) 840.00/297.16 -->_1 U46^#(ok(X)) -> c_114(U46^#(X)) :118 840.00/297.16 -->_1 U46^#(mark(X)) -> c_113(U46^#(X)) :117 840.00/297.16 840.00/297.16 119: U52^#(mark(X)) -> c_118(U52^#(X)) 840.00/297.16 -->_1 U52^#(ok(X)) -> c_119(U52^#(X)) :120 840.00/297.16 -->_1 U52^#(mark(X)) -> c_118(U52^#(X)) :119 840.00/297.16 840.00/297.16 120: U52^#(ok(X)) -> c_119(U52^#(X)) 840.00/297.16 -->_1 U52^#(ok(X)) -> c_119(U52^#(X)) :120 840.00/297.16 -->_1 U52^#(mark(X)) -> c_118(U52^#(X)) :119 840.00/297.16 840.00/297.16 121: U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) 840.00/297.16 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_127(U82^#(X1, X2, X3)) :122 840.00/297.16 -->_1 U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) :121 840.00/297.16 840.00/297.16 122: U82^#(ok(X1), ok(X2), ok(X3)) -> c_127(U82^#(X1, X2, X3)) 840.00/297.16 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_127(U82^#(X1, X2, X3)) :122 840.00/297.16 -->_1 U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) :121 840.00/297.16 840.00/297.16 123: U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) 840.00/297.16 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_129(U83^#(X1, X2, X3)) :124 840.00/297.16 -->_1 U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) :123 840.00/297.16 840.00/297.16 124: U83^#(ok(X1), ok(X2), ok(X3)) -> c_129(U83^#(X1, X2, X3)) 840.00/297.16 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.16 c_129(U83^#(X1, X2, X3)) :124 840.00/297.16 -->_1 U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) :123 840.00/297.17 840.00/297.17 125: U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) 840.00/297.17 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_131(U84^#(X1, X2, X3)) :126 840.00/297.17 -->_1 U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) :125 840.00/297.17 840.00/297.17 126: U84^#(ok(X1), ok(X2), ok(X3)) -> c_131(U84^#(X1, X2, X3)) 840.00/297.17 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_131(U84^#(X1, X2, X3)) :126 840.00/297.17 -->_1 U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) :125 840.00/297.17 840.00/297.17 127: U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) 840.00/297.17 -->_1 U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) :128 840.00/297.17 -->_1 U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) :127 840.00/297.17 840.00/297.17 128: U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) 840.00/297.17 -->_1 U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) :128 840.00/297.17 -->_1 U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) :127 840.00/297.17 840.00/297.17 129: U86^#(mark(X)) -> c_134(U86^#(X)) 840.00/297.17 -->_1 U86^#(ok(X)) -> c_135(U86^#(X)) :130 840.00/297.17 -->_1 U86^#(mark(X)) -> c_134(U86^#(X)) :129 840.00/297.17 840.00/297.17 130: U86^#(ok(X)) -> c_135(U86^#(X)) 840.00/297.17 -->_1 U86^#(ok(X)) -> c_135(U86^#(X)) :130 840.00/297.17 -->_1 U86^#(mark(X)) -> c_134(U86^#(X)) :129 840.00/297.17 840.00/297.17 131: U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) 840.00/297.17 -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_137(U91^#(X1, X2, X3)) :132 840.00/297.17 -->_1 U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) :131 840.00/297.17 840.00/297.17 132: U91^#(ok(X1), ok(X2), ok(X3)) -> c_137(U91^#(X1, X2, X3)) 840.00/297.17 -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_137(U91^#(X1, X2, X3)) :132 840.00/297.17 -->_1 U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) :131 840.00/297.17 840.00/297.17 133: U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) 840.00/297.17 -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_139(U92^#(X1, X2, X3)) :134 840.00/297.17 -->_1 U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) :133 840.00/297.17 840.00/297.17 134: U92^#(ok(X1), ok(X2), ok(X3)) -> c_139(U92^#(X1, X2, X3)) 840.00/297.17 -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_139(U92^#(X1, X2, X3)) :134 840.00/297.17 -->_1 U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) :133 840.00/297.17 840.00/297.17 135: U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) 840.00/297.17 -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_141(U93^#(X1, X2, X3)) :136 840.00/297.17 -->_1 U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) :135 840.00/297.17 840.00/297.17 136: U93^#(ok(X1), ok(X2), ok(X3)) -> c_141(U93^#(X1, X2, X3)) 840.00/297.17 -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_141(U93^#(X1, X2, X3)) :136 840.00/297.17 -->_1 U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) :135 840.00/297.17 840.00/297.17 137: U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) 840.00/297.17 -->_1 U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) :138 840.00/297.17 -->_1 U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) :137 840.00/297.17 840.00/297.17 138: U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) 840.00/297.17 -->_1 U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) :138 840.00/297.17 -->_1 U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) :137 840.00/297.17 840.00/297.17 139: s^#(mark(X)) -> c_144(s^#(X)) 840.00/297.17 -->_1 s^#(ok(X)) -> c_145(s^#(X)) :140 840.00/297.17 -->_1 s^#(mark(X)) -> c_144(s^#(X)) :139 840.00/297.17 840.00/297.17 140: s^#(ok(X)) -> c_145(s^#(X)) 840.00/297.17 -->_1 s^#(ok(X)) -> c_145(s^#(X)) :140 840.00/297.17 -->_1 s^#(mark(X)) -> c_144(s^#(X)) :139 840.00/297.17 840.00/297.17 141: length^#(mark(X)) -> c_146(length^#(X)) 840.00/297.17 -->_1 length^#(ok(X)) -> c_147(length^#(X)) :142 840.00/297.17 -->_1 length^#(mark(X)) -> c_146(length^#(X)) :141 840.00/297.17 840.00/297.17 142: length^#(ok(X)) -> c_147(length^#(X)) 840.00/297.17 -->_1 length^#(ok(X)) -> c_147(length^#(X)) :142 840.00/297.17 -->_1 length^#(mark(X)) -> c_146(length^#(X)) :141 840.00/297.17 840.00/297.17 143: isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) 840.00/297.17 -->_1 isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) :143 840.00/297.17 840.00/297.17 144: isNatList^#(ok(X)) -> c_88(isNatList^#(X)) 840.00/297.17 -->_1 isNatList^#(ok(X)) -> c_88(isNatList^#(X)) :144 840.00/297.17 840.00/297.17 145: isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) 840.00/297.17 -->_1 isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) :145 840.00/297.17 840.00/297.17 146: isNat^#(ok(X)) -> c_96(isNat^#(X)) 840.00/297.17 -->_1 isNat^#(ok(X)) -> c_96(isNat^#(X)) :146 840.00/297.17 840.00/297.17 147: isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) 840.00/297.17 -->_1 isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) :147 840.00/297.17 840.00/297.17 148: proper^#(zeros()) -> c_148() 840.00/297.17 840.00/297.17 149: proper^#(cons(X1, X2)) -> 840.00/297.17 c_149(cons^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) :80 840.00/297.17 -->_1 cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) :79 840.00/297.17 840.00/297.17 150: proper^#(0()) -> c_150() 840.00/297.17 840.00/297.17 151: proper^#(U11(X1, X2)) -> c_151(U11^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) :82 840.00/297.17 -->_1 U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) :81 840.00/297.17 840.00/297.17 152: proper^#(tt()) -> c_152() 840.00/297.17 840.00/297.17 153: proper^#(U12(X1, X2)) -> c_153(U12^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) :84 840.00/297.17 -->_1 U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) :83 840.00/297.17 840.00/297.17 154: proper^#(isNatIListKind(X)) -> 840.00/297.17 c_154(isNatIListKind^#(proper(X))) 840.00/297.17 -->_1 isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) :143 840.00/297.17 840.00/297.17 155: proper^#(U13(X)) -> c_155(U13^#(proper(X))) 840.00/297.17 -->_1 U13^#(ok(X)) -> c_87(U13^#(X)) :86 840.00/297.17 -->_1 U13^#(mark(X)) -> c_86(U13^#(X)) :85 840.00/297.17 840.00/297.17 156: proper^#(isNatList(X)) -> c_156(isNatList^#(proper(X))) 840.00/297.17 -->_1 isNatList^#(ok(X)) -> c_88(isNatList^#(X)) :144 840.00/297.17 840.00/297.17 157: proper^#(U21(X1, X2)) -> c_157(U21^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) :92 840.00/297.17 -->_1 U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) :91 840.00/297.17 840.00/297.17 158: proper^#(U22(X1, X2)) -> c_158(U22^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) :94 840.00/297.17 -->_1 U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) :93 840.00/297.17 840.00/297.17 159: proper^#(isNatKind(X)) -> c_159(isNatKind^#(proper(X))) 840.00/297.17 -->_1 isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) :145 840.00/297.17 840.00/297.17 160: proper^#(U23(X)) -> c_160(U23^#(proper(X))) 840.00/297.17 -->_1 U23^#(ok(X)) -> c_95(U23^#(X)) :96 840.00/297.17 -->_1 U23^#(mark(X)) -> c_94(U23^#(X)) :95 840.00/297.17 840.00/297.17 161: proper^#(isNat(X)) -> c_161(isNat^#(proper(X))) 840.00/297.17 -->_1 isNat^#(ok(X)) -> c_96(isNat^#(X)) :146 840.00/297.17 840.00/297.17 162: proper^#(U31(X1, X2)) -> c_162(U31^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) :102 840.00/297.17 -->_1 U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) :101 840.00/297.17 840.00/297.17 163: proper^#(U32(X1, X2)) -> c_163(U32^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) :104 840.00/297.17 -->_1 U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) :103 840.00/297.17 840.00/297.17 164: proper^#(U33(X)) -> c_164(U33^#(proper(X))) 840.00/297.17 -->_1 U33^#(ok(X)) -> c_102(U33^#(X)) :106 840.00/297.17 -->_1 U33^#(mark(X)) -> c_101(U33^#(X)) :105 840.00/297.17 840.00/297.17 165: proper^#(U41(X1, X2, X3)) -> 840.00/297.17 c_165(U41^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U41^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_104(U41^#(X1, X2, X3)) :108 840.00/297.17 -->_1 U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) :107 840.00/297.17 840.00/297.17 166: proper^#(U42(X1, X2, X3)) -> 840.00/297.17 c_166(U42^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U42^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_106(U42^#(X1, X2, X3)) :110 840.00/297.17 -->_1 U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) :109 840.00/297.17 840.00/297.17 167: proper^#(U43(X1, X2, X3)) -> 840.00/297.17 c_167(U43^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U43^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_108(U43^#(X1, X2, X3)) :112 840.00/297.17 -->_1 U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) :111 840.00/297.17 840.00/297.17 168: proper^#(U44(X1, X2, X3)) -> 840.00/297.17 c_168(U44^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U44^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_110(U44^#(X1, X2, X3)) :114 840.00/297.17 -->_1 U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) :113 840.00/297.17 840.00/297.17 169: proper^#(U45(X1, X2)) -> c_169(U45^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) :116 840.00/297.17 -->_1 U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) :115 840.00/297.17 840.00/297.17 170: proper^#(U46(X)) -> c_170(U46^#(proper(X))) 840.00/297.17 -->_1 U46^#(ok(X)) -> c_114(U46^#(X)) :118 840.00/297.17 -->_1 U46^#(mark(X)) -> c_113(U46^#(X)) :117 840.00/297.17 840.00/297.17 171: proper^#(isNatIList(X)) -> c_171(isNatIList^#(proper(X))) 840.00/297.17 -->_1 isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) :147 840.00/297.17 840.00/297.17 172: proper^#(U51(X1, X2)) -> c_172(U51^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) :88 840.00/297.17 -->_1 U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) :87 840.00/297.17 840.00/297.17 173: proper^#(U52(X)) -> c_173(U52^#(proper(X))) 840.00/297.17 -->_1 U52^#(ok(X)) -> c_119(U52^#(X)) :120 840.00/297.17 -->_1 U52^#(mark(X)) -> c_118(U52^#(X)) :119 840.00/297.17 840.00/297.17 174: proper^#(U61(X)) -> c_174(U61^#(proper(X))) 840.00/297.17 -->_1 U61^#(ok(X)) -> c_121(U61^#(X)) :100 840.00/297.17 -->_1 U61^#(mark(X)) -> c_120(U61^#(X)) :99 840.00/297.17 840.00/297.17 175: proper^#(U71(X)) -> c_175(U71^#(proper(X))) 840.00/297.17 -->_1 U71^#(ok(X)) -> c_123(U71^#(X)) :98 840.00/297.17 -->_1 U71^#(mark(X)) -> c_122(U71^#(X)) :97 840.00/297.17 840.00/297.17 176: proper^#(U81(X1, X2, X3)) -> 840.00/297.17 c_176(U81^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) :90 840.00/297.17 -->_1 U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) :89 840.00/297.17 840.00/297.17 177: proper^#(U82(X1, X2, X3)) -> 840.00/297.17 c_177(U82^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U82^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_127(U82^#(X1, X2, X3)) :122 840.00/297.17 -->_1 U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) :121 840.00/297.17 840.00/297.17 178: proper^#(U83(X1, X2, X3)) -> 840.00/297.17 c_178(U83^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U83^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_129(U83^#(X1, X2, X3)) :124 840.00/297.17 -->_1 U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) :123 840.00/297.17 840.00/297.17 179: proper^#(U84(X1, X2, X3)) -> 840.00/297.17 c_179(U84^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U84^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_131(U84^#(X1, X2, X3)) :126 840.00/297.17 -->_1 U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) :125 840.00/297.17 840.00/297.17 180: proper^#(U85(X1, X2)) -> c_180(U85^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) :128 840.00/297.17 -->_1 U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) :127 840.00/297.17 840.00/297.17 181: proper^#(U86(X)) -> c_181(U86^#(proper(X))) 840.00/297.17 -->_1 U86^#(ok(X)) -> c_135(U86^#(X)) :130 840.00/297.17 -->_1 U86^#(mark(X)) -> c_134(U86^#(X)) :129 840.00/297.17 840.00/297.17 182: proper^#(U91(X1, X2, X3)) -> 840.00/297.17 c_182(U91^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U91^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_137(U91^#(X1, X2, X3)) :132 840.00/297.17 -->_1 U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) :131 840.00/297.17 840.00/297.17 183: proper^#(U92(X1, X2, X3)) -> 840.00/297.17 c_183(U92^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U92^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_139(U92^#(X1, X2, X3)) :134 840.00/297.17 -->_1 U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) :133 840.00/297.17 840.00/297.17 184: proper^#(U93(X1, X2, X3)) -> 840.00/297.17 c_184(U93^#(proper(X1), proper(X2), proper(X3))) 840.00/297.17 -->_1 U93^#(ok(X1), ok(X2), ok(X3)) -> 840.00/297.17 c_141(U93^#(X1, X2, X3)) :136 840.00/297.17 -->_1 U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) :135 840.00/297.17 840.00/297.17 185: proper^#(U94(X1, X2)) -> c_185(U94^#(proper(X1), proper(X2))) 840.00/297.17 -->_1 U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) :138 840.00/297.17 -->_1 U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) :137 840.00/297.17 840.00/297.17 186: proper^#(s(X)) -> c_186(s^#(proper(X))) 840.00/297.17 -->_1 s^#(ok(X)) -> c_145(s^#(X)) :140 840.00/297.17 -->_1 s^#(mark(X)) -> c_144(s^#(X)) :139 840.00/297.17 840.00/297.17 187: proper^#(length(X)) -> c_187(length^#(proper(X))) 840.00/297.17 -->_1 length^#(ok(X)) -> c_147(length^#(X)) :142 840.00/297.17 -->_1 length^#(mark(X)) -> c_146(length^#(X)) :141 840.00/297.17 840.00/297.17 188: proper^#(nil()) -> c_188() 840.00/297.17 840.00/297.17 189: top^#(mark(X)) -> c_189(top^#(proper(X))) 840.00/297.17 -->_1 top^#(ok(X)) -> c_190(top^#(active(X))) :190 840.00/297.17 -->_1 top^#(mark(X)) -> c_189(top^#(proper(X))) :189 840.00/297.17 840.00/297.17 190: top^#(ok(X)) -> c_190(top^#(active(X))) 840.00/297.17 -->_1 top^#(ok(X)) -> c_190(top^#(active(X))) :190 840.00/297.17 -->_1 top^#(mark(X)) -> c_189(top^#(proper(X))) :189 840.00/297.17 840.00/297.17 840.00/297.17 Only the nodes 840.00/297.17 {1,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,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,150,152,188,189,190} 840.00/297.17 are reachable from nodes 840.00/297.17 {1,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,118,119,120,121,122,123,124,125,126,127,128,129,130,131,132,133,134,135,136,137,138,139,140,141,142,143,144,145,146,147,148,150,152,188,189,190} 840.00/297.17 that start derivation from marked basic terms. The nodes not 840.00/297.17 reachable are removed from the problem. 840.00/297.17 840.00/297.17 We are left with following problem, upon which TcT provides the 840.00/297.17 certificate MAYBE. 840.00/297.17 840.00/297.17 Strict DPs: 840.00/297.17 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 840.00/297.17 , cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) 840.00/297.17 , cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) 840.00/297.17 , U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) 840.00/297.17 , U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) 840.00/297.17 , U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) 840.00/297.17 , U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) 840.00/297.17 , U13^#(mark(X)) -> c_86(U13^#(X)) 840.00/297.17 , U13^#(ok(X)) -> c_87(U13^#(X)) 840.00/297.17 , U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) 840.00/297.17 , U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) 840.00/297.17 , U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) 840.00/297.17 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) 840.00/297.17 , U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) 840.00/297.17 , U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) 840.00/297.17 , U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) 840.00/297.17 , U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) 840.00/297.17 , U23^#(mark(X)) -> c_94(U23^#(X)) 840.00/297.17 , U23^#(ok(X)) -> c_95(U23^#(X)) 840.00/297.17 , U71^#(mark(X)) -> c_122(U71^#(X)) 840.00/297.17 , U71^#(ok(X)) -> c_123(U71^#(X)) 840.00/297.17 , U61^#(mark(X)) -> c_120(U61^#(X)) 840.00/297.17 , U61^#(ok(X)) -> c_121(U61^#(X)) 840.00/297.17 , U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) 840.00/297.17 , U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) 840.00/297.17 , U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) 840.00/297.17 , U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) 840.00/297.17 , U33^#(mark(X)) -> c_101(U33^#(X)) 840.00/297.17 , U33^#(ok(X)) -> c_102(U33^#(X)) 840.00/297.17 , U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) 840.00/297.17 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_104(U41^#(X1, X2, X3)) 840.00/297.17 , U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) 840.00/297.17 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_106(U42^#(X1, X2, X3)) 840.00/297.17 , U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) 840.00/297.17 , U43^#(ok(X1), ok(X2), ok(X3)) -> c_108(U43^#(X1, X2, X3)) 840.00/297.17 , U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) 840.00/297.17 , U44^#(ok(X1), ok(X2), ok(X3)) -> c_110(U44^#(X1, X2, X3)) 840.00/297.17 , U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) 840.00/297.17 , U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) 840.00/297.17 , U46^#(mark(X)) -> c_113(U46^#(X)) 840.00/297.17 , U46^#(ok(X)) -> c_114(U46^#(X)) 840.00/297.17 , U52^#(mark(X)) -> c_118(U52^#(X)) 840.00/297.17 , U52^#(ok(X)) -> c_119(U52^#(X)) 840.00/297.17 , U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) 840.00/297.17 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_127(U82^#(X1, X2, X3)) 840.00/297.17 , U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) 840.00/297.17 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_129(U83^#(X1, X2, X3)) 840.00/297.17 , U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) 840.00/297.17 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_131(U84^#(X1, X2, X3)) 840.00/297.17 , U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) 840.00/297.17 , U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) 840.00/297.17 , U86^#(mark(X)) -> c_134(U86^#(X)) 840.00/297.17 , U86^#(ok(X)) -> c_135(U86^#(X)) 840.00/297.17 , U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) 840.00/297.17 , U91^#(ok(X1), ok(X2), ok(X3)) -> c_137(U91^#(X1, X2, X3)) 840.00/297.17 , U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) 840.00/297.17 , U92^#(ok(X1), ok(X2), ok(X3)) -> c_139(U92^#(X1, X2, X3)) 840.00/297.17 , U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) 840.00/297.17 , U93^#(ok(X1), ok(X2), ok(X3)) -> c_141(U93^#(X1, X2, X3)) 840.00/297.17 , U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) 840.00/297.17 , U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) 840.00/297.17 , s^#(mark(X)) -> c_144(s^#(X)) 840.00/297.17 , s^#(ok(X)) -> c_145(s^#(X)) 840.00/297.17 , length^#(mark(X)) -> c_146(length^#(X)) 840.00/297.17 , length^#(ok(X)) -> c_147(length^#(X)) 840.00/297.17 , isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) 840.00/297.17 , isNatList^#(ok(X)) -> c_88(isNatList^#(X)) 840.00/297.17 , isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) 840.00/297.17 , isNat^#(ok(X)) -> c_96(isNat^#(X)) 840.00/297.17 , isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) 840.00/297.17 , proper^#(zeros()) -> c_148() 840.00/297.17 , proper^#(0()) -> c_150() 840.00/297.17 , proper^#(tt()) -> c_152() 840.00/297.17 , proper^#(nil()) -> c_188() 840.00/297.17 , top^#(mark(X)) -> c_189(top^#(proper(X))) 840.00/297.17 , top^#(ok(X)) -> c_190(top^#(active(X))) } 840.00/297.17 Strict Trs: 840.00/297.17 { active(zeros()) -> mark(cons(0(), zeros())) 840.00/297.17 , active(cons(X1, X2)) -> cons(active(X1), X2) 840.00/297.17 , active(U11(X1, X2)) -> U11(active(X1), X2) 840.00/297.17 , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) 840.00/297.17 , active(U12(X1, X2)) -> U12(active(X1), X2) 840.00/297.17 , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) 840.00/297.17 , active(isNatIListKind(zeros())) -> mark(tt()) 840.00/297.17 , active(isNatIListKind(cons(V1, V2))) -> 840.00/297.17 mark(U51(isNatKind(V1), V2)) 840.00/297.17 , active(isNatIListKind(nil())) -> mark(tt()) 840.00/297.17 , active(U13(X)) -> U13(active(X)) 840.00/297.17 , active(U13(tt())) -> mark(tt()) 840.00/297.17 , active(isNatList(cons(V1, V2))) -> 840.00/297.17 mark(U81(isNatKind(V1), V1, V2)) 840.00/297.17 , active(isNatList(nil())) -> mark(tt()) 840.00/297.17 , active(U21(X1, X2)) -> U21(active(X1), X2) 840.00/297.17 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 840.00/297.17 , active(U22(X1, X2)) -> U22(active(X1), X2) 840.00/297.17 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 840.00/297.17 , active(isNatKind(0())) -> mark(tt()) 840.00/297.17 , active(isNatKind(s(V1))) -> mark(U71(isNatKind(V1))) 840.00/297.17 , active(isNatKind(length(V1))) -> mark(U61(isNatIListKind(V1))) 840.00/297.17 , active(U23(X)) -> U23(active(X)) 840.00/297.17 , active(U23(tt())) -> mark(tt()) 840.00/297.17 , active(isNat(0())) -> mark(tt()) 840.00/297.17 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 840.00/297.17 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 840.00/297.17 , active(U31(X1, X2)) -> U31(active(X1), X2) 840.00/297.17 , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) 840.00/297.17 , active(U32(X1, X2)) -> U32(active(X1), X2) 840.00/297.17 , active(U32(tt(), V)) -> mark(U33(isNatList(V))) 840.00/297.17 , active(U33(X)) -> U33(active(X)) 840.00/297.17 , active(U33(tt())) -> mark(tt()) 840.00/297.17 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 840.00/297.17 , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) 840.00/297.17 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 840.00/297.17 , active(U42(tt(), V1, V2)) -> 840.00/297.17 mark(U43(isNatIListKind(V2), V1, V2)) 840.00/297.17 , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) 840.00/297.17 , active(U43(tt(), V1, V2)) -> 840.00/297.17 mark(U44(isNatIListKind(V2), V1, V2)) 840.00/297.17 , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) 840.00/297.17 , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) 840.00/297.17 , active(U45(X1, X2)) -> U45(active(X1), X2) 840.00/297.17 , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) 840.00/297.17 , active(U46(X)) -> U46(active(X)) 840.00/297.17 , active(U46(tt())) -> mark(tt()) 840.00/297.17 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 840.00/297.17 , active(isNatIList(zeros())) -> mark(tt()) 840.00/297.17 , active(isNatIList(cons(V1, V2))) -> 840.00/297.17 mark(U41(isNatKind(V1), V1, V2)) 840.00/297.17 , active(U51(X1, X2)) -> U51(active(X1), X2) 840.00/297.17 , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) 840.00/297.17 , active(U52(X)) -> U52(active(X)) 840.00/297.17 , active(U52(tt())) -> mark(tt()) 840.00/297.17 , active(U61(X)) -> U61(active(X)) 840.00/297.17 , active(U61(tt())) -> mark(tt()) 840.00/297.17 , active(U71(X)) -> U71(active(X)) 840.00/297.17 , active(U71(tt())) -> mark(tt()) 840.00/297.17 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 840.00/297.17 , active(U81(tt(), V1, V2)) -> mark(U82(isNatKind(V1), V1, V2)) 840.00/297.17 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 840.00/297.17 , active(U82(tt(), V1, V2)) -> 840.00/297.17 mark(U83(isNatIListKind(V2), V1, V2)) 840.00/297.17 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 840.00/297.17 , active(U83(tt(), V1, V2)) -> 840.00/297.17 mark(U84(isNatIListKind(V2), V1, V2)) 840.00/297.17 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 840.00/297.17 , active(U84(tt(), V1, V2)) -> mark(U85(isNat(V1), V2)) 840.00/297.17 , active(U85(X1, X2)) -> U85(active(X1), X2) 840.00/297.17 , active(U85(tt(), V2)) -> mark(U86(isNatList(V2))) 840.00/297.17 , active(U86(X)) -> U86(active(X)) 840.00/297.17 , active(U86(tt())) -> mark(tt()) 840.00/297.17 , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) 840.00/297.17 , active(U91(tt(), L, N)) -> mark(U92(isNatIListKind(L), L, N)) 840.00/297.17 , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) 840.00/297.17 , active(U92(tt(), L, N)) -> mark(U93(isNat(N), L, N)) 840.00/297.17 , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) 840.00/297.17 , active(U93(tt(), L, N)) -> mark(U94(isNatKind(N), L)) 840.00/297.17 , active(U94(X1, X2)) -> U94(active(X1), X2) 840.00/297.17 , active(U94(tt(), L)) -> mark(s(length(L))) 840.00/297.17 , active(s(X)) -> s(active(X)) 840.00/297.17 , active(length(X)) -> length(active(X)) 840.00/297.17 , active(length(cons(N, L))) -> mark(U91(isNatList(L), L, N)) 840.00/297.17 , active(length(nil())) -> mark(0()) 840.00/297.17 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 840.00/297.17 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 840.00/297.17 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 840.00/297.17 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 840.00/297.17 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 840.00/297.17 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 840.00/297.17 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 840.00/297.17 , U13(mark(X)) -> mark(U13(X)) 840.00/297.17 , U13(ok(X)) -> ok(U13(X)) 840.00/297.17 , isNatList(ok(X)) -> ok(isNatList(X)) 840.00/297.17 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 840.00/297.17 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 840.00/297.17 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 840.00/297.17 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 840.00/297.17 , isNatKind(ok(X)) -> ok(isNatKind(X)) 840.00/297.17 , U23(mark(X)) -> mark(U23(X)) 840.00/297.17 , U23(ok(X)) -> ok(U23(X)) 840.00/297.17 , isNat(ok(X)) -> ok(isNat(X)) 840.00/297.17 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 840.00/297.17 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 840.00/297.17 , U32(mark(X1), X2) -> mark(U32(X1, X2)) 840.00/297.17 , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) 840.00/297.17 , U33(mark(X)) -> mark(U33(X)) 840.00/297.17 , U33(ok(X)) -> ok(U33(X)) 840.00/297.17 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 840.00/297.17 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 840.00/297.17 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 840.00/297.17 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 840.00/297.17 , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) 840.00/297.17 , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) 840.00/297.17 , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) 840.00/297.17 , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) 840.00/297.17 , U45(mark(X1), X2) -> mark(U45(X1, X2)) 840.00/297.17 , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) 840.00/297.17 , U46(mark(X)) -> mark(U46(X)) 840.00/297.17 , U46(ok(X)) -> ok(U46(X)) 840.00/297.17 , isNatIList(ok(X)) -> ok(isNatIList(X)) 840.00/297.17 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 840.00/297.17 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 840.00/297.17 , U52(mark(X)) -> mark(U52(X)) 840.00/297.17 , U52(ok(X)) -> ok(U52(X)) 840.00/297.17 , U61(mark(X)) -> mark(U61(X)) 840.00/297.17 , U61(ok(X)) -> ok(U61(X)) 840.00/297.17 , U71(mark(X)) -> mark(U71(X)) 840.00/297.17 , U71(ok(X)) -> ok(U71(X)) 840.00/297.17 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 840.00/297.17 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 840.00/297.18 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 840.00/297.18 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 840.00/297.18 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 840.00/297.18 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 840.00/297.18 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 840.00/297.18 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 840.00/297.18 , U85(mark(X1), X2) -> mark(U85(X1, X2)) 840.00/297.18 , U85(ok(X1), ok(X2)) -> ok(U85(X1, X2)) 840.00/297.18 , U86(mark(X)) -> mark(U86(X)) 840.00/297.18 , U86(ok(X)) -> ok(U86(X)) 840.00/297.18 , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) 840.00/297.18 , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) 840.00/297.18 , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) 840.00/297.18 , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) 840.00/297.18 , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) 840.00/297.18 , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) 840.00/297.18 , U94(mark(X1), X2) -> mark(U94(X1, X2)) 840.00/297.18 , U94(ok(X1), ok(X2)) -> ok(U94(X1, X2)) 840.00/297.18 , s(mark(X)) -> mark(s(X)) 840.00/297.18 , s(ok(X)) -> ok(s(X)) 840.00/297.18 , length(mark(X)) -> mark(length(X)) 840.00/297.18 , length(ok(X)) -> ok(length(X)) 840.00/297.18 , proper(zeros()) -> ok(zeros()) 840.00/297.18 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 840.00/297.18 , proper(0()) -> ok(0()) 840.00/297.18 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 840.00/297.18 , proper(tt()) -> ok(tt()) 840.00/297.18 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 840.00/297.18 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 840.00/297.18 , proper(U13(X)) -> U13(proper(X)) 840.00/297.18 , proper(isNatList(X)) -> isNatList(proper(X)) 840.00/297.18 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 840.00/297.18 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 840.00/297.18 , proper(isNatKind(X)) -> isNatKind(proper(X)) 840.00/297.18 , proper(U23(X)) -> U23(proper(X)) 840.00/297.18 , proper(isNat(X)) -> isNat(proper(X)) 840.00/297.18 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 840.00/297.18 , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) 840.00/297.18 , proper(U33(X)) -> U33(proper(X)) 840.00/297.18 , proper(U41(X1, X2, X3)) -> 840.00/297.18 U41(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U42(X1, X2, X3)) -> 840.00/297.18 U42(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U43(X1, X2, X3)) -> 840.00/297.18 U43(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U44(X1, X2, X3)) -> 840.00/297.18 U44(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) 840.00/297.18 , proper(U46(X)) -> U46(proper(X)) 840.00/297.18 , proper(isNatIList(X)) -> isNatIList(proper(X)) 840.00/297.18 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 840.00/297.18 , proper(U52(X)) -> U52(proper(X)) 840.00/297.18 , proper(U61(X)) -> U61(proper(X)) 840.00/297.18 , proper(U71(X)) -> U71(proper(X)) 840.00/297.18 , proper(U81(X1, X2, X3)) -> 840.00/297.18 U81(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U82(X1, X2, X3)) -> 840.00/297.18 U82(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U83(X1, X2, X3)) -> 840.00/297.18 U83(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U84(X1, X2, X3)) -> 840.00/297.18 U84(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U85(X1, X2)) -> U85(proper(X1), proper(X2)) 840.00/297.18 , proper(U86(X)) -> U86(proper(X)) 840.00/297.18 , proper(U91(X1, X2, X3)) -> 840.00/297.18 U91(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U92(X1, X2, X3)) -> 840.00/297.18 U92(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U93(X1, X2, X3)) -> 840.00/297.18 U93(proper(X1), proper(X2), proper(X3)) 840.00/297.18 , proper(U94(X1, X2)) -> U94(proper(X1), proper(X2)) 840.00/297.18 , proper(s(X)) -> s(proper(X)) 840.00/297.18 , proper(length(X)) -> length(proper(X)) 840.00/297.18 , proper(nil()) -> ok(nil()) 840.00/297.18 , top(mark(X)) -> top(proper(X)) 840.00/297.18 , top(ok(X)) -> top(active(X)) } 840.00/297.18 Obligation: 840.00/297.18 runtime complexity 840.00/297.18 Answer: 840.00/297.18 MAYBE 840.00/297.18 840.00/297.18 We estimate the number of application of {1,71,72,73,74} by 840.00/297.18 applications of Pre({1,71,72,73,74}) = {}. Here rules are labeled 840.00/297.18 as follows: 840.00/297.18 840.00/297.18 DPs: 840.00/297.18 { 1: active^#(zeros()) -> c_1(cons^#(0(), zeros())) 840.00/297.18 , 2: cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) 840.00/297.18 , 3: cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) 840.00/297.18 , 4: U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) 840.00/297.18 , 5: U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) 840.00/297.18 , 6: U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) 840.00/297.18 , 7: U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) 840.00/297.18 , 8: U13^#(mark(X)) -> c_86(U13^#(X)) 840.00/297.18 , 9: U13^#(ok(X)) -> c_87(U13^#(X)) 840.00/297.18 , 10: U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) 840.00/297.18 , 11: U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) 840.00/297.18 , 12: U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) 840.00/297.18 , 13: U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) 840.00/297.18 , 14: U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) 840.00/297.18 , 15: U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) 840.00/297.18 , 16: U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) 840.00/297.18 , 17: U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) 840.00/297.18 , 18: U23^#(mark(X)) -> c_94(U23^#(X)) 840.00/297.18 , 19: U23^#(ok(X)) -> c_95(U23^#(X)) 840.00/297.18 , 20: U71^#(mark(X)) -> c_122(U71^#(X)) 840.00/297.18 , 21: U71^#(ok(X)) -> c_123(U71^#(X)) 840.00/297.18 , 22: U61^#(mark(X)) -> c_120(U61^#(X)) 840.00/297.18 , 23: U61^#(ok(X)) -> c_121(U61^#(X)) 840.00/297.18 , 24: U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) 840.00/297.18 , 25: U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) 840.00/297.18 , 26: U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) 840.00/297.18 , 27: U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) 840.00/297.18 , 28: U33^#(mark(X)) -> c_101(U33^#(X)) 840.00/297.18 , 29: U33^#(ok(X)) -> c_102(U33^#(X)) 840.00/297.18 , 30: U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) 840.00/297.18 , 31: U41^#(ok(X1), ok(X2), ok(X3)) -> c_104(U41^#(X1, X2, X3)) 840.00/297.18 , 32: U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) 840.00/297.18 , 33: U42^#(ok(X1), ok(X2), ok(X3)) -> c_106(U42^#(X1, X2, X3)) 840.00/297.18 , 34: U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) 840.00/297.18 , 35: U43^#(ok(X1), ok(X2), ok(X3)) -> c_108(U43^#(X1, X2, X3)) 840.00/297.18 , 36: U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) 840.00/297.18 , 37: U44^#(ok(X1), ok(X2), ok(X3)) -> c_110(U44^#(X1, X2, X3)) 840.00/297.18 , 38: U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) 840.00/297.18 , 39: U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) 840.00/297.18 , 40: U46^#(mark(X)) -> c_113(U46^#(X)) 840.00/297.18 , 41: U46^#(ok(X)) -> c_114(U46^#(X)) 840.00/297.18 , 42: U52^#(mark(X)) -> c_118(U52^#(X)) 840.00/297.18 , 43: U52^#(ok(X)) -> c_119(U52^#(X)) 840.00/297.18 , 44: U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) 840.00/297.18 , 45: U82^#(ok(X1), ok(X2), ok(X3)) -> c_127(U82^#(X1, X2, X3)) 840.00/297.18 , 46: U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) 840.00/297.18 , 47: U83^#(ok(X1), ok(X2), ok(X3)) -> c_129(U83^#(X1, X2, X3)) 840.00/297.18 , 48: U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) 840.00/297.18 , 49: U84^#(ok(X1), ok(X2), ok(X3)) -> c_131(U84^#(X1, X2, X3)) 840.00/297.18 , 50: U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) 840.00/297.18 , 51: U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) 840.00/297.18 , 52: U86^#(mark(X)) -> c_134(U86^#(X)) 840.00/297.18 , 53: U86^#(ok(X)) -> c_135(U86^#(X)) 840.00/297.18 , 54: U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) 840.00/297.18 , 55: U91^#(ok(X1), ok(X2), ok(X3)) -> c_137(U91^#(X1, X2, X3)) 840.00/297.18 , 56: U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) 840.00/297.18 , 57: U92^#(ok(X1), ok(X2), ok(X3)) -> c_139(U92^#(X1, X2, X3)) 840.00/297.18 , 58: U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) 840.00/297.18 , 59: U93^#(ok(X1), ok(X2), ok(X3)) -> c_141(U93^#(X1, X2, X3)) 840.00/297.18 , 60: U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) 840.00/297.18 , 61: U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) 840.00/297.18 , 62: s^#(mark(X)) -> c_144(s^#(X)) 840.00/297.18 , 63: s^#(ok(X)) -> c_145(s^#(X)) 840.00/297.18 , 64: length^#(mark(X)) -> c_146(length^#(X)) 840.00/297.18 , 65: length^#(ok(X)) -> c_147(length^#(X)) 840.00/297.18 , 66: isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) 840.00/297.18 , 67: isNatList^#(ok(X)) -> c_88(isNatList^#(X)) 840.00/297.18 , 68: isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) 840.00/297.18 , 69: isNat^#(ok(X)) -> c_96(isNat^#(X)) 840.00/297.18 , 70: isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) 840.00/297.18 , 71: proper^#(zeros()) -> c_148() 840.00/297.18 , 72: proper^#(0()) -> c_150() 840.00/297.18 , 73: proper^#(tt()) -> c_152() 840.00/297.18 , 74: proper^#(nil()) -> c_188() 840.00/297.18 , 75: top^#(mark(X)) -> c_189(top^#(proper(X))) 840.00/297.18 , 76: top^#(ok(X)) -> c_190(top^#(active(X))) } 840.00/297.18 840.00/297.18 We are left with following problem, upon which TcT provides the 840.00/297.18 certificate MAYBE. 840.00/297.18 840.00/297.18 Strict DPs: 840.00/297.18 { cons^#(mark(X1), X2) -> c_79(cons^#(X1, X2)) 840.00/297.18 , cons^#(ok(X1), ok(X2)) -> c_80(cons^#(X1, X2)) 840.00/297.18 , U11^#(mark(X1), X2) -> c_81(U11^#(X1, X2)) 840.00/297.18 , U11^#(ok(X1), ok(X2)) -> c_82(U11^#(X1, X2)) 840.00/297.18 , U12^#(mark(X1), X2) -> c_83(U12^#(X1, X2)) 840.00/297.18 , U12^#(ok(X1), ok(X2)) -> c_84(U12^#(X1, X2)) 840.00/297.18 , U13^#(mark(X)) -> c_86(U13^#(X)) 840.00/297.18 , U13^#(ok(X)) -> c_87(U13^#(X)) 840.00/297.18 , U51^#(mark(X1), X2) -> c_116(U51^#(X1, X2)) 840.00/297.18 , U51^#(ok(X1), ok(X2)) -> c_117(U51^#(X1, X2)) 840.00/297.18 , U81^#(mark(X1), X2, X3) -> c_124(U81^#(X1, X2, X3)) 840.00/297.18 , U81^#(ok(X1), ok(X2), ok(X3)) -> c_125(U81^#(X1, X2, X3)) 840.00/297.18 , U21^#(mark(X1), X2) -> c_89(U21^#(X1, X2)) 840.00/297.18 , U21^#(ok(X1), ok(X2)) -> c_90(U21^#(X1, X2)) 840.00/297.18 , U22^#(mark(X1), X2) -> c_91(U22^#(X1, X2)) 840.00/297.18 , U22^#(ok(X1), ok(X2)) -> c_92(U22^#(X1, X2)) 840.00/297.18 , U23^#(mark(X)) -> c_94(U23^#(X)) 840.00/297.18 , U23^#(ok(X)) -> c_95(U23^#(X)) 840.00/297.18 , U71^#(mark(X)) -> c_122(U71^#(X)) 840.00/297.18 , U71^#(ok(X)) -> c_123(U71^#(X)) 840.00/297.18 , U61^#(mark(X)) -> c_120(U61^#(X)) 840.00/297.18 , U61^#(ok(X)) -> c_121(U61^#(X)) 840.00/297.18 , U31^#(mark(X1), X2) -> c_97(U31^#(X1, X2)) 840.00/297.18 , U31^#(ok(X1), ok(X2)) -> c_98(U31^#(X1, X2)) 840.00/297.18 , U32^#(mark(X1), X2) -> c_99(U32^#(X1, X2)) 840.00/297.18 , U32^#(ok(X1), ok(X2)) -> c_100(U32^#(X1, X2)) 840.00/297.18 , U33^#(mark(X)) -> c_101(U33^#(X)) 840.00/297.18 , U33^#(ok(X)) -> c_102(U33^#(X)) 840.00/297.18 , U41^#(mark(X1), X2, X3) -> c_103(U41^#(X1, X2, X3)) 840.00/297.18 , U41^#(ok(X1), ok(X2), ok(X3)) -> c_104(U41^#(X1, X2, X3)) 840.00/297.18 , U42^#(mark(X1), X2, X3) -> c_105(U42^#(X1, X2, X3)) 840.00/297.18 , U42^#(ok(X1), ok(X2), ok(X3)) -> c_106(U42^#(X1, X2, X3)) 840.00/297.18 , U43^#(mark(X1), X2, X3) -> c_107(U43^#(X1, X2, X3)) 840.00/297.18 , U43^#(ok(X1), ok(X2), ok(X3)) -> c_108(U43^#(X1, X2, X3)) 840.00/297.18 , U44^#(mark(X1), X2, X3) -> c_109(U44^#(X1, X2, X3)) 840.00/297.18 , U44^#(ok(X1), ok(X2), ok(X3)) -> c_110(U44^#(X1, X2, X3)) 840.00/297.18 , U45^#(mark(X1), X2) -> c_111(U45^#(X1, X2)) 840.00/297.18 , U45^#(ok(X1), ok(X2)) -> c_112(U45^#(X1, X2)) 840.00/297.18 , U46^#(mark(X)) -> c_113(U46^#(X)) 840.00/297.18 , U46^#(ok(X)) -> c_114(U46^#(X)) 840.00/297.18 , U52^#(mark(X)) -> c_118(U52^#(X)) 840.00/297.18 , U52^#(ok(X)) -> c_119(U52^#(X)) 840.00/297.18 , U82^#(mark(X1), X2, X3) -> c_126(U82^#(X1, X2, X3)) 840.00/297.18 , U82^#(ok(X1), ok(X2), ok(X3)) -> c_127(U82^#(X1, X2, X3)) 840.00/297.18 , U83^#(mark(X1), X2, X3) -> c_128(U83^#(X1, X2, X3)) 840.00/297.18 , U83^#(ok(X1), ok(X2), ok(X3)) -> c_129(U83^#(X1, X2, X3)) 840.00/297.18 , U84^#(mark(X1), X2, X3) -> c_130(U84^#(X1, X2, X3)) 840.00/297.18 , U84^#(ok(X1), ok(X2), ok(X3)) -> c_131(U84^#(X1, X2, X3)) 840.00/297.18 , U85^#(mark(X1), X2) -> c_132(U85^#(X1, X2)) 840.00/297.18 , U85^#(ok(X1), ok(X2)) -> c_133(U85^#(X1, X2)) 840.00/297.18 , U86^#(mark(X)) -> c_134(U86^#(X)) 840.00/297.18 , U86^#(ok(X)) -> c_135(U86^#(X)) 840.00/297.18 , U91^#(mark(X1), X2, X3) -> c_136(U91^#(X1, X2, X3)) 840.00/297.18 , U91^#(ok(X1), ok(X2), ok(X3)) -> c_137(U91^#(X1, X2, X3)) 840.00/297.18 , U92^#(mark(X1), X2, X3) -> c_138(U92^#(X1, X2, X3)) 840.00/297.18 , U92^#(ok(X1), ok(X2), ok(X3)) -> c_139(U92^#(X1, X2, X3)) 840.00/297.18 , U93^#(mark(X1), X2, X3) -> c_140(U93^#(X1, X2, X3)) 840.00/297.18 , U93^#(ok(X1), ok(X2), ok(X3)) -> c_141(U93^#(X1, X2, X3)) 840.00/297.18 , U94^#(mark(X1), X2) -> c_142(U94^#(X1, X2)) 840.00/297.18 , U94^#(ok(X1), ok(X2)) -> c_143(U94^#(X1, X2)) 840.00/297.18 , s^#(mark(X)) -> c_144(s^#(X)) 840.00/297.18 , s^#(ok(X)) -> c_145(s^#(X)) 840.00/297.18 , length^#(mark(X)) -> c_146(length^#(X)) 840.00/297.18 , length^#(ok(X)) -> c_147(length^#(X)) 840.00/297.18 , isNatIListKind^#(ok(X)) -> c_85(isNatIListKind^#(X)) 840.00/297.18 , isNatList^#(ok(X)) -> c_88(isNatList^#(X)) 840.00/297.18 , isNatKind^#(ok(X)) -> c_93(isNatKind^#(X)) 840.00/297.18 , isNat^#(ok(X)) -> c_96(isNat^#(X)) 840.00/297.18 , isNatIList^#(ok(X)) -> c_115(isNatIList^#(X)) 840.00/297.18 , top^#(mark(X)) -> c_189(top^#(proper(X))) 840.00/297.18 , top^#(ok(X)) -> c_190(top^#(active(X))) } 840.00/297.18 Strict Trs: 840.00/297.18 { active(zeros()) -> mark(cons(0(), zeros())) 840.00/297.18 , active(cons(X1, X2)) -> cons(active(X1), X2) 840.00/297.18 , active(U11(X1, X2)) -> U11(active(X1), X2) 840.00/297.18 , active(U11(tt(), V1)) -> mark(U12(isNatIListKind(V1), V1)) 840.00/297.18 , active(U12(X1, X2)) -> U12(active(X1), X2) 840.00/297.18 , active(U12(tt(), V1)) -> mark(U13(isNatList(V1))) 840.00/297.18 , active(isNatIListKind(zeros())) -> mark(tt()) 840.00/297.18 , active(isNatIListKind(cons(V1, V2))) -> 840.00/297.18 mark(U51(isNatKind(V1), V2)) 840.00/297.18 , active(isNatIListKind(nil())) -> mark(tt()) 840.00/297.18 , active(U13(X)) -> U13(active(X)) 840.00/297.18 , active(U13(tt())) -> mark(tt()) 840.00/297.18 , active(isNatList(cons(V1, V2))) -> 840.00/297.18 mark(U81(isNatKind(V1), V1, V2)) 840.00/297.18 , active(isNatList(nil())) -> mark(tt()) 840.00/297.18 , active(U21(X1, X2)) -> U21(active(X1), X2) 840.00/297.18 , active(U21(tt(), V1)) -> mark(U22(isNatKind(V1), V1)) 840.00/297.18 , active(U22(X1, X2)) -> U22(active(X1), X2) 840.00/297.18 , active(U22(tt(), V1)) -> mark(U23(isNat(V1))) 840.00/297.18 , active(isNatKind(0())) -> mark(tt()) 840.00/297.18 , active(isNatKind(s(V1))) -> mark(U71(isNatKind(V1))) 840.00/297.18 , active(isNatKind(length(V1))) -> mark(U61(isNatIListKind(V1))) 840.00/297.18 , active(U23(X)) -> U23(active(X)) 840.00/297.18 , active(U23(tt())) -> mark(tt()) 840.00/297.18 , active(isNat(0())) -> mark(tt()) 840.00/297.18 , active(isNat(s(V1))) -> mark(U21(isNatKind(V1), V1)) 840.00/297.18 , active(isNat(length(V1))) -> mark(U11(isNatIListKind(V1), V1)) 840.00/297.18 , active(U31(X1, X2)) -> U31(active(X1), X2) 840.00/297.18 , active(U31(tt(), V)) -> mark(U32(isNatIListKind(V), V)) 840.00/297.18 , active(U32(X1, X2)) -> U32(active(X1), X2) 840.00/297.18 , active(U32(tt(), V)) -> mark(U33(isNatList(V))) 840.00/297.18 , active(U33(X)) -> U33(active(X)) 840.00/297.18 , active(U33(tt())) -> mark(tt()) 840.00/297.18 , active(U41(X1, X2, X3)) -> U41(active(X1), X2, X3) 840.00/297.18 , active(U41(tt(), V1, V2)) -> mark(U42(isNatKind(V1), V1, V2)) 840.00/297.18 , active(U42(X1, X2, X3)) -> U42(active(X1), X2, X3) 840.00/297.18 , active(U42(tt(), V1, V2)) -> 840.00/297.18 mark(U43(isNatIListKind(V2), V1, V2)) 840.00/297.18 , active(U43(X1, X2, X3)) -> U43(active(X1), X2, X3) 840.00/297.18 , active(U43(tt(), V1, V2)) -> 840.00/297.18 mark(U44(isNatIListKind(V2), V1, V2)) 840.00/297.18 , active(U44(X1, X2, X3)) -> U44(active(X1), X2, X3) 840.00/297.18 , active(U44(tt(), V1, V2)) -> mark(U45(isNat(V1), V2)) 840.00/297.18 , active(U45(X1, X2)) -> U45(active(X1), X2) 840.00/297.18 , active(U45(tt(), V2)) -> mark(U46(isNatIList(V2))) 840.00/297.18 , active(U46(X)) -> U46(active(X)) 840.00/297.18 , active(U46(tt())) -> mark(tt()) 840.00/297.18 , active(isNatIList(V)) -> mark(U31(isNatIListKind(V), V)) 840.00/297.18 , active(isNatIList(zeros())) -> mark(tt()) 840.00/297.18 , active(isNatIList(cons(V1, V2))) -> 840.00/297.18 mark(U41(isNatKind(V1), V1, V2)) 840.00/297.18 , active(U51(X1, X2)) -> U51(active(X1), X2) 840.00/297.18 , active(U51(tt(), V2)) -> mark(U52(isNatIListKind(V2))) 840.00/297.18 , active(U52(X)) -> U52(active(X)) 840.00/297.18 , active(U52(tt())) -> mark(tt()) 840.00/297.18 , active(U61(X)) -> U61(active(X)) 840.00/297.18 , active(U61(tt())) -> mark(tt()) 840.00/297.18 , active(U71(X)) -> U71(active(X)) 840.00/297.18 , active(U71(tt())) -> mark(tt()) 840.00/297.18 , active(U81(X1, X2, X3)) -> U81(active(X1), X2, X3) 840.00/297.18 , active(U81(tt(), V1, V2)) -> mark(U82(isNatKind(V1), V1, V2)) 840.00/297.18 , active(U82(X1, X2, X3)) -> U82(active(X1), X2, X3) 840.00/297.18 , active(U82(tt(), V1, V2)) -> 840.00/297.18 mark(U83(isNatIListKind(V2), V1, V2)) 840.00/297.18 , active(U83(X1, X2, X3)) -> U83(active(X1), X2, X3) 840.00/297.18 , active(U83(tt(), V1, V2)) -> 840.00/297.18 mark(U84(isNatIListKind(V2), V1, V2)) 840.00/297.18 , active(U84(X1, X2, X3)) -> U84(active(X1), X2, X3) 840.00/297.18 , active(U84(tt(), V1, V2)) -> mark(U85(isNat(V1), V2)) 840.00/297.18 , active(U85(X1, X2)) -> U85(active(X1), X2) 840.00/297.18 , active(U85(tt(), V2)) -> mark(U86(isNatList(V2))) 840.00/297.18 , active(U86(X)) -> U86(active(X)) 840.00/297.18 , active(U86(tt())) -> mark(tt()) 840.00/297.18 , active(U91(X1, X2, X3)) -> U91(active(X1), X2, X3) 840.00/297.18 , active(U91(tt(), L, N)) -> mark(U92(isNatIListKind(L), L, N)) 840.00/297.18 , active(U92(X1, X2, X3)) -> U92(active(X1), X2, X3) 840.00/297.18 , active(U92(tt(), L, N)) -> mark(U93(isNat(N), L, N)) 840.00/297.18 , active(U93(X1, X2, X3)) -> U93(active(X1), X2, X3) 840.00/297.18 , active(U93(tt(), L, N)) -> mark(U94(isNatKind(N), L)) 840.00/297.18 , active(U94(X1, X2)) -> U94(active(X1), X2) 840.00/297.18 , active(U94(tt(), L)) -> mark(s(length(L))) 840.00/297.18 , active(s(X)) -> s(active(X)) 840.00/297.18 , active(length(X)) -> length(active(X)) 840.00/297.18 , active(length(cons(N, L))) -> mark(U91(isNatList(L), L, N)) 840.00/297.18 , active(length(nil())) -> mark(0()) 840.00/297.18 , cons(mark(X1), X2) -> mark(cons(X1, X2)) 840.00/297.18 , cons(ok(X1), ok(X2)) -> ok(cons(X1, X2)) 840.00/297.18 , U11(mark(X1), X2) -> mark(U11(X1, X2)) 840.00/297.19 , U11(ok(X1), ok(X2)) -> ok(U11(X1, X2)) 840.00/297.19 , U12(mark(X1), X2) -> mark(U12(X1, X2)) 840.00/297.19 , U12(ok(X1), ok(X2)) -> ok(U12(X1, X2)) 840.00/297.19 , isNatIListKind(ok(X)) -> ok(isNatIListKind(X)) 840.00/297.19 , U13(mark(X)) -> mark(U13(X)) 840.00/297.19 , U13(ok(X)) -> ok(U13(X)) 840.00/297.19 , isNatList(ok(X)) -> ok(isNatList(X)) 840.00/297.19 , U21(mark(X1), X2) -> mark(U21(X1, X2)) 840.00/297.19 , U21(ok(X1), ok(X2)) -> ok(U21(X1, X2)) 840.00/297.19 , U22(mark(X1), X2) -> mark(U22(X1, X2)) 840.00/297.19 , U22(ok(X1), ok(X2)) -> ok(U22(X1, X2)) 840.00/297.19 , isNatKind(ok(X)) -> ok(isNatKind(X)) 840.00/297.19 , U23(mark(X)) -> mark(U23(X)) 840.00/297.19 , U23(ok(X)) -> ok(U23(X)) 840.00/297.19 , isNat(ok(X)) -> ok(isNat(X)) 840.00/297.19 , U31(mark(X1), X2) -> mark(U31(X1, X2)) 840.00/297.19 , U31(ok(X1), ok(X2)) -> ok(U31(X1, X2)) 840.00/297.19 , U32(mark(X1), X2) -> mark(U32(X1, X2)) 840.00/297.19 , U32(ok(X1), ok(X2)) -> ok(U32(X1, X2)) 840.00/297.19 , U33(mark(X)) -> mark(U33(X)) 840.00/297.19 , U33(ok(X)) -> ok(U33(X)) 840.00/297.19 , U41(mark(X1), X2, X3) -> mark(U41(X1, X2, X3)) 840.00/297.19 , U41(ok(X1), ok(X2), ok(X3)) -> ok(U41(X1, X2, X3)) 840.00/297.19 , U42(mark(X1), X2, X3) -> mark(U42(X1, X2, X3)) 840.00/297.19 , U42(ok(X1), ok(X2), ok(X3)) -> ok(U42(X1, X2, X3)) 840.00/297.19 , U43(mark(X1), X2, X3) -> mark(U43(X1, X2, X3)) 840.00/297.19 , U43(ok(X1), ok(X2), ok(X3)) -> ok(U43(X1, X2, X3)) 840.00/297.19 , U44(mark(X1), X2, X3) -> mark(U44(X1, X2, X3)) 840.00/297.19 , U44(ok(X1), ok(X2), ok(X3)) -> ok(U44(X1, X2, X3)) 840.00/297.19 , U45(mark(X1), X2) -> mark(U45(X1, X2)) 840.00/297.19 , U45(ok(X1), ok(X2)) -> ok(U45(X1, X2)) 840.00/297.19 , U46(mark(X)) -> mark(U46(X)) 840.00/297.19 , U46(ok(X)) -> ok(U46(X)) 840.00/297.19 , isNatIList(ok(X)) -> ok(isNatIList(X)) 840.00/297.19 , U51(mark(X1), X2) -> mark(U51(X1, X2)) 840.00/297.19 , U51(ok(X1), ok(X2)) -> ok(U51(X1, X2)) 840.00/297.19 , U52(mark(X)) -> mark(U52(X)) 840.00/297.19 , U52(ok(X)) -> ok(U52(X)) 840.00/297.19 , U61(mark(X)) -> mark(U61(X)) 840.00/297.19 , U61(ok(X)) -> ok(U61(X)) 840.00/297.19 , U71(mark(X)) -> mark(U71(X)) 840.00/297.19 , U71(ok(X)) -> ok(U71(X)) 840.00/297.19 , U81(mark(X1), X2, X3) -> mark(U81(X1, X2, X3)) 840.00/297.19 , U81(ok(X1), ok(X2), ok(X3)) -> ok(U81(X1, X2, X3)) 840.00/297.19 , U82(mark(X1), X2, X3) -> mark(U82(X1, X2, X3)) 840.00/297.19 , U82(ok(X1), ok(X2), ok(X3)) -> ok(U82(X1, X2, X3)) 840.00/297.19 , U83(mark(X1), X2, X3) -> mark(U83(X1, X2, X3)) 840.00/297.19 , U83(ok(X1), ok(X2), ok(X3)) -> ok(U83(X1, X2, X3)) 840.00/297.19 , U84(mark(X1), X2, X3) -> mark(U84(X1, X2, X3)) 840.00/297.19 , U84(ok(X1), ok(X2), ok(X3)) -> ok(U84(X1, X2, X3)) 840.00/297.19 , U85(mark(X1), X2) -> mark(U85(X1, X2)) 840.00/297.19 , U85(ok(X1), ok(X2)) -> ok(U85(X1, X2)) 840.00/297.19 , U86(mark(X)) -> mark(U86(X)) 840.00/297.19 , U86(ok(X)) -> ok(U86(X)) 840.00/297.19 , U91(mark(X1), X2, X3) -> mark(U91(X1, X2, X3)) 840.00/297.19 , U91(ok(X1), ok(X2), ok(X3)) -> ok(U91(X1, X2, X3)) 840.00/297.19 , U92(mark(X1), X2, X3) -> mark(U92(X1, X2, X3)) 840.00/297.19 , U92(ok(X1), ok(X2), ok(X3)) -> ok(U92(X1, X2, X3)) 840.00/297.19 , U93(mark(X1), X2, X3) -> mark(U93(X1, X2, X3)) 840.00/297.19 , U93(ok(X1), ok(X2), ok(X3)) -> ok(U93(X1, X2, X3)) 840.00/297.19 , U94(mark(X1), X2) -> mark(U94(X1, X2)) 840.00/297.19 , U94(ok(X1), ok(X2)) -> ok(U94(X1, X2)) 840.00/297.19 , s(mark(X)) -> mark(s(X)) 840.00/297.19 , s(ok(X)) -> ok(s(X)) 840.00/297.19 , length(mark(X)) -> mark(length(X)) 840.00/297.19 , length(ok(X)) -> ok(length(X)) 840.00/297.19 , proper(zeros()) -> ok(zeros()) 840.00/297.19 , proper(cons(X1, X2)) -> cons(proper(X1), proper(X2)) 840.00/297.19 , proper(0()) -> ok(0()) 840.00/297.19 , proper(U11(X1, X2)) -> U11(proper(X1), proper(X2)) 840.00/297.19 , proper(tt()) -> ok(tt()) 840.00/297.19 , proper(U12(X1, X2)) -> U12(proper(X1), proper(X2)) 840.00/297.19 , proper(isNatIListKind(X)) -> isNatIListKind(proper(X)) 840.00/297.19 , proper(U13(X)) -> U13(proper(X)) 840.00/297.19 , proper(isNatList(X)) -> isNatList(proper(X)) 840.00/297.19 , proper(U21(X1, X2)) -> U21(proper(X1), proper(X2)) 840.00/297.19 , proper(U22(X1, X2)) -> U22(proper(X1), proper(X2)) 840.00/297.19 , proper(isNatKind(X)) -> isNatKind(proper(X)) 840.00/297.19 , proper(U23(X)) -> U23(proper(X)) 840.00/297.19 , proper(isNat(X)) -> isNat(proper(X)) 840.00/297.19 , proper(U31(X1, X2)) -> U31(proper(X1), proper(X2)) 840.00/297.19 , proper(U32(X1, X2)) -> U32(proper(X1), proper(X2)) 840.00/297.19 , proper(U33(X)) -> U33(proper(X)) 840.00/297.19 , proper(U41(X1, X2, X3)) -> 840.00/297.19 U41(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U42(X1, X2, X3)) -> 840.00/297.19 U42(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U43(X1, X2, X3)) -> 840.00/297.19 U43(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U44(X1, X2, X3)) -> 840.00/297.19 U44(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U45(X1, X2)) -> U45(proper(X1), proper(X2)) 840.00/297.19 , proper(U46(X)) -> U46(proper(X)) 840.00/297.19 , proper(isNatIList(X)) -> isNatIList(proper(X)) 840.00/297.19 , proper(U51(X1, X2)) -> U51(proper(X1), proper(X2)) 840.00/297.19 , proper(U52(X)) -> U52(proper(X)) 840.00/297.19 , proper(U61(X)) -> U61(proper(X)) 840.00/297.19 , proper(U71(X)) -> U71(proper(X)) 840.00/297.19 , proper(U81(X1, X2, X3)) -> 840.00/297.19 U81(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U82(X1, X2, X3)) -> 840.00/297.19 U82(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U83(X1, X2, X3)) -> 840.00/297.19 U83(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U84(X1, X2, X3)) -> 840.00/297.19 U84(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U85(X1, X2)) -> U85(proper(X1), proper(X2)) 840.00/297.19 , proper(U86(X)) -> U86(proper(X)) 840.00/297.19 , proper(U91(X1, X2, X3)) -> 840.00/297.19 U91(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U92(X1, X2, X3)) -> 840.00/297.19 U92(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U93(X1, X2, X3)) -> 840.00/297.19 U93(proper(X1), proper(X2), proper(X3)) 840.00/297.19 , proper(U94(X1, X2)) -> U94(proper(X1), proper(X2)) 840.00/297.19 , proper(s(X)) -> s(proper(X)) 840.00/297.19 , proper(length(X)) -> length(proper(X)) 840.00/297.19 , proper(nil()) -> ok(nil()) 840.00/297.19 , top(mark(X)) -> top(proper(X)) 840.00/297.19 , top(ok(X)) -> top(active(X)) } 840.00/297.19 Weak DPs: 840.00/297.19 { active^#(zeros()) -> c_1(cons^#(0(), zeros())) 840.00/297.19 , proper^#(zeros()) -> c_148() 840.00/297.19 , proper^#(0()) -> c_150() 840.00/297.19 , proper^#(tt()) -> c_152() 840.00/297.19 , proper^#(nil()) -> c_188() } 840.00/297.19 Obligation: 840.00/297.19 runtime complexity 840.00/297.19 Answer: 840.00/297.19 MAYBE 840.00/297.19 840.00/297.19 Empty strict component of the problem is NOT empty. 840.00/297.19 840.00/297.19 840.00/297.19 Arrrr.. 840.19/297.27 EOF