33 |
33 |
34 pred_def "pred(A,x,r) == {y:A. <y,x>:r}" |
34 pred_def "pred(A,x,r) == {y:A. <y,x>:r}" |
35 |
35 |
36 ord_iso_map_def |
36 ord_iso_map_def |
37 "ord_iso_map(A,r,B,s) == |
37 "ord_iso_map(A,r,B,s) == |
38 UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). |
38 UN x:A. UN y:B. UN f: ord_iso(pred(A,x,r), r, pred(B,y,s), s). {<x,y>}" |
39 {<x,y>}" |
|
40 |
39 |
41 constdefs |
40 constdefs |
42 |
41 |
43 first :: [i, i, i] => o |
42 first :: [i, i, i] => o |
44 "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
43 "first(u, X, R) == u:X & (ALL v:X. v~=u --> <u,v> : R)" |
45 |
44 |
|
45 syntax (xsymbols) |
|
46 ord_iso :: [i,i,i,i]=>i ("('(_,_') \\<cong> '(_,_'))" 50) |
|
47 |
|
48 |
46 end |
49 end |