equal
deleted
inserted
replaced
69 apply (rule impI) |
69 apply (rule impI) |
70 apply (erule alpha_weird_raw.cases) |
70 apply (erule alpha_weird_raw.cases) |
71 apply (simp_all add: weird_inj) |
71 apply (simp_all add: weird_inj) |
72 apply (erule conjE)+ |
72 apply (erule conjE)+ |
73 apply (erule exE)+ |
73 apply (erule exE)+ |
|
74 apply (erule conjE)+ |
|
75 apply (erule exE)+ |
74 apply (rule conjI) |
76 apply (rule conjI) |
75 apply (rule_tac x="pica + pic" in exI) |
77 apply (rule_tac x="pica + pic" in exI) |
76 apply (erule alpha_gen_compose_trans) |
78 apply (erule alpha_gen_compose_trans) |
77 apply assumption |
79 apply assumption |
78 apply (simp add: alpha_eqvt) |
80 apply (simp add: alpha_eqvt) |
|
81 apply (rule_tac x="pia + pib" in exI) |
|
82 apply (rule_tac x="piaa + piba" in exI) |
79 apply (rule conjI) |
83 apply (rule conjI) |
80 defer |
|
81 apply (rule_tac x="pia + pi" in exI) |
|
82 apply (erule alpha_gen_compose_trans) |
84 apply (erule alpha_gen_compose_trans) |
83 apply assumption |
85 apply assumption |
84 apply (simp add: alpha_eqvt) |
86 apply (simp add: alpha_eqvt) |
85 (* Normally: (pia + pb + (pib + pa)) *) |
87 apply (rule conjI) |
86 apply (rule_tac x="piaa + pib" in exI) |
88 defer |
87 apply (rule_tac x="piab + piba" in exI) |
89 apply (rule_tac x="pid + pi" in exI) |
88 apply (erule alpha_gen_compose_trans) |
90 apply (erule alpha_gen_compose_trans) |
89 apply assumption |
91 apply assumption |
90 apply (simp add: alpha_eqvt) |
92 apply (simp add: alpha_eqvt) |
91 done |
93 done |
92 |
94 |