equal
deleted
inserted
replaced
18 |
18 |
19 Goal "acts <= Acts prg ==> stable acts (reachable prg)"; |
19 Goal "acts <= Acts prg ==> stable acts (reachable prg)"; |
20 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); |
20 by (blast_tac (claset() addIs ([stableI, constrainsI] @ reachable.intrs)) 1); |
21 qed "stable_reachable"; |
21 qed "stable_reachable"; |
22 |
22 |
|
23 Goal "(act : Acts(|Init=init, Acts=acts|)) = (act:acts)"; |
|
24 auto(); |
|
25 qed "Acts_eq"; |
|
26 |
|
27 Goal "(s : Init(|Init=init, Acts=acts|)) = (s:init)"; |
|
28 auto(); |
|
29 qed "Init_eq"; |
|
30 |
|
31 AddIffs [Acts_eq, Init_eq]; |