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