equal
deleted
inserted
replaced
68 apply (simp add: eqvt_at_def) |
68 apply (simp add: eqvt_at_def) |
69 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
69 apply (simp add: swap_fresh_fresh fresh_Pair_elim) |
70 apply (erule fresh_eqvt_at) |
70 apply (erule fresh_eqvt_at) |
71 apply (simp add: supp_Inr finite_supp) |
71 apply (simp add: supp_Inr finite_supp) |
72 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
72 apply (simp add: fresh_Inr fresh_Pair lt.fresh fresh_at_base) |
73 apply (simp only: ) |
73 apply (simp only:) |
|
74 apply (simp (no_asm)) |
74 apply (erule_tac c="a" in Abs_lst1_fcb2') |
75 apply (erule_tac c="a" in Abs_lst1_fcb2') |
75 apply (simp add: Abs_fresh_iff lt.fresh) |
76 apply (simp add: Abs_fresh_iff lt.fresh) |
76 apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base) |
77 apply (simp add: fresh_star_def fresh_Pair_elim lt.fresh fresh_at_base) |
77 apply (subgoal_tac "p \<bullet> CPS1_CPS2_sumC (Inr (M, a~)) = CPS1_CPS2_sumC (p \<bullet> (Inr (M, a~)))") |
|
78 apply (simp add: perm_supp_eq fresh_star_def lt.fresh) |
|
79 oops |
78 oops |
80 |
79 |
81 end |
80 end |
82 |
81 |
83 |
82 |