Nuprl - Pf bool_listify 1 1 1 2 1 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. T: Type
2. f: T
3. n:
4. f1: nT
5. Bij(n; T; f1)
6. k:
7. 0 < k
8. kn
9. fL: T*
10. t:T. mem_f(T;t;fL) f(t)
11. i:(k-1). f(f1(i)) mem_f(T;f1(i);fL)
12. f(f1(k-1))

fL:T*. (t:T. mem_f(T;t;fL) f(t)) & (i:k. f(f1(i)) mem_f(T;f1(i);fL))

By: InstConcl [f1(k-1).fL] THEN Reduce 0

Generated subgoals:

1 13. t: T
14. f1(k-1) = t mem_f(T;t;fL)
f(t)

2 13. i: k
14. f(f1(i))
f1(k-1) = f1(i) mem_f(T;f1(i);fL)

About:

1	13. `t:` `T` 14. `f1(k-1) = t mem_f(T;t;fL)` `f(t)`
2	13. `i:` `k` 14. `f(f1(i))` `f1(k-1) = f1(i) mem_f(T;f1(i);fL)`