equal
deleted
inserted
replaced
32 thm trm_lts.inducts[no_vars] |
32 thm trm_lts.inducts[no_vars] |
33 thm trm_lts.distinct |
33 thm trm_lts.distinct |
34 (*thm trm_lts.supp*) |
34 (*thm trm_lts.supp*) |
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
35 thm trm_lts.fv[simplified trm_lts.supp(1-2)] |
36 |
36 |
37 |
37 equivariance alpha_bn_raw |
38 declare permute_trm_raw_permute_lts_raw.simps[eqvt] |
|
39 |
|
40 equivariance alpha_trm_raw |
|
41 |
|
42 |
|
43 |
38 |
44 primrec |
39 primrec |
45 permute_bn_raw |
40 permute_bn_raw |
46 where |
41 where |
47 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |
42 "permute_bn_raw pi (Lnil_raw) = Lnil_raw" |