合金 - 一次論理で比較する

Question

合金の等価性をどのように比較しますか？次のようなものがあります。

--[(All x)(Exists y)[R(x,y)] 
-- and (All x)(All y)[R(x,y) -> R(y,x)]] 
-- = 
-- (All x)[R(x,x)] and 

assert checkEquality{ 
    (all m: Model, x:m.A| some y:m.A | (y in x.(m.R))) and 
    (all m: Model, x:m.A, y:m.A | (y in x.(m.R) -> x in y.(m.R))) = 
    (all m: Model, x:m.A | (x in x.(m.R)) 
} 

Answer 1

ここは初級です。 '（All x）（All y）[R（x、y） - > R（y、x）]]'部分で推測すると、おそらくもっと特別なことが考えられました。その場合は、さらに質問を明記してください。

sig Value {} 

pred p1 [x, y: Value] { 
    // ... 
} 

pred p2 [x, y: Value] { 
    // ...  
} 

assert equ_pred { 
    all x, y: Value | p1 [x, y] <=> p2 [x, y] 
} 

check equ_pred