| changeset 3852 | e694c660055b |
| parent 3073 | 88366253a09a |
| child 10212 | 33fe2d701ddd |
| 3851:fe9932a7cd46 | 3852:e694c660055b |
|---|---|
38 |
38 |
39 countm_nonempty_def |
39 countm_nonempty_def |
40 "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" |
40 "countm (addm M x) P == countm M P + (if P x then Suc 0 else 0)" |
41 |
41 |
42 count_def |
42 count_def |
43 "count M x == countm M (%y.y = x)" |
43 "count M x == countm M (%y. y = x)" |
44 |
44 |
45 induction |
45 induction |
46 "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)" |
46 "[| P({|}); !!M x. P(M) ==> P(addm M x) |] ==> P(M)" |
47 |
47 |
48 end |
48 end |