PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dist
func
1
1
1
1.
St:
Type
2.
n:
3.
n ~ St
eq:(St
St
).
x,y:St. eq(x,y)
x = y
By:
Analyze -1
THEN
Analyze -1
Generated subgoal:
1
3.
f:
n
St
4.
g:
St
n
5.
InvFuns(
n; St; f; g)
eq:(St
St
).
x,y:St. eq(x,y)
x = y
About:
n
Stnn; St; f; g)
eq:(StSt
). 
x,y:St. eq(x,y) 
x = yn ~ St eq:(StSt). x,y:St. eq(x,y) x = ynStnn; St; f; g) eq:(StSt). x,y:St. eq(x,y) x = y
