equal
deleted
inserted
replaced
158 apply (simp add: eqvt_at_def height_trm_def) |
158 apply (simp add: eqvt_at_def height_trm_def) |
159 apply (simp add: eqvt_at_def height_trm_def) |
159 apply (simp add: eqvt_at_def height_trm_def) |
160 apply (simp add: eqvt_at_def height_bp_def) |
160 apply (simp add: eqvt_at_def height_bp_def) |
161 apply (simp add: eqvt_at_def height_bp_def) |
161 apply (simp add: eqvt_at_def height_bp_def) |
162 --"I'd like to apply FCB here, but the following fails" |
162 --"I'd like to apply FCB here, but the following fails" |
163 apply (erule_tac c="()" and ba="bn" in Abs_lst_fcb2) |
163 apply (subgoal_tac "height_bp bp = height_bp bpa") |
164 |
164 apply (subgoal_tac "height_trm b = height_trm ba") |
165 prefer 8 |
165 apply simp |
166 apply(assumption) |
166 apply (subgoal_tac "(\<lambda>as x c. height_trm (snd (bp, b))) as x c = (\<lambda>as x c. height_trm (snd (bpa, ba))) as x c") |
167 apply (drule_tac c="()" in Abs_lst_fcb2) |
167 apply simp |
168 apply (simp add: Abs_eq_iff2) |
168 apply (erule_tac c="()" and ba="bn" and f="\<lambda>as x c. height_trm (snd x)" in Abs_lst_fcb2) |
169 apply (simp add: alphas) |
169 ... |
170 apply clarify |
|
171 apply (rule trans) |
|
172 apply(rule_tac p="p" in supp_perm_eq[symmetric]) |
|
173 apply (simp add: pure_supp fresh_star_def) |
|
174 apply (simp only: eqvts) |
|
175 apply (simp add: eqvt_at_def) |
|
176 done |
170 done |
177 |
171 |
178 termination by lexicographic_order |
172 termination by lexicographic_order |
179 |
173 |
180 end |
174 end |