11 Project = Extend + |
11 Project = Extend + |
12 |
12 |
13 constdefs |
13 constdefs |
14 projecting :: "['c program => 'c set, 'a*'b => 'c, |
14 projecting :: "['c program => 'c set, 'a*'b => 'c, |
15 'a program, 'c program set, 'a program set] => bool" |
15 'a program, 'c program set, 'a program set] => bool" |
16 "projecting C h F X' X == |
16 "projecting C h F X' X == |
17 ALL G. extend h F Join G : X' --> F Join project h (C G) G : X" |
17 ALL G. extend h F Join G : X' --> F Join project h (C G) G : X" |
18 |
18 |
19 extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program, |
19 extending :: "['c program => 'c set, 'a*'b => 'c, 'a program, |
20 'c program set, 'a program set] => bool" |
20 'c program set, 'a program set] => bool" |
21 "extending v C h F Y' Y == |
21 "extending C h F Y' Y == |
22 ALL G. G : preserves v --> F Join project h (C G) G : Y |
22 ALL G. extend h F ok G --> F Join project h (C G) G : Y |
23 --> extend h F Join G : Y'" |
23 --> extend h F Join G : Y'" |
|
24 |
|
25 subset_closed :: "'a set set => bool" |
|
26 "subset_closed U == ALL A: U. Pow A <= U" |
24 |
27 |
25 end |
28 end |