42 |
42 |
43 constdefs |
43 constdefs |
44 |
44 |
45 (*the set of all sets determined by f alone*) |
45 (*the set of all sets determined by f alone*) |
46 givenBy :: "['a => 'b] => 'a set set" |
46 givenBy :: "['a => 'b] => 'a set set" |
47 "givenBy f == range (%B. f-`` B)" |
47 "givenBy f == range (%B. f-` B)" |
48 |
48 |
49 (*visible version of the LEADS-TO relation*) |
49 (*visible version of the LEADS-TO relation*) |
50 leadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
50 leadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
51 ("(3_/ leadsTo[_]/ _)" [80,0,80] 80) |
51 ("(3_/ leadsTo[_]/ _)" [80,0,80] 80) |
52 "leadsETo A CC B == {F. (A,B) : elt CC F}" |
52 "leadsETo A CC B == {F. (A,B) : elt CC F}" |
53 |
53 |
54 LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
54 LeadsETo :: "['a set, 'a set set, 'a set] => 'a program set" |
55 ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80) |
55 ("(3_/ LeadsTo[_]/ _)" [80,0,80] 80) |
56 "LeadsETo A CC B == |
56 "LeadsETo A CC B == |
57 {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) `` CC] B}" |
57 {F. F : (reachable F Int A) leadsTo[(%C. reachable F Int C) ` CC] B}" |
58 |
58 |
59 end |
59 end |