equal
deleted
inserted
replaced
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 program => 'c set, 'a*'b => 'c, 'a program, |
19 extending :: "['c=>'d, 'c program => 'c set, 'a*'b => 'c, 'a program, |
20 'c program set, 'c program set, 'a program set] => bool" |
20 'c program set, 'a program set] => bool" |
21 "extending C h F X' Y' Y == |
21 "extending v C h F Y' Y == |
22 ALL G. F Join project h (C G) G : Y & extend h F Join G : X' |
22 ALL G. G : preserves v --> F Join project h (C G) G : Y |
23 --> extend h F Join G : Y'" |
23 --> extend h F Join G : Y'" |
24 |
24 |
25 end |
25 end |