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

PrintForm Definitions exponent Sections AutomataTheory Doc

At: fun enumer 1 2 1 2 2 1 2 1 1 2 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. b:(n(nm-1)). a:(n(nm-1)). f1(a) = b (n(nm-1))
9. b: (nm)

a:(mn). f1( < a(m-1),f(a) > ) = b

By: Witness8 b

Generated subgoals:

1 8. b: (nm)
b (n(nm-1))

2 8. b: (nm)
9. a:(n(nm-1)). f1(a) = b (n(nm-1))
a:(mn). f1( < a(m-1),f(a) > ) = b

About:

1	8. `b:` `(nm)` `b (n(nm-1))`
2	8. `b:` `(nm)` 9. `a:(n(nm-1)). f1(a) = b (n(nm-1))` `a:(mn). f1( < a(m-1),f(a) > ) = b`