equal
deleted
inserted
replaced
27 |
27 |
28 Range :: "('a*'b) set => 'b set" |
28 Range :: "('a*'b) set => 'b set" |
29 "Range(r) == Domain(r^-1)" |
29 "Range(r) == Domain(r^-1)" |
30 |
30 |
31 refl :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*) |
31 refl :: "['a set, ('a*'a) set] => bool" (*reflexivity over a set*) |
32 "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)" |
32 "refl A r == r <= A <*> A & (ALL x: A. (x,x) : r)" |
33 |
33 |
34 sym :: "('a*'a) set=>bool" (*symmetry predicate*) |
34 sym :: "('a*'a) set=>bool" (*symmetry predicate*) |
35 "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
35 "sym(r) == ALL x y. (x,y): r --> (y,x): r" |
36 |
36 |
37 antisym:: "('a * 'a)set => bool" (*antisymmetry predicate*) |
37 antisym:: "('a * 'a)set => bool" (*antisymmetry predicate*) |