equal
deleted
inserted
replaced
54 by Auto_tac; |
54 by Auto_tac; |
55 qed"live_implements"; |
55 qed"live_implements"; |
56 |
56 |
57 |
57 |
58 (* |
58 (* |
59 |
|
60 (* Classical Fairness and Fairness by Temporal Formula coincide *) |
|
61 |
|
62 Goal "!! ex. Finite (snd ex) ==> \ |
|
63 \ (ex |== WF A acts) = (~ Enabled A acts (laststate ex))"; |
|
64 |
|
65 In 3 steps: |
|
66 |
|
67 1) []<>P and <>[]P mean both P (Last`s) |
|
68 2) Transform this to executions and laststate |
|
69 3) plift is used to show that plift (laststate ex) : acts == False. |
|
70 |
|
71 |
|
72 |
|
73 *) |
|