equal
deleted
inserted
replaced
53 apply (auto simp add: eqvt_at_def) |
53 apply (auto simp add: eqvt_at_def) |
54 apply (metis Pair_eqvt perm_supp_eq) |
54 apply (metis Pair_eqvt perm_supp_eq) |
55 apply (metis Pair_eqvt perm_supp_eq) |
55 apply (metis Pair_eqvt perm_supp_eq) |
56 done |
56 done |
57 |
57 |
58 termination (in name_subst) (eqvt) by lexicographic_order |
58 nominal_termination (in name_subst) (eqvt) by lexicographic_order |
59 |
59 |
60 inductive (in name_subst) beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<longrightarrow>\<^sub>\<beta>" 90) |
60 inductive (in name_subst) beta :: "lam \<Rightarrow> lam \<Rightarrow> bool" (infix "\<longrightarrow>\<^sub>\<beta>" 90) |
61 where |
61 where |
62 redex: "supp xs \<sharp>* u \<Longrightarrow> (Lam xs. t) \<cdot> u \<longrightarrow>\<^sub>\<beta> t[xs::=u]" |
62 redex: "supp xs \<sharp>* u \<Longrightarrow> (Lam xs. t) \<cdot> u \<longrightarrow>\<^sub>\<beta> t[xs::=u]" |
63 | "s \<longrightarrow>\<^sub>\<beta> s' \<Longrightarrow> s \<cdot> t \<longrightarrow>\<^sub>\<beta> s' \<cdot> t" |
63 | "s \<longrightarrow>\<^sub>\<beta> s' \<Longrightarrow> s \<cdot> t \<longrightarrow>\<^sub>\<beta> s' \<cdot> t" |