sig Object {}: 代表学校里的所有学生。

sig File in Object {}: 代表篮球队的成员（他们也是学生）。

sig Dir in Object {}: 代表辩论队的成员（他们也是学生）。

x in File + Dir：x至少在File或Dir中的一个，允许x既是File 又是Dir。 ****情况二*****

sig Object {}: 代表学校里的所有学生。

sig File extends Object {}: 代表篮球队的成员（他们也是学生）。

sig Dir extends Object {}: 代表辩论队的成员（他们也是学生）。

x in File + Dir：x只能是File或Dir中的一个，因为extend限制了File和Dir不能相同

例如，考虑公式 one x, y : A | x->y in r 和 one x : A | one y : A | x in r ，并设 r = {(A0,A0),(A0,A1),(A1,A0)} 。前一个公式为假，因为在 r 中有三个元组。然而，后一个公式为真，因为在 r 中恰好有一个 x （ A1 ），对于它恰好有一个 y （ A0 ）。 one x,y : A | P --- 将x,y看做整体。只存在唯一的一对 (x, y) 组合，使得这个组合出现在我们的配对名单 r 上。 one x : A | one y : A | x->y in r -- 剥洋葱。这是对应x的判定，是否存在唯一一个x，使得存在唯一一个y，使这个组合出现在我们的配对名单 r 上。

请注意， disj 关键字仅适用于对同一集合进行量化的变量组。这意味着在公式 all disj x, y : A , w, z : B | P 中， w 和 z 可以取相同的值（但 x 和 y 不行）