PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
1
2
6
1
1
1
1.
T:
Type
2.
t:
T
3.
n:
4.
f:
n
T
5.
a1,a2:
n. f(a1) = f(a2)
a1 = a2
6.
Surj(
n; T; f)
7.
n > 0
8.
a1:
(n
n)
9.
a2:
(n
n)
10.
< f(a1
n),f(a1 rem n) > = < f(a2
n),f(a2 rem n) >
a1 = a2
By:
Analyze -1
THEN
Reduce -1
THEN
Reduce -2
Generated subgoal:
1
10.
f(a1
n) = f(a2
n)
11.
f(a1 rem n) = f(a2 rem n)
a1 = a2
About:
n) = f(a2 n)
a1 = a2
n
T
a1,a2:n. f(a1) = f(a2) 
a1 = a2n; T; f)(n
n)(nn) n),f(a1 rem n) > = < f(a2 n),f(a2 rem n) > a1 = a2 n) = f(a2 n) a1 = a2
