Nuprl - Pf fun_enumer 1 2 1 2 2 1 2 1 1 2 1 1 1 1 2 1 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 2 1 1 1 1 1

1. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-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)

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

By: Witness z.if z=m-1 1of(a) else a@0(z) fi

Generated subgoals:

1 (z.if z=m-1 1of(a) else a@0(z) fi) mn

2 f1( < (z.if z=m-1 1of(a) else a@0(z) fi)(m-1),f(z.if z=m-1 1of(a) else a@0(z) fi) > ) = b

3 12. a1: mn
f1( < a1(m-1),f(a1) > ) = b Prop

About:

1	`(z.if z=m-1 1of(a) else a@0(z) fi) mn`
2	`f1( < (z.if z=m-1 1of(a) else a@0(z) fi)(m-1),f(z.if z=m-1 1of(a) else a@0(z) fi) > ) = b`
3	12. `a1:` `mn` `f1( < a1(m-1),f(a1) > ) = b Prop`