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