PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: bool listify 1 1 2 1 1 1
1. T: Type
2. f: T
3. n:
4. f1: nT
5. Inj(n; T; f1)
6. b:T. a:n. f1(a) = b
7. k:. kn (fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:k. f(f1(i)) mem_f(T;f1(i);fL)))
8. fL: T*
9. t:T. mem_f(T;t;fL) f(t)
10. i:n. f(f1(i)) mem_f(T;f1(i);fL)
11. t: T
12. f(t)

mem_f(T;t;fL)
By:
InstHyp [t] 6
THEN
Analyze -1
THEN
RWH (RevHypC -1) 0
Generated subgoal:

113. a: n
14. f1(a) = t
mem_f(T;f1(a);fL)

About:
universefunctionboolnatural_numberallexists
equalapplyimplieslistandassert