PrintForm
Definitions
myhill
nerode
Sections
AutomataTheory
Doc
At:
fin
listify
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
mem_f(T;t;(f)[
n])
By:
Inst
Thm*
n:
, f:(
n
T), i:
n. ((f)[
n])[i] = f(i) [T;n;f;a]
Generated subgoal:
1
9.
((f)[
n])[a] = f(a)
mem_f(T;t;(f)[
n])
About:
n])[a] = f(a)
mem_f(T;t;(f)[n])n
Tn; T; f)
b:T. 
a:n. f(a) = bn mem_f(T;t;(f)[n])n:, f:(nT), i:n. ((f)[n])[i] = f(i)
[T;n;f;a]n])[a] = f(a) mem_f(T;t;(f)[n])
