equal
deleted
inserted
replaced
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 rules |
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))" |
18 |
18 |
19 lfp_def "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})" |
19 lfp_def "lfp(D,h) == Inter({X: Pow(D). h(X) <= X})" |