equal
deleted
inserted
replaced
13 Goal "cockpit =<| Info_while_Al"; |
13 Goal "cockpit =<| Info_while_Al"; |
14 by (is_sim_tac aut_simps 1); |
14 by (is_sim_tac aut_simps 1); |
15 qed"cockpit_implements_Info_while_Al"; |
15 qed"cockpit_implements_Info_while_Al"; |
16 |
16 |
17 (* to prove that before any alarm arrives (and after each acknowledgment), |
17 (* to prove that before any alarm arrives (and after each acknowledgment), |
18 info remains at None *) |
18 info remains at NONE *) |
19 Goal "cockpit =<| Info_before_Al"; |
19 Goal "cockpit =<| Info_before_Al"; |
20 by (is_sim_tac aut_simps 1); |
20 by (is_sim_tac aut_simps 1); |
21 qed"cockpit_implements_Info_before_Al"; |
21 qed"cockpit_implements_Info_before_Al"; |
22 |
22 |
23 (* to prove that before any alarm would be acknowledged, it must be arrived *) |
23 (* to prove that before any alarm would be acknowledged, it must be arrived *) |