Rules for array lengths and array write operations.
These rules say that the array write operations preserve array lengths. There is one rule for each <type1>-array-write function.