PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
prod
fin
is
fin
1
2
4
1.
T:
Type
2.
t:
T
3.
n:
4.
f:
n
T
5.
Bij(
n; T; f)
6.
n > 0
7.
x:
(n
n)
0
(x rem n)
By:
Inst
Thm*
a:
, n:
. 0
(a rem n) & (a rem n) < n [x;n]
THEN
ProveProp
Generated subgoals:
None
About:
n
Tn; T; f)(n
n)
0
(x rem n)
a:, n:
. 0(a rem n) & (a rem n) < n
[x;n]
