PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: bool listify 1 1 1
1. T: Type
2. f: T
3. n:
4. f1: nT
5. Bij(n; T; f1)

k:. kn (fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:k. f(f1(i)) mem_f(T;f1(i);fL)))
By:
Analyze 0
THEN
NatInd -1
Generated subgoals:

1 0n (fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:0. f(f1(i)) mem_f(T;f1(i);fL)))
26. k:
7. 0 < k
8. k-1n (fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:(k-1). f(f1(i)) mem_f(T;f1(i);fL)))
kn (fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:k. f(f1(i)) mem_f(T;f1(i);fL)))

About:
allimpliesexistslistandassert
applynatural_numberuniversefunctionbool