equal
deleted
inserted
replaced
6 Towards ordinal arithmetic |
6 Towards ordinal arithmetic |
7 *) |
7 *) |
8 |
8 |
9 OrderArith = Order + Sum + |
9 OrderArith = Order + Sum + |
10 consts |
10 consts |
11 radd, rmult :: "[i,i,i,i]=>i" |
11 radd, rmult :: [i,i,i,i]=>i |
12 rvimage :: "[i,i,i]=>i" |
12 rvimage :: [i,i,i]=>i |
13 |
13 |
14 defs |
14 defs |
15 (*disjoint sum of two relations; underlies ordinal addition*) |
15 (*disjoint sum of two relations; underlies ordinal addition*) |
16 radd_def "radd(A,r,B,s) == |
16 radd_def "radd(A,r,B,s) == |
17 {z: (A+B) * (A+B). |
17 {z: (A+B) * (A+B). |