PrintForm Definitions myhill nerode Sections AutomataTheory Doc

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

l:Alph*. L(l) (l.Auto(l))(l)
By:
RWH (HypC 7) 0
THEN
Unfold `languages` 2
THEN
Try (Reduce 0)
THEN
Try Auto
THEN
Try (Fold `languages` 0)
Generated subgoals:

12. L: Alph*Prop
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)
9. l: Alph*
L LangOver(Alph)
22. L: Alph*Prop
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)
9. l: Alph*
10. LangOf(Auto)(l)
Auto(l)
32. L: Alph*Prop
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)
9. l: Alph*
10. Auto(l)
LangOf(Auto)(l)

About:
alllistapplyassertlambdauniverseequalmember