PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dist
func
1
1.
St:
Type
2.
Fin(St)
eq:(St
St
).
x,y:St. eq(x,y)
x = y
By:
Analyze 2
Generated subgoal:
1
2.
n:
3.
f:(
n
St). Bij(
n; St; f)
eq:(St
St
).
x,y:St. eq(x,y)
x = y
About:
f:(n
St). Bij(n; St; f)
eq:(StSt
). 
x,y:St. eq(x,y) 
x = y eq:(StSt). x,y:St. eq(x,y) x = yf:(nSt). Bij(n; St; f) eq:(StSt). x,y:St. eq(x,y) x = y
