At: fun enumer 1 2 1 2 2 1 2 1 1 2 1 1 1 1 2 1 1 1 1 1 2 1 1 2 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. b: (nm)
8. a: n(nm-1)
9. f1(a) = b 
(n
(nm-1))
10. a@0: (m-1)n
11. f(a@0) = 2of(a)
12. m-1 = m-1
13. (
z.if z=
m-1
1of(a) else a@0(z) fi) = a@0
< 1of(a),2of(a) > = a
By: RWH
(LemmaC
Thm* 
B:(AType), p:a:AB(a). < 1of(p),2of(p) > = p a:AB(a))
0
Generated subgoals:None
About:
