Nuprl - Pf back_listify 1 2 1 1 1 1 1 1

PrintForm Definitions myhill nerode Sections AutomataTheory Doc

1. Alph: Type
2. S: ActionSet(Alph)
3. s: S.car
4. n:
5. f: nAlph
6. Bij(n; Alph; f)
7. n1:
8. f1: n1S.car
9. Bij(n1; S.car; f1)
10. BL: S.car*
11. t: S.car
12. i: ||(x. < f1(x),(y.S.act(f(y),f1(x)))[n] > )[n1]||
13. f1(i) = t
14. mem_f(S.car;s;(y.S.act(f(y),f1(i)))[n])
15. i1:||(y.S.act(f(y),f1(i)))[n]||. ((y.S.act(f(y),f1(i)))[n])[i1] = s

a:Alph. S.act(a,t) = s

By: RWH (LemmaC Thm* n:, f:(nT), i:n. ((f)[n])[i] = f(i)) -1 THEN Reduce -1 THEN Analyze -1

Generated subgoal:

1 15. i1: ||(y.S.act(f(y),f1(i)))[n]||
16. S.act(f(i1),f1(i)) = s
a:Alph. S.act(a,t) = s

About: