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. n:
2. m:
3. 0 < m
4. f: ((m-1)n)(nm-1)
5. b:(nm-1). a:((m-1)n). f(a) = b
6. n = 0
7. f1: n(nm-1)(nm)
8. b: (nm)
9. a: n(nm-1)
10. f1(a) = b (n(nm-1))

a:(mn). f1( < a(m-1),f(a) > ) = b
By: Witness5 2of(a)
Generated subgoal:

15. 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). f(a@0) = 2of(a)
a:(mn). f1( < a(m-1),f(a) > ) = b

About:
existsfunctionnatural_numberequalapplypair
subtractintless_thanallproductmultiply