13 thm lam.supp

    13 thm lam.supp

    14 lemmas supp_fn' = lam.fv[simplified lam.supp]

    14 lemmas supp_fn' = lam.fv[simplified lam.supp]

    15 

    15 

    16 declare lam.perm[eqvt]

    16 declare lam.perm[eqvt]

    17 

    17 

    19 equivariance alpha_lam_raw

    18 equivariance alpha_lam_raw

    20 

    19 

    21 section {* Strong Induction Principles*}

    20 section {* Strong Induction Principles*}

    22 

    21 

    23 (*

    22 (*

   257 | a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>

   256 | a2: "\<lbrakk>alpha_lam_raw' lam_raw1 lam_raw1a; alpha_lam_raw' lam_raw2 lam_raw2a\<rbrakk> \<Longrightarrow>

   258    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"

   257    alpha_lam_raw' (App_raw lam_raw1 lam_raw2) (App_raw lam_raw1a lam_raw2a)"

   259 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>

   258 | a3: "\<exists>pi. ({atom name}, lam_raw) \<approx>gen alpha_lam_raw' fv_lam_raw pi ({atom namea}, lam_rawa) \<Longrightarrow>

   260    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"

   259    alpha_lam_raw' (Lam_raw name lam_raw) (Lam_raw namea lam_rawa)"

   261 

   260 

   263 equivariance alpha_lam_raw'

   261 equivariance alpha_lam_raw'

   264 

   262 

   265 thm eqvts_raw

   263 thm eqvts_raw

   266 

   264 

   267 section {* size function *}

   265 section {* size function *}