PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
bool
listify
1
1
1
2
1
2
2
1.
T:
Type
2.
f:
T
3.
n:
4.
f1:
n
T
5.
Bij(
n; T; f1)
6.
k:
7.
0 < k
8.
k
n
9.
fL:
T*
10.
t:T. mem_f(T;t;fL)
f(t)
11.
i:
(k-1). f(f1(i))
mem_f(T;f1(i);fL)
12.
f(f1(k-1))
13.
i:
k
14.
f(f1(i))
mem_f(T;f1(i);fL)
By:
Decide (i = k-1)
Generated subgoals:
1
15.
i = k-1
mem_f(T;f1(i);fL)
2
15.
i = k-1
mem_f(T;f1(i);fL)
About:
mem_f(T;f1(i);fL)
i = k-1 mem_f(T;f1(i);fL)
nTn; T; f1)
n
t:T. mem_f(T;t;fL) 
f(t)i:(k-1). f(f1(i)) mem_f(T;f1(i);fL)f(f1(k-1))k mem_f(T;f1(i);fL) mem_f(T;f1(i);fL)i = k-1 mem_f(T;f1(i);fL)
