Alph*8. (
x,y:Alph*. (x (
x,y. x = y 
x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) y) 
h(x) = h(y))
& (x:Alph*. x (x,y. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) (h(x)))
Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c)Alph*q:St. (Result(Auto)c(q)) = q) & Fin(Alph) & Fin(St)
h:(Alph*Alph*).
(x,y:Alph*. (x (x,y. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) y) h(x) = h(y))
& (x:Alph*. x (x,y. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) (h(x))) Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c)| 1 | 7. h: Alph*Alph* 8. ( x,y:Alph*. (x (x,y. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) y) h(x) = h(y))
& (x:Alph*. x (x,y. x = y x,y:Alph*//(x LangOf(Auto)-induced Equiv y)) (h(x))) Surj(St; x,y:Alph*//(x LangOf(Auto)-induced Equiv y); c) |
About:
 |  |  |  |  |
 |  |  |  |  |