equal
deleted
inserted
replaced
45 apply(auto) |
45 apply(auto) |
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
46 apply(erule_tac c="()" in Abs_lst1_fcb2) |
47 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
47 apply(simp_all add: fresh_def pure_supp eqvt_at_def fresh_star_def) |
48 done |
48 done |
49 |
49 |
50 termination (eqvt) |
50 nominal_termination (eqvt) |
51 by lexicographic_order |
51 by lexicographic_order |
52 |
52 |
53 |
53 |
54 subsection {* Capture-Avoiding Substitution *} |
54 subsection {* Capture-Avoiding Substitution *} |
55 |
55 |
74 apply(simp add: perm_supp_eq fresh_star_Pair) |
74 apply(simp add: perm_supp_eq fresh_star_Pair) |
75 apply(simp add: eqvt_at_def) |
75 apply(simp add: eqvt_at_def) |
76 apply(simp add: perm_supp_eq fresh_star_Pair) |
76 apply(simp add: perm_supp_eq fresh_star_Pair) |
77 done |
77 done |
78 |
78 |
79 termination (eqvt) |
79 nominal_termination (eqvt) |
80 by lexicographic_order |
80 by lexicographic_order |
81 |
81 |
82 lemma fresh_fact: |
82 lemma fresh_fact: |
83 assumes a: "atom z \<sharp> s" |
83 assumes a: "atom z \<sharp> s" |
84 and b: "z = y \<or> atom z \<sharp> t" |
84 and b: "z = y \<or> atom z \<sharp> t" |