12 linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*) |
12 linear, tot_ord :: "[i,i]=>o" (*Strict total ordering*) |
13 well_ord :: "[i,i]=>o" (*Well-ordering*) |
13 well_ord :: "[i,i]=>o" (*Well-ordering*) |
14 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) |
14 ord_iso :: "[i,i,i,i]=>i" (*Order isomorphisms*) |
15 pred :: "[i,i,i]=>i" (*Set of predecessors*) |
15 pred :: "[i,i,i]=>i" (*Set of predecessors*) |
16 |
16 |
17 rules |
17 defs |
18 part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
18 part_ord_def "part_ord(A,r) == irrefl(A,r) & trans[A](r)" |
19 |
19 |
20 linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)" |
20 linear_def "linear(A,r) == (ALL x:A. ALL y:A. <x,y>:r | x=y | <y,x>:r)" |
21 |
21 |
22 tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" |
22 tot_ord_def "tot_ord(A,r) == part_ord(A,r) & linear(A,r)" |