equal
deleted
inserted
replaced
11 apply (case_tac a, simp_all) |
11 apply (case_tac a, simp_all) |
12 (* |
12 (* |
13 apply |
13 apply |
14 induct s, case tac e, every event analysis |
14 induct s, case tac e, every event analysis |
15 *) |
15 *) |
|
16 thm s2ss_def |
|
17 |
|
18 |
16 sorry |
19 sorry |
17 |
20 |
18 lemma d2s_main': |
21 lemma d2s_main': |
19 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
22 "\<lbrakk>alive s obj; co2sobj s obj= Some sobj\<rbrakk> \<Longrightarrow> sobj \<in> (s2ss s)" |
20 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |
23 by (simp add:s2ss_def, rule_tac x = obj in exI, simp) |