339 lemma trm1_supp:

   340   "supp (Vr1 x) = {atom x}"

   341   "supp (Ap1 t1 t2) = supp t1 \<union> supp t2"

   342   "supp (Lm1 x t) = (supp t) - {atom x}"

   343   "supp (Lt1 b t s) = supp t \<union> (supp s - bv1 b)"

   344   by (simp_all only: supp_fv fv_trm1)

   345 

   346 lemma trm1_induct_strong:

   347   assumes "\<And>name b. P b (Vr1 name)"

   348   and     "\<And>rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12\<rbrakk> \<Longrightarrow> P b (Ap1 rtrm11 rtrm12)"

   349   and     "\<And>name rtrm1 b. \<lbrakk>\<And>c. P c rtrm1; (atom name) \<sharp> b\<rbrakk> \<Longrightarrow> P b (Lm1 name rtrm1)"

   350   and     "\<And>bp rtrm11 rtrm12 b. \<lbrakk>\<And>c. P c rtrm11; \<And>c. P c rtrm12; bp1 bp \<sharp>* b\<rbrakk> \<Longrightarrow> P b (Lt1 bp rtrm11 rtrm12)"

   351   shows   "P a rtrma"

   352 

   353