how to handle multiple ordered pairs in Event-B

Question

I want to get the last two mapped elements of a deterministic ternary ordered pair in the form of binary ordered pairs, here's an example: set A = { 1 ↦ 2 ↦ 3,1 ↦ 5 ↦ 6} ，I want to get set B = {2 ↦ 3, 5 ↦ 6} ，what should I do? BTW:Is that possible?

I tried to get the domain and range of set A and use Cartesian product to get what I want,but I failed,the result set was disordered

Answer 1

A={ 1↦2↦3, 1↦5↦6} is the same as A={ (1↦2)↦3, (1↦5)↦6 }, so you have a set of pairs here.

What you want is a combination of the left and right side of each entry, so domain and range won't work here. But you can achieve it with a set comprehension:

B = {a,b,c · a↦b↦c∈A ∣ b↦c}

(Read: For all triples a↦b↦c store b↦c in B)

But what do you mean by "disordered"? Since A and B are sets, there is no defined order. It does not make a difference whether it is {2↦3, 5↦6} or {5↦6, 2↦3}.