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

PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun enumer 1 2 1 2 2 1 2 1 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. 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

By: InstHyp [ < a1(m-1),f(a1) > ; < a2(m-1),f(a2) > ] 8

Generated subgoals:

1 f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > ) (n(nm-1))

2 12. < a1(m-1),f(a1) > = < a2(m-1),f(a2) >
a1 = a2

About:

1	`f1( < a1(m-1),f(a1) > ) = f1( < a2(m-1),f(a2) > ) (n(nm-1))`
2	12. `< a1(m-1),f(a1) > = < a2(m-1),f(a2) >` `a1 = a2`