So the event reification pattern [aside, is anyone writing up Alloy/Electrum expertise in one of the defined Pattern forms?] defines a function in a way that I’d not seen before, what in this example I’m calling “product style”.

Given

```
let multiplication_table =
0 -> 0 -> 0
+ 0 -> 1 -> 0
+ 1 -> 0 -> 0
+ 1 -> 1 -> 1
+ 0 -> 2 -> 0
+ 2 -> 0 -> 0
+ 2 -> 1 -> 2
+ 1 -> 2 -> 2
+ 2 -> 2 -> 4
```

then these

```
fun mul_product_style: Int -> Int -> Int {
multiplication_table
}
fun mul_dereference_style[x, y: Int]: Int{
y::(x::(multiplication_table))
}
```

behave identically, as shown by

```
run {
all x, y: {i: Int | 0 <= i && i < 3} | {
let p = x fun/mul y | {
mul_product_style[x,y] = p
mul_product_style[x][y] = p
x::mul_product_style[y] = p
y::(x::mul_product_style) = p
y.(x.mul_product_style) = p
mul_dereference_style[x,y] = p
mul_dereference_style[x][y] = p
x::mul_dereference_style[y] = p
y::(x::mul_dereference_style) = p
y.(x.mul_dereference_style) = p
}
}
}
```

which along the way illustrates all the ways I know of to apply a function.

The crucial difference is that the `mul_product_style`

form *creates a relation in the instance*, which we can see in the evaluator

```
mul_product_style
┌─┬─┬─┐
│0│0│0│
│ ├─┼─┤
│ │1│0│
│ ├─┼─┤
│ │2│0│
├─┼─┼─┤
│1│0│0│
│ ├─┼─┤
│ │1│1│
│ ├─┼─┤
│ │2│2│
├─┼─┼─┤
│2│0│0│
│ ├─┼─┤
│ │1│2│
│ ├─┼─┤
│ │2│4│
└─┴─┴─┘
```

but `mul_dereference_style`

does not, it can only be named in an expression to be evaluated.