tests/iscc/dep2

   1 Write := [n] -> { F[i, j] -> t[j] : i >= 0 and j >= 0 and j <= -1 + n - i and j <= -1 + n; T[i] -> t[i] : i >= 0 and i <= -1 + n; B[i] -> b[i] : i >= 0 and i <= -1 + n };
   2 Read := [n] -> { F[i, j] -> t[1 + j] : i >= 0 and j >= 0 and j <= -1 + n - i and j <= -2 + n; F[i, j] -> t[j] : i >= 0 and j >= 0 and j <= -1 + n - i and j <= -1 + n; B[i] -> t[i] : i >= 0 and i <= -1 + n; T[i] -> a[i] : i >= 0 and i <= -1 + n };
   3 Sched := [n] -> { T[i] -> [0, i, 0]; B[i] -> [2, i, 0]; F[i, j] -> [1, i, j] };
   4 Dep1 := [n] -> { F[i, -1 + n - i] -> B[-1 + n - i] : i <= -1 + n and i >= 0; T[i] -> F[0, i] : i <= -1 + n and i >= 0; T[i] -> F[0, -1 + i] : i <= -1 + n and i >= 1; F[i, j] -> F[1 + i, j] : i >= 0 and j >= 0 and j <= -2 + n - i and j <= -1 + n; F[i, j] -> F[1 + i, -1 + j] : i >= 0 and j >= 1 and j <= -1 + n - i and j <= -1 + n };
   5 Dep2 := (last Write before Read under Sched)[0];
   6 assert(Dep1 = Dep2);