PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
bool
listify
1
1
2
1
2
1.
T:
Type
2.
f:
T
3.
n:
4.
f1:
n
T
5.
Bij(
n; T; f1)
6.
k:
. k
n
(
fL:T*. (
t:T. mem_f(T;t;fL)
f(t)) & (
i:
k. f(f1(i))
mem_f(T;f1(i);fL)))
7.
fL:
T*
8.
t:T. mem_f(T;t;fL)
f(t)
9.
i:
n. f(f1(i))
mem_f(T;f1(i);fL)
10.
t:
T
11.
mem_f(T;t;fL)
f(t)
By:
BackThru 8
Generated subgoals:
None
About:
nTn; T; f1)
k:. k
n 
(
fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:k. f(f1(i)) mem_f(T;f1(i);fL)))t:T. mem_f(T;t;fL) f(t)i:n. f(f1(i)) mem_f(T;f1(i);fL)
f(t)
