442 done

   442 done

   443 

   443 

   444 termination supp_lst 

   444 termination supp_lst 

   445   by (auto intro!: local.termination)

   445   by (auto intro!: local.termination)

   446 

   446 

   448   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"

   448   shows "(p \<bullet> supp_set x) = supp_set (p \<bullet> x)"

   449   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"

   449   and   "(p \<bullet> supp_res y) = supp_res (p \<bullet> y)"

   450   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"

   450   and   "(p \<bullet> supp_lst z) = supp_lst (p \<bullet> z)"

   451   apply(case_tac x rule: Abs_exhausts(1))

   451   apply(case_tac x rule: Abs_exhausts(1))

   452   apply(simp add: supp_eqvt Diff_eqvt)

   452   apply(simp add: supp_eqvt Diff_eqvt)

   459 lemma Abs_fresh_aux:

   459 lemma Abs_fresh_aux:

   460   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"

   460   shows "a \<sharp> Abs bs x \<Longrightarrow> a \<sharp> supp_set (Abs bs x)"

   461   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"

   461   and   "a \<sharp> Abs_res bs x \<Longrightarrow> a \<sharp> supp_res (Abs_res bs x)"

   462   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"

   462   and   "a \<sharp> Abs_lst cs x \<Longrightarrow> a \<sharp> supp_lst (Abs_lst cs x)"

   463   by (rule_tac [!] fresh_fun_eqvt_app)

   463   by (rule_tac [!] fresh_fun_eqvt_app)

   465 

   465 

   466 lemma Abs_supp_subset1:

   466 lemma Abs_supp_subset1:

   467   assumes a: "finite (supp x)"

   467   assumes a: "finite (supp x)"

   468   shows "(supp x) - as \<subseteq> supp (Abs_set as x)"

   468   shows "(supp x) - as \<subseteq> supp (Abs_set as x)"

   469   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"

   469   and   "(supp x) - as \<subseteq> supp (Abs_res as x)"