PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
bool
listify
1
1
1
2
1
2
2
1
1
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.
i:
k
13.
f(f1(i))
14.
i = k-1
f(f1(k-1))
By:
Assert (f1(i) = f1(k-1)) THENA Analyze
Generated subgoal:
1
15.
f1(i) = f1(k-1)
f(f1(k-1))
About:
f(f1(k-1))
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)k f(f1(k-1)) f(f1(k-1))
