Complete the Default Memory Model

[iconmaster5326]

Currently, the memory model cannot model common situations, like when you store an array and load an element of the array. We need to add axioms to the Why3 output to specify the behavior when this happens.