PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
1
2
6
2
1
1
1
4
1.
T:
Type
2.
t:
T
3.
n:
4.
f:
n
T
5.
Inj(
n; T; f)
6.
b:T.
a:
n. f(a) = b
7.
n > 0
8.
b1:
T
9.
b2:
T
10.
a:
n
11.
f(a) = b1
12.
a1:
n
13.
f(a1) = b2
14.
a2:
(n
n)
(
x. < f(x
n),f(x rem n) > )(a2)
T
T
By:
Reduce 0
Generated subgoals:
1
0
(a2
n)
2
(a2
n) < n
3
0
(a2 rem n)
4
(a2 rem n) < n
About:
0
(a2 
n)
T
b:T. 
a:
n)
x. < f(x 
T
T
