equal
deleted
inserted
replaced
28 (!i.P(Y i)) --> P(lub(range Y))" |
28 (!i.P(Y i)) --> P(lub(range Y))" |
29 |
29 |
30 admw_def "admw P == !F. (!n.P (iterate n F UU)) --> |
30 admw_def "admw P == !F. (!n.P (iterate n F UU)) --> |
31 P (lub(range (%i. iterate i F UU)))" |
31 P (lub(range (%i. iterate i F UU)))" |
32 |
32 |
33 (* further useful class for HOLCF *) |
|
34 |
|
35 axclass chfin<pcpo |
|
36 |
|
37 chfin "!Y.is_chain Y-->(? n.max_in_chain n Y)" |
|
38 |
|
39 axclass flat<pcpo |
|
40 |
|
41 ax_flat "! x y.x << y --> (x = UU) | (x=y)" |
|
42 |
|
43 end |
33 end |
44 |
34 |