Nuprl - Pf min_is_unique 1 1 1 1 1 2

PrintForm Definitions automata 5 Sections AutomataTheory Doc

1. Alph: Type
2. St: Type
3. Auto: Automata(Alph;St)
4. EquivRel x,y:Alph*. x LangOf(Auto)-induced Equiv y
5. St ~ (x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
6. Fin(Alph)
7. Fin(St)
8. f: StAlph*
9. s:St. (Result(Auto)f(s)) = s
10. f1: St(x,y:Alph*//(x LangOf(Auto)-induced Equiv y))
11. s: St
12. a: Alph

a.f1(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)

By: Assert (q:x,y:Alph*//(x LangOf(Auto)-induced Equiv y), b:Alph. b.q x,y:Alph*//(x LangOf(Auto)-induced Equiv y))

Generated subgoals:

1 q:x,y:Alph*//(x LangOf(Auto)-induced Equiv y), b:Alph. b.q x,y:Alph*//(x LangOf(Auto)-induced Equiv y)

2 13. q:x,y:Alph*//(x LangOf(Auto)-induced Equiv y), b:Alph. b.q x,y:Alph*//(x LangOf(Auto)-induced Equiv y)
a.f1(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)

About:

1	`q:x,y:Alph//(x LangOf(Auto)-induced Equiv y), b:Alph. b.q x,y:Alph//(x LangOf(Auto)-induced Equiv y)`
2	13. `q:x,y:Alph//(x LangOf(Auto)-induced Equiv y), b:Alph. b.q x,y:Alph//(x LangOf(Auto)-induced Equiv y)` `a.f1(s) x,y:Alph*//(x LangOf(Auto)-induced Equiv y)`