PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: bool listify 1 1 2 1
1. T: Type
2. f: T
3. n:
4. f1: nT
5. Bij(n; T; f1)
6. k:. kn (fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:k. f(f1(i)) mem_f(T;f1(i);fL)))
7. fL: T*
8. (t:T. mem_f(T;t;fL) f(t)) & (i:n. f(f1(i)) mem_f(T;f1(i);fL))

fL:T*. t:T. f(t) mem_f(T;t;fL)
By: InstConcl [fL]
Generated subgoals:

18. t:T. mem_f(T;t;fL) f(t)
9. i:n. f(f1(i)) mem_f(T;f1(i);fL)
10. t: T
11. f(t)
mem_f(T;t;fL)
28. t:T. mem_f(T;t;fL) f(t)
9. i:n. f(f1(i)) mem_f(T;f1(i);fL)
10. t: T
11. mem_f(T;t;fL)
f(t)

About:
existslistallassertapplyuniverse
functionboolnatural_numberimpliesand