PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
bool
listify
1
1.
T:
Type
2.
f:
T
3.
Fin(T)
fL:T*.
t:T. f(t)
mem_f(T;t;fL)
By:
Analyze -1
THEN
Analyze -1
Generated subgoal:
1
3.
n:
4.
f1:
n
T
5.
Bij(
n; T; f1)
fL:T*.
t:T. f(t)
mem_f(T;t;fL)
About:
n
Tn; T; f1)
fL:T*. 
t:T. f(t) 
mem_f(T;t;fL)
fL:T*. t:T. f(t) mem_f(T;t;fL)nTn; T; f1) fL:T*. t:T. f(t) mem_f(T;t;fL)
