equal
deleted
inserted
replaced
28 else {})" |
28 else {})" |
29 |
29 |
30 defs |
30 defs |
31 norRRset_def "norRRset m == BnorRset (m-#1,m)" |
31 norRRset_def "norRRset m == BnorRset (m-#1,m)" |
32 |
32 |
33 noXRRset_def "noXRRset m x == (%a. a*x)``(norRRset m)" |
33 noXRRset_def "noXRRset m x == (%a. a*x)`(norRRset m)" |
34 |
34 |
35 phi_def "phi m == card (norRRset m)" |
35 phi_def "phi m == card (norRRset m)" |
36 |
36 |
37 is_RRset_def "is_RRset A m == (A : (RsetR m)) & card(A) = (phi m)" |
37 is_RRset_def "is_RRset A m == (A : (RsetR m)) & card(A) = (phi m)" |
38 |
38 |