PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun enumer 1 2 1 2 2 1 2 1 1 1 1 1
1. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-1)
5. Bij((m-1)n; (nm-1); f)
6. n = 0
7. f1: n(nm-1)(nm)
8. Inj(n(nm-1); (n(nm-1)); f1)
9. a1: mn
10. a2: mn
11. f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )

a1 = a2
By: Unfold `inject` 8
Generated subgoal:

18. a1,a2:(n(nm-1)). f1(a1) = f1(a2) (n(nm-1)) a1 = a2
9. a1: mn
10. a2: mn
11. f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )
a1 = a2

About:
equalfunctionnatural_numberintless_than
subtractproductmultiplyapplypair