请求基于Z符号定义集合S的filter修改操作

现有集合定义 #

S: Id × Counter
Id: ℕ
Counter: ℕ

注：ℕ表示自然数集合，Id × Counter代表Id与Counter的笛卡尔积，即集合S的元素均为(id值, 计数器值)形式的二元组，两个分量都属于自然数。

filter操作定义 #

用Z语言的操作模式（Schema）实现该操作，具体如下：

filter ΔS
x?: ℕ
y?: ℕ
──────────────────────────────────────────────────────────────────
S' = (S \ { a ∈ S | first(a) = x }) ∪ 
     { (x, second(a) - y) | a ∈ S | first(a) = x ∧ second(a) - y > 0 }

逻辑说明 #

1. ΔS表示这是修改集合S的操作，S是修改前的原集合，S'是修改后的集合。
2. x?: ℕ和y?: ℕ是操作的两个输入参数，?标记参数为输入值。
3. 操作逻辑拆解：
   • 先从原集合S中移除所有first分量等于x的元素；
   • 对原集合里first分量等于x、且second分量减y后仍大于0的元素，生成新的二元组(x, second(a)-y)，再把这些新元素添加到第一步得到的集合中；
   • 最终得到的S'就是处理后的集合：符合条件的元素要么被移除（减y后≤0），要么被新的二元组替换；不匹配的元素保持原样。

补充说明 #

自然数集合ℕ中仅当被减数≥减数时减法有定义，这里刚好利用这一点：当second(a) < y时，second(a)-y不属于ℕ，对应的元素不会被加入新集合，等价于直接移除，完全贴合需求逻辑。

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