PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
fin
listify
1
1
1
1
1
1
1.
T:
Type
2.
n:
3.
f:
n
T
4.
Inj(
n; T; f)
5.
b:T.
a:
n. f(a) = b
6.
t:
T
7.
a:
n
8.
f(a) = t
9.
((f)[
n])[a] = f(a)
mem_f(T;t;(f)[
n])
By:
Inst
Thm*
L:T*, i:
||L||. mem_f(T;L[i];L) [T;(f)[
n];a]
Generated subgoal:
1
10.
mem_f(T;((f)[
n])[a];(f)[
n])
mem_f(T;t;(f)[
n])
About:
n])[a];(f)[n])
mem_f(T;t;(f)[n])n
Tn; T; f)
b:T. 
a:n. f(a) = bnn])[a] = f(a) mem_f(T;t;(f)[n])L:T*, i:||L||. mem_f(T;L[i];L)
[T;(f)[n];a]n])[a];(f)[n]) mem_f(T;t;(f)[n])
