-ndefinition new_addrarray ≝
- mk_Array8T ? (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
- (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
- (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉)
- (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉) (〈〈x0,x0〉;〈x0,x0〉;〈x0,x0〉〉).
+ndefinition new_addrarray : aux_addrarray_type ≝
+ mk_Array8T ? (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?)
+ (zeroc ?) (zeroc ?) (zeroc ?) (zeroc ?).