13 |
13 |
14 consts |
14 consts |
15 |
15 |
16 CEX ::"['a trans,'a pred, 'a]=>bool" |
16 CEX ::"['a trans,'a pred, 'a]=>bool" |
17 EG ::"['a trans,'a pred]=> 'a pred" |
17 EG ::"['a trans,'a pred]=> 'a pred" |
18 EU ::"['a trans,'a pred,'a pred]=> 'a pred" |
|
19 EF ::"['a trans,'a pred]=> 'a pred" |
|
20 AX ::"['a trans,'a pred]=> 'a pred" |
|
21 AF ::"['a trans,'a pred]=> 'a pred" |
|
22 AG ::"['a trans,'a pred]=> 'a pred" |
|
23 AU ::"['a trans,'a pred,'a pred]=> 'a pred" |
|
24 FairEG ::"['a trans,'a pred,'a pred]=> 'a pred" |
|
25 |
18 |
26 |
19 |
27 |
20 |
28 defs |
21 defs |
29 |
22 |
30 CEX_def "CEX N f x == (? y. (f y & (x,y):N))" |
23 CEX_def "CEX N f u == (? v. (f v & (u,v):N))" |
31 EG_def "EG N f == nu (% Q. % x.(f x & CEX N Q x))" |
24 EG_def "EG N f == nu (% Q. % u.(f u & CEX N Q u))" |
32 EU_def "EU N f g == mu (% Q. % x.(g x | (g x & CEX N Q x)))" |
|
33 EF_def "EF N f == EU N (%x. True) f" |
|
34 |
25 |
35 AX_def "AX N f x == ~ CEX N (%x. ~ f x) x" |
|
36 AF_def "AF N f x == ~ EG N (%x. ~ f x) x" |
|
37 AG_def "AG N f x == ~ EF N (%x. ~ f x) x" |
|
38 AU_def "AU N f g x == ~ EU N (%x. ~ g x) (%x. (~ f x) & (~ g x)) x & AF N g x" |
|
39 |
26 |
40 FairEG_def "FairEG N f fc == nu (% Q. %x. (f x & |
27 |
41 (mu (% P. CEX N (%y. f y & ((fc y & Q y) | P y)))) x))" |
28 |
42 |
29 |
|
30 |
43 end |
31 end |