equal
deleted
inserted
replaced
25 apply (simp_all add: Abs_fresh_iff)[2] |
25 apply (simp_all add: Abs_fresh_iff)[2] |
26 apply (erule fresh_eqvt_at) |
26 apply (erule fresh_eqvt_at) |
27 apply (simp add: finite_supp) |
27 apply (simp add: finite_supp) |
28 apply (simp add: fresh_Pair) |
28 apply (simp add: fresh_Pair) |
29 apply (simp add: eqvt_at_def) |
29 apply (simp add: eqvt_at_def) |
30 apply (simp add: swap_fresh_fresh) |
30 apply (simp add: flip_fresh_fresh) |
31 apply(simp) |
|
32 done |
31 done |
33 |
32 |
34 termination (eqvt) by lexicographic_order |
33 termination (eqvt) by lexicographic_order |
35 |
34 |
36 nominal_primrec |
35 nominal_primrec |
50 apply (simp_all add: Abs_fresh_iff) |
49 apply (simp_all add: Abs_fresh_iff) |
51 apply (erule fresh_eqvt_at) |
50 apply (erule fresh_eqvt_at) |
52 apply (simp add: finite_supp) |
51 apply (simp add: finite_supp) |
53 apply (simp add: fresh_Pair) |
52 apply (simp add: fresh_Pair) |
54 apply (simp add: eqvt_at_def) |
53 apply (simp add: eqvt_at_def) |
55 apply (simp add: swap_fresh_fresh) |
54 apply (simp add: flip_fresh_fresh) |
56 done |
55 done |
57 |
56 |
58 termination (eqvt) by lexicographic_order |
57 termination (eqvt) by lexicographic_order |
59 |
58 |
60 nominal_primrec |
59 nominal_primrec |