| changeset 2082 | 0854af516f14 |
| parent 2028 | 15c5a2926622 |
| child 2104 | 2205b572bc9b |
| 2081:9e7cf0a996d3 | 2082:0854af516f14 |
|---|---|
28 thm trm_pat.perm |
28 thm trm_pat.perm |
29 thm trm_pat.induct |
29 thm trm_pat.induct |
30 thm trm_pat.distinct |
30 thm trm_pat.distinct |
31 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
31 thm trm_pat.fv[simplified trm_pat.supp(1-2)] |
32 |
32 |
33 |
|
34 declare permute_trm_raw_permute_pat_raw.simps[eqvt] |
|
35 declare alpha_gen_eqvt[eqvt] |
|
36 |
|
37 equivariance alpha_trm_raw |
|
38 |
|
39 |
|
33 end |
40 end |
34 |
41 |
35 |
42 |
36 |
43 |