equal
deleted
inserted
replaced
40 definition nmsg_lte :: "nat => edge => state set" where |
40 definition nmsg_lte :: "nat => edge => state set" where |
41 "nmsg_lte k == %e. {s. nmsg s e \<le> k}" |
41 "nmsg_lte k == %e. {s. nmsg s e \<le> k}" |
42 |
42 |
43 definition final :: "state set" where |
43 definition final :: "state set" where |
44 "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> |
44 "final == (\<Inter>v\<in>V. reachable v <==> {s. (root, v) \<in> REACHABLE}) \<inter> |
45 (INTER E (nmsg_eq 0))" |
45 (\<Inter>((nmsg_eq 0) ` E))" |
46 |
46 |
47 axiomatization |
47 axiomatization |
48 where |
48 where |
49 Graph1: "root \<in> V" and |
49 Graph1: "root \<in> V" and |
50 |
50 |