PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
bool
listify
1
1
2
1
1
1
1
1.
T:
Type
2.
f:
T
3.
n:
4.
f1:
n
T
5.
Inj(
n; T; f1)
6.
b:T.
a:
n. f1(a) = b
7.
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)))
8.
fL:
T*
9.
t:T. mem_f(T;t;fL)
f(t)
10.
i:
n. f(f1(i))
mem_f(T;f1(i);fL)
11.
t:
T
12.
f(t)
13.
a:
n
14.
f1(a) = t
mem_f(T;f1(a);fL)
By:
RWH (RevHypC -1) -3
THEN
BackThru 10
Generated subgoals:
None
About:
nTn; T; f1)
b:T. 
a:n. f1(a) = bk:. 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)n
mem_f(T;f1(a);fL)
