PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
1
2
6
2
1
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.
b:
T
T
a:
(n
n). (
x. < f(x
n),f(x rem n) > )(a) = b
By:
Analyze 8
Generated subgoal:
1
8.
b1:
T
9.
b2:
T
a:
(n
n). (
x. < f(x
n),f(x rem n) > )(a) = < b1,b2 >
About:
a:
(n
n). (
x. < f(x 
n),f(x rem n) > )(a) = < b1,b2 > n
Tn; T; f)
b:T. a:n. f(a) = b
T a:(nn). (x. < f(x n),f(x rem n) > )(a) = b a:(nn). (x. < f(x n),f(x rem n) > )(a) = < b1,b2 > 
