PrintForm Definitions myhill nerode Sections AutomataTheory Doc

At: mn 12 1 2 2 1 2 1
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)

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

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

About:
existsfunctionquotientlistequalboolandall
applyassertimplieslambdauniversememberprop