added quantifier len-x behaviour for A[0]; special cases need a lot of work