PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 12 1 2
1. Alph: Type
2. L: LangOver(Alph)
3. Fin(Alph)
4. St: Type
5. Auto: Automata(Alph;St)
6. Fin(St)
7. L = LangOf(Auto)
8. EquivRel x,y:Alph*. (Result(Auto)x) = (Result(Auto)y)

R:(Alph*Alph*Prop). (EquivRel x,y:Alph*. x R y) c (g:((x,y:Alph*//R(x,y))). Fin(x,y:Alph*//R(x,y)) & (l:Alph*. L(l) g(l)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y)))
By: Witness x,y. (Result(Auto)x) = (Result(Auto)y)
Generated subgoals:

1 (x,y. (Result(Auto)x) = (Result(Auto)y)) Alph*Alph*Prop
2 (EquivRel x,y:Alph*. x (x,y. (Result(Auto)x) = (Result(Auto)y)) y) c (g:((x,y:Alph*//(x,y. (Result(Auto)x) = (Result(Auto)y))(x,y))). Fin(x,y:Alph*//(x,y. (Result(Auto)x) = (Result(Auto)y))(x,y)) & (l:Alph*. L(l) g(l)) & (x,y,z:Alph*. (x,y. (Result(Auto)x) = (Result(Auto)y))(x,y) (x,y. (Result(Auto)x) = (Result(Auto)y))((z @ x),z @ y)))
39. R: Alph*Alph*Prop
(EquivRel x,y:Alph*. x R y) c (g:((x,y:Alph*//R(x,y))). Fin(x,y:Alph*//R(x,y)) & (l:Alph*. L(l) g(l)) & (x,y,z:Alph*. R(x,y) R((z @ x),z @ y))) Prop

About:
existsfunctionlistpropquotientapplybooland
allassertimplieslambdaequaluniversemember