At: fun enumer 1 2 1 2 2 1 2 1 1 1 1 1 1 2 1 1 2 1 1 1 1 1
1. n: 
2. m: 
3. 0 < m
4. f: ((m-1)
n)(n
m-1)
5. 
n = 0
6. f1: n
(nm-1)(nm)
7. 
a1,a2:(n(nm-1)). f1(a1) = f1(a2) 
(n
(nm-1)) 
a1 = a2
8. a1: mn
9. a2: mn
10. f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > )
11. a1(m-1) = a2(m-1)
12. f(a1) = f(a2)
13. x: m
14. x = m-1 m
15. a1 = a2 (m-1)n
x (m-1)
By: Auto
Generated subgoal:| 1 | x < m-1 |
About:
