elementary-my-dear.snt

array5<array5<int5>> X;

X.each(function (row) {
  row.each(function (cell) {
    invariant cell.between?(1, 5);
  });
});

function valid?(ary) {
  invariant ary.uniq?;
};

X.each(*valid?);
X.transpose.each(*valid?);

invariant X[0][1] == 2;
invariant X[1][3] == 2;
invariant X[2][2] == 2;
invariant X[3][0] == 2;
invariant X[4][4] == 2;

invariant (X[0][0] * X[0][1]) + X[0][2] - X[0][3] + X[0][4] == 4;
invariant (X[1][0] + X[1][1] - X[1][2]) * X[1][3] + X[1][4] == 2;
invariant (X[2][0] + X[2][1]) * X[2][2] - X[2][3] + X[2][4] == 13;
invariant  X[3][0] * X[3][1] + X[3][2] - X[3][3] + X[3][4] == 11;
invariant (X[4][0] + X[4][1] - X[4][2] + X[4][3]) * X[4][4] == 14;

expose X;