| changeset 1558 | 9c6ebfab4e05 |
| parent 1475 | 7f5a4cd08209 |
| child 3947 | eb707467f8c5 |
| 1557:fe30812f5b5e | 1558:9c6ebfab4e05 |
|---|---|
5 |
5 |
6 The Knaster-Tarski Theorem |
6 The Knaster-Tarski Theorem |
7 *) |
7 *) |
8 |
8 |
9 Lfp = mono + Prod + |
9 Lfp = mono + Prod + |
10 consts lfp :: ['a set=>'a set] => 'a set |
10 |
11 defs |
11 constdefs |
12 (*least fixed point*) |
12 lfp :: ['a set=>'a set] => 'a set |
13 lfp_def "lfp(f) == Inter({u. f(u) <= u})" |
13 "lfp(f) == Inter({u. f(u) <= u})" (*least fixed point*) |
14 |
|
14 end |
15 end |