equal
deleted
inserted
replaced
41 "is_live_abstraction h CL AM == |
41 "is_live_abstraction h CL AM == |
42 is_abstraction h (fst CL) (fst AM) & |
42 is_abstraction h (fst CL) (fst AM) & |
43 temp_weakening (snd AM) (snd CL) h" |
43 temp_weakening (snd AM) (snd CL) h" |
44 |
44 |
45 cex_abs_def |
45 cex_abs_def |
46 "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))`(snd ex))" |
46 "cex_abs f ex == (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))" |
47 |
47 |
48 (* equals cex_abs on Sequneces -- after ex2seq application -- *) |
48 (* equals cex_abs on Sequneces -- after ex2seq application -- *) |
49 cex_absSeq_def |
49 cex_absSeq_def |
50 "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))`s" |
50 "cex_absSeq f == % s. Map (%(s,a,t). (f s,a,f t))$s" |
51 |
51 |
52 weakeningIOA_def |
52 weakeningIOA_def |
53 "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" |
53 "weakeningIOA A C h == ! ex. ex : executions C --> cex_abs h ex : executions A" |
54 |
54 |
55 temp_weakening_def |
55 temp_weakening_def |