PrintForm Definitions finite sets Sections AutomataTheory Doc

At: prod fin is fin 1 2 6 1 1
1. T: Type
2. t: T
3. n:
4. f: nT
5. a1,a2:n. f(a1) = f(a2) a1 = a2
6. Surj(n; T; f)
7. n > 0

a1,a2:(nn). (x. < f(x n),f(x rem n) > )(a1) = (x. < f(x n),f(x rem n) > )(a2) TT a1 = a2
By:
Reduce 0
THEN
RepD
Generated subgoals:

18. a1: (nn)
9. a2: (nn)
10. < f(a1 n),f(a1 rem n) > = < f(a2 n),f(a2 rem n) >
a1 = a2
28. a1: (nn)
9. a2: (nn)
0(a1 n)
38. a1: (nn)
9. a2: (nn)
(a1 n) < n
48. a1: (nn)
9. a2: (nn)
0(a1 rem n)
58. a1: (nn)
9. a2: (nn)
(a1 rem n) < n
68. a1: (nn)
9. a2: (nn)
0(a2 n)
78. a1: (nn)
9. a2: (nn)
(a2 n) < n
88. a1: (nn)
9. a2: (nn)
0(a2 rem n)
98. a1: (nn)
9. a2: (nn)
(a2 rem n) < n

About:
allnatural_numbermultiplyimpliesequalproductapply
lambdapairdivideremainderuniversefunctionless_than