
val aut_simps = [cockpit_def,cockpit_asig_def,cockpit_trans_def,
		cockpit_initial_def,cockpit_hide_def,
		Al_before_Ack_def,Al_before_Ack_asig_def,
		Al_before_Ack_initial_def,Al_before_Ack_trans_def,
		Info_while_Al_def,Info_while_Al_asig_def,
		Info_while_Al_initial_def,Info_while_Al_trans_def,
		Info_before_Al_def,Info_before_Al_asig_def,
		Info_before_Al_initial_def,Info_before_Al_trans_def];


(* to prove, that info is always set at the recent alarm *)
Goal "cockpit =<| Info_while_Al";
by (is_sim_tac aut_simps 1);
qed"cockpit_implements_Info_while_Al";

(* to prove that before any alarm arrives (and after each acknowledgment),
   info remains at None *)
Goal "cockpit =<| Info_before_Al";
by (is_sim_tac aut_simps 1);       
qed"cockpit_implements_Info_before_Al";

(* to prove that before any alarm would be acknowledged, it must be arrived *)
Goal "cockpit_hide =<| Al_before_Ack";
by (is_sim_tac aut_simps 1);       
by Auto_tac;
qed"cockpit_implements_Al_before_Ack";
