| changeset 2973 | d1038e67923a |
| parent 2971 | d629240f0f63 |
| child 2974 | b95a2065aa10 |
| 2972:84afb941df53 | 2973:d1038e67923a |
|---|---|
57 apply(simp add: eqvt_at_def) |
57 apply(simp add: eqvt_at_def) |
58 apply(perm_simp) |
58 apply(perm_simp) |
59 apply (simp add: permute_fun_def) |
59 apply (simp add: permute_fun_def) |
60 done |
60 done |
61 |
61 |
62 termination by lexicographic_order |
62 thm height_trm_def height_bp_def |
63 |
|
64 termination (eqvt) by lexicographic_order |
|
63 |
65 |
64 end |
66 end |
65 |
67 |
66 |
68 |
67 |
69 |