如何在Event-B中处理三元有序对并提取后二元有序对？

完全可行，核心思路是直接遍历每个三元有序对，提取其中绑定的后两个映射元素——你之前用定义域+笛卡尔积的方法失败，是因为笛卡尔积会打乱原有序对里的对应关系，生成所有可能的组合，而非保留原本的映射关联。

具体实现（以Python为例） #

根据你的三元有序对集合的存储结构，分两种常见情况处理：

情况1：集合元素是三元组（如 {(1, 2, 3), (1, 5, 6)}）

直接通过集合推导式提取每个三元组的后两个元素：

# 原始三元组集合
set_a = {(1, 2, 3), (1, 5, 6)}
# 生成二元有序对集合（用元组表示有序对）
set_b = {(item[1], item[2]) for item in set_a}
# 输出：{(2, 3), (5, 6)}

如果需要用映射（键值对）的形式存储，改用字典推导式：

dict_b = {item[1]: item[2] for item in set_a}
# 输出：{2: 3, 5: 6}

情况2：集合元素是嵌套映射（如 {1: {2: 3, 5: 6}}）

遍历嵌套的内层映射，直接提取其键值对：

# 原始嵌套映射集合
set_a = {1: {2: 3, 5: 6}}
set_b = set()
for inner_map in set_a.values():
    # 将内层映射的键值对转为元组，加入集合
    set_b.update(inner_map.items())
# 输出：{(2, 3), (5, 6)}

关键注意点 #

• 必须保留每个三元结构内部的对应关系，不能拆分定义域和值域后再组合——这是避免生成错误无序对的核心。
• 如果你的三元有序对用其他结构存储（如自定义类），只需要调整提取后两个元素的逻辑即可，核心思路不变。

内容的提问来源于stack exchange，提问作者PythonLee