Nuprl - Pf nd_auto_eq_auto 1 1 2 1 1 1 1 1 2 2 1 1 2 2 1 1 2 1 2 1 1 1 1 1 2

PrintForm Definitions nfa 1 Sections AutomataTheory Doc

At: nd auto eq auto 1 1 2 1 1 1 1 1 2 2 1 1 2 2 1 1 2 1 2 1 1 1 1 1 2

1. Alph: Type
2. St: Type
3. NDA: NDA(Alph;St)
4. Fin(St)
5. x,y:St, a:Alph. Dec(NDA(x,a,y))
6. y:St. Dec(I(NDA) = y)
7. g: St
8. t:St. I(NDA) = t g(t)
9. f:(St). Dec(s:St. f(s) & F(NDA)(s))
10. g1: (St)
11. t:(St). (s:St. t(s) & F(NDA)(s)) g1(t)
12. f:(St), a:Alph, y:St. Dec(s:St. f(s) & NDA(s,a,y))
13. g2: (St)AlphSt
14. t:((St)AlphSt). (s:St. 1of(t)(s) & NDA(s,1of(2of(t)),2of(2of(t)))) g2(t)
15. g0: (St)AlphSt
16. ds:(St), a:Alph, y:St. (s:St. ds(s) & NDA(s,a,y)) g0(ds,a,y)
17. l: Alph*
18. < g0,g,g1 > Automata(Alph;St)
19. m: Alph*
20. u: Alph
21. v: Alph*
22. q:St. NDA(v)q (Result( < g0,g,g1 > )v)(q)

q:St. NDA(u.v)q (Result( < g0,g,g1 > )u.v)(q)

By: RecUnfold `nd_compute_list` 0 THEN RecUnfold `compute_list` 0 THEN Reduce 0

Generated subgoal:

1 q:St. (t:St. NDA(v)t & NDA(t,u,q)) g0((Result( < g0,g,g1 > )v),u,q)

About: