Nuprl - Pf bool_listify 1 1 1 2 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)

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

By: Decide (f(f1(k-1)))

Generated subgoals:

1 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))

2 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))

About:

1	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))`
2	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))`