WORST_CASE(Omega(n^1),?) * Step 1: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c9() A__AND(tt(),z0) -> c8(MARK(z0)) A__ISNAT(z0) -> c13() A__ISNAT(0()) -> c10() A__ISNAT(length(z0)) -> c11(A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c12(A__ISNAT(z0)) A__ISNATILIST(z0) -> c14(A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c17() A__ISNATILIST(cons(z0,z1)) -> c16(A__AND(a__isNat(z0),isNatIList(z1)),A__ISNAT(z0)) A__ISNATILIST(zeros()) -> c15() A__ISNATLIST(z0) -> c21() A__ISNATLIST(cons(z0,z1)) -> c19(A__AND(a__isNat(z0),isNatList(z1)),A__ISNAT(z0)) A__ISNATLIST(nil()) -> c18() A__ISNATLIST(take(z0,z1)) -> c20(A__AND(a__isNat(z0),isNatIList(z1)),A__ISNAT(z0)) A__LENGTH(z0) -> c24() A__LENGTH(cons(z0,z1)) -> c23(A__U11(a__and(a__isNatList(z1),isNat(z0)),z1) ,A__AND(a__isNatList(z1),isNat(z0)) ,A__ISNATLIST(z1)) A__LENGTH(nil()) -> c22() A__TAKE(z0,z1) -> c27() A__TAKE(0(),z0) -> c25(A__U21(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c26(A__U31(a__and(a__isNatIList(z2),and(isNat(z0),isNat(z1))),z2,z0,z1) ,A__AND(a__isNatIList(z2),and(isNat(z0),isNat(z1))) ,A__ISNATILIST(z2)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__LENGTH(mark(z0)),MARK(z0)) A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0,z1,z2,z3) -> c7() A__U31(tt(),z0,z1,z2) -> c6(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c40() MARK(U11(z0,z1)) -> c29(A__U11(mark(z0),z1),MARK(z0)) MARK(U21(z0)) -> c31(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0,z1,z2,z3)) -> c32(A__U31(mark(z0),z1,z2,z3),MARK(z0)) MARK(and(z0,z1)) -> c35(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c39(MARK(z0)) MARK(isNat(z0)) -> c36(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c38(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c37(A__ISNATLIST(z0)) MARK(length(z0)) -> c30(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c43() MARK(s(z0)) -> c42(MARK(z0)) MARK(take(z0,z1)) -> c33(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c34(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c41() MARK(zeros()) -> c28(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> s(a__length(mark(z0))) a__U21(z0) -> U21(z0) a__U21(tt()) -> nil() a__U31(z0,z1,z2,z3) -> U31(z0,z1,z2,z3) a__U31(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__isNatList(z0) a__isNat(s(z0)) -> a__isNat(z0) a__isNatIList(z0) -> a__isNatList(z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__and(a__isNat(z0),isNatIList(z1)) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__and(a__isNat(z0),isNatList(z1)) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__and(a__isNat(z0),isNatIList(z1)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U11(a__and(a__isNatList(z1),isNat(z0)),z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U21(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__U31(a__and(a__isNatIList(z2),and(isNat(z0),isNat(z1))),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0,z1,z2,z3)) -> a__U31(mark(z0),z1,z2,z3) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatList(z0)) -> a__isNatList(z0) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__U11/2,A__U21/1,A__U31/4 ,A__ZEROS/0,MARK/1,a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1 ,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U21/1,U31/4,and/2,c/0,c1/0,c10/0,c11/1,c12/1,c13/0,c14/1,c15/0 ,c16/2,c17/0,c18/0,c19/2,c2/2,c20/2,c21/0,c22/0,c23/3,c24/0,c25/2,c26/3,c27/0,c28/1,c29/2,c3/0,c30/2,c31/2 ,c32/2,c33/2,c34/2,c35/2,c36/1,c37/1,c38/1,c39/1,c4/0,c40/0,c41/0,c42/1,c43/0,c5/0,c6/1,c7/0,c8/1,c9/0 ,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH ,A__TAKE,A__U11,A__U21,A__U31,A__ZEROS,MARK,a__U11,a__U21,a__U31,a__and,a__isNat,a__isNatIList,a__isNatList ,a__length,a__take,a__zeros,mark} and constructors {0,U11,U21,U31,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41 ,c42,c43,c5,c6,c7,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 2: Sum. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c9() A__AND(tt(),z0) -> c8(MARK(z0)) A__ISNAT(z0) -> c13() A__ISNAT(0()) -> c10() A__ISNAT(length(z0)) -> c11(A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c12(A__ISNAT(z0)) A__ISNATILIST(z0) -> c14(A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c17() A__ISNATILIST(cons(z0,z1)) -> c16(A__AND(a__isNat(z0),isNatIList(z1)),A__ISNAT(z0)) A__ISNATILIST(zeros()) -> c15() A__ISNATLIST(z0) -> c21() A__ISNATLIST(cons(z0,z1)) -> c19(A__AND(a__isNat(z0),isNatList(z1)),A__ISNAT(z0)) A__ISNATLIST(nil()) -> c18() A__ISNATLIST(take(z0,z1)) -> c20(A__AND(a__isNat(z0),isNatIList(z1)),A__ISNAT(z0)) A__LENGTH(z0) -> c24() A__LENGTH(cons(z0,z1)) -> c23(A__U11(a__and(a__isNatList(z1),isNat(z0)),z1) ,A__AND(a__isNatList(z1),isNat(z0)) ,A__ISNATLIST(z1)) A__LENGTH(nil()) -> c22() A__TAKE(z0,z1) -> c27() A__TAKE(0(),z0) -> c25(A__U21(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c26(A__U31(a__and(a__isNatIList(z2),and(isNat(z0),isNat(z1))),z2,z0,z1) ,A__AND(a__isNatIList(z2),and(isNat(z0),isNat(z1))) ,A__ISNATILIST(z2)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__LENGTH(mark(z0)),MARK(z0)) A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0,z1,z2,z3) -> c7() A__U31(tt(),z0,z1,z2) -> c6(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c40() MARK(U11(z0,z1)) -> c29(A__U11(mark(z0),z1),MARK(z0)) MARK(U21(z0)) -> c31(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0,z1,z2,z3)) -> c32(A__U31(mark(z0),z1,z2,z3),MARK(z0)) MARK(and(z0,z1)) -> c35(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c39(MARK(z0)) MARK(isNat(z0)) -> c36(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c38(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c37(A__ISNATLIST(z0)) MARK(length(z0)) -> c30(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c43() MARK(s(z0)) -> c42(MARK(z0)) MARK(take(z0,z1)) -> c33(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c34(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c41() MARK(zeros()) -> c28(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> s(a__length(mark(z0))) a__U21(z0) -> U21(z0) a__U21(tt()) -> nil() a__U31(z0,z1,z2,z3) -> U31(z0,z1,z2,z3) a__U31(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__isNatList(z0) a__isNat(s(z0)) -> a__isNat(z0) a__isNatIList(z0) -> a__isNatList(z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__and(a__isNat(z0),isNatIList(z1)) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__and(a__isNat(z0),isNatList(z1)) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__and(a__isNat(z0),isNatIList(z1)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U11(a__and(a__isNatList(z1),isNat(z0)),z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U21(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__U31(a__and(a__isNatIList(z2),and(isNat(z0),isNat(z1))),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0,z1,z2,z3)) -> a__U31(mark(z0),z1,z2,z3) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatList(z0)) -> a__isNatList(z0) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__U11/2,A__U21/1,A__U31/4 ,A__ZEROS/0,MARK/1,a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1 ,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U21/1,U31/4,and/2,c/0,c1/0,c10/0,c11/1,c12/1,c13/0,c14/1,c15/0 ,c16/2,c17/0,c18/0,c19/2,c2/2,c20/2,c21/0,c22/0,c23/3,c24/0,c25/2,c26/3,c27/0,c28/1,c29/2,c3/0,c30/2,c31/2 ,c32/2,c33/2,c34/2,c35/2,c36/1,c37/1,c38/1,c39/1,c4/0,c40/0,c41/0,c42/1,c43/0,c5/0,c6/1,c7/0,c8/1,c9/0 ,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH ,A__TAKE,A__U11,A__U21,A__U31,A__ZEROS,MARK,a__U11,a__U21,a__U31,a__and,a__isNat,a__isNatIList,a__isNatList ,a__length,a__take,a__zeros,mark} and constructors {0,U11,U21,U31,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41 ,c42,c43,c5,c6,c7,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: Sum {left = someStrategy, right = someStrategy} + Details: () * Step 3: DecreasingLoops. WORST_CASE(Omega(n^1),?) + Considered Problem: - Strict TRS: A__AND(z0,z1) -> c9() A__AND(tt(),z0) -> c8(MARK(z0)) A__ISNAT(z0) -> c13() A__ISNAT(0()) -> c10() A__ISNAT(length(z0)) -> c11(A__ISNATLIST(z0)) A__ISNAT(s(z0)) -> c12(A__ISNAT(z0)) A__ISNATILIST(z0) -> c14(A__ISNATLIST(z0)) A__ISNATILIST(z0) -> c17() A__ISNATILIST(cons(z0,z1)) -> c16(A__AND(a__isNat(z0),isNatIList(z1)),A__ISNAT(z0)) A__ISNATILIST(zeros()) -> c15() A__ISNATLIST(z0) -> c21() A__ISNATLIST(cons(z0,z1)) -> c19(A__AND(a__isNat(z0),isNatList(z1)),A__ISNAT(z0)) A__ISNATLIST(nil()) -> c18() A__ISNATLIST(take(z0,z1)) -> c20(A__AND(a__isNat(z0),isNatIList(z1)),A__ISNAT(z0)) A__LENGTH(z0) -> c24() A__LENGTH(cons(z0,z1)) -> c23(A__U11(a__and(a__isNatList(z1),isNat(z0)),z1) ,A__AND(a__isNatList(z1),isNat(z0)) ,A__ISNATLIST(z1)) A__LENGTH(nil()) -> c22() A__TAKE(z0,z1) -> c27() A__TAKE(0(),z0) -> c25(A__U21(a__isNatIList(z0)),A__ISNATILIST(z0)) A__TAKE(s(z0),cons(z1,z2)) -> c26(A__U31(a__and(a__isNatIList(z2),and(isNat(z0),isNat(z1))),z2,z0,z1) ,A__AND(a__isNatIList(z2),and(isNat(z0),isNat(z1))) ,A__ISNATILIST(z2)) A__U11(z0,z1) -> c3() A__U11(tt(),z0) -> c2(A__LENGTH(mark(z0)),MARK(z0)) A__U21(z0) -> c5() A__U21(tt()) -> c4() A__U31(z0,z1,z2,z3) -> c7() A__U31(tt(),z0,z1,z2) -> c6(MARK(z2)) A__ZEROS() -> c() A__ZEROS() -> c1() MARK(0()) -> c40() MARK(U11(z0,z1)) -> c29(A__U11(mark(z0),z1),MARK(z0)) MARK(U21(z0)) -> c31(A__U21(mark(z0)),MARK(z0)) MARK(U31(z0,z1,z2,z3)) -> c32(A__U31(mark(z0),z1,z2,z3),MARK(z0)) MARK(and(z0,z1)) -> c35(A__AND(mark(z0),z1),MARK(z0)) MARK(cons(z0,z1)) -> c39(MARK(z0)) MARK(isNat(z0)) -> c36(A__ISNAT(z0)) MARK(isNatIList(z0)) -> c38(A__ISNATILIST(z0)) MARK(isNatList(z0)) -> c37(A__ISNATLIST(z0)) MARK(length(z0)) -> c30(A__LENGTH(mark(z0)),MARK(z0)) MARK(nil()) -> c43() MARK(s(z0)) -> c42(MARK(z0)) MARK(take(z0,z1)) -> c33(A__TAKE(mark(z0),mark(z1)),MARK(z0)) MARK(take(z0,z1)) -> c34(A__TAKE(mark(z0),mark(z1)),MARK(z1)) MARK(tt()) -> c41() MARK(zeros()) -> c28(A__ZEROS()) - Weak TRS: a__U11(z0,z1) -> U11(z0,z1) a__U11(tt(),z0) -> s(a__length(mark(z0))) a__U21(z0) -> U21(z0) a__U21(tt()) -> nil() a__U31(z0,z1,z2,z3) -> U31(z0,z1,z2,z3) a__U31(tt(),z0,z1,z2) -> cons(mark(z2),take(z1,z0)) a__and(z0,z1) -> and(z0,z1) a__and(tt(),z0) -> mark(z0) a__isNat(z0) -> isNat(z0) a__isNat(0()) -> tt() a__isNat(length(z0)) -> a__isNatList(z0) a__isNat(s(z0)) -> a__isNat(z0) a__isNatIList(z0) -> a__isNatList(z0) a__isNatIList(z0) -> isNatIList(z0) a__isNatIList(cons(z0,z1)) -> a__and(a__isNat(z0),isNatIList(z1)) a__isNatIList(zeros()) -> tt() a__isNatList(z0) -> isNatList(z0) a__isNatList(cons(z0,z1)) -> a__and(a__isNat(z0),isNatList(z1)) a__isNatList(nil()) -> tt() a__isNatList(take(z0,z1)) -> a__and(a__isNat(z0),isNatIList(z1)) a__length(z0) -> length(z0) a__length(cons(z0,z1)) -> a__U11(a__and(a__isNatList(z1),isNat(z0)),z1) a__length(nil()) -> 0() a__take(z0,z1) -> take(z0,z1) a__take(0(),z0) -> a__U21(a__isNatIList(z0)) a__take(s(z0),cons(z1,z2)) -> a__U31(a__and(a__isNatIList(z2),and(isNat(z0),isNat(z1))),z2,z0,z1) a__zeros() -> cons(0(),zeros()) a__zeros() -> zeros() mark(0()) -> 0() mark(U11(z0,z1)) -> a__U11(mark(z0),z1) mark(U21(z0)) -> a__U21(mark(z0)) mark(U31(z0,z1,z2,z3)) -> a__U31(mark(z0),z1,z2,z3) mark(and(z0,z1)) -> a__and(mark(z0),z1) mark(cons(z0,z1)) -> cons(mark(z0),z1) mark(isNat(z0)) -> a__isNat(z0) mark(isNatIList(z0)) -> a__isNatIList(z0) mark(isNatList(z0)) -> a__isNatList(z0) mark(length(z0)) -> a__length(mark(z0)) mark(nil()) -> nil() mark(s(z0)) -> s(mark(z0)) mark(take(z0,z1)) -> a__take(mark(z0),mark(z1)) mark(tt()) -> tt() mark(zeros()) -> a__zeros() - Signature: {A__AND/2,A__ISNAT/1,A__ISNATILIST/1,A__ISNATLIST/1,A__LENGTH/1,A__TAKE/2,A__U11/2,A__U21/1,A__U31/4 ,A__ZEROS/0,MARK/1,a__U11/2,a__U21/1,a__U31/4,a__and/2,a__isNat/1,a__isNatIList/1,a__isNatList/1,a__length/1 ,a__take/2,a__zeros/0,mark/1} / {0/0,U11/2,U21/1,U31/4,and/2,c/0,c1/0,c10/0,c11/1,c12/1,c13/0,c14/1,c15/0 ,c16/2,c17/0,c18/0,c19/2,c2/2,c20/2,c21/0,c22/0,c23/3,c24/0,c25/2,c26/3,c27/0,c28/1,c29/2,c3/0,c30/2,c31/2 ,c32/2,c33/2,c34/2,c35/2,c36/1,c37/1,c38/1,c39/1,c4/0,c40/0,c41/0,c42/1,c43/0,c5/0,c6/1,c7/0,c8/1,c9/0 ,cons/2,isNat/1,isNatIList/1,isNatList/1,length/1,nil/0,s/1,take/2,tt/0,zeros/0} - Obligation: innermost runtime complexity wrt. defined symbols {A__AND,A__ISNAT,A__ISNATILIST,A__ISNATLIST,A__LENGTH ,A__TAKE,A__U11,A__U21,A__U31,A__ZEROS,MARK,a__U11,a__U21,a__U31,a__and,a__isNat,a__isNatIList,a__isNatList ,a__length,a__take,a__zeros,mark} and constructors {0,U11,U21,U31,and,c,c1,c10,c11,c12,c13,c14,c15,c16,c17 ,c18,c19,c2,c20,c21,c22,c23,c24,c25,c26,c27,c28,c29,c3,c30,c31,c32,c33,c34,c35,c36,c37,c38,c39,c4,c40,c41 ,c42,c43,c5,c6,c7,c8,c9,cons,isNat,isNatIList,isNatList,length,nil,s,take,tt,zeros} + Applied Processor: DecreasingLoops {bound = AnyLoop, narrow = 10} + Details: The system has following decreasing Loops: A__ISNAT(x){x -> s(x)} = A__ISNAT(s(x)) ->^+ c12(A__ISNAT(x)) = C[A__ISNAT(x) = A__ISNAT(x){}] WORST_CASE(Omega(n^1),?)