equal
deleted
inserted
replaced
13 |
13 |
14 datatype pvar = Sent | Rcvd | Idle |
14 datatype pvar = Sent | Rcvd | Idle |
15 |
15 |
16 datatype pname = Aproc | Bproc |
16 datatype pname = Aproc | Bproc |
17 |
17 |
18 types state = "pname * pvar => nat" |
18 type_synonym state = "pname * pvar => nat" |
19 |
19 |
20 locale F_props = |
20 locale F_props = |
21 fixes F |
21 fixes F |
22 assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}" |
22 assumes rsA: "F \<in> stable {s. s(Bproc,Rcvd) \<le> s(Aproc,Sent)}" |
23 and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}" |
23 and rsB: "F \<in> stable {s. s(Aproc,Rcvd) \<le> s(Bproc,Sent)}" |