equal
deleted
inserted
replaced
17 transient :: "[('a * 'a)set set, 'a set] => bool" |
17 transient :: "[('a * 'a)set set, 'a set] => bool" |
18 "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A" |
18 "transient Acts A == EX act:Acts. A <= Domain act & act^^A <= Compl A" |
19 |
19 |
20 ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
20 ensures :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
21 "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)" |
21 "ensures Acts A B == constrains Acts (A-B) (A Un B) & transient Acts (A-B)" |
|
22 (*(unless Acts A B) would be equivalent*) |
22 |
23 |
23 consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
24 consts leadsTo :: "[('a * 'a)set set, 'a set, 'a set] => bool" |
24 leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set" |
25 leadsto :: "[('a * 'a)set set] => ('a set * 'a set) set" |
25 |
26 |
26 translations |
27 translations |