equal
deleted
inserted
replaced
41 (is_ref_map f (fst CL ) (fst AM) & |
41 (is_ref_map f (fst CL ) (fst AM) & |
42 (! exec : executions (fst CL). (exec |== (snd CL)) --> |
42 (! exec : executions (fst CL). (exec |== (snd CL)) --> |
43 ((corresp_ex (fst AM) f exec) |== (snd AM))))" |
43 ((corresp_ex (fst AM) f exec) |== (snd AM))))" |
44 |
44 |
45 |
45 |
46 declare split_paired_Ex [simp del] |
|
47 |
|
48 lemma live_implements_trans: |
46 lemma live_implements_trans: |
49 "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] |
47 "!!LC. [| live_implements (A,LA) (B,LB); live_implements (B,LB) (C,LC) |] |
50 ==> live_implements (A,LA) (C,LC)" |
48 ==> live_implements (A,LA) (C,LC)" |
51 apply (unfold live_implements_def) |
49 apply (unfold live_implements_def) |
52 apply auto |
50 apply auto |