equal
deleted
inserted
replaced
11 UNITY = LessThan + |
11 UNITY = LessThan + |
12 |
12 |
13 constdefs |
13 constdefs |
14 |
14 |
15 constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
15 constrains :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
16 "constrains Acts A B == ALL act:Acts. act^^A <= B" |
16 "constrains acts A B == ALL act:acts. act^^A <= B" |
17 |
17 |
18 stable :: "('a * 'a)set set => 'a set => bool" |
18 stable :: "('a * 'a)set set => 'a set => bool" |
19 "stable Acts A == constrains Acts A A" |
19 "stable acts A == constrains acts A A" |
20 |
20 |
21 strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set" |
21 strongest_rhs :: "[('a * 'a)set set, 'a set] => 'a set" |
22 "strongest_rhs Acts A == Inter {B. constrains Acts A B}" |
22 "strongest_rhs acts A == Inter {B. constrains acts A B}" |
23 |
23 |
24 unless :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
24 unless :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
25 "unless Acts A B == constrains Acts (A-B) (A Un B)" |
25 "unless acts A B == constrains acts (A-B) (A Un B)" |
26 |
26 |
27 end |
27 end |