Second_Feb6th_ArrayFramework Works

take error condition out of the forall axiom tree, and use exist
quantifier to represent property formula