PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun enumer 1

1. n:
2. m:

f:((mn)(nm)). Bij(mn; (nm); f)

By: NatInd 2

Generated subgoals:

1 f:((0n)(n0)). Bij(0n; (n0); f)
22. m:
3. 0 < m
4. f:(((m-1)n)(nm-1)). Bij((m-1)n; (nm-1); f)
f:((mn)(nm)). Bij(mn; (nm); f)


About:
existsfunctionnatural_number