equal
deleted
inserted
replaced
85 apply (rule_tac x="q" in exI) |
85 apply (rule_tac x="q" in exI) |
86 apply (simp add: alphas) |
86 apply (simp add: alphas) |
87 apply (simp add: permute_bn_alpha_bn) |
87 apply (simp add: permute_bn_alpha_bn) |
88 apply (simp add: perm_bn[symmetric]) |
88 apply (simp add: perm_bn[symmetric]) |
89 apply (simp add: eqvts[symmetric]) |
89 apply (simp add: eqvts[symmetric]) |
90 apply (simp add: supp_Abs) |
90 apply (simp add: supp_abs) |
91 apply (simp add: trm_lts.supp) |
91 apply (simp add: trm_lts.supp) |
92 apply (rule supp_perm_eq[symmetric]) |
92 apply (rule supp_perm_eq[symmetric]) |
93 apply (subst supp_finite_atom_set) |
93 apply (subst supp_finite_atom_set) |
94 apply (rule finite_Diff) |
94 apply (rule finite_Diff) |
95 apply (simp add: finite_supp) |
95 apply (simp add: finite_supp) |
155 apply(drule_tac x="q + p" in meta_spec) |
155 apply(drule_tac x="q + p" in meta_spec) |
156 apply(simp) |
156 apply(simp) |
157 apply(rule at_set_avoiding2) |
157 apply(rule at_set_avoiding2) |
158 apply(rule fin_bn) |
158 apply(rule fin_bn) |
159 apply(simp add: finite_supp) |
159 apply(simp add: finite_supp) |
160 apply(simp add: supp_Abs) |
160 apply(simp add: supp_abs) |
161 apply(rule finite_Diff) |
161 apply(rule finite_Diff) |
162 apply(simp add: finite_supp) |
162 apply(simp add: finite_supp) |
163 apply(simp add: fresh_star_def fresh_def supp_Abs) |
163 apply(simp add: fresh_star_def fresh_def supp_abs) |
164 apply(simp add: eqvts permute_bn) |
164 apply(simp add: eqvts permute_bn) |
165 apply(rule a5) |
165 apply(rule a5) |
166 apply(simp add: permute_bn) |
166 apply(simp add: permute_bn) |
167 apply(rule a6) |
167 apply(rule a6) |
168 apply simp |
168 apply simp |