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