equal
deleted
inserted
replaced
48 primrec sees list |
48 primrec sees list |
49 sees_Nil "sees lost A [] = initState lost A" |
49 sees_Nil "sees lost A [] = initState lost A" |
50 sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" |
50 sees_Cons "sees lost A (ev#evs) = sees1 A ev Un sees lost A evs" |
51 |
51 |
52 |
52 |
|
53 constdefs |
|
54 (*Set of items that might be visible to somebody: complement of the set |
|
55 of fresh items*) |
|
56 used :: event list => msg set |
|
57 "used evs == parts (UN lost B. sees lost B evs)" |
|
58 |
|
59 |
53 (*Agents generate "random" nonces, uniquely determined by their argument.*) |
60 (*Agents generate "random" nonces, uniquely determined by their argument.*) |
54 consts |
61 consts |
55 newN :: nat => nat |
62 newN :: nat => nat |
56 |
63 |
57 rules |
64 rules |