equal
deleted
inserted
replaced
52 newK :: "event list => key" |
52 newK :: "event list => key" |
53 |
53 |
54 rules |
54 rules |
55 inj_shrK "inj shrK" |
55 inj_shrK "inj shrK" |
56 |
56 |
57 inj_newN "inj newN" |
57 newN_length "(newN evs = newN evt) ==> (length evs = length evt)" |
|
58 newK_length "(newK evs = newK evt) ==> (length evs = length evt)" |
58 |
59 |
59 inj_newK "inj newK" |
|
60 newK_neq_shrK "newK evs ~= shrK A" |
60 newK_neq_shrK "newK evs ~= shrK A" |
61 isSym_newK "isSymKey (newK evs)" |
61 isSym_newK "isSymKey (newK evs)" |
62 |
62 |
63 end |
63 end |