equal
deleted
inserted
replaced
6 Least and greatest fixed points |
6 Least and greatest fixed points |
7 *) |
7 *) |
8 |
8 |
9 Fixedpt = domrange + |
9 Fixedpt = domrange + |
10 |
10 |
11 global |
|
12 |
|
13 consts |
11 consts |
14 bnd_mono :: [i,i=>i]=>o |
12 bnd_mono :: [i,i=>i]=>o |
15 lfp, gfp :: [i,i=>i]=>i |
13 lfp, gfp :: [i,i=>i]=>i |
16 |
|
17 local |
|
18 |
14 |
19 defs |
15 defs |
20 (*monotone operator from Pow(D) to itself*) |
16 (*monotone operator from Pow(D) to itself*) |
21 bnd_mono_def |
17 bnd_mono_def |
22 "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))" |
18 "bnd_mono(D,h) == h(D)<=D & (ALL W X. W<=X --> X<=D --> h(W) <= h(X))" |