24 |
24 |
25 iterate_def "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])" |
25 iterate_def "iterate(n,F,c) == nat_rec(n,c,%n x.F[x])" |
26 Ifix_def "Ifix(F) == lub(range(%i.iterate(i,F,UU)))" |
26 Ifix_def "Ifix(F) == lub(range(%i.iterate(i,F,UU)))" |
27 fix_def "fix == (LAM f. Ifix(f))" |
27 fix_def "fix == (LAM f. Ifix(f))" |
28 |
28 |
29 adm_def "adm(P) == !Y. is_chain(Y) --> \ |
29 adm_def "adm(P) == !Y. is_chain(Y) --> |
30 \ (!i.P(Y(i))) --> P(lub(range(Y)))" |
30 (!i.P(Y(i))) --> P(lub(range(Y)))" |
31 |
31 |
32 admw_def "admw(P)== (!F.((!n.P(iterate(n,F,UU)))-->\ |
32 admw_def "admw(P)== (!F.((!n.P(iterate(n,F,UU)))--> |
33 \ P(lub(range(%i.iterate(i,F,UU))))))" |
33 P(lub(range(%i.iterate(i,F,UU))))))" |
34 |
34 |
35 chain_finite_def "chain_finite(x::'a)==\ |
35 chain_finite_def "chain_finite(x::'a)== |
36 \ !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))" |
36 !Y. is_chain(Y::nat=>'a) --> (? n.max_in_chain(n,Y))" |
37 |
37 |
38 flat_def "flat(x::'a) ==\ |
38 flat_def "flat(x::'a) == |
39 \ ! x y. (x::'a) << y --> (x = UU) | (x=y)" |
39 ! x y. (x::'a) << y --> (x = UU) | (x=y)" |
40 |
40 |
41 end |
41 end |
42 |
42 |