47 \<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)" |
47 \<Longrightarrow> alpha_trm_raw (Foo1_raw pat_raw1 pat_raw2 trm_raw) (Foo1_raw pat_raw1a pat_raw2a trm_rawa)" |
48 | "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa); |
48 | "\<lbrakk>\<exists>p. ({atom name} \<union> f_raw pat_raw, trm_raw) \<approx>gen alpha_trm_raw fv_trm_raw p ({atom namea} \<union> f_raw pat_rawa, trm_rawa); |
49 alpha_f_raw pat_raw pat_rawa\<rbrakk> |
49 alpha_f_raw pat_raw pat_rawa\<rbrakk> |
50 \<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)" |
50 \<Longrightarrow> alpha_trm_raw (Foo2_raw name pat_raw trm_raw) (Foo2_raw namea pat_rawa trm_rawa)" |
51 |
51 |
|
52 (* alpha_pat_raw *) |
52 | "alpha_pat_raw PN_raw PN_raw" |
53 | "alpha_pat_raw PN_raw PN_raw" |
53 | "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)" |
54 | "name = namea \<Longrightarrow> alpha_pat_raw (PS_raw name) (PS_raw namea)" |
54 | "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk> |
55 | "\<lbrakk>alpha_pat_raw pat_raw1 pat_raw1a; alpha_pat_raw pat_raw2 pat_raw2a\<rbrakk> |
55 \<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
56 \<Longrightarrow> alpha_pat_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
56 |
57 |
|
58 (* alpha_f_raw *) |
57 | "alpha_f_raw PN_raw PN_raw" |
59 | "alpha_f_raw PN_raw PN_raw" |
58 | "alpha_f_raw (PS_raw name) (PS_raw namea)" |
60 | "alpha_f_raw (PS_raw name) (PS_raw namea)" |
59 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk> |
61 | "\<lbrakk>alpha_f_raw pat_raw1 pat_raw1a; alpha_f_raw pat_raw2 pat_raw2a\<rbrakk> |
60 \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
62 \<Longrightarrow> alpha_f_raw (PD_raw pat_raw1 pat_raw2) (PD_raw pat_raw1a pat_raw2a)" |
61 |
63 |