equal
deleted
inserted
replaced
32 apply(simp add: fresh_star_def fresh_Pair) |
32 apply(simp add: fresh_star_def fresh_Pair) |
33 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
33 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
34 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
34 apply(simp add: eqvt_at_def atom_eqvt fresh_star_Pair perm_supp_eq) |
35 done |
35 done |
36 |
36 |
37 termination (eqvt) |
37 nominal_termination (eqvt) |
38 by lexicographic_order |
38 by lexicographic_order |
39 |
39 |
40 lemma forget: |
40 lemma forget: |
41 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
41 shows "atom x \<sharp> t \<Longrightarrow> t[x ::= s] = t" |
42 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |
42 by (nominal_induct t avoiding: x s rule: lam.strong_induct) |