equal
deleted
inserted
replaced
44 apply (case_tac a rule: let_rec.exhaust(1)) |
44 apply (case_tac a rule: let_rec.exhaust(1)) |
45 apply auto |
45 apply auto |
46 apply (case_tac b rule: let_rec.exhaust(2)) |
46 apply (case_tac b rule: let_rec.exhaust(2)) |
47 apply blast |
47 apply blast |
48 apply (erule Abs_set_fcb) |
48 apply (erule Abs_set_fcb) |
49 apply (simp_all add: pure_fresh) |
49 apply (simp_all add: pure_fresh)[2] |
50 apply (simp add: eqvt_at_def) |
50 apply (simp only: eqvt_at_def) |
|
51 apply(perm_simp) |
|
52 apply(simp) |
51 apply (simp add: Abs_eq_iff2) |
53 apply (simp add: Abs_eq_iff2) |
52 apply (simp add: alphas) |
54 apply (simp add: alphas) |
53 apply clarify |
55 apply clarify |
54 apply (rule trans) |
56 apply (rule trans) |
55 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
57 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
56 apply (simp add: pure_supp fresh_star_def) |
58 apply (simp add: pure_supp fresh_star_def) |
57 apply(simp add: eqvt_at_def) |
59 apply(simp add: eqvt_at_def) |
58 apply(perm_simp) |
|
59 apply (simp add: permute_fun_def) |
|
60 done |
60 done |
61 |
61 |
62 termination (eqvt) by lexicographic_order |
62 termination (eqvt) by lexicographic_order |
63 |
63 |
64 thm height_trm_height_bp.eqvt |
64 thm height_trm_height_bp.eqvt |