predicate inverse(array[int] of var int: f, array[int] of var int: invf) = forall(j in index_set(invf))(invf[j] in index_set(f)) /\ forall(i in index_set(f))( f[i] in index_set(invf) /\ forall(j in index_set(invf))(j == f[i] <-> i == invf[j]) );