PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
fin
listify
1
1
1
1.
T:
Type
2.
n:
3.
f:
n
T
4.
Bij(
n; T; f)
5.
t:
T
mem_f(T;t;(f)[
n])
By:
Analyze -2
THEN
Unfold `surject` -2
Generated subgoal:
1
4.
Inj(
n; T; f)
5.
b:T.
a:
n. f(a) = b
6.
t:
T
mem_f(T;t;(f)[
n])
About:
n; T; f)
b:T. 
a:n. f(a) = b
mem_f(T;t;(f)[n])n
Tn; T; f) mem_f(T;t;(f)[n])n; T; f)b:T. a:n. f(a) = b mem_f(T;t;(f)[n])
