我真的很困惑为什么我的以下断言总是有一个反例。
//assertions must NEVER by wrong
assert Symmetric{
all r: univ -> univ | some ~r iff (some x, y: univ | x not in y and y not in x and
(x->y in r) and (y->x in r))
}
check Symmetric
反例总是显示 1 univ set 中的元素。然而,这不应该是这样,因为我指定会有一些 ~r iff x 不在 y 中并且 y 不在 x 中。唯一的元素不应该满足这个陈述。
然而,为什么该模型总是对我的断言提出反例呢?
---INSTANCE---
integers={}
univ={Univ$0}
Int={}
seq/Int={}
String={}
none={}
this/Univ={Univ$0}
skolem $Symmetric_r={Univ$0->Univ$0}
非常感谢一些指导!