equal
deleted
inserted
replaced
167 "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
167 "(Lt5 (Lcons x (Vr5 y) Lnil) (Vr5 x)) = (Lt5 (Lcons y (Vr5 y) Lnil) (Vr5 y))" |
168 apply (simp add: alpha5_INJ) |
168 apply (simp add: alpha5_INJ) |
169 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
169 apply (rule_tac x="(x \<leftrightarrow> y)" in exI) |
170 apply (simp_all add: alpha_gen) |
170 apply (simp_all add: alpha_gen) |
171 apply (simp add: permute_trm5_lts fresh_star_def) |
171 apply (simp add: permute_trm5_lts fresh_star_def) |
172 apply (metis flip_at_simps(1) supp_at_base supp_eqvt) |
|
173 done |
172 done |
174 |
173 |
175 lemma lets_ok3: |
174 lemma lets_ok3: |
176 "x \<noteq> y \<Longrightarrow> |
175 "x \<noteq> y \<Longrightarrow> |
177 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
176 (Lt5 (Lcons x (Ap5 (Vr5 y) (Vr5 x)) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) \<noteq> |
184 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
183 "(Lt5 (Lcons x (Vr5 x) (Lcons y (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y))) = |
185 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
184 (Lt5 (Lcons y (Vr5 x) (Lcons x (Vr5 y) Lnil)) (Ap5 (Vr5 x) (Vr5 y)))" |
186 apply (simp add: alpha5_INJ alpha_gen) |
185 apply (simp add: alpha5_INJ alpha_gen) |
187 apply (rule_tac x="0::perm" in exI) |
186 apply (rule_tac x="0::perm" in exI) |
188 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
187 apply (simp add: permute_trm5_lts fresh_star_def alpha5_INJ(5) alpha5_INJ(2) alpha5_INJ(1) eqvts) |
189 apply auto |
|
190 done |
188 done |
191 |
189 |
192 lemma distinct_helper: |
190 lemma distinct_helper: |
193 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
191 shows "\<not>(rVr5 x \<approx>5 rAp5 y z)" |
194 apply auto |
192 apply auto |