equal
deleted
inserted
replaced
7 Version incorporating Lowe's fix (inclusion of B's identity in round 2). |
7 Version incorporating Lowe's fix (inclusion of B's identity in round 2). |
8 *) |
8 *) |
9 |
9 |
10 NS_Public = Public + |
10 NS_Public = Public + |
11 |
11 |
12 consts lost :: agent set (*No need for it to be a variable*) |
12 consts lost :: agent set (*No need for it to be a variable*) |
13 ns_public :: event list set |
13 ns_public :: event list set |
|
14 |
14 inductive ns_public |
15 inductive ns_public |
15 intrs |
16 intrs |
16 (*Initial trace is empty*) |
17 (*Initial trace is empty*) |
17 Nil "[]: ns_public" |
18 Nil "[]: ns_public" |
18 |
19 |