Nuprl - Pf fun_enumer 1 2 1 2 2 1 2 1 1 1 1 1 1 2 1 1 2 1 1

PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun enumer 1 2 1 2 2 1 2 1 1 1 1 1 1 2 1 1 2 1 1

1. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-1)
5. a1,a2:((m-1)n). f(a1) = f(a2) a1 = a2
6. n = 0
7. f1: n(nm-1)(nm)
8. 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) > )
12. a1(m-1) = a2(m-1)
13. f(a1) = f(a2)
14. x: m
15. x = m-1 m

a1(x) = a2(x)

By: Witness5 a1

Generated subgoal:

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. a2:((m-1)n). f(a1) = f(a2) a1 = a2 (m-1)n
a1(x) = a2(x)

About: