equal
deleted
inserted
replaced
13 | "(x~)^l = l $$ (x~)" |
13 | "(x~)^l = l $$ (x~)" |
14 | "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))" |
14 | "(M$$N)^l = M*(%m. (N*(%n.((m $$ n) $$ l))))" |
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))" |
15 | "atom c \<sharp> (x, M) \<Longrightarrow> (Lam x M)^l = l $$ (Lam x (Lam c (M^(c~))))" |
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
16 apply (simp only: eqvt_def CPS1_CPS2_graph_def) |
17 apply (rule, perm_simp, rule) |
17 apply (rule, perm_simp, rule) |
|
18 using [[simproc del: alpha_lst]] |
18 apply auto |
19 apply auto |
19 apply (case_tac x) |
20 apply (case_tac x) |
20 apply (case_tac a) |
21 apply (case_tac a) |
21 apply (case_tac "eqvt b") |
22 apply (case_tac "eqvt b") |
22 apply (rule_tac y="aa" in lt.strong_exhaust) |
23 apply (rule_tac y="aa" in lt.strong_exhaust) |