それで、私は 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