equal
deleted
inserted
replaced
215 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
215 apply (metis Nominal2_Base.swap_commute fresh_permute_iff permute_swap_cancel2) |
216 apply (simp add: fresh_def supp_at_base) |
216 apply (simp add: fresh_def supp_at_base) |
217 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
217 apply (metis atom_eq_iff permute_swap_cancel2 swap_atom_simps(3)) |
218 done |
218 done |
219 |
219 |
220 termination |
220 termination (eqvt) |
221 by lexicographic_order |
221 by lexicographic_order |
222 |
222 |
223 definition psi:: "lt => lt" |
223 definition psi:: "lt => lt" |
224 where [simp]: "psi V == V*(\<lambda>x. x)" |
224 where [simp]: "psi V == V*(\<lambda>x. x)" |
225 |
225 |