PrintForm
Definitions
finite
sets
Sections
AutomataTheory
Doc
At:
fin
dist
func
1
1
1
1
1.
St:
Type
2.
n:
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
By:
InstConcl [
x,y. g(x)=
g(y)]
Generated subgoal:
1
x,y:St. (
x,y. g(x)=
g(y))(x,y)
x = y
About:
x,y:St. (
x,y. g(x)=
g(y))(x,y) 
x = y
n
Stnn; St; f; g) 
eq:(StSt
). x,y:St. eq(x,y) x = yx,y. g(x)=g(y)] x,y:St. (x,y. g(x)=g(y))(x,y) x = y
