equal
deleted
inserted
replaced
8 |
8 |
9 |
9 |
10 types |
10 types |
11 'a trans = "('a * 'a) set" |
11 'a trans = "('a * 'a) set" |
12 |
12 |
13 |
|
14 consts |
13 consts |
15 |
14 CEX ::"['a trans,'a pred, 'a]=>bool" |
16 CEX ::"['a trans,'a pred, 'a]=>bool" |
15 EG ::"['a trans,'a pred]=> 'a pred" |
17 EG ::"['a trans,'a pred]=> 'a pred" |
|
18 |
|
19 |
|
20 |
16 |
21 defs |
17 defs |
22 |
18 CEX_def "CEX N f u == (? v. (f v & (u,v):N))" |
23 CEX_def "CEX N f u == (? v. (f v & (u,v):N))" |
19 EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))" |
24 EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))" |
|
25 |
|
26 |
|
27 |
|
28 |
|
29 |
|
30 |
20 |
31 end |
21 end |