$input int n;
$assume(n > 0);

int b[3*n][3*n];

int main() {
  int a[n][n] = (int[n][n])$lambda(int i,j) i*n+j;
 
  b = (int[3*n][3*n])$lambda(int i,j) n<=i&&i<2*n&&n<=j&&j<2*n ? a[i-n][j-n] : b[i][j];
  $assert($forall (int i:n..2*n-1) $forall (int j:n..2*n-1) b[i][j] == a[i-n][j-n]);
  $assert($forall (int i, j | (0<=i&&i<n) || (2*n<=i&&i<3*n) || (0<=j&&j<n) || (2*n<=j&&j<3*n)) b[i][j] == 0);
}