Как заполнить отношение аксиомой в событии b

Question

Итак, у меня есть проект Rodin event-b, и я хотел бы определить известную статическую связь. В качестве примера, допустим, у меня есть набор {a,b,c}, и я хотел бы указать константу отношения, которая равна {(a,1),(a,2),(b,3)} в аксиома контекста. (Может быть многострочным, но предпочтительно одинарным, если возможно)

Как мне это сделать?

CONTEXT

example 

SETS

list 

CONSTANTS  
a       
b  
c 

relation 

AXIOMS

axm1   :    partition(list, {a}, {b}, {c}) 

axm2   :    relation ∈ list↔1‥5 

axm3   : ???


END

Answer 1

axm3:  relation = {a↦1, a↦2, b↦3}