equal
deleted
inserted
replaced
20 apply perm_simp |
20 apply perm_simp |
21 apply auto |
21 apply auto |
22 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
22 apply (rule_tac y="a" and c="b" in cpsctxt.strong_exhaust) |
23 apply (auto simp add: fresh_star_def) |
23 apply (auto simp add: fresh_star_def) |
24 apply (erule Abs_lst1_fcb) |
24 apply (erule Abs_lst1_fcb) |
25 apply (simp_all add: Abs_fresh_iff) |
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 swap_fresh_fresh) |
29 apply (simp add: eqvt_at_def) |
|
30 apply (simp add: swap_fresh_fresh) |
|
31 apply(simp) |
30 done |
32 done |
31 |
33 |
32 termination (eqvt) by lexicographic_order |
34 termination (eqvt) by lexicographic_order |
33 |
35 |
34 nominal_primrec |
36 nominal_primrec |
47 apply (erule Abs_lst1_fcb) |
49 apply (erule Abs_lst1_fcb) |
48 apply (simp_all add: Abs_fresh_iff) |
50 apply (simp_all add: Abs_fresh_iff) |
49 apply (erule fresh_eqvt_at) |
51 apply (erule fresh_eqvt_at) |
50 apply (simp add: finite_supp) |
52 apply (simp add: finite_supp) |
51 apply (simp add: fresh_Pair) |
53 apply (simp add: fresh_Pair) |
52 apply (simp add: eqvt_at_def swap_fresh_fresh) |
54 apply (simp add: eqvt_at_def) |
|
55 apply (simp add: swap_fresh_fresh) |
53 done |
56 done |
54 |
57 |
55 termination (eqvt) by lexicographic_order |
58 termination (eqvt) by lexicographic_order |
56 |
59 |
57 nominal_primrec |
60 nominal_primrec |