MAYBE 908.68/297.13 MAYBE 908.68/297.13 908.68/297.13 We are left with following problem, upon which TcT provides the 908.68/297.13 certificate MAYBE. 908.68/297.13 908.68/297.13 Strict Trs: 908.68/297.13 { a__zeros() -> cons(0(), zeros()) 908.68/297.13 , a__zeros() -> zeros() 908.68/297.13 , a__U11(X) -> U11(X) 908.68/297.13 , a__U11(tt()) -> tt() 908.68/297.13 , a__U21(X) -> U21(X) 908.68/297.13 , a__U21(tt()) -> tt() 908.68/297.13 , a__U31(X) -> U31(X) 908.68/297.13 , a__U31(tt()) -> tt() 908.68/297.13 , a__U41(X1, X2) -> U41(X1, X2) 908.68/297.13 , a__U41(tt(), V2) -> a__U42(a__isNatIList(V2)) 908.68/297.13 , a__U42(X) -> U42(X) 908.68/297.13 , a__U42(tt()) -> tt() 908.68/297.13 , a__isNatIList(V) -> a__U31(a__isNatList(V)) 908.68/297.13 , a__isNatIList(X) -> isNatIList(X) 908.68/297.13 , a__isNatIList(cons(V1, V2)) -> a__U41(a__isNat(V1), V2) 908.68/297.13 , a__isNatIList(zeros()) -> tt() 908.68/297.13 , a__U51(X1, X2) -> U51(X1, X2) 908.68/297.13 , a__U51(tt(), V2) -> a__U52(a__isNatList(V2)) 908.68/297.13 , a__U52(X) -> U52(X) 908.68/297.13 , a__U52(tt()) -> tt() 908.68/297.13 , a__isNatList(X) -> isNatList(X) 908.68/297.13 , a__isNatList(cons(V1, V2)) -> a__U51(a__isNat(V1), V2) 908.68/297.13 , a__isNatList(nil()) -> tt() 908.68/297.13 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 908.68/297.13 , a__U61(tt(), L, N) -> a__U62(a__isNat(N), L) 908.68/297.13 , a__U62(X1, X2) -> U62(X1, X2) 908.68/297.13 , a__U62(tt(), L) -> s(a__length(mark(L))) 908.68/297.13 , a__isNat(X) -> isNat(X) 908.68/297.13 , a__isNat(0()) -> tt() 908.68/297.13 , a__isNat(s(V1)) -> a__U21(a__isNat(V1)) 908.68/297.13 , a__isNat(length(V1)) -> a__U11(a__isNatList(V1)) 908.68/297.13 , a__length(X) -> length(X) 908.68/297.13 , a__length(cons(N, L)) -> a__U61(a__isNatList(L), L, N) 908.68/297.13 , a__length(nil()) -> 0() 908.68/297.13 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 908.68/297.13 , mark(0()) -> 0() 908.68/297.13 , mark(zeros()) -> a__zeros() 908.68/297.13 , mark(tt()) -> tt() 908.68/297.13 , mark(s(X)) -> s(mark(X)) 908.68/297.13 , mark(length(X)) -> a__length(mark(X)) 908.68/297.13 , mark(nil()) -> nil() 908.68/297.13 , mark(U11(X)) -> a__U11(mark(X)) 908.68/297.13 , mark(U21(X)) -> a__U21(mark(X)) 908.68/297.13 , mark(U31(X)) -> a__U31(mark(X)) 908.68/297.13 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 908.68/297.13 , mark(U42(X)) -> a__U42(mark(X)) 908.68/297.13 , mark(isNatIList(X)) -> a__isNatIList(X) 908.68/297.13 , mark(U51(X1, X2)) -> a__U51(mark(X1), X2) 908.68/297.13 , mark(U52(X)) -> a__U52(mark(X)) 908.68/297.13 , mark(isNatList(X)) -> a__isNatList(X) 908.68/297.13 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 908.68/297.13 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 908.68/297.13 , mark(isNat(X)) -> a__isNat(X) } 908.68/297.13 Obligation: 908.68/297.13 runtime complexity 908.68/297.14 Answer: 908.68/297.14 MAYBE 908.68/297.14 908.68/297.14 None of the processors succeeded. 908.68/297.14 908.68/297.14 Details of failed attempt(s): 908.68/297.14 ----------------------------- 908.68/297.14 1) 'With Problem ... (timeout of 297 seconds)' failed due to the 908.68/297.14 following reason: 908.68/297.14 908.68/297.14 Computation stopped due to timeout after 297.0 seconds. 908.68/297.14 908.68/297.14 2) 'Best' failed due to the following reason: 908.68/297.14 908.68/297.14 None of the processors succeeded. 908.68/297.14 908.68/297.14 Details of failed attempt(s): 908.68/297.14 ----------------------------- 908.68/297.14 1) 'With Problem ... (timeout of 148 seconds) (timeout of 297 908.68/297.14 seconds)' failed due to the following reason: 908.68/297.14 908.68/297.14 Computation stopped due to timeout after 148.0 seconds. 908.68/297.14 908.68/297.14 2) 'Fastest (timeout of 24 seconds) (timeout of 297 seconds)' 908.68/297.14 failed due to the following reason: 908.68/297.14 908.68/297.14 None of the processors succeeded. 908.68/297.14 908.68/297.14 Details of failed attempt(s): 908.68/297.14 ----------------------------- 908.68/297.14 1) 'Bounds with perSymbol-enrichment and initial automaton 'match'' 908.68/297.14 failed due to the following reason: 908.68/297.14 908.68/297.14 match-boundness of the problem could not be verified. 908.68/297.14 908.68/297.14 2) 'Bounds with minimal-enrichment and initial automaton 'match'' 908.68/297.14 failed due to the following reason: 908.68/297.14 908.68/297.14 match-boundness of the problem could not be verified. 908.68/297.14 908.68/297.14 908.68/297.14 3) 'Best' failed due to the following reason: 908.68/297.14 908.68/297.14 None of the processors succeeded. 908.68/297.14 908.68/297.14 Details of failed attempt(s): 908.68/297.14 ----------------------------- 908.68/297.14 1) 'Polynomial Path Order (PS) (timeout of 297 seconds)' failed due 908.68/297.14 to the following reason: 908.68/297.14 908.68/297.14 The processor is inapplicable, reason: 908.68/297.14 Processor only applicable for innermost runtime complexity analysis 908.68/297.14 908.68/297.14 2) 'bsearch-popstar (timeout of 297 seconds)' failed due to the 908.68/297.14 following reason: 908.68/297.14 908.68/297.14 The processor is inapplicable, reason: 908.68/297.14 Processor only applicable for innermost runtime complexity analysis 908.68/297.14 908.68/297.14 908.68/297.14 908.68/297.14 3) 'Weak Dependency Pairs (timeout of 297 seconds)' failed due to 908.68/297.14 the following reason: 908.68/297.14 908.68/297.14 We add the following weak dependency pairs: 908.68/297.14 908.68/297.14 Strict DPs: 908.68/297.14 { a__zeros^#() -> c_1() 908.68/297.14 , a__zeros^#() -> c_2() 908.68/297.14 , a__U11^#(X) -> c_3(X) 908.68/297.14 , a__U11^#(tt()) -> c_4() 908.68/297.14 , a__U21^#(X) -> c_5(X) 908.68/297.14 , a__U21^#(tt()) -> c_6() 908.68/297.14 , a__U31^#(X) -> c_7(X) 908.68/297.14 , a__U31^#(tt()) -> c_8() 908.68/297.14 , a__U41^#(X1, X2) -> c_9(X1, X2) 908.68/297.14 , a__U41^#(tt(), V2) -> c_10(a__U42^#(a__isNatIList(V2))) 908.68/297.14 , a__U42^#(X) -> c_11(X) 908.68/297.14 , a__U42^#(tt()) -> c_12() 908.68/297.14 , a__isNatIList^#(V) -> c_13(a__U31^#(a__isNatList(V))) 908.68/297.14 , a__isNatIList^#(X) -> c_14(X) 908.68/297.14 , a__isNatIList^#(cons(V1, V2)) -> c_15(a__U41^#(a__isNat(V1), V2)) 908.68/297.14 , a__isNatIList^#(zeros()) -> c_16() 908.68/297.14 , a__U51^#(X1, X2) -> c_17(X1, X2) 908.68/297.14 , a__U51^#(tt(), V2) -> c_18(a__U52^#(a__isNatList(V2))) 908.68/297.14 , a__U52^#(X) -> c_19(X) 908.68/297.14 , a__U52^#(tt()) -> c_20() 908.68/297.14 , a__isNatList^#(X) -> c_21(X) 908.68/297.14 , a__isNatList^#(cons(V1, V2)) -> c_22(a__U51^#(a__isNat(V1), V2)) 908.68/297.14 , a__isNatList^#(nil()) -> c_23() 908.68/297.14 , a__U61^#(X1, X2, X3) -> c_24(X1, X2, X3) 908.68/297.14 , a__U61^#(tt(), L, N) -> c_25(a__U62^#(a__isNat(N), L)) 908.68/297.14 , a__U62^#(X1, X2) -> c_26(X1, X2) 908.68/297.14 , a__U62^#(tt(), L) -> c_27(a__length^#(mark(L))) 908.68/297.14 , a__length^#(X) -> c_32(X) 908.68/297.14 , a__length^#(cons(N, L)) -> c_33(a__U61^#(a__isNatList(L), L, N)) 908.68/297.14 , a__length^#(nil()) -> c_34() 908.68/297.14 , a__isNat^#(X) -> c_28(X) 908.68/297.14 , a__isNat^#(0()) -> c_29() 908.68/297.14 , a__isNat^#(s(V1)) -> c_30(a__U21^#(a__isNat(V1))) 908.68/297.14 , a__isNat^#(length(V1)) -> c_31(a__U11^#(a__isNatList(V1))) 908.68/297.14 , mark^#(cons(X1, X2)) -> c_35(mark^#(X1), X2) 908.68/297.14 , mark^#(0()) -> c_36() 908.68/297.14 , mark^#(zeros()) -> c_37(a__zeros^#()) 908.68/297.14 , mark^#(tt()) -> c_38() 908.68/297.14 , mark^#(s(X)) -> c_39(mark^#(X)) 908.68/297.14 , mark^#(length(X)) -> c_40(a__length^#(mark(X))) 908.68/297.14 , mark^#(nil()) -> c_41() 908.68/297.14 , mark^#(U11(X)) -> c_42(a__U11^#(mark(X))) 908.68/297.14 , mark^#(U21(X)) -> c_43(a__U21^#(mark(X))) 908.68/297.14 , mark^#(U31(X)) -> c_44(a__U31^#(mark(X))) 908.68/297.14 , mark^#(U41(X1, X2)) -> c_45(a__U41^#(mark(X1), X2)) 908.68/297.14 , mark^#(U42(X)) -> c_46(a__U42^#(mark(X))) 908.68/297.14 , mark^#(isNatIList(X)) -> c_47(a__isNatIList^#(X)) 908.68/297.14 , mark^#(U51(X1, X2)) -> c_48(a__U51^#(mark(X1), X2)) 908.68/297.14 , mark^#(U52(X)) -> c_49(a__U52^#(mark(X))) 908.68/297.14 , mark^#(isNatList(X)) -> c_50(a__isNatList^#(X)) 908.68/297.14 , mark^#(U61(X1, X2, X3)) -> c_51(a__U61^#(mark(X1), X2, X3)) 908.68/297.14 , mark^#(U62(X1, X2)) -> c_52(a__U62^#(mark(X1), X2)) 908.68/297.14 , mark^#(isNat(X)) -> c_53(a__isNat^#(X)) } 908.68/297.14 908.68/297.14 and mark the set of starting terms. 908.68/297.14 908.68/297.14 We are left with following problem, upon which TcT provides the 908.68/297.14 certificate MAYBE. 908.68/297.14 908.68/297.14 Strict DPs: 908.68/297.14 { a__zeros^#() -> c_1() 908.68/297.14 , a__zeros^#() -> c_2() 908.68/297.14 , a__U11^#(X) -> c_3(X) 908.68/297.14 , a__U11^#(tt()) -> c_4() 908.68/297.14 , a__U21^#(X) -> c_5(X) 908.68/297.14 , a__U21^#(tt()) -> c_6() 908.68/297.14 , a__U31^#(X) -> c_7(X) 908.68/297.14 , a__U31^#(tt()) -> c_8() 908.68/297.14 , a__U41^#(X1, X2) -> c_9(X1, X2) 908.68/297.14 , a__U41^#(tt(), V2) -> c_10(a__U42^#(a__isNatIList(V2))) 908.68/297.14 , a__U42^#(X) -> c_11(X) 908.68/297.14 , a__U42^#(tt()) -> c_12() 908.68/297.14 , a__isNatIList^#(V) -> c_13(a__U31^#(a__isNatList(V))) 908.68/297.14 , a__isNatIList^#(X) -> c_14(X) 908.68/297.14 , a__isNatIList^#(cons(V1, V2)) -> c_15(a__U41^#(a__isNat(V1), V2)) 908.68/297.14 , a__isNatIList^#(zeros()) -> c_16() 908.68/297.14 , a__U51^#(X1, X2) -> c_17(X1, X2) 908.68/297.14 , a__U51^#(tt(), V2) -> c_18(a__U52^#(a__isNatList(V2))) 908.68/297.14 , a__U52^#(X) -> c_19(X) 908.68/297.14 , a__U52^#(tt()) -> c_20() 908.68/297.14 , a__isNatList^#(X) -> c_21(X) 908.68/297.14 , a__isNatList^#(cons(V1, V2)) -> c_22(a__U51^#(a__isNat(V1), V2)) 908.68/297.14 , a__isNatList^#(nil()) -> c_23() 908.68/297.14 , a__U61^#(X1, X2, X3) -> c_24(X1, X2, X3) 908.68/297.14 , a__U61^#(tt(), L, N) -> c_25(a__U62^#(a__isNat(N), L)) 908.68/297.14 , a__U62^#(X1, X2) -> c_26(X1, X2) 908.68/297.14 , a__U62^#(tt(), L) -> c_27(a__length^#(mark(L))) 908.68/297.14 , a__length^#(X) -> c_32(X) 908.68/297.14 , a__length^#(cons(N, L)) -> c_33(a__U61^#(a__isNatList(L), L, N)) 908.68/297.14 , a__length^#(nil()) -> c_34() 908.68/297.14 , a__isNat^#(X) -> c_28(X) 908.68/297.14 , a__isNat^#(0()) -> c_29() 908.68/297.14 , a__isNat^#(s(V1)) -> c_30(a__U21^#(a__isNat(V1))) 908.68/297.14 , a__isNat^#(length(V1)) -> c_31(a__U11^#(a__isNatList(V1))) 908.68/297.14 , mark^#(cons(X1, X2)) -> c_35(mark^#(X1), X2) 908.68/297.14 , mark^#(0()) -> c_36() 908.68/297.14 , mark^#(zeros()) -> c_37(a__zeros^#()) 908.68/297.14 , mark^#(tt()) -> c_38() 908.68/297.14 , mark^#(s(X)) -> c_39(mark^#(X)) 908.68/297.14 , mark^#(length(X)) -> c_40(a__length^#(mark(X))) 908.68/297.14 , mark^#(nil()) -> c_41() 908.68/297.14 , mark^#(U11(X)) -> c_42(a__U11^#(mark(X))) 908.68/297.14 , mark^#(U21(X)) -> c_43(a__U21^#(mark(X))) 908.68/297.14 , mark^#(U31(X)) -> c_44(a__U31^#(mark(X))) 908.68/297.14 , mark^#(U41(X1, X2)) -> c_45(a__U41^#(mark(X1), X2)) 908.68/297.14 , mark^#(U42(X)) -> c_46(a__U42^#(mark(X))) 908.68/297.14 , mark^#(isNatIList(X)) -> c_47(a__isNatIList^#(X)) 908.68/297.14 , mark^#(U51(X1, X2)) -> c_48(a__U51^#(mark(X1), X2)) 908.68/297.14 , mark^#(U52(X)) -> c_49(a__U52^#(mark(X))) 908.68/297.14 , mark^#(isNatList(X)) -> c_50(a__isNatList^#(X)) 908.68/297.14 , mark^#(U61(X1, X2, X3)) -> c_51(a__U61^#(mark(X1), X2, X3)) 908.68/297.14 , mark^#(U62(X1, X2)) -> c_52(a__U62^#(mark(X1), X2)) 908.68/297.14 , mark^#(isNat(X)) -> c_53(a__isNat^#(X)) } 908.68/297.14 Strict Trs: 908.68/297.14 { a__zeros() -> cons(0(), zeros()) 908.68/297.14 , a__zeros() -> zeros() 908.68/297.14 , a__U11(X) -> U11(X) 908.68/297.14 , a__U11(tt()) -> tt() 908.68/297.14 , a__U21(X) -> U21(X) 908.68/297.14 , a__U21(tt()) -> tt() 908.68/297.14 , a__U31(X) -> U31(X) 908.68/297.14 , a__U31(tt()) -> tt() 908.68/297.14 , a__U41(X1, X2) -> U41(X1, X2) 908.68/297.14 , a__U41(tt(), V2) -> a__U42(a__isNatIList(V2)) 908.68/297.14 , a__U42(X) -> U42(X) 908.68/297.14 , a__U42(tt()) -> tt() 908.68/297.14 , a__isNatIList(V) -> a__U31(a__isNatList(V)) 908.68/297.14 , a__isNatIList(X) -> isNatIList(X) 908.68/297.14 , a__isNatIList(cons(V1, V2)) -> a__U41(a__isNat(V1), V2) 908.68/297.14 , a__isNatIList(zeros()) -> tt() 908.68/297.14 , a__U51(X1, X2) -> U51(X1, X2) 908.68/297.14 , a__U51(tt(), V2) -> a__U52(a__isNatList(V2)) 908.68/297.14 , a__U52(X) -> U52(X) 908.68/297.14 , a__U52(tt()) -> tt() 908.68/297.14 , a__isNatList(X) -> isNatList(X) 908.68/297.14 , a__isNatList(cons(V1, V2)) -> a__U51(a__isNat(V1), V2) 908.68/297.14 , a__isNatList(nil()) -> tt() 908.68/297.14 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 908.68/297.14 , a__U61(tt(), L, N) -> a__U62(a__isNat(N), L) 908.68/297.14 , a__U62(X1, X2) -> U62(X1, X2) 908.68/297.14 , a__U62(tt(), L) -> s(a__length(mark(L))) 908.68/297.14 , a__isNat(X) -> isNat(X) 908.68/297.14 , a__isNat(0()) -> tt() 908.68/297.14 , a__isNat(s(V1)) -> a__U21(a__isNat(V1)) 908.68/297.14 , a__isNat(length(V1)) -> a__U11(a__isNatList(V1)) 908.68/297.14 , a__length(X) -> length(X) 908.68/297.14 , a__length(cons(N, L)) -> a__U61(a__isNatList(L), L, N) 908.68/297.14 , a__length(nil()) -> 0() 908.68/297.14 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 908.68/297.14 , mark(0()) -> 0() 908.68/297.14 , mark(zeros()) -> a__zeros() 908.68/297.14 , mark(tt()) -> tt() 908.68/297.14 , mark(s(X)) -> s(mark(X)) 908.68/297.14 , mark(length(X)) -> a__length(mark(X)) 908.68/297.14 , mark(nil()) -> nil() 908.68/297.14 , mark(U11(X)) -> a__U11(mark(X)) 908.68/297.14 , mark(U21(X)) -> a__U21(mark(X)) 908.68/297.14 , mark(U31(X)) -> a__U31(mark(X)) 908.68/297.14 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 908.68/297.14 , mark(U42(X)) -> a__U42(mark(X)) 908.68/297.14 , mark(isNatIList(X)) -> a__isNatIList(X) 908.68/297.14 , mark(U51(X1, X2)) -> a__U51(mark(X1), X2) 908.68/297.14 , mark(U52(X)) -> a__U52(mark(X)) 908.68/297.14 , mark(isNatList(X)) -> a__isNatList(X) 908.68/297.14 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 908.68/297.14 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 908.68/297.14 , mark(isNat(X)) -> a__isNat(X) } 908.68/297.14 Obligation: 908.68/297.14 runtime complexity 908.68/297.14 Answer: 908.68/297.14 MAYBE 908.68/297.14 908.68/297.14 We estimate the number of application of 908.68/297.14 {1,2,4,6,8,12,16,20,23,30,32,36,38,41} by applications of 908.68/297.14 Pre({1,2,4,6,8,12,16,20,23,30,32,36,38,41}) = 908.68/297.14 {3,5,7,9,10,11,13,14,17,18,19,21,24,26,27,28,31,33,34,35,37,39,40,42,43,44,46,47,49,50,53}. 908.68/297.14 Here rules are labeled as follows: 908.68/297.14 908.68/297.14 DPs: 908.68/297.14 { 1: a__zeros^#() -> c_1() 908.68/297.14 , 2: a__zeros^#() -> c_2() 908.68/297.14 , 3: a__U11^#(X) -> c_3(X) 908.68/297.14 , 4: a__U11^#(tt()) -> c_4() 908.68/297.14 , 5: a__U21^#(X) -> c_5(X) 908.68/297.14 , 6: a__U21^#(tt()) -> c_6() 908.68/297.14 , 7: a__U31^#(X) -> c_7(X) 908.68/297.14 , 8: a__U31^#(tt()) -> c_8() 908.68/297.14 , 9: a__U41^#(X1, X2) -> c_9(X1, X2) 908.68/297.14 , 10: a__U41^#(tt(), V2) -> c_10(a__U42^#(a__isNatIList(V2))) 908.68/297.14 , 11: a__U42^#(X) -> c_11(X) 908.68/297.14 , 12: a__U42^#(tt()) -> c_12() 908.68/297.14 , 13: a__isNatIList^#(V) -> c_13(a__U31^#(a__isNatList(V))) 908.68/297.14 , 14: a__isNatIList^#(X) -> c_14(X) 908.68/297.14 , 15: a__isNatIList^#(cons(V1, V2)) -> 908.68/297.14 c_15(a__U41^#(a__isNat(V1), V2)) 908.68/297.14 , 16: a__isNatIList^#(zeros()) -> c_16() 908.68/297.14 , 17: a__U51^#(X1, X2) -> c_17(X1, X2) 908.68/297.14 , 18: a__U51^#(tt(), V2) -> c_18(a__U52^#(a__isNatList(V2))) 908.68/297.14 , 19: a__U52^#(X) -> c_19(X) 908.68/297.14 , 20: a__U52^#(tt()) -> c_20() 908.68/297.14 , 21: a__isNatList^#(X) -> c_21(X) 908.68/297.14 , 22: a__isNatList^#(cons(V1, V2)) -> 908.68/297.14 c_22(a__U51^#(a__isNat(V1), V2)) 908.68/297.14 , 23: a__isNatList^#(nil()) -> c_23() 908.68/297.14 , 24: a__U61^#(X1, X2, X3) -> c_24(X1, X2, X3) 908.68/297.14 , 25: a__U61^#(tt(), L, N) -> c_25(a__U62^#(a__isNat(N), L)) 908.68/297.14 , 26: a__U62^#(X1, X2) -> c_26(X1, X2) 908.68/297.14 , 27: a__U62^#(tt(), L) -> c_27(a__length^#(mark(L))) 908.68/297.14 , 28: a__length^#(X) -> c_32(X) 908.68/297.14 , 29: a__length^#(cons(N, L)) -> 908.68/297.14 c_33(a__U61^#(a__isNatList(L), L, N)) 908.68/297.14 , 30: a__length^#(nil()) -> c_34() 908.68/297.14 , 31: a__isNat^#(X) -> c_28(X) 908.68/297.14 , 32: a__isNat^#(0()) -> c_29() 908.68/297.14 , 33: a__isNat^#(s(V1)) -> c_30(a__U21^#(a__isNat(V1))) 908.68/297.14 , 34: a__isNat^#(length(V1)) -> c_31(a__U11^#(a__isNatList(V1))) 908.68/297.14 , 35: mark^#(cons(X1, X2)) -> c_35(mark^#(X1), X2) 908.68/297.14 , 36: mark^#(0()) -> c_36() 908.68/297.14 , 37: mark^#(zeros()) -> c_37(a__zeros^#()) 908.68/297.14 , 38: mark^#(tt()) -> c_38() 908.68/297.14 , 39: mark^#(s(X)) -> c_39(mark^#(X)) 908.68/297.14 , 40: mark^#(length(X)) -> c_40(a__length^#(mark(X))) 908.68/297.14 , 41: mark^#(nil()) -> c_41() 908.68/297.14 , 42: mark^#(U11(X)) -> c_42(a__U11^#(mark(X))) 908.68/297.14 , 43: mark^#(U21(X)) -> c_43(a__U21^#(mark(X))) 908.68/297.14 , 44: mark^#(U31(X)) -> c_44(a__U31^#(mark(X))) 908.68/297.14 , 45: mark^#(U41(X1, X2)) -> c_45(a__U41^#(mark(X1), X2)) 908.68/297.14 , 46: mark^#(U42(X)) -> c_46(a__U42^#(mark(X))) 908.68/297.14 , 47: mark^#(isNatIList(X)) -> c_47(a__isNatIList^#(X)) 908.68/297.14 , 48: mark^#(U51(X1, X2)) -> c_48(a__U51^#(mark(X1), X2)) 908.68/297.14 , 49: mark^#(U52(X)) -> c_49(a__U52^#(mark(X))) 908.68/297.14 , 50: mark^#(isNatList(X)) -> c_50(a__isNatList^#(X)) 908.68/297.14 , 51: mark^#(U61(X1, X2, X3)) -> c_51(a__U61^#(mark(X1), X2, X3)) 908.68/297.14 , 52: mark^#(U62(X1, X2)) -> c_52(a__U62^#(mark(X1), X2)) 908.68/297.14 , 53: mark^#(isNat(X)) -> c_53(a__isNat^#(X)) } 908.68/297.14 908.68/297.14 We are left with following problem, upon which TcT provides the 908.68/297.14 certificate MAYBE. 908.68/297.14 908.68/297.14 Strict DPs: 908.68/297.14 { a__U11^#(X) -> c_3(X) 908.68/297.14 , a__U21^#(X) -> c_5(X) 908.68/297.14 , a__U31^#(X) -> c_7(X) 908.68/297.14 , a__U41^#(X1, X2) -> c_9(X1, X2) 908.68/297.14 , a__U41^#(tt(), V2) -> c_10(a__U42^#(a__isNatIList(V2))) 908.68/297.14 , a__U42^#(X) -> c_11(X) 908.68/297.14 , a__isNatIList^#(V) -> c_13(a__U31^#(a__isNatList(V))) 908.68/297.14 , a__isNatIList^#(X) -> c_14(X) 908.68/297.14 , a__isNatIList^#(cons(V1, V2)) -> c_15(a__U41^#(a__isNat(V1), V2)) 908.68/297.14 , a__U51^#(X1, X2) -> c_17(X1, X2) 908.68/297.14 , a__U51^#(tt(), V2) -> c_18(a__U52^#(a__isNatList(V2))) 908.68/297.14 , a__U52^#(X) -> c_19(X) 908.68/297.14 , a__isNatList^#(X) -> c_21(X) 908.68/297.14 , a__isNatList^#(cons(V1, V2)) -> c_22(a__U51^#(a__isNat(V1), V2)) 908.68/297.14 , a__U61^#(X1, X2, X3) -> c_24(X1, X2, X3) 908.68/297.14 , a__U61^#(tt(), L, N) -> c_25(a__U62^#(a__isNat(N), L)) 908.68/297.14 , a__U62^#(X1, X2) -> c_26(X1, X2) 908.68/297.14 , a__U62^#(tt(), L) -> c_27(a__length^#(mark(L))) 908.68/297.14 , a__length^#(X) -> c_32(X) 908.68/297.14 , a__length^#(cons(N, L)) -> c_33(a__U61^#(a__isNatList(L), L, N)) 908.68/297.14 , a__isNat^#(X) -> c_28(X) 908.68/297.14 , a__isNat^#(s(V1)) -> c_30(a__U21^#(a__isNat(V1))) 908.68/297.14 , a__isNat^#(length(V1)) -> c_31(a__U11^#(a__isNatList(V1))) 908.68/297.14 , mark^#(cons(X1, X2)) -> c_35(mark^#(X1), X2) 908.68/297.14 , mark^#(zeros()) -> c_37(a__zeros^#()) 908.68/297.14 , mark^#(s(X)) -> c_39(mark^#(X)) 908.68/297.14 , mark^#(length(X)) -> c_40(a__length^#(mark(X))) 908.68/297.14 , mark^#(U11(X)) -> c_42(a__U11^#(mark(X))) 908.68/297.14 , mark^#(U21(X)) -> c_43(a__U21^#(mark(X))) 908.68/297.14 , mark^#(U31(X)) -> c_44(a__U31^#(mark(X))) 908.68/297.14 , mark^#(U41(X1, X2)) -> c_45(a__U41^#(mark(X1), X2)) 908.68/297.14 , mark^#(U42(X)) -> c_46(a__U42^#(mark(X))) 908.68/297.14 , mark^#(isNatIList(X)) -> c_47(a__isNatIList^#(X)) 908.68/297.14 , mark^#(U51(X1, X2)) -> c_48(a__U51^#(mark(X1), X2)) 908.68/297.14 , mark^#(U52(X)) -> c_49(a__U52^#(mark(X))) 908.68/297.14 , mark^#(isNatList(X)) -> c_50(a__isNatList^#(X)) 908.68/297.14 , mark^#(U61(X1, X2, X3)) -> c_51(a__U61^#(mark(X1), X2, X3)) 908.68/297.14 , mark^#(U62(X1, X2)) -> c_52(a__U62^#(mark(X1), X2)) 908.68/297.14 , mark^#(isNat(X)) -> c_53(a__isNat^#(X)) } 908.68/297.14 Strict Trs: 908.68/297.14 { a__zeros() -> cons(0(), zeros()) 908.68/297.14 , a__zeros() -> zeros() 908.68/297.14 , a__U11(X) -> U11(X) 908.68/297.14 , a__U11(tt()) -> tt() 908.68/297.14 , a__U21(X) -> U21(X) 908.68/297.14 , a__U21(tt()) -> tt() 908.68/297.14 , a__U31(X) -> U31(X) 908.68/297.14 , a__U31(tt()) -> tt() 908.68/297.14 , a__U41(X1, X2) -> U41(X1, X2) 908.68/297.14 , a__U41(tt(), V2) -> a__U42(a__isNatIList(V2)) 908.68/297.14 , a__U42(X) -> U42(X) 908.68/297.14 , a__U42(tt()) -> tt() 908.68/297.14 , a__isNatIList(V) -> a__U31(a__isNatList(V)) 908.68/297.14 , a__isNatIList(X) -> isNatIList(X) 908.68/297.14 , a__isNatIList(cons(V1, V2)) -> a__U41(a__isNat(V1), V2) 908.68/297.14 , a__isNatIList(zeros()) -> tt() 908.68/297.14 , a__U51(X1, X2) -> U51(X1, X2) 908.68/297.14 , a__U51(tt(), V2) -> a__U52(a__isNatList(V2)) 908.68/297.14 , a__U52(X) -> U52(X) 908.68/297.14 , a__U52(tt()) -> tt() 908.68/297.14 , a__isNatList(X) -> isNatList(X) 908.68/297.14 , a__isNatList(cons(V1, V2)) -> a__U51(a__isNat(V1), V2) 908.68/297.14 , a__isNatList(nil()) -> tt() 908.68/297.14 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 908.68/297.14 , a__U61(tt(), L, N) -> a__U62(a__isNat(N), L) 908.68/297.14 , a__U62(X1, X2) -> U62(X1, X2) 908.68/297.14 , a__U62(tt(), L) -> s(a__length(mark(L))) 908.68/297.14 , a__isNat(X) -> isNat(X) 908.68/297.14 , a__isNat(0()) -> tt() 908.68/297.14 , a__isNat(s(V1)) -> a__U21(a__isNat(V1)) 908.68/297.14 , a__isNat(length(V1)) -> a__U11(a__isNatList(V1)) 908.68/297.14 , a__length(X) -> length(X) 908.68/297.14 , a__length(cons(N, L)) -> a__U61(a__isNatList(L), L, N) 908.68/297.14 , a__length(nil()) -> 0() 908.68/297.14 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 908.68/297.14 , mark(0()) -> 0() 908.68/297.14 , mark(zeros()) -> a__zeros() 908.68/297.14 , mark(tt()) -> tt() 908.68/297.14 , mark(s(X)) -> s(mark(X)) 908.68/297.14 , mark(length(X)) -> a__length(mark(X)) 908.68/297.14 , mark(nil()) -> nil() 908.68/297.14 , mark(U11(X)) -> a__U11(mark(X)) 908.68/297.14 , mark(U21(X)) -> a__U21(mark(X)) 908.68/297.14 , mark(U31(X)) -> a__U31(mark(X)) 908.68/297.14 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 908.68/297.14 , mark(U42(X)) -> a__U42(mark(X)) 908.68/297.14 , mark(isNatIList(X)) -> a__isNatIList(X) 908.68/297.14 , mark(U51(X1, X2)) -> a__U51(mark(X1), X2) 908.68/297.14 , mark(U52(X)) -> a__U52(mark(X)) 908.68/297.14 , mark(isNatList(X)) -> a__isNatList(X) 908.68/297.14 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 908.68/297.14 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 908.68/297.14 , mark(isNat(X)) -> a__isNat(X) } 908.68/297.14 Weak DPs: 908.68/297.14 { a__zeros^#() -> c_1() 908.68/297.14 , a__zeros^#() -> c_2() 908.68/297.14 , a__U11^#(tt()) -> c_4() 908.68/297.14 , a__U21^#(tt()) -> c_6() 908.68/297.14 , a__U31^#(tt()) -> c_8() 908.68/297.14 , a__U42^#(tt()) -> c_12() 908.68/297.14 , a__isNatIList^#(zeros()) -> c_16() 908.68/297.14 , a__U52^#(tt()) -> c_20() 908.68/297.14 , a__isNatList^#(nil()) -> c_23() 908.68/297.14 , a__length^#(nil()) -> c_34() 908.68/297.14 , a__isNat^#(0()) -> c_29() 908.68/297.14 , mark^#(0()) -> c_36() 908.68/297.14 , mark^#(tt()) -> c_38() 908.68/297.14 , mark^#(nil()) -> c_41() } 908.68/297.14 Obligation: 908.68/297.14 runtime complexity 908.68/297.14 Answer: 908.68/297.14 MAYBE 908.68/297.14 908.68/297.14 We estimate the number of application of {25} by applications of 908.68/297.14 Pre({25}) = {1,2,3,4,6,8,10,12,13,15,17,19,21,24,26}. Here rules 908.68/297.14 are labeled as follows: 908.68/297.14 908.68/297.14 DPs: 908.68/297.14 { 1: a__U11^#(X) -> c_3(X) 908.68/297.14 , 2: a__U21^#(X) -> c_5(X) 908.68/297.14 , 3: a__U31^#(X) -> c_7(X) 908.68/297.14 , 4: a__U41^#(X1, X2) -> c_9(X1, X2) 908.68/297.14 , 5: a__U41^#(tt(), V2) -> c_10(a__U42^#(a__isNatIList(V2))) 908.68/297.14 , 6: a__U42^#(X) -> c_11(X) 908.68/297.14 , 7: a__isNatIList^#(V) -> c_13(a__U31^#(a__isNatList(V))) 908.68/297.14 , 8: a__isNatIList^#(X) -> c_14(X) 908.68/297.14 , 9: a__isNatIList^#(cons(V1, V2)) -> 908.68/297.14 c_15(a__U41^#(a__isNat(V1), V2)) 908.68/297.14 , 10: a__U51^#(X1, X2) -> c_17(X1, X2) 908.68/297.14 , 11: a__U51^#(tt(), V2) -> c_18(a__U52^#(a__isNatList(V2))) 908.68/297.14 , 12: a__U52^#(X) -> c_19(X) 908.68/297.14 , 13: a__isNatList^#(X) -> c_21(X) 908.68/297.14 , 14: a__isNatList^#(cons(V1, V2)) -> 908.68/297.14 c_22(a__U51^#(a__isNat(V1), V2)) 908.68/297.14 , 15: a__U61^#(X1, X2, X3) -> c_24(X1, X2, X3) 908.68/297.14 , 16: a__U61^#(tt(), L, N) -> c_25(a__U62^#(a__isNat(N), L)) 908.68/297.14 , 17: a__U62^#(X1, X2) -> c_26(X1, X2) 908.68/297.14 , 18: a__U62^#(tt(), L) -> c_27(a__length^#(mark(L))) 908.68/297.14 , 19: a__length^#(X) -> c_32(X) 908.68/297.14 , 20: a__length^#(cons(N, L)) -> 908.68/297.14 c_33(a__U61^#(a__isNatList(L), L, N)) 908.68/297.14 , 21: a__isNat^#(X) -> c_28(X) 908.68/297.14 , 22: a__isNat^#(s(V1)) -> c_30(a__U21^#(a__isNat(V1))) 908.68/297.14 , 23: a__isNat^#(length(V1)) -> c_31(a__U11^#(a__isNatList(V1))) 908.68/297.14 , 24: mark^#(cons(X1, X2)) -> c_35(mark^#(X1), X2) 908.68/297.14 , 25: mark^#(zeros()) -> c_37(a__zeros^#()) 908.68/297.14 , 26: mark^#(s(X)) -> c_39(mark^#(X)) 908.68/297.14 , 27: mark^#(length(X)) -> c_40(a__length^#(mark(X))) 908.68/297.14 , 28: mark^#(U11(X)) -> c_42(a__U11^#(mark(X))) 908.68/297.14 , 29: mark^#(U21(X)) -> c_43(a__U21^#(mark(X))) 908.68/297.14 , 30: mark^#(U31(X)) -> c_44(a__U31^#(mark(X))) 908.68/297.14 , 31: mark^#(U41(X1, X2)) -> c_45(a__U41^#(mark(X1), X2)) 908.68/297.14 , 32: mark^#(U42(X)) -> c_46(a__U42^#(mark(X))) 908.68/297.14 , 33: mark^#(isNatIList(X)) -> c_47(a__isNatIList^#(X)) 908.68/297.14 , 34: mark^#(U51(X1, X2)) -> c_48(a__U51^#(mark(X1), X2)) 908.68/297.14 , 35: mark^#(U52(X)) -> c_49(a__U52^#(mark(X))) 908.68/297.14 , 36: mark^#(isNatList(X)) -> c_50(a__isNatList^#(X)) 908.68/297.14 , 37: mark^#(U61(X1, X2, X3)) -> c_51(a__U61^#(mark(X1), X2, X3)) 908.68/297.14 , 38: mark^#(U62(X1, X2)) -> c_52(a__U62^#(mark(X1), X2)) 908.68/297.14 , 39: mark^#(isNat(X)) -> c_53(a__isNat^#(X)) 908.68/297.14 , 40: a__zeros^#() -> c_1() 908.68/297.14 , 41: a__zeros^#() -> c_2() 908.68/297.14 , 42: a__U11^#(tt()) -> c_4() 908.68/297.14 , 43: a__U21^#(tt()) -> c_6() 908.68/297.14 , 44: a__U31^#(tt()) -> c_8() 908.68/297.14 , 45: a__U42^#(tt()) -> c_12() 908.68/297.14 , 46: a__isNatIList^#(zeros()) -> c_16() 908.68/297.14 , 47: a__U52^#(tt()) -> c_20() 908.68/297.14 , 48: a__isNatList^#(nil()) -> c_23() 908.68/297.14 , 49: a__length^#(nil()) -> c_34() 908.68/297.14 , 50: a__isNat^#(0()) -> c_29() 908.68/297.14 , 51: mark^#(0()) -> c_36() 908.68/297.14 , 52: mark^#(tt()) -> c_38() 908.68/297.14 , 53: mark^#(nil()) -> c_41() } 908.68/297.14 908.68/297.14 We are left with following problem, upon which TcT provides the 908.68/297.14 certificate MAYBE. 908.68/297.14 908.68/297.14 Strict DPs: 908.68/297.14 { a__U11^#(X) -> c_3(X) 908.68/297.14 , a__U21^#(X) -> c_5(X) 908.68/297.14 , a__U31^#(X) -> c_7(X) 908.68/297.14 , a__U41^#(X1, X2) -> c_9(X1, X2) 908.68/297.14 , a__U41^#(tt(), V2) -> c_10(a__U42^#(a__isNatIList(V2))) 908.68/297.14 , a__U42^#(X) -> c_11(X) 908.68/297.14 , a__isNatIList^#(V) -> c_13(a__U31^#(a__isNatList(V))) 908.68/297.14 , a__isNatIList^#(X) -> c_14(X) 908.68/297.14 , a__isNatIList^#(cons(V1, V2)) -> c_15(a__U41^#(a__isNat(V1), V2)) 908.68/297.14 , a__U51^#(X1, X2) -> c_17(X1, X2) 908.68/297.14 , a__U51^#(tt(), V2) -> c_18(a__U52^#(a__isNatList(V2))) 908.68/297.14 , a__U52^#(X) -> c_19(X) 908.68/297.14 , a__isNatList^#(X) -> c_21(X) 908.68/297.14 , a__isNatList^#(cons(V1, V2)) -> c_22(a__U51^#(a__isNat(V1), V2)) 908.68/297.14 , a__U61^#(X1, X2, X3) -> c_24(X1, X2, X3) 908.68/297.14 , a__U61^#(tt(), L, N) -> c_25(a__U62^#(a__isNat(N), L)) 908.68/297.14 , a__U62^#(X1, X2) -> c_26(X1, X2) 908.68/297.14 , a__U62^#(tt(), L) -> c_27(a__length^#(mark(L))) 908.68/297.14 , a__length^#(X) -> c_32(X) 908.68/297.14 , a__length^#(cons(N, L)) -> c_33(a__U61^#(a__isNatList(L), L, N)) 908.68/297.14 , a__isNat^#(X) -> c_28(X) 908.68/297.14 , a__isNat^#(s(V1)) -> c_30(a__U21^#(a__isNat(V1))) 908.68/297.14 , a__isNat^#(length(V1)) -> c_31(a__U11^#(a__isNatList(V1))) 908.68/297.14 , mark^#(cons(X1, X2)) -> c_35(mark^#(X1), X2) 908.68/297.14 , mark^#(s(X)) -> c_39(mark^#(X)) 908.68/297.14 , mark^#(length(X)) -> c_40(a__length^#(mark(X))) 908.68/297.14 , mark^#(U11(X)) -> c_42(a__U11^#(mark(X))) 908.68/297.14 , mark^#(U21(X)) -> c_43(a__U21^#(mark(X))) 908.68/297.14 , mark^#(U31(X)) -> c_44(a__U31^#(mark(X))) 908.68/297.14 , mark^#(U41(X1, X2)) -> c_45(a__U41^#(mark(X1), X2)) 908.68/297.14 , mark^#(U42(X)) -> c_46(a__U42^#(mark(X))) 908.68/297.14 , mark^#(isNatIList(X)) -> c_47(a__isNatIList^#(X)) 908.68/297.14 , mark^#(U51(X1, X2)) -> c_48(a__U51^#(mark(X1), X2)) 908.68/297.14 , mark^#(U52(X)) -> c_49(a__U52^#(mark(X))) 908.68/297.14 , mark^#(isNatList(X)) -> c_50(a__isNatList^#(X)) 908.68/297.14 , mark^#(U61(X1, X2, X3)) -> c_51(a__U61^#(mark(X1), X2, X3)) 908.68/297.14 , mark^#(U62(X1, X2)) -> c_52(a__U62^#(mark(X1), X2)) 908.68/297.14 , mark^#(isNat(X)) -> c_53(a__isNat^#(X)) } 908.68/297.14 Strict Trs: 908.68/297.14 { a__zeros() -> cons(0(), zeros()) 908.68/297.14 , a__zeros() -> zeros() 908.68/297.14 , a__U11(X) -> U11(X) 908.68/297.14 , a__U11(tt()) -> tt() 908.68/297.14 , a__U21(X) -> U21(X) 908.68/297.14 , a__U21(tt()) -> tt() 908.68/297.14 , a__U31(X) -> U31(X) 908.68/297.14 , a__U31(tt()) -> tt() 908.68/297.14 , a__U41(X1, X2) -> U41(X1, X2) 908.68/297.14 , a__U41(tt(), V2) -> a__U42(a__isNatIList(V2)) 908.68/297.14 , a__U42(X) -> U42(X) 908.68/297.14 , a__U42(tt()) -> tt() 908.68/297.14 , a__isNatIList(V) -> a__U31(a__isNatList(V)) 908.68/297.14 , a__isNatIList(X) -> isNatIList(X) 908.68/297.14 , a__isNatIList(cons(V1, V2)) -> a__U41(a__isNat(V1), V2) 908.68/297.14 , a__isNatIList(zeros()) -> tt() 908.68/297.14 , a__U51(X1, X2) -> U51(X1, X2) 908.68/297.14 , a__U51(tt(), V2) -> a__U52(a__isNatList(V2)) 908.68/297.14 , a__U52(X) -> U52(X) 908.68/297.14 , a__U52(tt()) -> tt() 908.68/297.14 , a__isNatList(X) -> isNatList(X) 908.68/297.14 , a__isNatList(cons(V1, V2)) -> a__U51(a__isNat(V1), V2) 908.68/297.14 , a__isNatList(nil()) -> tt() 908.68/297.14 , a__U61(X1, X2, X3) -> U61(X1, X2, X3) 908.68/297.14 , a__U61(tt(), L, N) -> a__U62(a__isNat(N), L) 908.68/297.14 , a__U62(X1, X2) -> U62(X1, X2) 908.68/297.14 , a__U62(tt(), L) -> s(a__length(mark(L))) 908.68/297.14 , a__isNat(X) -> isNat(X) 908.68/297.14 , a__isNat(0()) -> tt() 908.68/297.14 , a__isNat(s(V1)) -> a__U21(a__isNat(V1)) 908.68/297.14 , a__isNat(length(V1)) -> a__U11(a__isNatList(V1)) 908.68/297.14 , a__length(X) -> length(X) 908.68/297.14 , a__length(cons(N, L)) -> a__U61(a__isNatList(L), L, N) 908.68/297.14 , a__length(nil()) -> 0() 908.68/297.14 , mark(cons(X1, X2)) -> cons(mark(X1), X2) 908.68/297.14 , mark(0()) -> 0() 908.68/297.14 , mark(zeros()) -> a__zeros() 908.68/297.14 , mark(tt()) -> tt() 908.68/297.14 , mark(s(X)) -> s(mark(X)) 908.68/297.14 , mark(length(X)) -> a__length(mark(X)) 908.68/297.14 , mark(nil()) -> nil() 908.68/297.14 , mark(U11(X)) -> a__U11(mark(X)) 908.68/297.14 , mark(U21(X)) -> a__U21(mark(X)) 908.68/297.14 , mark(U31(X)) -> a__U31(mark(X)) 908.68/297.14 , mark(U41(X1, X2)) -> a__U41(mark(X1), X2) 908.68/297.14 , mark(U42(X)) -> a__U42(mark(X)) 908.68/297.14 , mark(isNatIList(X)) -> a__isNatIList(X) 908.68/297.14 , mark(U51(X1, X2)) -> a__U51(mark(X1), X2) 908.68/297.14 , mark(U52(X)) -> a__U52(mark(X)) 908.68/297.14 , mark(isNatList(X)) -> a__isNatList(X) 908.68/297.14 , mark(U61(X1, X2, X3)) -> a__U61(mark(X1), X2, X3) 908.68/297.14 , mark(U62(X1, X2)) -> a__U62(mark(X1), X2) 908.68/297.14 , mark(isNat(X)) -> a__isNat(X) } 908.68/297.14 Weak DPs: 908.68/297.14 { a__zeros^#() -> c_1() 908.68/297.14 , a__zeros^#() -> c_2() 908.68/297.14 , a__U11^#(tt()) -> c_4() 908.68/297.14 , a__U21^#(tt()) -> c_6() 908.68/297.14 , a__U31^#(tt()) -> c_8() 908.68/297.14 , a__U42^#(tt()) -> c_12() 908.68/297.14 , a__isNatIList^#(zeros()) -> c_16() 908.68/297.14 , a__U52^#(tt()) -> c_20() 908.68/297.14 , a__isNatList^#(nil()) -> c_23() 908.68/297.14 , a__length^#(nil()) -> c_34() 908.68/297.14 , a__isNat^#(0()) -> c_29() 908.68/297.14 , mark^#(0()) -> c_36() 908.68/297.14 , mark^#(zeros()) -> c_37(a__zeros^#()) 908.68/297.14 , mark^#(tt()) -> c_38() 908.68/297.14 , mark^#(nil()) -> c_41() } 908.68/297.14 Obligation: 908.68/297.14 runtime complexity 908.68/297.14 Answer: 908.68/297.14 MAYBE 908.68/297.14 908.68/297.14 Empty strict component of the problem is NOT empty. 908.68/297.14 908.68/297.14 908.68/297.14 Arrrr.. 908.68/297.17 EOF