11 qed"exis_elim"; |
11 qed"exis_elim"; |
12 |
12 |
13 Delsimps [split_paired_All]; |
13 Delsimps [split_paired_All]; |
14 Addsimps |
14 Addsimps |
15 ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, |
15 ([srch_asig_def, rsch_asig_def, rsch_ioa_def, srch_ioa_def, ch_ioa_def, |
16 ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, asig_of_def, |
16 ch_asig_def, srch_actions_def, rsch_actions_def, rename_def, rename_set_def, asig_of_def, |
17 actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, |
17 actions_def, exis_elim, srch_trans_def, rsch_trans_def, ch_trans_def, |
18 trans_of_def] @ asig_projections @ set_lemmas); |
18 trans_of_def] @ asig_projections @ set_lemmas); |
19 |
19 |
20 val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, |
20 val abschannel_fin = [srch_fin_asig_def, rsch_fin_asig_def, |
21 rsch_fin_ioa_def, srch_fin_ioa_def, |
21 rsch_fin_ioa_def, srch_fin_ioa_def, |