PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
fin
listify
1
1
1.
T:
Type
2.
n:
3.
f:
n
T
4.
Bij(
n; T; f)
TL:T*.
t:T. mem_f(T;t;TL)
By:
InstConcl [(f)[
n]]
Generated subgoal:
1
5.
t:
T
mem_f(T;t;(f)[
n])
About:
mem_f(T;t;(f)[
n])n
Tn; T; f) 
TL:T*. 
t:T. mem_f(T;t;TL)n]] mem_f(T;t;(f)[n])
