equal
deleted
inserted
replaced
52 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
52 "xb \<approx>l ya \<Longrightarrow> (x \<bullet> xb) \<approx>l (x \<bullet> ya)" |
53 "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)" |
53 "alpha_rbv5 a b c \<Longrightarrow> alpha_rbv5 (x \<bullet> a) (x \<bullet> b) (x \<bullet> c)" |
54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
54 apply (induct rule: alpha_rtrm5_alpha_rlts_alpha_rbv5.inducts) |
55 apply (simp_all add: alpha5_inj permute_eqvt[symmetric]) |
55 apply (simp_all add: alpha5_inj permute_eqvt[symmetric]) |
56 apply (erule exE) |
56 apply (erule exE) |
57 apply (rule_tac x="pi" in exI) |
57 apply (rule_tac x="x \<bullet> pi" in exI) |
58 apply (simp add: alpha_gen) |
58 apply (erule conjE)+ |
59 apply clarify |
59 apply (rule conjI) |
60 apply (simp add: fv_rtrm5_rlts_eqvt[symmetric] rbv5_eqvt[symmetric]) |
60 apply (erule alpha_gen_compose_eqvt) |
|
61 apply (simp_all add: eqvts) |
|
62 apply (simp add: permute_eqvt[symmetric]) |
61 apply (subst eqvts[symmetric]) |
63 apply (subst eqvts[symmetric]) |
62 apply (subst eqvts[symmetric]) |
64 apply (simp add: eqvts) |
63 apply (subst permute_eqvt) |
65 done |
64 apply simp |
|
65 sorry |
|
66 |
66 |
67 lemma alpha5_equivp: |
67 lemma alpha5_equivp: |
68 "equivp alpha_rtrm5" |
68 "equivp alpha_rtrm5" |
69 "equivp alpha_rlts" |
69 "equivp alpha_rlts" |
70 sorry |
70 sorry |